:: Several Differentiation Formulas of Special Functions -- Part {III}
:: by Bo Li , Yan Zhang and Xiquan Liang
::
:: Received March 22, 2006
:: Copyright (c) 2006-2011 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;