:: Several Differentiable Formulas of Special Functions
:: by Yan Zhang and Xiquan Liang
::
:: Received July 6, 2005
:: Copyright (c) 2005-2021 Association of Mizar Users


:: 1 $f.x=ln(a+x)$
theorem Th1: :: FDIFF_4:1
for a being Real
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom (ln * f) & ( for x being Real st x in Z holds
( f . x = a + x & f . x > 0 ) ) holds
( ln * f is_differentiable_on Z & ( for x being Real st x in Z holds
((ln * f) `| Z) . x = 1 / (a + x) ) )
proof end;

:: 2 $f.x=ln(x-a)$
theorem Th2: :: FDIFF_4:2
for a being Real
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom (ln * f) & ( for x being Real st x in Z holds
( f . x = x - a & f . x > 0 ) ) holds
( ln * f is_differentiable_on Z & ( for x being Real st x in Z holds
((ln * f) `| Z) . x = 1 / (x - a) ) )
proof end;

:: 3 $f.x=-ln(a-x)$
theorem :: FDIFF_4:3
for a being Real
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom (- (ln * f)) & ( for x being Real st x in Z holds
( f . x = a - x & f . x > 0 ) ) holds
( - (ln * f) is_differentiable_on Z & ( for x being Real st x in Z holds
((- (ln * f)) `| Z) . x = 1 / (a - x) ) )
proof end;

:: 4 f.x=x-a*ln(a+x)
theorem :: FDIFF_4:4
for a being Real
for Z being open Subset of REAL
for f, f1 being PartFunc of REAL,REAL st Z c= dom ((id Z) - (a (#) f)) & f = ln * f1 & ( for x being Real st x in Z holds
( f1 . x = a + x & f1 . x > 0 ) ) holds
( (id Z) - (a (#) f) is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) - (a (#) f)) `| Z) . x = x / (a + x) ) )
proof end;

