:: Inverse Trigonometric Functions Arctan and Arccot
:: by Xiquan Liang and Bing Xie
::
:: Received March 18, 2008
:: Copyright (c) 2008-2012 Association of Mizar Users


begin

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

theorem Th2: :: SIN_COS9:2
].0,PI.[ c= dom cot
proof end;

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

Lm2: cot is_differentiable_on ].0,PI.[
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 ].0,PI.[ 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 Lm1, Lm3;

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

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

theorem :: SIN_COS9:6
cot | ].0,PI.[ is continuous by Lm2, FDIFF_1:25;

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

theorem Th8: :: SIN_COS9:8
cot | ].0,PI.[ is decreasing
proof end;

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

theorem :: SIN_COS9:10
cot | ].0,PI.[ is one-to-one by Th8, FCONT_3:8;

registration
cluster K77(tan,].(- (PI / 2)),(PI / 2).[) -> one-to-one ;
coherence
tan | ].(- (PI / 2)),(PI / 2).[ is one-to-one by Th7, FCONT_3:8;
cluster K77(cot,].0,PI.[) -> one-to-one ;
coherence
cot | ].0,PI.[ is one-to-one by Th8, FCONT_3:8;
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
(cot | ].0,PI.[) " ;
coherence
(cot | ].0,PI.[) " 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 = (cot | ].0,PI.[) " ;

definition
let r be Real;
func arctan r -> set equals :: SIN_COS9:def 3
arctan . r;
coherence
arctan . r is set ;
func arccot r -> set equals :: SIN_COS9:def 4
arccot . r;
coherence
arccot . r is set ;
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;

definition
let r be Real;
:: original: arctan
redefine func arctan r -> Real;
coherence
arctan r is Real ;
:: original: arccot
redefine func arccot r -> Real;
coherence
arccot r is Real ;
end;

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

Lm6: arccot " = cot | ].0,PI.[
by FUNCT_1:43;

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

theorem Th12: :: SIN_COS9:12
rng arccot = ].0,PI.[
proof end;

registration
cluster arctan -> one-to-one ;
coherence
arctan is one-to-one ;
cluster arccot -> one-to-one ;
coherence
arccot is one-to-one ;
end;

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

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

Lm9: PI / 4 in ].0,PI.[
proof end;

Lm10: (3 / 4) * PI in ].0,PI.[
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 number st x in ].(- (PI / 2)),(PI / 2).[ holds
tan . x = tan x
proof end;

theorem Th14: :: SIN_COS9:14
for x being real number st x in ].0,PI.[ 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 K77(tan,[.(- (PI / 4)),(PI / 4).]) -> one-to-one ;
coherence
tan | [.(- (PI / 4)),(PI / 4).] is one-to-one by Lm15;
cluster K77(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 Th21, Th25, FUNCT_1:39;

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

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

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

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

theorem Th32: :: SIN_COS9:32
arccot * (cot | ].0,PI.[) = id ].0,PI.[ by Lm6, Th12, FUNCT_1:39;

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

theorem :: SIN_COS9:34
arccot * (cot | ].0,PI.[) = id ].0,PI.[ by Lm6, Th12, FUNCT_1:39;

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
( tan . 0 = 0 & tan 0 = 0 )
proof end;

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

theorem :: SIN_COS9:43
( arctan 0 = 0 & arctan . 0 = 0 )
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
arccot | (cot .: ].0,PI.[) is decreasing
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 (arctan r) = r
proof end;

theorem Th52: :: SIN_COS9:52
for r being Real st - 1 <= r & r <= 1 holds
cot (arccot r) = 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 Th17, Th51;

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

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

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

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 Th18, Th52;

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 (arctan r) = 1 / r
proof end;

theorem :: SIN_COS9:70
for r being Real st - 1 <= r & r <= 1 holds
tan (arccot r) = 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
arccot is_differentiable_on cot .: ].0,PI.[
proof end;

theorem Th73: :: SIN_COS9:73
arctan is_differentiable_on ].(- 1),1.[
proof end;

theorem Th74: :: SIN_COS9:74
arccot is_differentiable_on ].(- 1),1.[
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 Th71, FDIFF_1:25;

theorem :: SIN_COS9:78
arccot | (cot .: ].0,PI.[) is continuous by Th72, FDIFF_1:25;

theorem :: SIN_COS9:79
dom arctan is open
proof end;

theorem :: SIN_COS9:80
dom arccot is open
proof end;

begin

:: 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
(arctan `| Z) . 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
(arccot `| Z) . 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
((r (#) arctan) `| 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
((r (#) arccot) `| 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 ((arctan * f),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 ((arccot * f),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 (arctan * f) & ( 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
((arctan * f) `| 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 (arccot * f) & ( 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
((arccot * f) `| 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 (ln * arctan) & 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
((ln * arctan) `| Z) . x = 1 / ((1 + (x ^2)) * (arctan . x)) ) )
proof end;

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

::f.x=arccot.(exp_R.x)
theorem :: SIN_COS9:116
for Z being open Subset of REAL st Z c= dom (arccot * exp_R) & ( 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
((arccot * exp_R) `| Z) . x = - ((exp_R . x) / (1 + ((exp_R . x) ^2))) ) )
proof end;

::f.x=arctan.(ln.x)
theorem :: SIN_COS9:117
for Z being open Subset of REAL st Z c= dom (arctan * ln) & ( 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
((arctan * ln) `| 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 (arccot * ln) & ( 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
((arccot * ln) `| 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 (exp_R * arctan) & Z c= ].(- 1),1.[ holds
( exp_R * arctan is_differentiable_on Z & ( for x being Real st x in Z holds
((exp_R * arctan) `| Z) . x = (exp_R . (arctan . x)) / (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 (exp_R * arccot) & Z c= ].(- 1),1.[ holds
( exp_R * arccot is_differentiable_on Z & ( for x being Real st x in Z holds
((exp_R * arccot) `| Z) . x = - ((exp_R . (arccot . x)) / (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 ((- arccot) - (id Z)) & Z c= ].(- 1),1.[ holds
( (- arccot) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds
(((- arccot) - (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
((exp_R (#) arctan) `| Z) . x = ((exp_R . x) * (arctan . x)) + ((exp_R . 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
((exp_R (#) arccot) `| Z) . x = ((exp_R . x) * (arccot . x)) - ((exp_R . 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) (#) (arctan * f)) - (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) (#) (arctan * f)) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds
((((1 / r) (#) (arctan * f)) - (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)) (#) (arccot * f)) - (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)) (#) (arccot * f)) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds
((((- (1 / r)) (#) (arccot * f)) - (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 (ln (#) arctan) & Z c= ].(- 1),1.[ holds
( ln (#) arctan is_differentiable_on Z & ( for x being Real st x in Z holds
((ln (#) arctan) `| Z) . x = ((arctan . 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 (ln (#) arccot) & Z c= ].(- 1),1.[ holds
( ln (#) arccot is_differentiable_on Z & ( for x being Real st x in Z holds
((ln (#) arccot) `| Z) . x = ((arccot . 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 = (- ((arctan . 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 = (- ((arccot . x) / (x ^2))) - (1 / (x * (1 + (x ^2)))) ) )
proof end;