:: by Xiquan Liang and Bing Xie

::

:: Received March 18, 2008

:: Copyright (c) 2008-2012 Association of Mizar Users

begin

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

theorem :: SIN_COS9:4

registration

coherence

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

coherence

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

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

coherence

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

definition

coherence

(tan | ].(- (PI / 2)),(PI / 2).[) " is PartFunc of REAL,REAL ;

coherence

(cot | ].0,PI.[) " is PartFunc of REAL,REAL ;

end;
(tan | ].(- (PI / 2)),(PI / 2).[) " is PartFunc of REAL,REAL ;

coherence

(cot | ].0,PI.[) " is PartFunc of REAL,REAL ;

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;
:: original: arctan

redefine func arctan r -> Real;

coherence

arctan r is Real ;

:: original: arccot

redefine func arccot r -> Real;

coherence

arccot r is Real ;

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

by FUNCT_1:43;

Lm6: arccot " = cot | ].0,PI.[

by FUNCT_1:43;

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;

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

coherence

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

coherence

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

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

coherence

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

theorem :: SIN_COS9:27

theorem :: SIN_COS9:28

theorem :: SIN_COS9:29

theorem :: SIN_COS9:30

theorem :: SIN_COS9:33

theorem :: SIN_COS9:57

theorem :: SIN_COS9:58

theorem :: SIN_COS9:59

theorem :: SIN_COS9:60

theorem :: SIN_COS9:62

theorem :: SIN_COS9:77

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)) ) )

( 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))) ) )

( 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)) ) )

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))) ) )

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)) )

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))) )

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)) ) )

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))) ) )

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)) ) )

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))) ) )

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)) ) )

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))) ) )

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)) ) )

( (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))) ) )

( (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))) ) )

( (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))) ) )

( (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))) ) )

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))) ) )

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)) ) )

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))) ) )

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 ) )

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)) ) )

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 ) )

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 ) )

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)))) ) )

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)))) ) )

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) ) )

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))) ) )

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) ) )

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) ) )

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))) ) )

( ((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)) ) )

( ((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)) ) )

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))) ) )

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)) ) )

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))) ) )

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))) ) )

( 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)))) ) )

( 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)) ) )

( 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))) ) )

( 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))) ) )

( 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))) ) )

( (- 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))) ) )

( 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))) ) )

( 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))) ) )

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))) ) )

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))) ) )

( 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))) ) )

( 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)))) ) )

( ((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)))) ) )

( ((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;