:: 5 f.x=(2*a)*ln(a+x)-x
theorem :: FDIFF_4:5
for a being Real
for Z being open Subset of REAL
for f, f1 being PartFunc of REAL,REAL st Z c= dom (((2 * a) (#) f) - (id Z)) & f = ln * f1 & ( for x being Real st x in Z holds
( f1 . x = a + x & f1 . x > 0 ) ) holds
( ((2 * a) (#) f) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds
((((2 * a) (#) f) - (id Z)) `| Z) . x = (a - x) / (a + x) ) )
proof end;

:: 6 f.x=x-(2*a)*ln(x+a)
theorem :: FDIFF_4:6
for a being Real
for Z being open Subset of REAL
for f, f1 being PartFunc of REAL,REAL st Z c= dom ((id Z) - ((2 * a) (#) f)) & f = ln * f1 & ( for x being Real st x in Z holds
( f1 . x = x + a & f1 . x > 0 ) ) holds
( (id Z) - ((2 * a) (#) f) is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) - ((2 * a) (#) f)) `| Z) . x = (x - a) / (x + a) ) )
proof end;

:: 7 f.x=x + (2*a)*ln(x-a)
theorem :: FDIFF_4:7
for a being Real
for Z being open Subset of REAL
for f, f1 being PartFunc of REAL,REAL st Z c= dom ((id Z) + ((2 * a) (#) f)) & f = ln * f1 & ( for x being Real st x in Z holds
( f1 . x = x - a & f1 . x > 0 ) ) holds
( (id Z) + ((2 * a) (#) f) is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) + ((2 * a) (#) f)) `| Z) . x = (x + a) / (x - a) ) )
proof end;

:: 8 f.x=x+ (a-b)*ln(x+b)
theorem :: FDIFF_4:8
for a, b being Real
for Z being open Subset of REAL
for f, f1 being PartFunc of REAL,REAL st Z c= dom ((id Z) + ((a - b) (#) f)) & f = ln * f1 & ( for x being Real st x in Z holds
( f1 . x = x + b & f1 . x > 0 ) ) holds
( (id Z) + ((a - b) (#) f) is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) + ((a - b) (#) f)) `| Z) . x = (x + a) / (x + b) ) )
proof end;

:: 9 f.x=x+ (a+b)*ln(x-b)
theorem :: FDIFF_4:9
for a, b being Real
for Z being open Subset of REAL
for f, f1 being PartFunc of REAL,REAL st Z c= dom ((id Z) + ((a + b) (#) f)) & f = ln * f1 & ( for x being Real st x in Z holds
( f1 . x = x - b & f1 . x > 0 ) ) holds
( (id Z) + ((a + b) (#) f) is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) + ((a + b) (#) f)) `| Z) . x = (x + a) / (x - b) ) )
proof end;

:: 10 f.x=x- (a+b)*ln(x+b)
theorem :: FDIFF_4:10
for a, b being Real
for Z being open Subset of REAL
for f, f1 being PartFunc of REAL,REAL st Z c= dom ((id Z) - ((a + b) (#) f)) & f = ln * f1 & ( for x being Real st x in Z holds
( f1 . x = x + b & f1 . x > 0 ) ) holds
( (id Z) - ((a + b) (#) f) is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) - ((a + b) (#) f)) `| Z) . x = (x - a) / (x + b) ) )
proof end;

:: 11 f.x=x+ (b-a)*ln(x-b)
theorem :: FDIFF_4:11
for a, b being Real
for Z being open Subset of REAL
for f, f1 being PartFunc of REAL,REAL st Z c= dom ((id Z) + ((b - a) (#) f)) & f = ln * f1 & ( for x being Real st x in Z holds
( f1 . x = x - b & f1 . x > 0 ) ) holds
( (id Z) + ((b - a) (#) f) is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) + ((b - a) (#) f)) `| Z) . x = (x - a) / (x - b) ) )
proof end;

:: 12 f.x=a+b*x+c*x^2
theorem Th12: :: FDIFF_4:12
for a, b, c being Real
for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL,REAL st Z c= dom (f1 + (c (#) f2)) & ( for x being Real st x in Z holds
f1 . x = a + (b * x) ) & f2 = #Z 2 holds
( f1 + (c (#) f2) is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 + (c (#) f2)) `| Z) . x = b + ((2 * c) * x) ) )
proof end;

:: 13 f.x=ln(a+b*x+c*x^2)
theorem Th13: :: FDIFF_4:13
for a, b, c being Real
for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL,REAL st Z c= dom (ln * (f1 + (c (#) f2))) & f2 = #Z 2 & ( for x being Real st x in Z holds
( f1 . x = a + (b * x) & (f1 + (c (#) f2)) . x > 0 ) ) holds
( ln * (f1 + (c (#) f2)) is_differentiable_on Z & ( for x being Real st x in Z holds
((ln * (f1 + (c (#) f2))) `| Z) . x = (b + ((2 * c) * x)) / ((a + (b * x)) + (c * (x |^ 2))) ) )
proof end;

:: 14 f.x=1/(a+x)
theorem Th14: :: FDIFF_4:14
for a being Real
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom f & ( for x being Real st x in Z holds
( f . x = a + x & f . x <> 0 ) ) holds
( f ^ is_differentiable_on Z & ( for x being Real st x in Z holds
((f ^) `| Z) . x = - (1 / ((a + x) ^2)) ) )
proof end;

:: 15 f.x=-1/(a+x)
theorem :: FDIFF_4:15
for a being Real
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom ((- 1) (#) (f ^)) & ( for x being Real st x in Z holds
( f . x = a + x & f . x <> 0 ) ) holds
( (- 1) (#) (f ^) is_differentiable_on Z & ( for x being Real st x in Z holds
(((- 1) (#) (f ^)) `| Z) . x = 1 / ((a + x) ^2) ) )
proof end;

:: 16 f.x=1/(a-x)
theorem :: FDIFF_4:16
for a being Real
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom f & ( for x being Real st x in Z holds
( f . x = a - x & f . x <> 0 ) ) holds
( f ^ is_differentiable_on Z & ( for x being Real st x in Z holds
((f ^) `| Z) . x = 1 / ((a - x) ^2) ) )
proof end;

:: 17 f.x=a^2+x^2
theorem Th17: :: FDIFF_4:17
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 ^2 ) & 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;

:: 18 f.x=ln(a^2+x^2)
theorem :: FDIFF_4:18
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)) & f2 = #Z 2 & ( for x being Real st x in Z holds
( f1 . x = a ^2 & (f1 + f2) . x > 0 ) ) holds
( ln * (f1 + f2) is_differentiable_on Z & ( for x being Real st x in Z holds
((ln * (f1 + f2)) `| Z) . x = (2 * x) / ((a ^2) + (x |^ 2)) ) )
proof end;

:: 19 f.x=-ln(a^2-x^2)
theorem :: FDIFF_4:19
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))) & f2 = #Z 2 & ( for x being Real st x in Z holds
( f1 . x = a ^2 & (f1 - f2) . x > 0 ) ) holds
( - (ln * (f1 - f2)) is_differentiable_on Z & ( for x being Real st x in Z holds
((- (ln * (f1 - f2))) `| Z) . x = (2 * x) / ((a ^2) - (x |^ 2)) ) )
proof end;

:: 20 f.x=a+x^3
theorem Th20: :: FDIFF_4:20
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 3 holds
( f1 + f2 is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 + f2) `| Z) . x = 3 * (x |^ 2) ) )
proof end;

:: 21 f.x=ln(a+x^3)
theorem :: FDIFF_4:21
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)) & f2 = #Z 3 & ( for x being Real st x in Z holds
( f1 . x = a & (f1 + f2) . x > 0 ) ) holds
( ln * (f1 + f2) is_differentiable_on Z & ( for x being Real st x in Z holds
((ln * (f1 + f2)) `| Z) . x = (3 * (x |^ 2)) / (a + (x |^ 3)) ) )
proof end;

:: 22 f.x=ln((a+x)/(a-x))
theorem :: FDIFF_4:22
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)) & ( for x being Real st x in Z holds
( f1 . x = a + x & f1 . x > 0 & f2 . x = a - x & f2 . x > 0 ) ) holds
( ln * (f1 / f2) is_differentiable_on Z & ( for x being Real st x in Z holds
((ln * (f1 / f2)) `| Z) . x = (2 * a) / ((a ^2) - (x ^2)) ) )
proof end;

:: 23 f.x=ln((x-a)/(x+a))
theorem :: FDIFF_4: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)) & ( for x being Real st x in Z holds
( f1 . x = x - a & f1 . x > 0 & f2 . x = x + a & f2 . x > 0 ) ) holds
( ln * (f1 / f2) is_differentiable_on Z & ( for x being Real st x in Z holds
((ln * (f1 / f2)) `| Z) . x = (2 * a) / ((x ^2) - (a ^2)) ) )
proof end;

:: 24 f.x=ln((x-a)/(x-b))
theorem Th24: :: FDIFF_4:24
for a, b being Real
for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL,REAL st Z c= dom (ln * (f1 / f2)) & ( for x being Real st x in Z holds
( f1 . x = x - a & f1 . x > 0 & f2 . x = x - b & f2 . x > 0 ) ) holds
( ln * (f1 / f2) is_differentiable_on Z & ( for x being Real st x in Z holds
((ln * (f1 / f2)) `| Z) . x = (a - b) / ((x - a) * (x - b)) ) )
proof end;

:: 25 f.x=(1/(a-b))*ln((x-a)/(x-b))
theorem :: FDIFF_4:25
for a, b being Real
for Z being open Subset of REAL
for f, f1, f2 being PartFunc of REAL,REAL st Z c= dom ((1 / (a - b)) (#) f) & f = ln * (f1 / f2) & ( for x being Real st x in Z holds
( f1 . x = x - a & f1 . x > 0 & f2 . x = x - b & f2 . x > 0 & a - b <> 0 ) ) holds
( (1 / (a - b)) (#) f is_differentiable_on Z & ( for x being Real st x in Z holds
(((1 / (a - b)) (#) f) `| Z) . x = 1 / ((x - a) * (x - b)) ) )
proof end;

:: 26 f.x=ln((x-a)/x^2)
theorem :: FDIFF_4:26
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)) & f2 = #Z 2 & ( for x being Real st x in Z holds
( f1 . x = x - a & f1 . x > 0 & f2 . x > 0 & x <> 0 ) ) holds
( ln * (f1 / f2) is_differentiable_on Z & ( for x being Real st x in Z holds
((ln * (f1 / f2)) `| Z) . x = ((2 * a) - x) / (x * (x - a)) ) )
proof end;

:: irrational function
:: 27 f.x=(a+x) ^ (3/2)
theorem Th27: :: FDIFF_4:27
for a being Real
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom ((#R (3 / 2)) * f) & ( for x being Real st x in Z holds
( f . x = a + x & f . x > 0 ) ) holds
( (#R (3 / 2)) * f is_differentiable_on Z & ( for x being Real st x in Z holds
(((#R (3 / 2)) * f) `| Z) . x = (3 / 2) * ((a + x) #R (1 / 2)) ) )
proof end;

:: 28 f.x=(a+x) ^ (2/3)
theorem :: FDIFF_4:28
for a being Real
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom ((2 / 3) (#) ((#R (3 / 2)) * f)) & ( for x being Real st x in Z holds
( f . x = a + x & f . x > 0 ) ) holds
( (2 / 3) (#) ((#R (3 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds
(((2 / 3) (#) ((#R (3 / 2)) * f)) `| Z) . x = (a + x) #R (1 / 2) ) )
proof end;

:: 29 f.x=(-2/3)*(a+x) ^ (2/3)
theorem :: FDIFF_4:29
for a being Real
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom ((- (2 / 3)) (#) ((#R (3 / 2)) * f)) & ( for x being Real st x in Z holds
( f . x = a - x & f . x > 0 ) ) holds
( (- (2 / 3)) (#) ((#R (3 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds
(((- (2 / 3)) (#) ((#R (3 / 2)) * f)) `| Z) . x = (a - x) #R (1 / 2) ) )
proof end;

:: 30 f.x=2*(a+x) ^ (1/2)
theorem :: FDIFF_4:30
for a being Real
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom (2 (#) ((#R (1 / 2)) * f)) & ( for x being Real st x in Z holds
( f . x = a + x & f . x > 0 ) ) holds
( 2 (#) ((#R (1 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds
((2 (#) ((#R (1 / 2)) * f)) `| Z) . x = (a + x) #R (- (1 / 2)) ) )
proof end;

:: 31 f.x=(-2)*(a-x) ^ (1/2)
theorem :: FDIFF_4:31
for a being Real
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom ((- 2) (#) ((#R (1 / 2)) * f)) & ( for x being Real st x in Z holds
( f . x = a - x & f . x > 0 ) ) holds
( (- 2) (#) ((#R (1 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds
(((- 2) (#) ((#R (1 / 2)) * f)) `| Z) . x = (a - x) #R (- (1 / 2)) ) )
proof end;

:: 32 f.x=(2/(3*b))*((a+b*x) ^ (3/2))
theorem :: FDIFF_4:32
for a, b being Real
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom ((2 / (3 * b)) (#) ((#R (3 / 2)) * f)) & ( for x being Real st x in Z holds
( f . x = a + (b * x) & b <> 0 & f . x > 0 ) ) holds
( (2 / (3 * b)) (#) ((#R (3 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds
(((2 / (3 * b)) (#) ((#R (3 / 2)) * f)) `| Z) . x = (a + (b * x)) #R (1 / 2) ) )
proof end;

:: 33 f.x=(-2/(3*b))*((a-b*x) ^ (3/2))
theorem :: FDIFF_4:33
for a, b being Real
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom ((- (2 / (3 * b))) (#) ((#R (3 / 2)) * f)) & ( for x being Real st x in Z holds
( f . x = a - (b * x) & b <> 0 & f . x > 0 ) ) holds
( (- (2 / (3 * b))) (#) ((#R (3 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds
(((- (2 / (3 * b))) (#) ((#R (3 / 2)) * f)) `| Z) . x = (a - (b * x)) #R (1 / 2) ) )
proof end;

:: 34 f.x=(a^2+x|^2) ^ (1/2)
theorem :: FDIFF_4:34
for a being Real
for Z being open Subset of REAL
for f, f1, f2 being PartFunc of REAL,REAL st Z c= dom ((#R (1 / 2)) * f) & f = f1 + f2 & f2 = #Z 2 & ( for x being Real st x in Z holds
( f1 . x = a ^2 & 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 = x * (((a ^2) + (x |^ 2)) #R (- (1 / 2))) ) )
proof end;

:: 35 f.x=-(a^2-x|^2) ^ (1/2)
theorem :: FDIFF_4:35
for a being Real
for Z being open Subset of REAL
for f, f1, f2 being PartFunc of REAL,REAL st Z c= dom (- ((#R (1 / 2)) * f)) & f = f1 - f2 & f2 = #Z 2 & ( for x being Real st x in Z holds
( f1 . x = a ^2 & 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 = x * (((a ^2) - (x |^ 2)) #R (- (1 / 2))) ) )
proof end;

:: 36 f.x=(x+x|^2) ^ (1/2)
theorem :: FDIFF_4:36
for Z being open Subset of REAL
for f, f1, f2 being PartFunc of REAL,REAL st Z c= dom (2 (#) ((#R (1 / 2)) * f)) & f = f1 + f2 & f2 = #Z 2 & ( for x being Real st x in Z holds
( f1 . x = x & f . x > 0 ) ) holds
( 2 (#) ((#R (1 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds
((2 (#) ((#R (1 / 2)) * f)) `| Z) . x = ((2 * x) + 1) * (((x |^ 2) + x) #R (- (1 / 2))) ) )
proof end;

:: trigonometric functions
:: 37 f.x=sin(a*x+b)
theorem :: FDIFF_4:37
for a, b being Real
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom (sin * f) & ( for x being Real st x in Z holds
f . x = (a * x) + b ) holds
( sin * f is_differentiable_on Z & ( for x being Real st x in Z holds
((sin * f) `| Z) . x = a * (cos . ((a * x) + b)) ) )
proof end;

:: 38 f.x=sin(a*x+b)
theorem :: FDIFF_4:38
for a, b being Real
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom (cos * f) & ( for x being Real st x in Z holds
f . x = (a * x) + b ) holds
( cos * f is_differentiable_on Z & ( for x being Real st x in Z holds
((cos * f) `| Z) . x = - (a * (sin . ((a * x) + b))) ) )
proof end;

:: 39 f.x=1/cos.x
theorem :: FDIFF_4:39
for Z being open Subset of REAL st ( for x being Real st x in Z holds
cos . x <> 0 ) holds
( cos ^ is_differentiable_on Z & ( for x being Real st x in Z holds
((cos ^) `| Z) . x = (sin . x) / ((cos . x) ^2) ) )
proof end;

:: 40 f.x=1/sin.x
theorem :: FDIFF_4:40
for Z being open Subset of REAL st ( for x being Real st x in Z holds
sin . x <> 0 ) holds
( sin ^ is_differentiable_on Z & ( for x being Real st x in Z holds
((sin ^) `| Z) . x = - ((cos . x) / ((sin . x) ^2)) ) )
proof end;

:: 41 f.x=sin.x*cos.x
theorem :: FDIFF_4:41
for Z being open Subset of REAL st Z c= dom (sin (#) cos) holds
( sin (#) cos is_differentiable_on Z & ( for x being Real st x in Z holds
((sin (#) cos) `| Z) . x = cos (2 * x) ) )
proof end;

:: 42 f.x=ln(cos.x)
theorem :: FDIFF_4:42
for Z being open Subset of REAL st Z c= dom (ln * cos) & ( for x being Real st x in Z holds
cos . x > 0 ) holds
( ln * cos is_differentiable_on Z & ( for x being Real st x in Z holds
((ln * cos) `| Z) . x = - (tan x) ) )
proof end;

:: 43 f.x=ln(sin.x)
theorem :: FDIFF_4:43
for Z being open Subset of REAL st Z c= dom (ln * sin) & ( for x being Real st x in Z holds
sin . x > 0 ) holds
( ln * sin is_differentiable_on Z & ( for x being Real st x in Z holds
((ln * sin) `| Z) . x = cot x ) )
proof end;

:: 44 f.x=-x*cos.x
theorem Th44: :: FDIFF_4:44
for Z being open Subset of REAL st 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 = (- (cos . x)) + (x * (sin . x)) ) )
proof end;

:: f.x=x*sin.x
theorem Th45: :: FDIFF_4:45
for Z being open Subset of REAL st 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 = (sin . x) + (x * (cos . x)) ) )
proof end;

:: 46 f.x=-x*cos.x+sin.x
theorem :: FDIFF_4:46
for Z being open Subset of REAL st Z c= dom (((- (id Z)) (#) cos) + sin) holds
( ((- (id Z)) (#) cos) + sin is_differentiable_on Z & ( for x being Real st x in Z holds
((((- (id Z)) (#) cos) + sin) `| Z) . x = x * (sin . x) ) )
proof end;

:: 47 f.x=x*sin.x+cos.x
theorem :: FDIFF_4:47
for Z being open Subset of REAL st Z c= dom (((id Z) (#) sin) + cos) holds
( ((id Z) (#) sin) + cos is_differentiable_on Z & ( for x being Real st x in Z holds
((((id Z) (#) sin) + cos) `| Z) . x = x * (cos . x) ) )
proof end;

:: 48 f.x=2*(sin.x ^ (1/2))
theorem :: FDIFF_4:48
for Z being open Subset of REAL st Z c= dom (2 (#) ((#R (1 / 2)) * sin)) & ( for x being Real st x in Z holds
sin . x > 0 ) holds
( 2 (#) ((#R (1 / 2)) * sin) is_differentiable_on Z & ( for x being Real st x in Z holds
((2 (#) ((#R (1 / 2)) * sin)) `| Z) . x = (cos . x) * ((sin . x) #R (- (1 / 2))) ) )
proof end;

theorem Th49: :: FDIFF_4:49
for Z being open Subset of REAL st Z c= dom ((1 / 2) (#) ((#Z 2) * sin)) holds
( (1 / 2) (#) ((#Z 2) * sin) is_differentiable_on Z & ( for x being Real st x in Z holds
(((1 / 2) (#) ((#Z 2) * sin)) `| Z) . x = (sin . x) * (cos . x) ) )
proof end;

:: 50 f.x=sin.x+(1/2)*(sin.x ^ 2)
theorem :: FDIFF_4:50
for Z being open Subset of REAL st Z c= dom (sin + ((1 / 2) (#) ((#Z 2) * sin))) & ( for x being Real st x in Z holds
( sin . x > 0 & sin . x < 1 ) ) holds
( sin + ((1 / 2) (#) ((#Z 2) * sin)) is_differentiable_on Z & ( for x being Real st x in Z holds
((sin + ((1 / 2) (#) ((#Z 2) * sin))) `| Z) . x = ((cos . x) |^ 3) / (1 - (sin . x)) ) )
proof end;

:: 51 f.x=(1/2)*(sin.x ^ 2)-cos.x
theorem :: FDIFF_4:51
for Z being open Subset of REAL st Z c= dom (((1 / 2) (#) ((#Z 2) * sin)) - cos) & ( for x being Real st x in Z holds
( sin . x > 0 & cos . x < 1 ) ) holds
( ((1 / 2) (#) ((#Z 2) * sin)) - cos is_differentiable_on Z & ( for x being Real st x in Z holds
((((1 / 2) (#) ((#Z 2) * sin)) - cos) `| Z) . x = ((sin . x) |^ 3) / (1 - (cos . x)) ) )
proof end;

:: 52 f.x=sin.x-(1/2)*(sin ^ 2)
theorem :: FDIFF_4:52
for Z being open Subset of REAL st Z c= dom (sin - ((1 / 2) (#) ((#Z 2) * sin))) & ( for x being Real st x in Z holds
( sin . x > 0 & sin . x > - 1 ) ) holds
( sin - ((1 / 2) (#) ((#Z 2) * sin)) is_differentiable_on Z & ( for x being Real st x in Z holds
((sin - ((1 / 2) (#) ((#Z 2) * sin))) `| Z) . x = ((cos . x) |^ 3) / (1 + (sin . x)) ) )
proof end;

:: 53 f.x=-cos.x-(1/2)*(sin.x ^ 2)
theorem :: FDIFF_4:53
for Z being open Subset of REAL st Z c= dom ((- cos) - ((1 / 2) (#) ((#Z 2) * sin))) & ( for x being Real st x in Z holds
( sin . x > 0 & cos . x > - 1 ) ) holds
( (- cos) - ((1 / 2) (#) ((#Z 2) * sin)) is_differentiable_on Z & ( for x being Real st x in Z holds
(((- cos) - ((1 / 2) (#) ((#Z 2) * sin))) `| Z) . x = ((sin . x) |^ 3) / (1 + (cos . x)) ) )
proof end;

:: 54 f.x=(1/n)*(sin.x ^ n)
theorem :: FDIFF_4:54
for n being Element of NAT
for Z being open Subset of REAL st Z c= dom ((1 / n) (#) ((#Z n) * sin)) & n > 0 holds
( (1 / n) (#) ((#Z n) * sin) is_differentiable_on Z & ( for x being Real st x in Z holds
(((1 / n) (#) ((#Z n) * sin)) `| Z) . x = ((sin . x) #Z (n - 1)) * (cos . x) ) )
proof end;

:: exponential function
:: 55 f.x=exp.x*(x-1)
theorem :: FDIFF_4:55
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom (exp_R (#) f) & ( for x being Real st x in Z holds
f . x = x - 1 ) holds
( exp_R (#) f is_differentiable_on Z & ( for x being Real st x in Z holds
((exp_R (#) f) `| Z) . x = x * (exp_R . x) ) )
proof end;

:: 56 f.x=ln(exp.x/(exp.x+1))
theorem :: FDIFF_4:56
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom (ln * (exp_R / (exp_R + f))) & ( for x being Real st x in Z holds
f . x = 1 ) holds
( ln * (exp_R / (exp_R + f)) is_differentiable_on Z & ( for x being Real st x in Z holds
((ln * (exp_R / (exp_R + f))) `| Z) . x = 1 / ((exp_R . x) + 1) ) )
proof end;

:: 57 f.x=ln((exp.x-1)/exp.x)
theorem :: FDIFF_4:57
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom (ln * ((exp_R - f) / exp_R)) & ( for x being Real st x in Z holds
( f . x = 1 & (exp_R - f) . x > 0 ) ) holds
( ln * ((exp_R - f) / exp_R) is_differentiable_on Z & ( for x being Real st x in Z holds
((ln * ((exp_R - f) / exp_R)) `| Z) . x = 1 / ((exp_R . x) - 1) ) )
proof end;