:: Inverse Trigonometric Functions Arctan and Arccot
:: by Xiquan Liang and Bing Xie
::
:: Copyright (c) 2008-2021 Association of Mizar Users

theorem Th1: :: SIN_COS9:1
].(- (PI / 2)),(PI / 2).[ c= dom tan
proof end;

theorem Th2: :: SIN_COS9:2
proof end;

Lm1: tan is_differentiable_on ].(- (PI / 2)),(PI / 2).[
proof end;

Lm2:
proof end;

Lm3: for x being Real st x in ].(- (PI / 2)),(PI / 2).[ holds
diff (tan,x) = 1 / ((cos . x) ^2)

proof end;

Lm4: for x being Real st x in holds
diff (cot,x) = - (1 / ((sin . x) ^2))

proof end;

theorem :: SIN_COS9:3
( tan is_differentiable_on ].(- (PI / 2)),(PI / 2).[ & ( for x being Real st x in ].(- (PI / 2)),(PI / 2).[ holds
diff (tan,x) = 1 / ((cos . x) ^2) ) ) by ;

theorem :: SIN_COS9:4
( cot is_differentiable_on & ( for x being Real st x in holds
diff (cot,x) = - (1 / ((sin . x) ^2)) ) ) by ;

theorem :: SIN_COS9:5
tan | ].(- (PI / 2)),(PI / 2).[ is continuous by ;

theorem :: SIN_COS9:6

theorem Th7: :: SIN_COS9:7
tan | ].(- (PI / 2)),(PI / 2).[ is increasing
proof end;

theorem Th8: :: SIN_COS9:8
proof end;

theorem :: SIN_COS9:9
tan | ].(- (PI / 2)),(PI / 2).[ is one-to-one by ;

theorem :: SIN_COS9:10

registration
cluster K5(tan,].(- (PI / 2)),(PI / 2).[) -> one-to-one ;
coherence
tan | ].(- (PI / 2)),(PI / 2).[ is one-to-one
by ;
coherence by ;
end;

definition
func arctan -> PartFunc of REAL,REAL equals :: SIN_COS9:def 1
(tan | ].(- (PI / 2)),(PI / 2).[) " ;
coherence
(tan | ].(- (PI / 2)),(PI / 2).[) " is PartFunc of REAL,REAL
;
func arccot -> PartFunc of REAL,REAL equals :: SIN_COS9:def 2
() " ;
coherence
() " is PartFunc of REAL,REAL
;
end;

:: deftheorem defines arctan SIN_COS9:def 1 :
arctan = (tan | ].(- (PI / 2)),(PI / 2).[) " ;

:: deftheorem defines arccot SIN_COS9:def 2 :
arccot = () " ;

definition
let r be Real;
func arctan r -> number equals :: SIN_COS9:def 3
arctan . r;
coherence ;
func arccot r -> number equals :: SIN_COS9:def 4
arccot . r;
coherence ;
end;

:: deftheorem defines arctan SIN_COS9:def 3 :
for r being Real holds arctan r = arctan . r;

:: deftheorem defines arccot SIN_COS9:def 4 :
for r being Real holds arccot r = arccot . r;

registration
let r be Real;
coherence
arctan r is real
;
coherence
arccot r is real
;
end;

Lm5: arctan " = tan | ].(- (PI / 2)),(PI / 2).[
by FUNCT_1:43;

Lm6:
by FUNCT_1:43;

theorem Th11: :: SIN_COS9:11
rng arctan = ].(- (PI / 2)),(PI / 2).[
proof end;

theorem Th12: :: SIN_COS9:12
proof end;

registration
coherence ;
coherence ;
end;

Lm7: - (PI / 4) in ].(- (PI / 2)),(PI / 2).[
proof end;

Lm8: PI / 4 in ].(- (PI / 2)),(PI / 2).[
proof end;

Lm9:
proof end;

Lm10: (3 / 4) * PI in
proof end;

Lm11: dom (tan | [.(- (PI / 4)),(PI / 4).]) = [.(- (PI / 4)),(PI / 4).]
proof end;

Lm12: dom (cot | [.(PI / 4),((3 / 4) * PI).]) = [.(PI / 4),((3 / 4) * PI).]
proof end;

theorem Th13: :: SIN_COS9:13
for x being Real st x in ].(- (PI / 2)),(PI / 2).[ holds
tan . x = tan x
proof end;

theorem Th14: :: SIN_COS9:14
for x being Real st x in holds
cot . x = cot x
proof end;

theorem :: SIN_COS9:15
for x being Real st cos . x <> 0 holds
tan . x = tan x
proof end;

theorem :: SIN_COS9:16
for x being Real st sin . x <> 0 holds
cot . x = cot x
proof end;

theorem Th17: :: SIN_COS9:17
( tan . (- (PI / 4)) = - 1 & tan (- (PI / 4)) = - 1 )
proof end;

theorem Th18: :: SIN_COS9:18
( cot . (PI / 4) = 1 & cot (PI / 4) = 1 & cot . ((3 / 4) * PI) = - 1 & cot ((3 / 4) * PI) = - 1 )
proof end;

theorem Th19: :: SIN_COS9:19
for x being set st x in [.(- (PI / 4)),(PI / 4).] holds
tan . x in [.(- 1),1.]
proof end;

theorem Th20: :: SIN_COS9:20
for x being set st x in [.(PI / 4),((3 / 4) * PI).] holds
cot . x in [.(- 1),1.]
proof end;

theorem Th21: :: SIN_COS9:21
rng (tan | [.(- (PI / 4)),(PI / 4).]) = [.(- 1),1.]
proof end;

theorem Th22: :: SIN_COS9:22
rng (cot | [.(PI / 4),((3 / 4) * PI).]) = [.(- 1),1.]
proof end;

theorem Th23: :: SIN_COS9:23
[.(- 1),1.] c= dom arctan
proof end;

theorem Th24: :: SIN_COS9:24
[.(- 1),1.] c= dom arccot
proof end;

Lm13: (tan | [.(- (PI / 4)),(PI / 4).]) | [.(- (PI / 4)),(PI / 4).] is increasing
proof end;

Lm14: (cot | [.(PI / 4),((3 / 4) * PI).]) | [.(PI / 4),((3 / 4) * PI).] is decreasing
proof end;

Lm15: tan | [.(- (PI / 4)),(PI / 4).] is one-to-one
proof end;

Lm16: cot | [.(PI / 4),((3 / 4) * PI).] is one-to-one
proof end;

registration
cluster K5(tan,[.(- (PI / 4)),(PI / 4).]) -> one-to-one ;
coherence
tan | [.(- (PI / 4)),(PI / 4).] is one-to-one
by Lm15;
cluster K5(cot,[.(PI / 4),((3 / 4) * PI).]) -> one-to-one ;
coherence
cot | [.(PI / 4),((3 / 4) * PI).] is one-to-one
by Lm16;
end;

theorem Th25: :: SIN_COS9:25
arctan | [.(- 1),1.] = (tan | [.(- (PI / 4)),(PI / 4).]) "
proof end;

theorem Th26: :: SIN_COS9:26
arccot | [.(- 1),1.] = (cot | [.(PI / 4),((3 / 4) * PI).]) "
proof end;

theorem :: SIN_COS9:27
(tan | [.(- (PI / 4)),(PI / 4).]) * (arctan | [.(- 1),1.]) = id [.(- 1),1.] by ;

theorem :: SIN_COS9:28
(cot | [.(PI / 4),((3 / 4) * PI).]) * (arccot | [.(- 1),1.]) = id [.(- 1),1.] by ;

theorem :: SIN_COS9:29
(tan | [.(- (PI / 4)),(PI / 4).]) * (arctan | [.(- 1),1.]) = id [.(- 1),1.] by ;

theorem :: SIN_COS9:30
(cot | [.(PI / 4),((3 / 4) * PI).]) * (arccot | [.(- 1),1.]) = id [.(- 1),1.] by ;

theorem Th31: :: SIN_COS9:31
arctan * (tan | ].(- (PI / 2)),(PI / 2).[) = id ].(- (PI / 2)),(PI / 2).[ by ;

theorem Th32: :: SIN_COS9:32
arccot * () = id by ;

theorem :: SIN_COS9:33
arctan * (tan | ].(- (PI / 2)),(PI / 2).[) = id ].(- (PI / 2)),(PI / 2).[ by ;

theorem :: SIN_COS9:34
arccot * () = id by ;

theorem Th35: :: SIN_COS9:35
for r being Real st - (PI / 2) < r & r < PI / 2 holds
( arctan (tan . r) = r & arctan (tan r) = r )
proof end;

theorem Th36: :: SIN_COS9:36
for r being Real st 0 < r & r < PI holds
( arccot (cot . r) = r & arccot (cot r) = r )
proof end;

theorem Th37: :: SIN_COS9:37
( arctan (- 1) = - (PI / 4) & arctan . (- 1) = - (PI / 4) )
proof end;

theorem Th38: :: SIN_COS9:38
( arccot (- 1) = (3 / 4) * PI & arccot . (- 1) = (3 / 4) * PI )
proof end;

theorem Th39: :: SIN_COS9:39
( arctan 1 = PI / 4 & arctan . 1 = PI / 4 )
proof end;

theorem Th40: :: SIN_COS9:40
( arccot 1 = PI / 4 & arccot . 1 = PI / 4 )
proof end;

theorem Th41: :: SIN_COS9:41
proof end;

theorem Th42: :: SIN_COS9:42
( cot . (PI / 2) = 0 & cot (PI / 2) = 0 )
proof end;

theorem :: SIN_COS9:43
proof end;

theorem :: SIN_COS9:44
( arccot 0 = PI / 2 & arccot . 0 = PI / 2 )
proof end;

theorem Th45: :: SIN_COS9:45
arctan | (tan .: ].(- (PI / 2)),(PI / 2).[) is increasing
proof end;

theorem Th46: :: SIN_COS9:46
proof end;

theorem Th47: :: SIN_COS9:47
arctan | [.(- 1),1.] is increasing
proof end;

theorem Th48: :: SIN_COS9:48
arccot | [.(- 1),1.] is decreasing
proof end;

theorem Th49: :: SIN_COS9:49
for x being set st x in [.(- 1),1.] holds
arctan . x in [.(- (PI / 4)),(PI / 4).]
proof end;

theorem Th50: :: SIN_COS9:50
for x being set st x in [.(- 1),1.] holds
arccot . x in [.(PI / 4),((3 / 4) * PI).]
proof end;

theorem Th51: :: SIN_COS9:51
for r being Real st - 1 <= r & r <= 1 holds
tan () = r
proof end;

theorem Th52: :: SIN_COS9:52
for r being Real st - 1 <= r & r <= 1 holds
cot () = r
proof end;

theorem Th53: :: SIN_COS9:53
arctan | [.(- 1),1.] is continuous
proof end;

theorem Th54: :: SIN_COS9:54
arccot | [.(- 1),1.] is continuous
proof end;

theorem Th55: :: SIN_COS9:55
rng (arctan | [.(- 1),1.]) = [.(- (PI / 4)),(PI / 4).]
proof end;

theorem Th56: :: SIN_COS9:56
rng (arccot | [.(- 1),1.]) = [.(PI / 4),((3 / 4) * PI).]
proof end;

theorem :: SIN_COS9:57
for r being Real st - 1 <= r & r <= 1 & arctan r = - (PI / 4) holds
r = - 1 by ;

theorem :: SIN_COS9:58
for r being Real st - 1 <= r & r <= 1 & arccot r = (3 / 4) * PI holds
r = - 1 by ;

theorem :: SIN_COS9:59
for r being Real st - 1 <= r & r <= 1 & arctan r = 0 holds
r = 0 by ;

theorem :: SIN_COS9:60
for r being Real st - 1 <= r & r <= 1 & arccot r = PI / 2 holds
r = 0 by ;

theorem :: SIN_COS9:61
for r being Real st - 1 <= r & r <= 1 & arctan r = PI / 4 holds
r = 1
proof end;

theorem :: SIN_COS9:62
for r being Real st - 1 <= r & r <= 1 & arccot r = PI / 4 holds
r = 1 by ;

theorem Th63: :: SIN_COS9:63
for r being Real st - 1 <= r & r <= 1 holds
( - (PI / 4) <= arctan r & arctan r <= PI / 4 )
proof end;

theorem Th64: :: SIN_COS9:64
for r being Real st - 1 <= r & r <= 1 holds
( PI / 4 <= arccot r & arccot r <= (3 / 4) * PI )
proof end;

theorem :: SIN_COS9:65
for r being Real st - 1 < r & r < 1 holds
( - (PI / 4) < arctan r & arctan r < PI / 4 )
proof end;

theorem :: SIN_COS9:66
for r being Real st - 1 < r & r < 1 holds
( PI / 4 < arccot r & arccot r < (3 / 4) * PI )
proof end;

theorem :: SIN_COS9:67
for r being Real st - 1 <= r & r <= 1 holds
arctan r = - (arctan (- r))
proof end;

theorem :: SIN_COS9:68
for r being Real st - 1 <= r & r <= 1 holds
arccot r = PI - (arccot (- r))
proof end;

theorem :: SIN_COS9:69
for r being Real st - 1 <= r & r <= 1 holds
cot () = 1 / r
proof end;

theorem :: SIN_COS9:70
for r being Real st - 1 <= r & r <= 1 holds
tan () = 1 / r
proof end;

theorem Th71: :: SIN_COS9:71
arctan is_differentiable_on tan .: ].(- (PI / 2)),(PI / 2).[
proof end;

theorem Th72: :: SIN_COS9:72
proof end;

theorem Th73: :: SIN_COS9:73
proof end;

theorem Th74: :: SIN_COS9:74
proof end;

theorem Th75: :: SIN_COS9:75
for r being Real st - 1 <= r & r <= 1 holds
diff (arctan,r) = 1 / (1 + (r ^2))
proof end;

theorem Th76: :: SIN_COS9:76
for r being Real st - 1 <= r & r <= 1 holds
diff (arccot,r) = - (1 / (1 + (r ^2)))
proof end;

theorem :: SIN_COS9:77
arctan | (tan .: ].(- (PI / 2)),(PI / 2).[) is continuous by ;

theorem :: SIN_COS9:78
arccot | () is continuous by ;

theorem :: SIN_COS9:79
proof end;

theorem :: SIN_COS9:80
proof end;

:: f.x=arctan.x
theorem Th81: :: SIN_COS9:81
for Z being open Subset of REAL st Z c= ].(- 1),1.[ holds
( arctan is_differentiable_on Z & ( for x being Real st x in Z holds
() . x = 1 / (1 + (x ^2)) ) )
proof end;

:: f.x=arccot.x
theorem Th82: :: SIN_COS9:82
for Z being open Subset of REAL st Z c= ].(- 1),1.[ holds
( arccot is_differentiable_on Z & ( for x being Real st x in Z holds
() . x = - (1 / (1 + (x ^2))) ) )
proof end;

::f.x=r*arctanx
theorem :: SIN_COS9:83
for r being Real
for Z being open Subset of REAL st Z c= ].(- 1),1.[ holds
( r (#) arctan is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = r / (1 + (x ^2)) ) )
proof end;

::f.x=r*arccotx
theorem :: SIN_COS9:84
for r being Real
for Z being open Subset of REAL st Z c= ].(- 1),1.[ holds
( r (#) arccot is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = - (r / (1 + (x ^2))) ) )
proof end;

theorem Th85: :: SIN_COS9:85
for x being Real
for f being PartFunc of REAL,REAL st f is_differentiable_in x & f . x > - 1 & f . x < 1 holds
( arctan * f is_differentiable_in x & diff ((),x) = (diff (f,x)) / (1 + ((f . x) ^2)) )
proof end;

theorem Th86: :: SIN_COS9:86
for x being Real
for f being PartFunc of REAL,REAL st f is_differentiable_in x & f . x > - 1 & f . x < 1 holds
( arccot * f is_differentiable_in x & diff ((),x) = - ((diff (f,x)) / (1 + ((f . x) ^2))) )
proof end;

::f.x=arctan.(r*x+s)
theorem Th87: :: SIN_COS9:87
for r, s being Real
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom () & ( for x being Real st x in Z holds
( f . x = (r * x) + s & f . x > - 1 & f . x < 1 ) ) holds
( arctan * f is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = r / (1 + (((r * x) + s) ^2)) ) )
proof end;

::f.x=arccot.(r*x+s)
theorem Th88: :: SIN_COS9:88
for r, s being Real
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom () & ( for x being Real st x in Z holds
( f . x = (r * x) + s & f . x > - 1 & f . x < 1 ) ) holds
( arccot * f is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = - (r / (1 + (((r * x) + s) ^2))) ) )
proof end;

::f.x=ln(arctan.x)
theorem :: SIN_COS9:89
for Z being open Subset of REAL st Z c= dom () & Z c= ].(- 1),1.[ & ( for x being Real st x in Z holds
arctan . x > 0 ) holds
( ln * arctan is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = 1 / ((1 + (x ^2)) * ()) ) )
proof end;

::f.x=ln(arccot.x)
theorem :: SIN_COS9:90
for Z being open Subset of REAL st Z c= dom () & Z c= ].(- 1),1.[ & ( for x being Real st x in Z holds
arccot . x > 0 ) holds
( ln * arccot is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = - (1 / ((1 + (x ^2)) * ())) ) )
proof end;

::f.x=(arctan)|^n
theorem Th91: :: SIN_COS9:91
for n being Element of NAT
for Z being open Subset of REAL st Z c= dom ((#Z n) * arctan) & Z c= ].(- 1),1.[ holds
( (#Z n) * arctan is_differentiable_on Z & ( for x being Real st x in Z holds
(((#Z n) * arctan) | Z) . x = (n * (() #Z (n - 1))) / (1 + (x ^2)) ) )
proof end;

::f.x=(arccot)|^n
theorem Th92: :: SIN_COS9:92
for n being Element of NAT
for Z being open Subset of REAL st Z c= dom ((#Z n) * arccot) & Z c= ].(- 1),1.[ holds
( (#Z n) * arccot is_differentiable_on Z & ( for x being Real st x in Z holds
(((#Z n) * arccot) | Z) . x = - ((n * (() #Z (n - 1))) / (1 + (x ^2))) ) )
proof end;

::f.x=(1/2)*(arctan)|^2
theorem :: SIN_COS9:93
for Z being open Subset of REAL st Z c= dom ((1 / 2) (#) ((#Z 2) * arctan)) & Z c= ].(- 1),1.[ holds
( (1 / 2) (#) ((#Z 2) * arctan) is_differentiable_on Z & ( for x being Real st x in Z holds
(((1 / 2) (#) ((#Z 2) * arctan)) | Z) . x = () / (1 + (x ^2)) ) )
proof end;

::f.x=(1/2)*(arccot)|^2
theorem :: SIN_COS9:94
for Z being open Subset of REAL st Z c= dom ((1 / 2) (#) ((#Z 2) * arccot)) & Z c= ].(- 1),1.[ holds
( (1 / 2) (#) ((#Z 2) * arccot) is_differentiable_on Z & ( for x being Real st x in Z holds
(((1 / 2) (#) ((#Z 2) * arccot)) | Z) . x = - (() / (1 + (x ^2))) ) )
proof end;

::f.x=x*arctan.x
theorem Th95: :: SIN_COS9:95
for Z being open Subset of REAL st Z c= ].(- 1),1.[ holds
( (id Z) (#) arctan is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) (#) arctan) | Z) . x = () + (x / (1 + (x ^2))) ) )
proof end;

::f.x=x*arccot.x
theorem Th96: :: SIN_COS9:96
for Z being open Subset of REAL st Z c= ].(- 1),1.[ holds
( (id Z) (#) arccot is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) (#) arccot) | Z) . x = () - (x / (1 + (x ^2))) ) )
proof end;

::f.x=(r*x+s)*arctan.x
theorem :: SIN_COS9:97
for r, s being Real
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom () & Z c= ].(- 1),1.[ & ( for x being Real st x in Z holds
f . x = (r * x) + s ) holds
( f (#) arctan is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = (r * ()) + (((r * x) + s) / (1 + (x ^2))) ) )
proof end;

::f.x=(r*x+s)*arccot.x
theorem :: SIN_COS9:98
for r, s being Real
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom () & Z c= ].(- 1),1.[ & ( for x being Real st x in Z holds
f . x = (r * x) + s ) holds
( f (#) arccot is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = (r * ()) - (((r * x) + s) / (1 + (x ^2))) ) )
proof end;

::f.x=(1/2)*arctan(2*x)
theorem :: SIN_COS9:99
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom ((1 / 2) (#) ()) & ( for x being Real st x in Z holds
( f . x = 2 * x & f . x > - 1 & f . x < 1 ) ) holds
( (1 / 2) (#) () is_differentiable_on Z & ( for x being Real st x in Z holds
(((1 / 2) (#) ()) | Z) . x = 1 / (1 + ((2 * x) ^2)) ) )
proof end;

::f.x=(1/2)*arccot(2*x)
theorem :: SIN_COS9:100
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom ((1 / 2) (#) ()) & ( for x being Real st x in Z holds
( f . x = 2 * x & f . x > - 1 & f . x < 1 ) ) holds
( (1 / 2) (#) () is_differentiable_on Z & ( for x being Real st x in Z holds
(((1 / 2) (#) ()) | Z) . x = - (1 / (1 + ((2 * x) ^2))) ) )
proof end;

::f.x=1+x|^2
theorem Th101: :: SIN_COS9:101
for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL,REAL st Z c= dom (f1 + f2) & ( for x being Real st x in Z holds
f1 . x = 1 ) & f2 = #Z 2 holds
( f1 + f2 is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 + f2) | Z) . x = 2 * x ) )
proof end;

::f.x=(1/2)ln(1+x|^2)
theorem Th102: :: SIN_COS9:102
for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL,REAL st Z c= dom ((1 / 2) (#) (ln * (f1 + f2))) & f2 = #Z 2 & ( for x being Real st x in Z holds
f1 . x = 1 ) holds
( (1 / 2) (#) (ln * (f1 + f2)) is_differentiable_on Z & ( for x being Real st x in Z holds
(((1 / 2) (#) (ln * (f1 + f2))) | Z) . x = x / (1 + (x ^2)) ) )
proof end;

::f.x=x*arctan.x-(1/2)ln(1+x|^2)
theorem :: SIN_COS9:103
for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL,REAL st Z c= dom (((id Z) (#) arctan) - ((1 / 2) (#) (ln * (f1 + f2)))) & Z c= ].(- 1),1.[ & f2 = #Z 2 & ( for x being Real st x in Z holds
f1 . x = 1 ) holds
( ((id Z) (#) arctan) - ((1 / 2) (#) (ln * (f1 + f2))) is_differentiable_on Z & ( for x being Real st x in Z holds
((((id Z) (#) arctan) - ((1 / 2) (#) (ln * (f1 + f2)))) | Z) . x = arctan . x ) )
proof end;

::f.x=x*arccot.x+(1/2)ln(1+x|^2)
theorem :: SIN_COS9:104
for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL,REAL st Z c= dom (((id Z) (#) arccot) + ((1 / 2) (#) (ln * (f1 + f2)))) & Z c= ].(- 1),1.[ & f2 = #Z 2 & ( for x being Real st x in Z holds
f1 . x = 1 ) holds
( ((id Z) (#) arccot) + ((1 / 2) (#) (ln * (f1 + f2))) is_differentiable_on Z & ( for x being Real st x in Z holds
((((id Z) (#) arccot) + ((1 / 2) (#) (ln * (f1 + f2)))) | Z) . x = arccot . x ) )
proof end;

::f.x=x*arctan(x/r)
theorem Th105: :: SIN_COS9:105
for r being Real
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom ((id Z) (#) ()) & ( for x being Real st x in Z holds
( f . x = x / r & f . x > - 1 & f . x < 1 ) ) holds
( (id Z) (#) () is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) (#) ()) | Z) . x = (arctan . (x / r)) + (x / (r * (1 + ((x / r) ^2)))) ) )
proof end;

::f.x=x*arccot(x/r)
theorem Th106: :: SIN_COS9:106
for r being Real
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom ((id Z) (#) ()) & ( for x being Real st x in Z holds
( f . x = x / r & f . x > - 1 & f . x < 1 ) ) holds
( (id Z) (#) () is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) (#) ()) | Z) . x = (arccot . (x / r)) - (x / (r * (1 + ((x / r) ^2)))) ) )
proof end;

::f.x=1+(x/r)^2
theorem Th107: :: SIN_COS9:107
for r being Real
for Z being open Subset of REAL
for f, f1, f2 being PartFunc of REAL,REAL st Z c= dom (f1 + f2) & ( for x being Real st x in Z holds
f1 . x = 1 ) & f2 = (#Z 2) * f & ( for x being Real st x in Z holds
f . x = x / r ) holds
( f1 + f2 is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 + f2) | Z) . x = (2 * x) / (r ^2) ) )
proof end;

::f.x=(r/2)ln(1+(x/r)^2)
theorem Th108: :: SIN_COS9:108
for r being Real
for Z being open Subset of REAL
for f, f1, f2 being PartFunc of REAL,REAL st Z c= dom ((r / 2) (#) (ln * (f1 + f2))) & ( for x being Real st x in Z holds
f1 . x = 1 ) & r <> 0 & f2 = (#Z 2) * f & ( for x being Real st x in Z holds
f . x = x / r ) holds
( (r / 2) (#) (ln * (f1 + f2)) is_differentiable_on Z & ( for x being Real st x in Z holds
(((r / 2) (#) (ln * (f1 + f2))) | Z) . x = x / (r * (1 + ((x / r) ^2))) ) )
proof end;

::f.x=x*arctan.(x/r)-(r/2)ln(1+(x/r)^2)
theorem :: SIN_COS9:109
for r being Real
for Z being open Subset of REAL
for f, f1, f2 being PartFunc of REAL,REAL st Z c= dom (((id Z) (#) ()) - ((r / 2) (#) (ln * (f1 + f2)))) & r <> 0 & ( for x being Real st x in Z holds
( f . x = x / r & f . x > - 1 & f . x < 1 ) ) & ( for x being Real st x in Z holds
f1 . x = 1 ) & f2 = (#Z 2) * f & ( for x being Real st x in Z holds
f . x = x / r ) holds
( ((id Z) (#) ()) - ((r / 2) (#) (ln * (f1 + f2))) is_differentiable_on Z & ( for x being Real st x in Z holds
((((id Z) (#) ()) - ((r / 2) (#) (ln * (f1 + f2)))) | Z) . x = arctan . (x / r) ) )
proof end;

::f.x=x*arccot.(x/r)+(r/2)ln(1+(x/r)^2)
theorem :: SIN_COS9:110
for r being Real
for Z being open Subset of REAL
for f, f1, f2 being PartFunc of REAL,REAL st Z c= dom (((id Z) (#) ()) + ((r / 2) (#) (ln * (f1 + f2)))) & r <> 0 & ( for x being Real st x in Z holds
( f . x = x / r & f . x > - 1 & f . x < 1 ) ) & ( for x being Real st x in Z holds
f1 . x = 1 ) & f2 = (#Z 2) * f & ( for x being Real st x in Z holds
f . x = x / r ) holds
( ((id Z) (#) ()) + ((r / 2) (#) (ln * (f1 + f2))) is_differentiable_on Z & ( for x being Real st x in Z holds
((((id Z) (#) ()) + ((r / 2) (#) (ln * (f1 + f2)))) | Z) . x = arccot . (x / r) ) )
proof end;

::f.x=arctan.(1/x)
theorem :: SIN_COS9:111
for Z being open Subset of REAL st not 0 in Z & Z c= dom (arctan * ((id Z) ^)) & ( for x being Real st x in Z holds
( ((id Z) ^) . x > - 1 & ((id Z) ^) . x < 1 ) ) holds
( arctan * ((id Z) ^) is_differentiable_on Z & ( for x being Real st x in Z holds
((arctan * ((id Z) ^)) | Z) . x = - (1 / (1 + (x ^2))) ) )
proof end;

::f.x=arccot.(1/x)
theorem :: SIN_COS9:112
for Z being open Subset of REAL st not 0 in Z & Z c= dom (arccot * ((id Z) ^)) & ( for x being Real st x in Z holds
( ((id Z) ^) . x > - 1 & ((id Z) ^) . x < 1 ) ) holds
( arccot * ((id Z) ^) is_differentiable_on Z & ( for x being Real st x in Z holds
((arccot * ((id Z) ^)) | Z) . x = 1 / (1 + (x ^2)) ) )
proof end;

::f.x=arctan.(r+s*x+h*x^2)
theorem :: SIN_COS9:113
for r, s, h being Real
for Z being open Subset of REAL
for f, f1, f2 being PartFunc of REAL,REAL st Z c= dom () & f = f1 + (h (#) f2) & ( for x being Real st x in Z holds
( f . x > - 1 & f . x < 1 ) ) & ( for x being Real st x in Z holds
f1 . x = r + (s * x) ) & f2 = #Z 2 holds
( arctan * (f1 + (h (#) f2)) is_differentiable_on Z & ( for x being Real st x in Z holds
((arctan * (f1 + (h (#) f2))) | Z) . x = (s + ((2 * h) * x)) / (1 + (((r + (s * x)) + (h * (x ^2))) ^2)) ) )
proof end;

::f.x=arccot.(r+s*x+h*x^2)
theorem :: SIN_COS9:114
for r, s, h being Real
for Z being open Subset of REAL
for f, f1, f2 being PartFunc of REAL,REAL st Z c= dom () & f = f1 + (h (#) f2) & ( for x being Real st x in Z holds
( f . x > - 1 & f . x < 1 ) ) & ( for x being Real st x in Z holds
f1 . x = r + (s * x) ) & f2 = #Z 2 holds
( arccot * (f1 + (h (#) f2)) is_differentiable_on Z & ( for x being Real st x in Z holds
((arccot * (f1 + (h (#) f2))) | Z) . x = - ((s + ((2 * h) * x)) / (1 + (((r + (s * x)) + (h * (x ^2))) ^2))) ) )
proof end;

::f.x=arctan.(exp_R.x)
theorem :: SIN_COS9:115
for Z being open Subset of REAL st Z c= dom () & ( for x being Real st x in Z holds
exp_R . x < 1 ) holds
( arctan * exp_R is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = () / (1 + (() ^2)) ) )
proof end;

::f.x=arccot.(exp_R.x)
theorem :: SIN_COS9:116
for Z being open Subset of REAL st Z c= dom () & ( for x being Real st x in Z holds
exp_R . x < 1 ) holds
( arccot * exp_R is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = - (() / (1 + (() ^2))) ) )
proof end;

::f.x=arctan.(ln.x)
theorem :: SIN_COS9:117
for Z being open Subset of REAL st Z c= dom () & ( for x being Real st x in Z holds
( ln . x > - 1 & ln . x < 1 ) ) holds
( arctan * ln is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = 1 / (x * (1 + ((ln . x) ^2))) ) )
proof end;

::f.x=arccot.(ln.x)
theorem :: SIN_COS9:118
for Z being open Subset of REAL st Z c= dom () & ( for x being Real st x in Z holds
( ln . x > - 1 & ln . x < 1 ) ) holds
( arccot * ln is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = - (1 / (x * (1 + ((ln . x) ^2)))) ) )
proof end;

::f.x=exp_R.(arctan.x)
theorem :: SIN_COS9:119
for Z being open Subset of REAL st Z c= dom () & Z c= ].(- 1),1.[ holds
( exp_R * arctan is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = (exp_R . ()) / (1 + (x ^2)) ) )
proof end;

::f.x=exp_R.(arccot.x)
theorem :: SIN_COS9:120
for Z being open Subset of REAL st Z c= dom () & Z c= ].(- 1),1.[ holds
( exp_R * arccot is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = - ((exp_R . ()) / (1 + (x ^2))) ) )
proof end;

::f.x=arctan.x-x
theorem :: SIN_COS9:121
for Z being open Subset of REAL st Z c= dom (arctan - (id Z)) & Z c= ].(- 1),1.[ holds
( arctan - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds
((arctan - (id Z)) | Z) . x = - ((x ^2) / (1 + (x ^2))) ) )
proof end;

::f.x=-arccot.x-x
theorem :: SIN_COS9:122
for Z being open Subset of REAL st Z c= dom (() - (id Z)) & Z c= ].(- 1),1.[ holds
( () - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds
((() - (id Z)) | Z) . x = - ((x ^2) / (1 + (x ^2))) ) )
proof end;

::f.x=exp_R.x*arctan.x
theorem :: SIN_COS9:123
for Z being open Subset of REAL st Z c= ].(- 1),1.[ holds
( exp_R (#) arctan is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = (() * ()) + (() / (1 + (x ^2))) ) )
proof end;

::f.x=exp_R.x*arccot.x
theorem :: SIN_COS9:124
for Z being open Subset of REAL st Z c= ].(- 1),1.[ holds
( exp_R (#) arccot is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = (() * ()) - (() / (1 + (x ^2))) ) )
proof end;

::f.x=(1/r)*arctan.(r*x)-x
theorem :: SIN_COS9:125
for r being Real
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom (((1 / r) (#) ()) - (id Z)) & ( for x being Real st x in Z holds
( f . x = r * x & r <> 0 & f . x > - 1 & f . x < 1 ) ) holds
( ((1 / r) (#) ()) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds
((((1 / r) (#) ()) - (id Z)) | Z) . x = - (((r * x) ^2) / (1 + ((r * x) ^2))) ) )
proof end;

::f.x=(-1/r)*arccot.(r*x)-x
theorem :: SIN_COS9:126
for r being Real
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom (((- (1 / r)) (#) ()) - (id Z)) & ( for x being Real st x in Z holds
( f . x = r * x & r <> 0 & f . x > - 1 & f . x < 1 ) ) holds
( ((- (1 / r)) (#) ()) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds
((((- (1 / r)) (#) ()) - (id Z)) | Z) . x = - (((r * x) ^2) / (1 + ((r * x) ^2))) ) )
proof end;

::f.x=ln.x*arctan.x
theorem :: SIN_COS9:127
for Z being open Subset of REAL st Z c= dom () & Z c= ].(- 1),1.[ holds
( ln (#) arctan is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = (() / x) + ((ln . x) / (1 + (x ^2))) ) )
proof end;

::f.x=ln.x*arccot.x
theorem :: SIN_COS9:128
for Z being open Subset of REAL st Z c= dom () & Z c= ].(- 1),1.[ holds
( ln (#) arccot is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = (() / x) - ((ln . x) / (1 + (x ^2))) ) )
proof end;

::f.x=1/x*arctan.x
theorem :: SIN_COS9:129
for Z being open Subset of REAL st not 0 in Z & Z c= dom (((id Z) ^) (#) arctan) & Z c= ].(- 1),1.[ holds
( ((id Z) ^) (#) arctan is_differentiable_on Z & ( for x being Real st x in Z holds
((((id Z) ^) (#) arctan) | Z) . x = (- (() / (x ^2))) + (1 / (x * (1 + (x ^2)))) ) )
proof end;

::f.x=1/x*arccot.x
theorem :: SIN_COS9:130
for Z being open Subset of REAL st not 0 in Z & Z c= dom (((id Z) ^) (#) arccot) & Z c= ].(- 1),1.[ holds
( ((id Z) ^) (#) arccot is_differentiable_on Z & ( for x being Real st x in Z holds
((((id Z) ^) (#) arccot) | Z) . x = (- (() / (x ^2))) - (1 / (x * (1 + (x ^2)))) ) )
proof end;