:: Some Differentiable Formulas of Special Functions
:: by Jianbing Cao , Fahui Zhai and Xiquan Liang
::
:: Received November 7, 2005
:: Copyright (c) 2005-2021 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 ) )
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;

:: 1 f.x=(a+x)/(a-x)
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;

:: 2 f.x=(x-a)/(x+a)
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;

:: 3 f.x=(x-a)/(x-b)
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;

:: 4 f.x=1/x
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;

:: 6 f.x=cos(1/x)
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;

:: 7 f.x=x*sin(1/x)
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;

:: 8 f.x=x*cos(1/x)
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;

:: 9 f.x=sin(1/x)*cos(1/x)
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;

:: 10 f.x=sin(n*x)*(sin x ^ n)
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;

:: 11 f.x=cos(n*x)*(sin x ^ n)
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;

:: 12 f.x=cos(n*x)*(cos x ^ n)
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;

:: 13 f.x=sin(n*x)*(cos x ^ n)
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;

:: 14 f.x=(1/x)*sin x
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;

:: 15 f.x=(1/x)*cos x
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;

:: 16 f.x=sin.x+x^(1/2)
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;

:: 17 f.x=x^2*sin(1/x)
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;

:: 18 f.x=x^2*cos(1/x)
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;

:: 20 f.x=x*ln(x)
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;

:: 21 f.x=x^2*ln(x)
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;

:: 22 f.x=(a+x^2)/(a-x^2)
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;

:: 23 f.x=ln((a+x^2)/(a-x^2))
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;

:: 24 f.x=(1/x)*ln(x)
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;

:: 25 f.x=1/ln(x)
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;