:: Some Differentiable Formulas of Special Functions
:: by Jianbing Cao , Fahui Zhai and Xiquan Liang
::
:: Received November 7, 2005
:: Copyright (c) 2005-2011 Association of Mizar Users

begin

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 ) )

proof end;

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) ) )

proof end;

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))) ) )

proof end;

theorem :: FDIFF_5:1

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 + x & f2 . x = a - x & f2 . x <> 0 ) ) holds
( f1 / f2 is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 / f2) `| Z) . x = (2 * a) / ((a - x) ^2) ) )

proof end;

theorem :: FDIFF_5:2

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 = x - a & f2 . x = x + a & f2 . x <> 0 ) ) holds
( f1 / f2 is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 / f2) `| Z) . x = (2 * a) / ((x + a) ^2) ) )

proof end;

theorem :: FDIFF_5:3

for a, b 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 = x - a & f2 . x = x - b & f2 . x <> 0 ) ) holds
( f1 / f2 is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 / f2) `| Z) . x = (a - b) / ((x - b) ^2) ) )

proof end;

theorem Th4: :: FDIFF_5:4

for Z being open Subset of REAL st not 0 in Z holds
( (id Z) ^ is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) ^) `| Z) . x = - (1 / (x ^2)) ) )

proof end;

Lm4: for Z being open Subset of REAL st not 0 in Z holds
dom (sin * ((id Z) ^)) = Z

proof end;

theorem Th5: :: FDIFF_5:5

for Z being open Subset of REAL st not 0 in Z holds
( sin * ((id Z) ^) is_differentiable_on Z & ( for x being Real st x in Z holds
((sin * ((id Z) ^)) `| Z) . x = - ((1 / (x ^2)) * (cos . (1 / x))) ) )

proof end;

theorem Th6: :: FDIFF_5:6

for Z being open Subset of REAL st not 0 in Z & Z c= dom (cos * ((id Z) ^)) holds
( cos * ((id Z) ^) is_differentiable_on Z & ( for x being Real st x in Z holds
((cos * ((id Z) ^)) `| Z) . x = (1 / (x ^2)) * (sin . (1 / x)) ) )

proof end;

theorem :: FDIFF_5:7

