:: Some Differentiable Formulas of Special Functions
:: by Jianbing Cao , Fahui Zhai and Xiquan Liang
::
:: Received November 7, 2005
:: Copyright (c) 2005 Association of Mizar Users
Lm1:
for a being Real
for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL ,REAL st Z c= dom (f1 + f2) & ( for x being Real st x in Z holds
f1 . x = a ) & f2 = #Z 2 holds
( f1 + f2 is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 + f2) `| Z) . x = 2 * x ) )
Lm2:
for a being Real
for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL ,REAL st Z c= dom (f1 - f2) & ( for x being Real st x in Z holds
f1 . x = a ) & f2 = #Z 2 holds
( f1 - f2 is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 - f2) `| Z) . x = - (2 * x) ) )
Lm3:
for Z being open Subset of REAL st Z c= dom (#R (1 / 2)) holds
( #R (1 / 2) is_differentiable_on Z & ( for x being Real st x in Z holds
((#R (1 / 2)) `| Z) . x = (1 / 2) * (x #R (- (1 / 2))) ) )
theorem :: FDIFF_5:1
theorem :: FDIFF_5:2
theorem :: FDIFF_5:3
theorem Th4: :: FDIFF_5:4
Lm4:
for Z being open Subset of REAL st not 0 in Z holds
dom (sin * ((id Z) ^ )) = Z
theorem Th5: :: FDIFF_5:5
theorem Th6: :: FDIFF_5:6
theorem :: FDIFF_5:7
theorem :: FDIFF_5:8
theorem :: FDIFF_5:9
theorem :: FDIFF_5:10
theorem :: FDIFF_5:11
theorem :: FDIFF_5:12
theorem :: FDIFF_5:13
theorem :: FDIFF_5:14
theorem :: FDIFF_5:15
theorem :: FDIFF_5:16
theorem :: FDIFF_5:17
theorem :: FDIFF_5:18
Lm5:
for x being Real st x in dom ln holds
x > 0
by TAYLOR_1:18, XXREAL_1:4;
theorem Th19: :: FDIFF_5:19
theorem :: FDIFF_5:20
theorem :: FDIFF_5:21
theorem Th22: :: FDIFF_5:22
theorem :: FDIFF_5:23
theorem :: FDIFF_5:24
theorem :: FDIFF_5:25