:: 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
for f being PartFunc of REAL , REAL st Z c= dom ((#R (1 / 2)) * f) & ( for x being Real st x in Z holds
( f . x = x & f . x > 0 ) ) holds
( (#R (1 / 2)) * f is_differentiable_on Z & ( for x being Real st x in Z holds
(((#R (1 / 2)) * f) `| 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
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
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