for Z being open Subset of REAL st Z c= dom ((id Z) (#) (sin * ((id Z) ^))) & not 0 in Z holds
( (id Z) (#) (sin * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) (#) (sin * ((id Z) ^))) `| Z) . x = (sin . (1 / x)) - ((1 / x) * (cos . (1 / x))) ) )

proof end;

theorem :: FDIFF_5:8

for Z being open Subset of REAL st Z c= dom ((id Z) (#) (cos * ((id Z) ^))) & not 0 in Z holds
( (id Z) (#) (cos * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) (#) (cos * ((id Z) ^))) `| Z) . x = (cos . (1 / x)) + ((1 / x) * (sin . (1 / x))) ) )

proof end;

theorem :: FDIFF_5:9

for Z being open Subset of REAL st Z c= dom ((sin * ((id Z) ^)) (#) (cos * ((id Z) ^))) & not 0 in Z holds
( (sin * ((id Z) ^)) (#) (cos * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds
(((sin * ((id Z) ^)) (#) (cos * ((id Z) ^))) `| Z) . x = (1 / (x ^2)) * (((sin . (1 / x)) ^2) - ((cos . (1 / x)) ^2)) ) )

proof end;

theorem :: FDIFF_5:10

for n being Element of NAT
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom ((sin * f) (#) ((#Z n) * sin)) & n >= 1 & ( for x being Real st x in Z holds
f . x = n * x ) holds
( (sin * f) (#) ((#Z n) * sin) is_differentiable_on Z & ( for x being Real st x in Z holds
(((sin * f) (#) ((#Z n) * sin)) `| Z) . x = (n * ((sin . x) #Z (n - 1))) * (sin . ((n + 1) * x)) ) )

proof end;

theorem :: FDIFF_5:11

for n being Element of NAT
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom ((cos * f) (#) ((#Z n) * sin)) & n >= 1 & ( for x being Real st x in Z holds
f . x = n * x ) holds
( (cos * f) (#) ((#Z n) * sin) is_differentiable_on Z & ( for x being Real st x in Z holds
(((cos * f) (#) ((#Z n) * sin)) `| Z) . x = (n * ((sin . x) #Z (n - 1))) * (cos . ((n + 1) * x)) ) )

proof end;

theorem :: FDIFF_5:12

for n being Element of NAT
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom ((cos * f) (#) ((#Z n) * cos)) & n >= 1 & ( for x being Real st x in Z holds
f . x = n * x ) holds
( (cos * f) (#) ((#Z n) * cos) is_differentiable_on Z & ( for x being Real st x in Z holds
(((cos * f) (#) ((#Z n) * cos)) `| Z) . x = - ((n * ((cos . x) #Z (n - 1))) * (sin . ((n + 1) * x))) ) )

proof end;

theorem :: FDIFF_5:13

for n being Element of NAT
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom ((sin * f) (#) ((#Z n) * cos)) & n >= 1 & ( for x being Real st x in Z holds
f . x = n * x ) holds
( (sin * f) (#) ((#Z n) * cos) is_differentiable_on Z & ( for x being Real st x in Z holds
(((sin * f) (#) ((#Z n) * cos)) `| Z) . x = (n * ((cos . x) #Z (n - 1))) * (cos . ((n + 1) * x)) ) )

proof end;

theorem :: FDIFF_5:14

for Z being open Subset of REAL st not 0 in Z & Z c= dom (((id Z) ^) (#) sin) holds
( ((id Z) ^) (#) sin is_differentiable_on Z & ( for x being Real st x in Z holds
((((id Z) ^) (#) sin) `| Z) . x = ((1 / x) * (cos . x)) - ((1 / (x ^2)) * (sin . x)) ) )

proof end;

theorem :: FDIFF_5:15

for Z being open Subset of REAL st not 0 in Z & Z c= dom (((id Z) ^) (#) cos) holds
( ((id Z) ^) (#) cos is_differentiable_on Z & ( for x being Real st x in Z holds
((((id Z) ^) (#) cos) `| Z) . x = (- ((1 / x) * (sin . x))) - ((1 / (x ^2)) * (cos . x)) ) )

proof end;

theorem :: FDIFF_5:16

for Z being open Subset of REAL st Z c= dom (sin + (#R (1 / 2))) holds
( sin + (#R (1 / 2)) is_differentiable_on Z & ( for x being Real st x in Z holds
((sin + (#R (1 / 2))) `| Z) . x = (cos . x) + ((1 / 2) * (x #R (- (1 / 2)))) ) )

proof end;

theorem :: FDIFF_5:17

for Z being open Subset of REAL
for g being PartFunc of REAL,REAL st not 0 in Z & Z c= dom (g (#) (sin * ((id Z) ^))) & g = #Z 2 holds
( g (#) (sin * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds
((g (#) (sin * ((id Z) ^))) `| Z) . x = ((2 * x) * (sin . (1 / x))) - (cos . (1 / x)) ) )

proof end;

theorem :: FDIFF_5:18

for Z being open Subset of REAL
for g being PartFunc of REAL,REAL st not 0 in Z & Z c= dom (g (#) (cos * ((id Z) ^))) & g = #Z 2 holds
( g (#) (cos * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds
((g (#) (cos * ((id Z) ^))) `| Z) . x = ((2 * x) * (cos . (1 / x))) + (sin . (1 / x)) ) )

proof end;

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

for Z being open Subset of REAL st Z c= dom ln holds
( ln is_differentiable_on Z & ( for x being Real st x in Z holds
(ln `| Z) . x = 1 / x ) )

proof end;

theorem :: FDIFF_5:20

for Z being open Subset of REAL st Z c= dom ((id Z) (#) ln) holds
( (id Z) (#) ln is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) (#) ln) `| Z) . x = 1 + (ln . x) ) )

proof end;

theorem :: FDIFF_5:21

for Z being open Subset of REAL
for g being PartFunc of REAL,REAL st Z c= dom (g (#) ln) & g = #Z 2 & ( for x being Real st x in Z holds
x > 0 ) holds
( g (#) ln is_differentiable_on Z & ( for x being Real st x in Z holds
((g (#) ln) `| Z) . x = x + ((2 * x) * (ln . x)) ) )

proof end;

theorem Th22: :: FDIFF_5:22

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) / (f1 - f2)) & ( for x being Real st x in Z holds
f1 . x = a ) & f2 = #Z 2 & ( for x being Real st x in Z holds
(f1 - f2) . x > 0 ) holds
( (f1 + f2) / (f1 - f2) is_differentiable_on Z & ( for x being Real st x in Z holds
(((f1 + f2) / (f1 - f2)) `| Z) . x = ((4 * a) * x) / ((a - (x |^ 2)) |^ 2) ) )

proof end;

theorem :: FDIFF_5:23

for a being Real
for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL,REAL st Z c= dom (ln * ((f1 + f2) / (f1 - f2))) & ( for x being Real st x in Z holds
f1 . x = a ) & f2 = #Z 2 & ( for x being Real st x in Z holds
(f1 - f2) . x > 0 ) & ( for x being Real st x in Z holds
(f1 + f2) . x > 0 ) holds
( ln * ((f1 + f2) / (f1 - f2)) is_differentiable_on Z & ( for x being Real st x in Z holds
((ln * ((f1 + f2) / (f1 - f2))) `| Z) . x = ((4 * a) * x) / ((a |^ 2) - (x |^ 4)) ) )

proof end;

theorem :: FDIFF_5:24

for Z being open Subset of REAL st Z c= dom (((id Z) ^) (#) ln) & ( for x being Real st x in Z holds
x > 0 ) holds
( ((id Z) ^) (#) ln is_differentiable_on Z & ( for x being Real st x in Z holds
((((id Z) ^) (#) ln) `| Z) . x = (1 / (x ^2)) * (1 - (ln . x)) ) )

proof end;

theorem :: FDIFF_5:25

for Z being open Subset of REAL st Z c= dom (ln ^) & ( for x being Real st x in Z holds
ln . x <> 0 ) holds
( ln ^ is_differentiable_on Z & ( for x being Real st x in Z holds
((ln ^) `| Z) . x = - (1 / (x * ((ln . x) ^2))) ) )

proof end;