:: Several Differentiation Formulas of Special Functions -- Part {III}
:: by Bo Li , Yan Zhang and Xiquan Liang
::
:: Received March 22, 2006
:: Copyright (c) 2006 Association of Mizar Users

begin

theorem Th1: :: FDIFF_7:1

for x being Real holds x #Z 2 = x ^2

proof end;

theorem Th2: :: FDIFF_7:2

for x being Real st x > 0 holds
x #R (1 / 2) = sqrt x

proof end;

theorem Th3: :: FDIFF_7:3

for x being Real st x > 0 holds
x #R (- (1 / 2)) = 1 / (sqrt x)

proof end;

Lm1: for x being Real holds 2 * ((cos . (x / 2)) ^2 ) = 1 + (cos . x)

proof end;

Lm2: for x being Real holds 2 * ((sin . (x / 2)) ^2 ) = 1 - (cos . x)

proof end;

theorem :: FDIFF_7:4

for r being Real
for Z being open Subset of REAL st Z c= ].(- 1),1.[ & Z c= dom (r (#) arcsin ) holds
( r (#) arcsin is_differentiable_on Z & ( for x being Real st x in Z holds
((r (#) arcsin ) `| Z) . x = r / (sqrt (1 - (x ^2 ))) ) )

proof end;

theorem :: FDIFF_7:5

for r being Real
for Z being open Subset of REAL st Z c= ].(- 1),1.[ & Z c= dom (r (#) arccos ) holds
( r (#) arccos is_differentiable_on Z & ( for x being Real st x in Z holds
((r (#) arccos ) `| Z) . x = - (r / (sqrt (1 - (x ^2 )))) ) )

proof end;

theorem Th6: :: FDIFF_7:6

for x being Real
for f being PartFunc of REAL ,REAL st f is_differentiable_in x & f . x > - 1 & f . x < 1 holds
( arcsin * f is_differentiable_in x & diff (arcsin * f),x = (diff f,x) / (sqrt (1 - ((f . x) ^2 ))) )

proof end;

theorem Th7: :: FDIFF_7:7

for x being Real
for f being PartFunc of REAL ,REAL st f is_differentiable_in x & f . x > - 1 & f . x < 1 holds
( arccos * f is_differentiable_in x & diff (arccos * f),x = - ((diff f,x) / (sqrt (1 - ((f . x) ^2 )))) )

proof end;

theorem :: FDIFF_7:8

for Z being open Subset of REAL st Z c= dom (ln * arcsin ) & Z c= ].(- 1),1.[ & ( for x being Real st x in Z holds
arcsin . x > 0 ) holds
( ln * arcsin is_differentiable_on Z & ( for x being Real st x in Z holds
((ln * arcsin ) `| Z) . x = 1 / ((sqrt (1 - (x ^2 ))) * (arcsin . x)) ) )

proof end;

theorem :: FDIFF_7:9

for Z being open Subset of REAL st Z c= dom (ln * arccos ) & Z c= ].(- 1),1.[ & ( for x being Real st x in Z holds
arccos . x > 0 ) holds
( ln * arccos is_differentiable_on Z & ( for x being Real st x in Z holds
((ln * arccos ) `| Z) . x = - (1 / ((sqrt (1 - (x ^2 ))) * (arccos . x))) ) )

proof end;

theorem Th10: :: FDIFF_7:10

for n being Element of NAT
for Z being open Subset of REAL st Z c= dom ((#Z n) * arcsin ) & Z c= ].(- 1),1.[ holds
( (#Z n) * arcsin is_differentiable_on Z & ( for x being Real st x in Z holds
(((#Z n) * arcsin ) `| Z) . x = (n * ((arcsin . x) #Z (n - 1))) / (sqrt (1 - (x ^2 ))) ) )

proof end;

theorem Th11: :: FDIFF_7:11

for n being Element of NAT
for Z being open Subset of REAL st Z c= dom ((#Z n) * arccos ) & Z c= ].(- 1),1.[ holds
( (#Z n) * arccos is_differentiable_on Z & ( for x being Real st x in Z holds
(((#Z n) * arccos ) `| Z) . x = - ((n * ((arccos . x) #Z (n - 1))) / (sqrt (1 - (x ^2 )))) ) )

proof end;

theorem :: FDIFF_7:12

for Z being open Subset of REAL st Z c= dom ((1 / 2) (#) ((#Z 2) * arcsin )) & Z c= ].(- 1),1.[ holds
( (1 / 2) (#) ((#Z 2) * arcsin ) is_differentiable_on Z & ( for x being Real st x in Z holds
(((1 / 2) (#) ((#Z 2) * arcsin )) `| Z) . x = (arcsin . x) / (sqrt (1 - (x ^2 ))) ) )

proof end;

theorem :: FDIFF_7:13

for Z being open Subset of REAL st Z c= dom ((1 / 2) (#) ((#Z 2) * arccos )) & Z c= ].(- 1),1.[ holds
( (1 / 2) (#) ((#Z 2) * arccos ) is_differentiable_on Z & ( for x being Real st x in Z holds
(((1 / 2) (#) ((#Z 2) * arccos )) `| Z) . x = - ((arccos . x) / (sqrt (1 - (x ^2 )))) ) )

proof end;

theorem Th14: :: FDIFF_7:14

for a, b being Real
for Z being open Subset of REAL
for f being PartFunc of REAL ,REAL st Z c= dom (arcsin * f) & ( for x being Real st x in Z holds
( f . x = (a * x) + b & f . x > - 1 & f . x < 1 ) ) holds
( arcsin * f is_differentiable_on Z & ( for x being Real st x in Z holds
((arcsin * f) `| Z) . x = a / (sqrt (1 - (((a * x) + b) ^2 ))) ) )

proof end;

theorem Th15: :: FDIFF_7:15

for a, b being Real
for Z being open Subset of REAL
for f being PartFunc of REAL ,REAL st Z c= dom (arccos * f) & ( for x being Real st x in Z holds
( f . x = (a * x) + b & f . x > - 1 & f . x < 1 ) ) holds
( arccos * f is_differentiable_on Z & ( for x being Real st x in Z holds
((arccos * f) `| Z) . x = - (a / (sqrt (1 - (((a * x) + b) ^2 )))) ) )

proof end;

theorem Th16: :: FDIFF_7:16

for Z being open Subset of REAL st Z c= dom ((id Z) (#) arcsin ) & Z c= ].(- 1),1.[ holds
( (id Z) (#) arcsin is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) (#) arcsin ) `| Z) . x = (arcsin . x) + (x / (sqrt (1 - (x ^2 )))) ) )

proof end;

theorem Th17: :: FDIFF_7:17

for Z being open Subset of REAL st Z c= dom ((id Z) (#) arccos ) & Z c= ].(- 1),1.[ holds
( (id Z) (#) arccos is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) (#) arccos ) `| Z) . x = (arccos . x) - (x / (sqrt (1 - (x ^2 )))) ) )

proof end;

theorem :: FDIFF_7:18

for a, b being Real
for Z being open Subset of REAL
for f being PartFunc of REAL ,REAL st Z c= dom (f (#) arcsin ) & Z c= ].(- 1),1.[ & ( for x being Real st x in Z holds
f . x = (a * x) + b ) holds
( f (#) arcsin is_differentiable_on Z & ( for x being Real st x in Z holds
((f (#) arcsin ) `| Z) . x = (a * (arcsin . x)) + (((a * x) + b) / (sqrt (1 - (x ^2 )))) ) )

proof end;

theorem :: FDIFF_7:19

for a, b being Real
for Z being open Subset of REAL
for f being PartFunc of REAL ,REAL st Z c= dom (f (#) arccos ) & Z c= ].(- 1),1.[ & ( for x being Real st x in Z holds
f . x = (a * x) + b ) holds
( f (#) arccos is_differentiable_on Z & ( for x being Real st x in Z holds
((f (#) arccos ) `| Z) . x = (a * (arccos . x)) - (((a * x) + b) / (sqrt (1 - (x ^2 )))) ) )

proof end;

theorem :: FDIFF_7:20

for Z being open Subset of REAL
for f being PartFunc of REAL ,REAL st Z c= dom ((1 / 2) (#) (arcsin * f)) & ( for x being Real st x in Z holds
( f . x = 2 * x & f . x > - 1 & f . x < 1 ) ) holds
( (1 / 2) (#) (arcsin * f) is_differentiable_on Z & ( for x being Real st x in Z holds
(((1 / 2) (#) (arcsin * f)) `| Z) . x = 1 / (sqrt (1 - ((2 * x) ^2 ))) ) )

proof end;

theorem :: FDIFF_7:21

for Z being open Subset of REAL
for f being PartFunc of REAL ,REAL st Z c= dom ((1 / 2) (#) (arccos * f)) & ( for x being Real st x in Z holds
( f . x = 2 * x & f . x > - 1 & f . x < 1 ) ) holds
( (1 / 2) (#) (arccos * f) is_differentiable_on Z & ( for x being Real st x in Z holds
(((1 / 2) (#) (arccos * f)) `| Z) . x = - (1 / (sqrt (1 - ((2 * x) ^2 )))) ) )

proof end;

theorem Th22: :: FDIFF_7:22

for Z being open Subset of REAL
for f, f1, f2 being PartFunc of REAL ,REAL st Z c= dom ((#R (1 / 2)) * f) & f = f1 - f2 & f2 = #Z 2 & ( for x being Real st x in Z holds
( f1 . x = 1 & f . x > 0 ) ) holds
( (#R (1 / 2)) * f is_differentiable_on Z & ( for x being Real st x in Z holds
(((#R (1 / 2)) * f) `| Z) . x = - (x * ((1 - (x #Z 2)) #R (- (1 / 2)))) ) )

proof end;

theorem :: FDIFF_7:23

for Z being open Subset of REAL
for f, f1, f2 being PartFunc of REAL ,REAL st Z c= dom (((id Z) (#) arcsin ) + ((#R (1 / 2)) * f)) & Z c= ].(- 1),1.[ & f = f1 - f2 & f2 = #Z 2 & ( for x being Real st x in Z holds
( f1 . x = 1 & f . x > 0 & x <> 0 ) ) holds
( ((id Z) (#) arcsin ) + ((#R (1 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds
((((id Z) (#) arcsin ) + ((#R (1 / 2)) * f)) `| Z) . x = arcsin . x ) )

proof end;

theorem :: FDIFF_7:24

for Z being open Subset of REAL
for f, f1, f2 being PartFunc of REAL ,REAL st Z c= dom (((id Z) (#) arccos ) - ((#R (1 / 2)) * f)) & Z c= ].(- 1),1.[ & f = f1 - f2 & f2 = #Z 2 & ( for x being Real st x in Z holds
( f1 . x = 1 & f . x > 0 & x <> 0 ) ) holds
( ((id Z) (#) arccos ) - ((#R (1 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds
((((id Z) (#) arccos ) - ((#R (1 / 2)) * f)) `| Z) . x = arccos . x ) )

proof end;

theorem Th25: :: FDIFF_7:25

for a being Real
for Z being open Subset of REAL
for f being PartFunc of REAL ,REAL st Z c= dom ((id Z) (#) (arcsin * f)) & ( for x being Real st x in Z holds
( f . x = x / a & f . x > - 1 & f . x < 1 ) ) holds
( (id Z) (#) (arcsin * f) is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) (#) (arcsin * f)) `| Z) . x = (arcsin . (x / a)) + (x / (a * (sqrt (1 - ((x / a) ^2 ))))) ) )

proof end;

theorem Th26: :: FDIFF_7:26

for a being Real
for Z being open Subset of REAL
for f being PartFunc of REAL ,REAL st Z c= dom ((id Z) (#) (arccos * f)) & ( for x being Real st x in Z holds
( f . x = x / a & f . x > - 1 & f . x < 1 ) ) holds
( (id Z) (#) (arccos * f) is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) (#) (arccos * f)) `| Z) . x = (arccos . (x / a)) - (x / (a * (sqrt (1 - ((x / a) ^2 ))))) ) )

proof end;

theorem Th27: :: FDIFF_7:27

for a being Real
for Z being open Subset of REAL
for f, f1, f2 being PartFunc of REAL ,REAL st Z c= dom ((#R (1 / 2)) * f) & f = f1 - f2 & f2 = #Z 2 & ( for x being Real st x in Z holds
( f1 . x = a ^2 & f . x > 0 ) ) holds
( (#R (1 / 2)) * f is_differentiable_on Z & ( for x being Real st x in Z holds
(((#R (1 / 2)) * f) `| Z) . x = - (x * (((a ^2 ) - (x #Z 2)) #R (- (1 / 2)))) ) )

proof end;

theorem :: FDIFF_7:28

for a being Real
for Z being open Subset of REAL
for f3, f, f1, f2 being PartFunc of REAL ,REAL st Z c= dom (((id Z) (#) (arcsin * f3)) + ((#R (1 / 2)) * f)) & f = f1 - f2 & f2 = #Z 2 & ( for x being Real st x in Z holds
( f1 . x = a ^2 & f . x > 0 & f3 . x = x / a & f3 . x > - 1 & f3 . x < 1 & x <> 0 & a > 0 ) ) holds
( ((id Z) (#) (arcsin * f3)) + ((#R (1 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds
((((id Z) (#) (arcsin * f3)) + ((#R (1 / 2)) * f)) `| Z) . x = arcsin . (x / a) ) )

proof end;

theorem :: FDIFF_7:29

for a being Real
for Z being open Subset of REAL
for f3, f, f1, f2 being PartFunc of REAL ,REAL st Z c= dom (((id Z) (#) (arccos * f3)) - ((#R (1 / 2)) * f)) & f = f1 - f2 & f2 = #Z 2 & ( for x being Real st x in Z holds
( f1 . x = a ^2 & f . x > 0 & f3 . x = x / a & f3 . x > - 1 & f3 . x < 1 & x <> 0 & a > 0 ) ) holds
( ((id Z) (#) (arccos * f3)) - ((#R (1 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds
((((id Z) (#) (arccos * f3)) - ((#R (1 / 2)) * f)) `| Z) . x = arccos . (x / a) ) )

proof end;

theorem :: FDIFF_7:30

for n being Element of NAT
for Z being open Subset of REAL st Z c= dom ((- (1 / n)) (#) ((#Z n) * (sin ^ ))) & n > 0 & ( for x being Real st x in Z holds
sin . x <> 0 ) holds
( (- (1 / n)) (#) ((#Z n) * (sin ^ )) is_differentiable_on Z & ( for x being Real st x in Z holds
(((- (1 / n)) (#) ((#Z n) * (sin ^ ))) `| Z) . x = (cos . x) / ((sin . x) #Z (n + 1)) ) )

proof end;

theorem :: FDIFF_7:31

for n being Element of NAT
for Z being open Subset of REAL st Z c= dom ((1 / n) (#) ((#Z n) * (cos ^ ))) & n > 0 & ( for x being Real st x in Z holds
cos . x <> 0 ) holds
( (1 / n) (#) ((#Z n) * (cos ^ )) is_differentiable_on Z & ( for x being Real st x in Z holds
(((1 / n) (#) ((#Z n) * (cos ^ ))) `| Z) . x = (sin . x) / ((cos . x) #Z (n + 1)) ) )

proof end;

Lm3: right_open_halfline 0 = { g where g is Real : 0 < g }
by XXREAL_1:230;

theorem :: FDIFF_7:32

for Z being open Subset of REAL st Z c= dom (sin * ln ) & ( for x being Real st x in Z holds
x > 0 ) holds
( sin * ln is_differentiable_on Z & ( for x being Real st x in Z holds
((sin * ln ) `| Z) . x = (cos . (ln . x)) / x ) )

proof end;

theorem :: FDIFF_7:33

for Z being open Subset of REAL st Z c= dom (cos * ln ) & ( for x being Real st x in Z holds
x > 0 ) holds
( cos * ln is_differentiable_on Z & ( for x being Real st x in Z holds
((cos * ln ) `| Z) . x = - ((sin . (ln . x)) / x) ) )

proof end;

theorem :: FDIFF_7:34

for Z being open Subset of REAL st Z c= dom (sin * exp_R ) holds
( sin * exp_R is_differentiable_on Z & ( for x being Real st x in Z holds
((sin * exp_R ) `| Z) . x = (exp_R . x) * (cos . (exp_R . x)) ) )

proof end;

theorem :: FDIFF_7:35

for Z being open Subset of REAL st Z c= dom (cos * exp_R ) holds
( cos * exp_R is_differentiable_on Z & ( for x being Real st x in Z holds
((cos * exp_R ) `| Z) . x = - ((exp_R . x) * (sin . (exp_R . x))) ) )

proof end;

theorem :: FDIFF_7:36

for Z being open Subset of REAL st Z c= dom (exp_R * cos ) holds
( exp_R * cos is_differentiable_on Z & ( for x being Real st x in Z holds
((exp_R * cos ) `| Z) . x = - ((exp_R . (cos . x)) * (sin . x)) ) )

proof end;

theorem :: FDIFF_7:37

for Z being open Subset of REAL st Z c= dom (exp_R * sin ) holds
( exp_R * sin is_differentiable_on Z & ( for x being Real st x in Z holds
((exp_R * sin ) `| Z) . x = (exp_R . (sin . x)) * (cos . x) ) )

proof end;

theorem Th38: :: FDIFF_7:38

for Z being open Subset of REAL st Z c= dom (sin + cos ) holds
( sin + cos is_differentiable_on Z & ( for x being Real st x in Z holds
((sin + cos ) `| Z) . x = (cos . x) - (sin . x) ) )

proof end;

theorem Th39: :: FDIFF_7:39

for Z being open Subset of REAL st Z c= dom (sin - cos ) holds
( sin - cos is_differentiable_on Z & ( for x being Real st x in Z holds
((sin - cos ) `| Z) . x = (cos . x) + (sin . x) ) )

proof end;

theorem :: FDIFF_7:40

for Z being open Subset of REAL st Z c= dom (exp_R (#) (sin - cos )) holds
( exp_R (#) (sin - cos ) is_differentiable_on Z & ( for x being Real st x in Z holds
((exp_R (#) (sin - cos )) `| Z) . x = (2 * (exp_R . x)) * (sin . x) ) )

proof end;

theorem :: FDIFF_7:41

for Z being open Subset of REAL st Z c= dom (exp_R (#) (sin + cos )) holds
( exp_R (#) (sin + cos ) is_differentiable_on Z & ( for x being Real st x in Z holds
((exp_R (#) (sin + cos )) `| Z) . x = (2 * (exp_R . x)) * (cos . x) ) )

proof end;

theorem :: FDIFF_7:42

for Z being open Subset of REAL st Z c= dom ((sin + cos ) / exp_R ) holds
( (sin + cos ) / exp_R is_differentiable_on Z & ( for x being Real st x in Z holds
(((sin + cos ) / exp_R ) `| Z) . x = - ((2 * (sin . x)) / (exp_R . x)) ) )

proof end;

theorem :: FDIFF_7:43

for Z being open Subset of REAL st Z c= dom ((sin - cos ) / exp_R ) holds
( (sin - cos ) / exp_R is_differentiable_on Z & ( for x being Real st x in Z holds
(((sin - cos ) / exp_R ) `| Z) . x = (2 * (cos . x)) / (exp_R . x) ) )

proof end;

theorem :: FDIFF_7:44

for Z being open Subset of REAL st Z c= dom (exp_R (#) sin ) holds
( exp_R (#) sin is_differentiable_on Z & ( for x being Real st x in Z holds
((exp_R (#) sin ) `| Z) . x = (exp_R . x) * ((sin . x) + (cos . x)) ) )

proof end;

theorem :: FDIFF_7:45

for Z being open Subset of REAL st Z c= dom (exp_R (#) cos ) holds
( exp_R (#) cos is_differentiable_on Z & ( for x being Real st x in Z holds
((exp_R (#) cos ) `| Z) . x = (exp_R . x) * ((cos . x) - (sin . x)) ) )

proof end;

theorem Th46: :: FDIFF_7:46

for x being Real st cos . x <> 0 holds
( sin / cos is_differentiable_in x & diff (sin / cos ),x = 1 / ((cos . x) ^2 ) )

proof end;

theorem Th47: :: FDIFF_7:47

for x being Real st sin . x <> 0 holds
( cos / sin is_differentiable_in x & diff (cos / sin ),x = - (1 / ((sin . x) ^2 )) )

proof end;

theorem :: FDIFF_7:48

for Z being open Subset of REAL st Z c= dom ((#Z 2) * (sin / cos )) & ( for x being Real st x in Z holds
cos . x <> 0 ) holds
( (#Z 2) * (sin / cos ) is_differentiable_on Z & ( for x being Real st x in Z holds
(((#Z 2) * (sin / cos )) `| Z) . x = (2 * (sin . x)) / ((cos . x) #Z 3) ) )

proof end;

theorem :: FDIFF_7:49

for Z being open Subset of REAL st Z c= dom ((#Z 2) * (cos / sin )) & ( for x being Real st x in Z holds
sin . x <> 0 ) holds
( (#Z 2) * (cos / sin ) is_differentiable_on Z & ( for x being Real st x in Z holds
(((#Z 2) * (cos / sin )) `| Z) . x = - ((2 * (cos . x)) / ((sin . x) #Z 3)) ) )

proof end;

theorem :: FDIFF_7:50

for Z being open Subset of REAL
for f being PartFunc of REAL ,REAL st Z c= dom ((sin / cos ) * f) & ( for x being Real st x in Z holds
( f . x = x / 2 & cos . (f . x) <> 0 ) ) holds
( (sin / cos ) * f is_differentiable_on Z & ( for x being Real st x in Z holds
(((sin / cos ) * f) `| Z) . x = 1 / (1 + (cos . x)) ) )

proof end;

theorem :: FDIFF_7:51

for Z being open Subset of REAL
for f being PartFunc of REAL ,REAL st Z c= dom ((cos / sin ) * f) & ( for x being Real st x in Z holds
( f . x = x / 2 & sin . (f . x) <> 0 ) ) holds
( (cos / sin ) * f is_differentiable_on Z & ( for x being Real st x in Z holds
(((cos / sin ) * f) `| Z) . x = - (1 / (1 - (cos . x))) ) )

proof end;