:: Several Higher Differentiation Formulas of Special Functions
:: by Junjie Zhao , Xiquan Liang and Li Yan
::
:: Received March 18, 2008
:: Copyright (c) 2008-2011 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

proof end;

theorem Th2: :: HFDIFF_1:2

for f1, f2 being PartFunc of REAL,REAL holds (- f1) (#) (- f2) = f1 (#) f2

proof end;

theorem Th3: :: HFDIFF_1:3

for n being Element of NAT st n >= 1 holds
( dom ((#Z n) ^) = REAL \ {0} & (#Z n) " {0} = {0} )

proof end;

theorem :: HFDIFF_1:4

for r, p being Real
for n being Element of NAT holds (r * p) (#) ((#Z n) ^) = r (#) (p (#) ((#Z n) ^))

proof end;

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

proof end;

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

proof end;

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

proof end;

theorem Th8: :: HFDIFF_1:8

for n being Element of NAT holds #Z n is_differentiable_on REAL

proof end;

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)

proof end;

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

proof end;

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

proof end;

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)

proof end;

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

proof end;

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

proof end;

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)

proof end;

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)

proof end;

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 & f2 is_differentiable_on n,Z & i <= n holds
(diff ((f1 + f2),Z)) . i = ((diff (f1,Z)) . i) + ((diff (f2,Z)) . i)

proof end;

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 & f2 is_differentiable_on n,Z & i <= n holds
(diff ((f1 - f2),Z)) . i = ((diff (f1,Z)) . i) - ((diff (f2,Z)) . i)

proof end;

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 & f2 is_differentiable_on n,Z holds
f1 + f2 is_differentiable_on n,Z

proof end;

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 & f2 is_differentiable_on n,Z holds
f1 - f2 is_differentiable_on n,Z

proof end;

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)

proof end;

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

proof end;

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

proof end;

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 & f1 is_differentiable_on n,Z holds
(diff (f1,Z)) . 1 = f1 `| Z

proof end;

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

proof end;

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

proof end;

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)

proof end;

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

proof end;

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 & diff (((#Z n) ^),x) = - ((n * (x #Z (n - 1))) / ((x #Z n) ^2)) )

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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) & - f is_differentiable_on n,Z )

proof end;

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 !) & (Taylor (cos,Z,x0,x)) . n = ((cos . (x0 + ((n * PI) / 2))) * ((x - x0) |^ n)) / (n !) )

proof end;

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 !) & (Maclaurin (cos,].(- r),r.[,x)) . n = ((cos . ((n * PI) / 2)) * (x |^ n)) / (n !) )

proof end;

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 & x in Z holds
((diff ((#Z n),Z)) . m) . x = ((n choose m) * (m !)) * (x #Z (n - m))

proof end;

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 !

proof end;

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

proof end;

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 & n > m holds
((diff ((a (#) (#Z n)),Z)) . m) . x = ((a * (n choose m)) * (m !)) * (x #Z (n - m))

proof end;

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

proof end;

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 & n > m holds
( (Taylor ((#Z n),Z,x0,x)) . m = ((n choose m) * (x0 #Z (n - m))) * ((x - x0) |^ m) & (Taylor ((#Z n),Z,x0,x)) . n = (x - x0) |^ n )

proof end;

theorem :: HFDIFF_1:42

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

proof end;

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

proof end;

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 & x0 in Z holds
(((#Z n) ^) `| Z) . x0 = - (n / ((#Z (n + 1)) . x0))

proof end;

Lm2: #Z 1 = id REAL

proof end;

theorem Th45: :: HFDIFF_1:45

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

proof end;

theorem :: HFDIFF_1:46

for Z being open Subset of REAL st not 0 in Z holds
((id REAL) ^) `| Z = ((- 1) (#) ((#Z 2) ^)) | Z

proof end;

theorem Th47: :: HFDIFF_1:47

for x being Real st x <> 0 holds
( (#Z 2) ^ is_differentiable_in x & diff (((#Z 2) ^),x) = - ((2 * x) / ((x #Z 2) ^2)) )

proof end;

theorem :: HFDIFF_1:48

for Z being open Subset of REAL st not 0 in Z holds
((#Z 2) ^) `| Z = ((- 2) (#) ((#Z 3) ^)) | Z

proof end;

theorem Th49: :: HFDIFF_1:49

for n being Element of NAT
for Z being open Subset of REAL st not 0 in Z & n >= 1 holds
((#Z n) ^) `| Z = ((- n) (#) ((#Z (n + 1)) ^)) | Z

proof end;

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

proof end;

theorem :: HFDIFF_1:51

for Z being open Subset of REAL st Z c= dom ln & Z c= dom ((id REAL) ^) holds
ln `| Z = ((id REAL) ^) | Z

proof end;

theorem :: HFDIFF_1:52

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

proof end;

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

proof end;

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

proof end;

theorem :: HFDIFF_1:55

for Z being open Subset of REAL holds (diff ((sin (#) cos),Z)) . 2 = 4 (#) (((- sin) (#) cos) | Z)

proof end;

theorem Th56: :: HFDIFF_1:56

for Z being open Subset of REAL st Z c= dom tan holds
( tan is_differentiable_on Z & tan `| Z = ((cos ^) ^2) | Z )

proof end;

theorem Th57: :: HFDIFF_1:57

for Z being open Subset of REAL st Z c= dom tan holds
( cos ^ is_differentiable_on Z & (cos ^) `| Z = ((cos ^) (#) tan) | Z )

proof end;

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)

proof end;

theorem Th59: :: HFDIFF_1:59

for Z being open Subset of REAL st Z c= dom cot holds
( cot is_differentiable_on Z & cot `| Z = ((- 1) (#) ((sin ^) ^2)) | Z )

proof end;

theorem Th60: :: HFDIFF_1:60

for Z being open Subset of REAL st Z c= dom cot holds
( sin ^ is_differentiable_on Z & (sin ^) `| Z = (- ((sin ^) (#) cot)) | Z )

proof end;

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)

proof end;

theorem :: HFDIFF_1:62

for Z being open Subset of REAL holds (diff ((exp_R (#) sin),Z)) . 2 = 2 (#) ((exp_R (#) cos) | Z)

proof end;

theorem :: HFDIFF_1:63

for Z being open Subset of REAL holds (diff ((exp_R (#) cos),Z)) . 2 = 2 (#) ((exp_R (#) (- sin)) | Z)

proof end;

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

proof end;

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

proof end;

theorem :: HFDIFF_1:65

for Z being open Subset of REAL holds (diff ((sin ^2),Z)) . 3 = (- 8) (#) ((cos (#) sin) | Z)

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

theorem :: HFDIFF_1:68

for Z being open Subset of REAL holds (diff ((exp_R (#) sin),Z)) . 3 = (2 (#) (exp_R (#) ((- sin) + cos))) | Z

proof end;