:: 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 Th1: :: HFDIFF_1:1
theorem Th2: :: HFDIFF_1:2
theorem Th3: :: HFDIFF_1:3
theorem :: HFDIFF_1:4
theorem Th5: :: HFDIFF_1:5
theorem Th6: :: HFDIFF_1:6
theorem Th7: :: HFDIFF_1:7
theorem Th8: :: HFDIFF_1:8
theorem :: HFDIFF_1:9
theorem :: HFDIFF_1:10
theorem Th11: :: HFDIFF_1:11
theorem :: HFDIFF_1:12
theorem :: HFDIFF_1:13
theorem Th14: :: HFDIFF_1:14
theorem Th15: :: HFDIFF_1:15
theorem Th16: :: HFDIFF_1:16
theorem Th17: :: HFDIFF_1:17
theorem Th18: :: HFDIFF_1:18
theorem :: HFDIFF_1:19
theorem :: HFDIFF_1:20
theorem Th21: :: HFDIFF_1:21
theorem Th22: :: HFDIFF_1:22
theorem :: HFDIFF_1:23
theorem :: HFDIFF_1:24
theorem :: HFDIFF_1:25
theorem :: HFDIFF_1:26
theorem :: HFDIFF_1:27
theorem Th28: :: HFDIFF_1:28
theorem Th29: :: HFDIFF_1:29
theorem Th30: :: HFDIFF_1:30
theorem :: HFDIFF_1:31
Lm1:
for n, m being Element of NAT st n > 1 holds
((m ! ) / (n ! )) * n = (m ! ) / ((n -' 1) ! )
theorem Th32: :: HFDIFF_1:32
theorem :: HFDIFF_1:33
theorem :: HFDIFF_1:34
theorem :: HFDIFF_1:35
theorem Th36: :: HFDIFF_1:36
theorem Th37: :: HFDIFF_1:37
theorem Th38: :: HFDIFF_1:38
theorem :: HFDIFF_1:39
theorem :: HFDIFF_1:40
theorem Th41: :: HFDIFF_1:41
theorem :: HFDIFF_1:42
theorem Th43: :: HFDIFF_1:43
theorem :: HFDIFF_1:44
Lm2:
#Z 1 = id REAL
theorem Th45: :: HFDIFF_1:45
theorem :: HFDIFF_1:46
theorem Th47: :: HFDIFF_1:47
theorem :: HFDIFF_1:48
theorem Th49: :: HFDIFF_1:49
theorem Th50: :: HFDIFF_1:50
theorem :: HFDIFF_1:51
theorem :: HFDIFF_1:52
theorem :: HFDIFF_1:53
theorem :: HFDIFF_1:54
theorem :: HFDIFF_1:55
theorem Th56: :: HFDIFF_1:56
theorem Th57: :: HFDIFF_1:57
theorem :: HFDIFF_1:58
theorem Th59: :: HFDIFF_1:59
theorem Th60: :: HFDIFF_1:60
theorem :: HFDIFF_1:61
theorem :: HFDIFF_1:62
theorem :: HFDIFF_1:63
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
theorem Th64: :: HFDIFF_1:64
theorem :: HFDIFF_1:65
theorem :: HFDIFF_1:66
Lm4:
for f being PartFunc of REAL ,REAL holds f / f = ((dom f) \ (f " {0 })) --> 1
Lm5:
for f being PartFunc of REAL ,REAL holds (f (#) (f (#) f)) " {0 } = f " {0 }
theorem :: HFDIFF_1:67
theorem :: HFDIFF_1:68