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

theorem LemX: :: 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 ThB6: :: HFDIFF_1:2

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

proof end;

theorem Th36: :: HFDIFF_1:3

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

proof end;

Lm2: for r being Real holds ].0 ,r.[ c= REAL \ {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 ThB2: :: 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 ThB1: :: 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 ThB19: :: 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 Th18: :: 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 Th3: :: 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 Th6: :: 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 Th7: :: 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 Th8: :: 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 Th9: :: 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 Th10: :: 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 Th13: :: 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 Th14: :: 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 Th19: :: 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 Th20: :: 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 Th21: :: 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 Th23: :: 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 Th27: :: 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 Th28: :: 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 Th29: :: 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 Th31: :: 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 Th34: :: HFDIFF_1:43

for r being Real
for n being Element of NAT holds (#Z n) ^ is_differentiable_on ].0 ,r.[

proof end;

theorem :: HFDIFF_1:44

for x0, r being Real
for n being Element of NAT st x0 in ].0 ,r.[ holds
(((#Z n) ^ ) `| ].0 ,r.[) . x0 = - (n / ((#Z (n + 1)) . x0))

proof end;

theorem ThA: :: HFDIFF_1:45

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

proof end;

theorem :: HFDIFF_1:46

for r being Real st ].0 ,r.[ c= dom ((#Z 2) ^ ) holds
((#Z 1) ^ ) `| ].0 ,r.[ = ((- 1) (#) ((#Z 2) ^ )) | ].0 ,r.[

proof end;

theorem ThB: :: HFDIFF_1:47

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

proof end;

theorem :: HFDIFF_1:48

for r being Real st ].0 ,r.[ c= dom ((#Z 3) ^ ) holds
((#Z 2) ^ ) `| ].0 ,r.[ = ((- 2) (#) ((#Z 3) ^ )) | ].0 ,r.[

proof end;

theorem Th37: :: HFDIFF_1:49

for r being Real
for n being Element of NAT st n >= 1 holds
((#Z n) ^ ) `| ].0 ,r.[ = ((- n) (#) ((#Z (n + 1)) ^ )) | ].0 ,r.[

proof end;

theorem ThB3: :: 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 ((#Z 1) ^ ) holds
ln `| Z = ((#Z 1) ^ ) | Z

proof end;

theorem :: HFDIFF_1:52

for x0, r being Real
for n being Element of NAT st n >= 1 & x0 in ].0 ,r.[ holds
((diff ((#Z n) ^ ),].0 ,r.[) . 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 (#) sin ),Z) . 2 = (2 (#) ((cos (#) cos ) | Z)) + ((- 2) (#) ((sin (#) sin ) | Z))

proof end;

theorem :: HFDIFF_1:54

for Z being open Subset of REAL holds (diff (cos (#) cos ),Z) . 2 = (2 (#) ((sin (#) sin ) | Z)) + ((- 2) (#) ((cos (#) cos ) | 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 ThB10: :: HFDIFF_1:56

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

proof end;

theorem ThB11: :: 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 ThB14: :: 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 ^ ) (#) (sin ^ ))) | Z )

proof end;

theorem ThB15: :: 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;

Lm1: 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 Th21: :: 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 (#) sin ),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 (#) f),Z) . 2 = (2 (#) (f (#) ((diff f,Z) . 2))) + (2 (#) ((f `| Z) (#) (f `| Z)))

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 = (f / f) (#) ((((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;