:: 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;