:: Inverse Trigonometric Functions Arctan and Arccot
:: by Xiquan Liang and Bing Xie
::
:: Received March 18, 2008
:: Copyright (c) 2008-2011 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:33;

theorem :: SIN_COS9:6

cot | ].0,PI.[ is continuous by Lm2, FDIFF_1:33;

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:16;

theorem :: SIN_COS9:10

cot | ].0,PI.[ is one-to-one by Th8, FCONT_3:16;

registration

cluster K79(tan,].(- (PI / 2)),(PI / 2).[) -> one-to-one ;
coherence
tan | ].(- (PI / 2)),(PI / 2).[ is one-to-one by Th7, FCONT_3:16;
cluster K79(cot,].0,PI.[) -> one-to-one ;
coherence
cot | ].0,PI.[ is one-to-one by Th8, FCONT_3:16;

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:65;

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

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 K79(tan,[.(- (PI / 4)),(PI / 4).]) -> one-to-one ;
coherence
tan | [.(- (PI / 4)),(PI / 4).] is one-to-one by Lm15;
cluster K79(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:61;

theorem :: SIN_COS9:28

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

theorem :: SIN_COS9:29

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

theorem :: SIN_COS9:30

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

theorem Th31: :: SIN_COS9:31

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

theorem Th32: :: SIN_COS9:32

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

theorem :: SIN_COS9:33

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

theorem :: SIN_COS9:34

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

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:33;

theorem :: SIN_COS9:78

arccot | (cot .: ].0,PI.[) is continuous by Th72, FDIFF_1:33;

theorem :: SIN_COS9:79

dom arctan is open

proof end;

theorem :: SIN_COS9:80

dom arccot is open

proof end;

begin

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;