:: Several Higher Differentiation Formulas of Special Functions
:: by Junjie Zhao , Xiquan Liang and Li Yan
::
:: Received March 18, 2008
:: Copyright (c) 2008-2012 Association of Mizar Users


begin

theorem Th1: :: HFDIFF_1:1
for Z being open Subset of REAL
for f being Function of REAL,REAL holds dom (f | Z) = Z
proofend;

theorem Th2: :: HFDIFF_1:2
for f1, f2 being PartFunc of REAL,REAL holds (- f1) (#) (- f2) = f1 (#) f2
proofend;

theorem Th3: :: HFDIFF_1:3
for n being Element of NAT st n >= 1 holds
( dom ((#Z n) ^) = REAL \ {0} & (#Z n) " {0} = {0} )
proofend;

theorem :: HFDIFF_1:4
for r, p being Real
for n being Element of NAT holds (r * p) (#) ((#Z n) ^) = r (#) (p (#) ((#Z n) ^))
proofend;

theorem Th5: :: HFDIFF_1:5
for f1 being PartFunc of REAL,REAL
for n, m being Element of REAL holds (n (#) f1) + (m (#) f1) = (n + m) (#) f1
proofend;

theorem Th6: :: HFDIFF_1:6
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st f | Z is_differentiable_on Z holds
f is_differentiable_on Z
proofend;

theorem Th7: :: HFDIFF_1:7
for n being Element of NAT
for Z being open Subset of REAL
for f1 being PartFunc of REAL,REAL st n >= 1 & f1 is_differentiable_on n,Z holds
f1 is_differentiable_on Z
proofend;

theorem Th8: :: HFDIFF_1:8
for n being Element of NAT holds #Z n is_differentiable_on REAL
proofend;

:: 1 f.x = sin.x
theorem :: HFDIFF_1:9
for x being Real
for Z being open Subset of REAL st x in Z holds
((diff (sin,Z)) . 2) . x = - (sin . x)
proofend;

theorem :: HFDIFF_1:10
for x being Real
for Z being open Subset of REAL st x in Z holds
((diff (sin,Z)) . 3) . x = (- cos) . x
proofend;

theorem Th11: :: HFDIFF_1:11
for x being Real
for n being Element of NAT
for Z being open Subset of REAL st x in Z holds
((diff (sin,Z)) . n) . x = sin . (x + ((n * PI) / 2))
proofend;

:: 2 f.x = cos.x
theorem :: HFDIFF_1:12
for x being Real
for Z being open Subset of REAL st x in Z holds
((diff (cos,Z)) . 2) . x = - (cos . x)
proofend;

theorem :: HFDIFF_1:13
for x being Real
for Z being open Subset of REAL st x in Z holds
((diff (cos,Z)) . 3) . x = sin . x
proofend;

theorem Th14: :: HFDIFF_1:14
for x being Real
for n being Element of NAT
for Z being open Subset of REAL st x in Z holds
((diff (cos,Z)) . n) . x = cos . (x + ((n * PI) / 2))
proofend;

theorem Th15: :: HFDIFF_1:15
for n being Element of NAT
for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_on n,Z & f2 is_differentiable_on n,Z holds
(diff ((f1 + f2),Z)) . n = ((diff (f1,Z)) . n) + ((diff (f2,Z)) . n)
proofend;

theorem Th16: :: HFDIFF_1:16
for n being Element of NAT
for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_on n,Z & f2 is_differentiable_on n,Z holds
(diff ((f1 - f2),Z)) . n = ((diff (f1,Z)) . n) - ((diff (f2,Z)) . n)
proofend;

theorem Th17: :: HFDIFF_1:17
for n, i being Element of NAT
for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_on n,Z &amp; f2 is_differentiable_on n,Z &amp; i <= n holds
(diff ((f1 + f2),Z)) . i = ((diff (f1,Z)) . i) + ((diff (f2,Z)) . i)
proofend;

theorem Th18: :: HFDIFF_1:18
for n, i being Element of NAT
for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_on n,Z &amp; f2 is_differentiable_on n,Z &amp; i <= n holds
(diff ((f1 - f2),Z)) . i = ((diff (f1,Z)) . i) - ((diff (f2,Z)) . i)
proofend;

theorem :: HFDIFF_1:19
for n being Element of NAT
for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_on n,Z &amp; f2 is_differentiable_on n,Z holds
f1 + f2 is_differentiable_on n,Z
proofend;

theorem :: HFDIFF_1:20
for n being Element of NAT
for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_on n,Z &amp; f2 is_differentiable_on n,Z holds
f1 - f2 is_differentiable_on n,Z
proofend;

theorem Th21: :: HFDIFF_1:21
for r being Real
for n being Element of NAT
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st f is_differentiable_on n,Z holds
(diff ((r (#) f),Z)) . n = r (#) ((diff (f,Z)) . n)
proofend;

theorem Th22: :: HFDIFF_1:22
for r being Real
for n being Element of NAT
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st f is_differentiable_on n,Z holds
r (#) f is_differentiable_on n,Z
proofend;

theorem :: HFDIFF_1:23
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st f is_differentiable_on Z holds
(diff (f,Z)) . 1 = f `| Z
proofend;

theorem :: HFDIFF_1:24
for n being Element of NAT
for Z being open Subset of REAL
for f1 being PartFunc of REAL,REAL st n >= 1 &amp; f1 is_differentiable_on n,Z holds
(diff (f1,Z)) . 1 = f1 `| Z
proofend;

theorem :: HFDIFF_1:25
for x, r being Real
for n being Element of NAT
for Z being open Subset of REAL st x in Z holds
((diff ((r (#) sin),Z)) . n) . x = r * (sin . (x + ((n * PI) / 2)))
proofend;

theorem :: HFDIFF_1:26
for x, r being Real
for n being Element of NAT
for Z being open Subset of REAL st x in Z holds
((diff ((r (#) cos),Z)) . n) . x = r * (cos . (x + ((n * PI) / 2)))
proofend;

theorem :: HFDIFF_1:27
for x, r being Real
for n being Element of NAT
for Z being open Subset of REAL st x in Z holds
((diff ((r (#) exp_R),Z)) . n) . x = r * (exp_R . x)
proofend;

theorem Th28: :: HFDIFF_1:28
for n being Element of NAT
for Z being open Subset of REAL holds (#Z n) `| Z = (n (#) (#Z (n - 1))) | Z
proofend;

theorem Th29: :: HFDIFF_1:29
for x being Real
for n being Element of NAT st x <> 0 holds
( (#Z n) ^ is_differentiable_in x &amp; diff (((#Z n) ^),x) = - ((n * (x #Z (n - 1))) / ((x #Z n) ^2)) )
proofend;

theorem Th30: :: HFDIFF_1:30
for n being Element of NAT
for Z being open Subset of REAL st n >= 1 holds
(diff ((#Z n),Z)) . 2 = ((n * (n - 1)) (#) (#Z (n - 2))) | Z
proofend;

theorem :: HFDIFF_1:31
for n being Element of NAT
for Z being open Subset of REAL st n >= 2 holds
(diff ((#Z n),Z)) . 3 = (((n * (n - 1)) * (n - 2)) (#) (#Z (n - 3))) | Z
proofend;

Lm1:  for n, m being Element of NAT st n > 1 holds
((m !) / (n !)) * n = (m !) / ((n -' 1) !)
proofend;

theorem Th32: :: HFDIFF_1:32
for n, m being Element of NAT
for Z being open Subset of REAL st n > m holds
(diff ((#Z n),Z)) . m = (((n choose m) * (m !)) (#) (#Z (n - m))) | Z
proofend;

theorem :: HFDIFF_1:33
for n being Element of NAT
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st f is_differentiable_on n,Z holds
( (diff ((- f),Z)) . n = - ((diff (f,Z)) . n) &amp; - f is_differentiable_on n,Z )
proofend;

theorem :: HFDIFF_1:34
for x0, x being Real
for n being Element of NAT
for Z being open Subset of REAL st x0 in Z holds
( (Taylor (sin,Z,x0,x)) . n = ((sin . (x0 + ((n * PI) / 2))) * ((x - x0) |^ n)) / (n !) &amp; (Taylor (cos,Z,x0,x)) . n = ((cos . (x0 + ((n * PI) / 2))) * ((x - x0) |^ n)) / (n !) )
proofend;

theorem :: HFDIFF_1:35
for r, x being Real
for n being Element of NAT st r > 0 holds
( (Maclaurin (sin,].(- r),r.[,x)) . n = ((sin . ((n * PI) / 2)) * (x |^ n)) / (n !) &amp; (Maclaurin (cos,].(- r),r.[,x)) . n = ((cos . ((n * PI) / 2)) * (x |^ n)) / (n !) )
proofend;

theorem Th36: :: HFDIFF_1:36
for x being Real
for n, m being Element of NAT
for Z being open Subset of REAL st n > m &amp; x in Z holds
((diff ((#Z n),Z)) . m) . x = ((n choose m) * (m !)) * (x #Z (n - m))
proofend;

theorem Th37: :: HFDIFF_1:37
for x being Real
for m being Element of NAT
for Z being open Subset of REAL st x in Z holds
((diff ((#Z m),Z)) . m) . x = m !
proofend;

theorem Th38: :: HFDIFF_1:38
for n being Element of NAT
for Z being open Subset of REAL holds #Z n is_differentiable_on n,Z
proofend;

theorem :: HFDIFF_1:39
for x, a being Real
for n, m being Element of NAT
for Z being open Subset of REAL st x in Z &amp; n > m holds
((diff ((a (#) (#Z n)),Z)) . m) . x = ((a * (n choose m)) * (m !)) * (x #Z (n - m))
proofend;

theorem :: HFDIFF_1:40
for x, a being Real
for n being Element of NAT
for Z being open Subset of REAL st x in Z holds
((diff ((a (#) (#Z n)),Z)) . n) . x = a * (n !)
proofend;

theorem Th41: :: HFDIFF_1:41
for x0, x being Real
for n, m being Element of NAT
for Z being open Subset of REAL st x0 in Z &amp; n > m holds
( (Taylor ((#Z n),Z,x0,x)) . m = ((n choose m) * (x0 #Z (n - m))) * ((x - x0) |^ m) &amp; (Taylor ((#Z n),Z,x0,x)) . n = (x - x0) |^ n )
proofend;

theorem :: HFDIFF_1:42
for n, m being Element of NAT
for r, x being Real st n > m &amp; r > 0 holds
( (Maclaurin ((#Z n),].(- r),r.[,x)) . m = 0 &amp; (Maclaurin ((#Z n),].(- r),r.[,x)) . n = x |^ n )
proofend;

theorem Th43: :: HFDIFF_1:43
for n being Element of NAT
for Z being open Subset of REAL st not 0 in Z holds
(#Z n) ^ is_differentiable_on Z
proofend;

theorem :: HFDIFF_1:44
for x0 being Real
for n being Element of NAT
for Z being open Subset of REAL st not 0 in Z &amp; x0 in Z holds
(((#Z n) ^) `| Z) . x0 = - (n / ((#Z (n + 1)) . x0))
proofend;

Lm2:  #Z 1 = id REAL
proofend;

theorem Th45: :: HFDIFF_1:45
for x being Real st x <> 0 holds
( (id REAL) ^ is_differentiable_in x &amp; diff (((id REAL) ^),x) = - (1 / (x ^2)) )
proofend;

theorem :: HFDIFF_1:46
for Z being open Subset of REAL st not 0 in Z holds
((id REAL) ^) `| Z = ((- 1) (#) ((#Z 2) ^)) | Z
proofend;

theorem Th47: :: HFDIFF_1:47
for x being Real st x <> 0 holds
( (#Z 2) ^ is_differentiable_in x &amp; diff (((#Z 2) ^),x) = - ((2 * x) / ((x #Z 2) ^2)) )
proofend;

theorem :: HFDIFF_1:48
for Z being open Subset of REAL st not 0 in Z holds
((#Z 2) ^) `| Z = ((- 2) (#) ((#Z 3) ^)) | Z
proofend;

theorem Th49: :: HFDIFF_1:49
for n being Element of NAT
for Z being open Subset of REAL st not 0 in Z &amp; n >= 1 holds
((#Z n) ^) `| Z = ((- n) (#) ((#Z (n + 1)) ^)) | Z
proofend;

theorem Th50: :: HFDIFF_1:50
for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_on 2,Z &amp; f2 is_differentiable_on 2,Z holds
(diff ((f1 (#) f2),Z)) . 2 = ((((diff (f1,Z)) . 2) (#) f2) + (2 (#) ((f1 `| Z) (#) (f2 `| Z)))) + (f1 (#) ((diff (f2,Z)) . 2))
proofend;

theorem :: HFDIFF_1:51
for Z being open Subset of REAL st Z c= dom ln &amp; Z c= dom ((id REAL) ^) holds
ln `| Z = ((id REAL) ^) | Z
proofend;

theorem :: HFDIFF_1:52
for x0 being Real
for n being Element of NAT
for Z being open Subset of REAL st n >= 1 &amp; x0 in Z &amp; not 0 in Z holds
((diff (((#Z n) ^),Z)) . 2) . x0 = (n * (n + 1)) * (((#Z (n + 2)) ^) . x0)
proofend;

theorem :: HFDIFF_1:53
for Z being open Subset of REAL holds (diff ((sin ^2),Z)) . 2 = (2 (#) ((cos ^2) | Z)) + ((- 2) (#) ((sin ^2) | Z))
proofend;

theorem :: HFDIFF_1:54
for Z being open Subset of REAL holds (diff ((cos ^2),Z)) . 2 = (2 (#) ((sin ^2) | Z)) + ((- 2) (#) ((cos ^2) | Z))
proofend;

theorem :: HFDIFF_1:55
for Z being open Subset of REAL holds (diff ((sin (#) cos),Z)) . 2 = 4 (#) (((- sin) (#) cos) | Z)
proofend;

theorem Th56: :: HFDIFF_1:56
for Z being open Subset of REAL st Z c= dom tan holds
( tan is_differentiable_on Z &amp; tan `| Z = ((cos ^) ^2) | Z )
proofend;

theorem Th57: :: HFDIFF_1:57
for Z being open Subset of REAL st Z c= dom tan holds
( cos ^ is_differentiable_on Z &amp; (cos ^) `| Z = ((cos ^) (#) tan) | Z )
proofend;

theorem :: HFDIFF_1:58
for Z being open Subset of REAL st Z c= dom tan holds
(diff (tan,Z)) . 2 = 2 (#) (((tan (#) (cos ^)) (#) (cos ^)) | Z)
proofend;

theorem Th59: :: HFDIFF_1:59
for Z being open Subset of REAL st Z c= dom cot holds
( cot is_differentiable_on Z &amp; cot `| Z = ((- 1) (#) ((sin ^) ^2)) | Z )
proofend;

theorem Th60: :: HFDIFF_1:60
for Z being open Subset of REAL st Z c= dom cot holds
( sin ^ is_differentiable_on Z &amp; (sin ^) `| Z = (- ((sin ^) (#) cot)) | Z )
proofend;

theorem :: HFDIFF_1:61
for Z being open Subset of REAL st Z c= dom cot holds
(diff (cot,Z)) . 2 = 2 (#) (((cot (#) (sin ^)) (#) (sin ^)) | Z)
proofend;

theorem :: HFDIFF_1:62
for Z being open Subset of REAL holds (diff ((exp_R (#) sin),Z)) . 2 = 2 (#) ((exp_R (#) cos) | Z)
proofend;

theorem :: HFDIFF_1:63
for Z being open Subset of REAL holds (diff ((exp_R (#) cos),Z)) . 2 = 2 (#) ((exp_R (#) (- sin)) | Z)
proofend;

Lm3:  for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st f is_differentiable_on Z holds
(f `| Z) `| Z = (diff (f,Z)) . 2
proofend;

theorem Th64: :: HFDIFF_1:64
for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_on 3,Z &amp; f2 is_differentiable_on 3,Z holds
(diff ((f1 (#) f2),Z)) . 3 = ((((diff (f1,Z)) . 3) (#) f2) + ((3 (#) (((diff (f1,Z)) . 2) (#) (f2 `| Z))) + (3 (#) ((f1 `| Z) (#) ((diff (f2,Z)) . 2))))) + (f1 (#) ((diff (f2,Z)) . 3))
proofend;

theorem :: HFDIFF_1:65
for Z being open Subset of REAL holds (diff ((sin ^2),Z)) . 3 = (- 8) (#) ((cos (#) sin) | Z)
proofend;

theorem :: HFDIFF_1:66
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st f is_differentiable_on 2,Z holds
(diff ((f ^2),Z)) . 2 = (2 (#) (f (#) ((diff (f,Z)) . 2))) + (2 (#) ((f `| Z) ^2))
proofend;

Lm4:  for f being PartFunc of REAL,REAL holds f / f = ((dom f) \ (f " {0})) --> 1
proofend;

Lm5:  for f being PartFunc of REAL,REAL holds (f (#) (f (#) f)) " {0} = f " {0}
proofend;

theorem :: HFDIFF_1:67
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st f is_differentiable_on 2,Z &amp; ( for x0 being Real st x0 in Z holds
f . x0 <> 0 ) holds
(diff ((f ^),Z)) . 2 = (((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f))
proofend;

theorem :: HFDIFF_1:68
for Z being open Subset of REAL holds (diff ((exp_R (#) sin),Z)) . 3 = (2 (#) (exp_R (#) ((- sin) + cos))) | Z
proofend;