:: 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
theorem ThB6: :: HFDIFF_1:2
theorem Th36: :: HFDIFF_1:3
Lm2:
for r being Real holds ].0 ,r.[ c= REAL \ {0 }
theorem :: HFDIFF_1:4
theorem ThB2: :: HFDIFF_1:5
theorem ThB1: :: HFDIFF_1:6
theorem ThB19: :: HFDIFF_1:7
theorem Th18: :: HFDIFF_1:8
theorem :: HFDIFF_1:9
theorem :: HFDIFF_1:10
theorem Th3: :: HFDIFF_1:11
theorem :: HFDIFF_1:12
theorem :: HFDIFF_1:13
theorem Th6: :: HFDIFF_1:14
theorem Th7: :: HFDIFF_1:15
theorem Th8: :: HFDIFF_1:16
theorem Th9: :: HFDIFF_1:17
theorem Th10: :: HFDIFF_1:18
theorem :: HFDIFF_1:19
theorem :: HFDIFF_1:20
theorem Th13: :: HFDIFF_1:21
theorem Th14: :: HFDIFF_1:22
theorem :: HFDIFF_1:23
theorem :: HFDIFF_1:24
theorem :: HFDIFF_1:25
theorem :: HFDIFF_1:26
theorem :: HFDIFF_1:27
theorem Th19: :: HFDIFF_1:28
theorem Th20: :: HFDIFF_1:29
theorem Th21: :: 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 Th23: :: HFDIFF_1:32
theorem :: HFDIFF_1:33
theorem :: HFDIFF_1:34
theorem :: HFDIFF_1:35
theorem Th27: :: HFDIFF_1:36
theorem Th28: :: HFDIFF_1:37
theorem Th29: :: HFDIFF_1:38
theorem :: HFDIFF_1:39
theorem :: HFDIFF_1:40
theorem Th31: :: HFDIFF_1:41
theorem :: HFDIFF_1:42
theorem Th34: :: HFDIFF_1:43
theorem :: HFDIFF_1:44
theorem ThA: :: HFDIFF_1:45
theorem :: HFDIFF_1:46
theorem ThB: :: HFDIFF_1:47
theorem :: HFDIFF_1:48
theorem Th37: :: HFDIFF_1:49
theorem ThB3: :: HFDIFF_1:50
theorem :: HFDIFF_1:51
theorem :: HFDIFF_1:52
theorem :: HFDIFF_1:53
theorem :: HFDIFF_1:54
theorem :: HFDIFF_1:55
theorem ThB10: :: HFDIFF_1:56
theorem ThB11: :: HFDIFF_1:57
theorem :: HFDIFF_1:58
theorem ThB14: :: HFDIFF_1:59
theorem ThB15: :: HFDIFF_1:60
theorem :: HFDIFF_1:61
theorem :: HFDIFF_1:62
theorem :: HFDIFF_1:63
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
theorem Th21: :: HFDIFF_1:64
theorem :: HFDIFF_1:65
theorem :: HFDIFF_1:66
theorem :: HFDIFF_1:67
theorem :: HFDIFF_1:68