:: Several Differentiable Formulas of Special Functions -- Part {II}
:: by Yan Zhang , Bo Li and Xiquan Liang
::
:: Received November 23, 2005
:: Copyright (c) 2005-2021 Association of Mizar Users

Lm1: for x being Real holds 1 - (cos (2 * x)) = 2 * ((sin x) ^2)

proof end;

Lm2: for x being Real holds 1 + (cos (2 * x)) = 2 * ((cos x) ^2)

proof end;

Lm3: for x being Real st sin . x > 0 holds
sin . x = ((1 - (cos . x)) * (1 + (cos . x))) #R (1 / 2)

proof end;

Lm4: for x being Real st sin . x > 0 & cos . x < 1 & cos . x > - 1 holds
(sin . x) / ((1 - (cos . x)) #R (1 / 2)) = (1 + (cos . x)) #R (1 / 2)

proof end;

:: a ^ x=exp.(x*ln a)

theorem Th1: :: FDIFF_6:1

for x, a being Real st a > 0 holds
exp_R . (x * (log (number_e,a))) = a #R x

proof end;

:: 15 a ^ (-x)=exp.(-x*ln a)

theorem Th2: :: FDIFF_6:2

for x, a being Real st a > 0 holds
exp_R . (- (x * (log (number_e,a)))) = a #R (- x)

proof end;

Lm5: for x being Real st sin . x > 0 & cos . x < 1 & cos . x > - 1 holds
(sin . x) / ((1 + (cos . x)) #R (1 / 2)) = (1 - (cos . x)) #R (1 / 2)

proof end;

:: 1 f.x=a^2-x^2

theorem Th3: :: FDIFF_6:3

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;

:: 2 f.x=(a^2+x^2)/(a^2-x^2)

theorem Th4: :: FDIFF_6:4

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

proof end;

:: 3 f.x=ln((a^2+x^2)/(a^2-x^2))

theorem Th5: :: FDIFF_6:5

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

proof end;

:: 4 f.x=(1/(4*a^2))*ln((a^2+x^2)/(a^2-x^2))

theorem :: FDIFF_6:6

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

proof end;

:: 5 f.x=x^2/(1+x^2)

theorem Th7: :: FDIFF_6:7

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

proof end;

:: 6 f.x=(1/2)*ln(x^2/(1+x^2))

theorem :: FDIFF_6:8

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

proof end;

:: 7 f.x=ln(x^n)

theorem :: FDIFF_6:9

for n being Element of NAT
for Z being open Subset of REAL st Z c= dom (ln * (#Z n)) & ( for x being Real st x in Z holds
x > 0 ) holds
( ln * (#Z n) is_differentiable_on Z & ( for x being Real st x in Z holds
((ln * (#Z n)) `| Z) . x = n / x ) )

proof end;

:: 8 f.x=1/x+ln((x-1)/x)

theorem :: FDIFF_6:10

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

proof end;

:: 10 f.x=a ^ x=exp.(x*ln a)

theorem Th11: :: FDIFF_6:11

for a being Real
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 * (log (number_e,a)) ) & a > 0 holds
( exp_R * f is_differentiable_on Z & ( for x being Real st x in Z holds
((exp_R * f) `| Z) . x = (a #R x) * (log (number_e,a)) ) )

proof end;

:: 11 f.x=(a ^ x)*(x-1/ln a)/ln a

theorem :: FDIFF_6:12

for a being Real
for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL,REAL st Z c= dom ((1 / (log (number_e,a))) (#) ((exp_R * f1) (#) f2)) & ( for x being Real st x in Z holds
( f1 . x = x * (log (number_e,a)) & f2 . x = x - (1 / (log (number_e,a))) ) ) & a > 0 & a <> 1 holds
( (1 / (log (number_e,a))) (#) ((exp_R * f1) (#) f2) is_differentiable_on Z & ( for x being Real st x in Z holds
(((1 / (log (number_e,a))) (#) ((exp_R * f1) (#) f2)) `| Z) . x = x * (a #R x) ) )

proof end;

:: 12 f.x=a ^ x*exp(x)/(1+ln a)

theorem :: FDIFF_6:13

for a being Real
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom ((1 / (1 + (log (number_e,a)))) (#) ((exp_R * f) (#) exp_R)) & ( for x being Real st x in Z holds
f . x = x * (log (number_e,a)) ) & a > 0 & a <> 1 / number_e holds
( (1 / (1 + (log (number_e,a)))) (#) ((exp_R * f) (#) exp_R) is_differentiable_on Z & ( for x being Real st x in Z holds
(((1 / (1 + (log (number_e,a)))) (#) ((exp_R * f) (#) exp_R)) `| Z) . x = (a #R x) * (exp_R . x) ) )

proof end;

:: 13 f.x=exp_R(-x)

theorem Th14: :: FDIFF_6:14

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 ) holds
( exp_R * f is_differentiable_on Z & ( for x being Real st x in Z holds
((exp_R * f) `| Z) . x = - (exp_R (- x)) ) )

proof end;

:: 14 f.x=-(x+1)*exp_R(-x)

theorem :: FDIFF_6:15

for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL,REAL st Z c= dom (f1 (#) (exp_R * f2)) & ( for x being Real st x in Z holds
( f1 . x = (- x) - 1 & f2 . x = - x ) ) holds
( f1 (#) (exp_R * f2) is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 (#) (exp_R * f2)) `| Z) . x = x / (exp_R x) ) )

proof end;

:: 16 f.x=a ^ (-x)=exp_R.(-x*ln a)

theorem Th16: :: FDIFF_6:16

for a being Real
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 * (log (number_e,a))) ) & a > 0 holds
( - (exp_R * f) is_differentiable_on Z & ( for x being Real st x in Z holds
((- (exp_R * f)) `| Z) . x = (a #R (- x)) * (log (number_e,a)) ) )

proof end;

:: 17 f.x=-(a ^ -x)*(x+1/ln a)/ln a

theorem :: FDIFF_6:17

for a being Real
for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL,REAL st Z c= dom ((1 / (log (number_e,a))) (#) ((- (exp_R * f1)) (#) f2)) & ( for x being Real st x in Z holds
( f1 . x = - (x * (log (number_e,a))) & f2 . x = x + (1 / (log (number_e,a))) ) ) & a > 0 & a <> 1 holds
( (1 / (log (number_e,a))) (#) ((- (exp_R * f1)) (#) f2) is_differentiable_on Z & ( for x being Real st x in Z holds
(((1 / (log (number_e,a))) (#) ((- (exp_R * f1)) (#) f2)) `| Z) . x = x / (a #R x) ) )

proof end;

:: 18 f.x=(1/(ln a-1))*a ^ x/exp_R(x)

theorem :: FDIFF_6:18

for a being Real
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom ((1 / ((log (number_e,a)) - 1)) (#) ((exp_R * f) / exp_R)) & ( for x being Real st x in Z holds
f . x = x * (log (number_e,a)) ) & a > 0 & a <> number_e holds
( (1 / ((log (number_e,a)) - 1)) (#) ((exp_R * f) / exp_R) is_differentiable_on Z & ( for x being Real st x in Z holds
(((1 / ((log (number_e,a)) - 1)) (#) ((exp_R * f) / exp_R)) `| Z) . x = (a #R x) / (exp_R . x) ) )

proof end;

:: 19 f.x=(1/(1-ln a))*exp_R(x)/a ^ x

theorem :: FDIFF_6:19

for a being Real
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom ((1 / (1 - (log (number_e,a)))) (#) (exp_R / (exp_R * f))) & ( for x being Real st x in Z holds
f . x = x * (log (number_e,a)) ) & a > 0 & a <> number_e holds
( (1 / (1 - (log (number_e,a)))) (#) (exp_R / (exp_R * f)) is_differentiable_on Z & ( for x being Real st x in Z holds
(((1 / (1 - (log (number_e,a)))) (#) (exp_R / (exp_R * f))) `| Z) . x = (exp_R . x) / (a #R x) ) )

proof end;

:: 20 f.x=ln(exp_R.x+1)

theorem :: FDIFF_6:20

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

proof end;

:: 21 f.x=ln(exp_R.x-1)

theorem :: FDIFF_6:21

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

proof end;

:: 22 f.x=-ln(1-exp_R.x)

theorem :: FDIFF_6:22

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

proof end;

:: 23 f.x=exp_R(2*x)+1

theorem Th23: :: FDIFF_6:23

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

proof end;

:: 24 f.x=(1/2)*ln(exp_R(2*x)+1)

theorem :: FDIFF_6:24

for Z being open Subset of REAL
for f, f1 being PartFunc of REAL,REAL st Z c= dom ((1 / 2) (#) (ln * f)) & f = ((#Z 2) * exp_R) + f1 & ( for x being Real st x in Z holds
f1 . x = 1 ) holds
( (1 / 2) (#) (ln * f) is_differentiable_on Z & ( for x being Real st x in Z holds
(((1 / 2) (#) (ln * f)) `| Z) . x = (exp_R x) / ((exp_R x) + (exp_R (- x))) ) )

proof end;

:: 25 f.x=exp_R(2*x)-1

theorem Th25: :: FDIFF_6:25

for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom (((#Z 2) * exp_R) - f) & ( for x being Real st x in Z holds
f . x = 1 ) holds
( ((#Z 2) * exp_R) - f is_differentiable_on Z & ( for x being Real st x in Z holds
((((#Z 2) * exp_R) - f) `| Z) . x = 2 * (exp_R (2 * x)) ) )

proof end;

:: 26 f.x=(1/2)*ln(exp_R(2*x)-1)

theorem :: FDIFF_6:26

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

proof end;

:: 27 f.x=(exp_R.x-1)^2

theorem Th27: :: FDIFF_6:27

for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom ((#Z 2) * (exp_R - f)) & ( for x being Real st x in Z holds
f . x = 1 ) holds
( (#Z 2) * (exp_R - f) is_differentiable_on Z & ( for x being Real st x in Z holds
(((#Z 2) * (exp_R - f)) `| Z) . x = (2 * (exp_R . x)) * ((exp_R . x) - 1) ) )

proof end;

:: 28 f.x=ln((exp_R.x-1)^2/exp_R.x)

theorem :: FDIFF_6:28

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

proof end;

:: 29 f.x=(exp_R.x+1)^2

theorem Th29: :: FDIFF_6:29

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

proof end;

:: 30 f.x=ln((exp_R.x+1)^2/exp_R.x)

theorem :: FDIFF_6:30

for Z being open Subset of REAL
for f, f1 being PartFunc of REAL,REAL st Z c= dom f & f = ln * (((#Z 2) * (exp_R + f1)) / exp_R) & ( for x being Real st x in Z holds
f1 . x = 1 ) holds
( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = ((exp_R . x) - 1) / ((exp_R . x) + 1) ) )

proof end;

:: 31 f.x=(1-exp_R.x)^2

theorem Th31: :: FDIFF_6:31

for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom ((#Z 2) * (f - exp_R)) & ( for x being Real st x in Z holds
f . x = 1 ) holds
( (#Z 2) * (f - exp_R) is_differentiable_on Z & ( for x being Real st x in Z holds
(((#Z 2) * (f - exp_R)) `| Z) . x = - ((2 * (exp_R . x)) * (1 - (exp_R . x))) ) )

proof end;

:: 32 f.x=ln(exp_R.x/(1-exp_R.x)^2)

theorem :: FDIFF_6:32

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

proof end;

:: 33 f.x=ln(exp_R.x/(1+exp_R.x)^2)

theorem :: FDIFF_6:33

for Z being open Subset of REAL
for f, f1 being PartFunc of REAL,REAL st Z c= dom f & f = ln * (exp_R / ((#Z 2) * (f1 + exp_R))) & ( for x being Real st x in Z holds
f1 . x = 1 ) holds
( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = (1 - (exp_R . x)) / (1 + (exp_R . x)) ) )

proof end;

:: 34 f.x=ln(exp_R(x)+exp_R(-x))

theorem :: FDIFF_6:34

for Z being open Subset of REAL
for f, f1 being PartFunc of REAL,REAL st Z c= dom (ln * f) & f = exp_R + (exp_R * f1) & ( for x being Real st x in Z holds
f1 . x = - x ) holds
( ln * f is_differentiable_on Z & ( for x being Real st x in Z holds
((ln * f) `| Z) . x = ((exp_R x) - (exp_R (- x))) / ((exp_R x) + (exp_R (- x))) ) )

proof end;

:: 35 f.x=ln(exp_R(x)-exp_R(-x))

theorem :: FDIFF_6:35

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

proof end;

:: 36 f.x=(2/3)*((1+exp_R.x) ^ (3/2))

theorem :: FDIFF_6:36

for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom ((2 / 3) (#) ((#R (3 / 2)) * (f + exp_R))) & ( for x being Real st x in Z holds
f . x = 1 ) holds
( (2 / 3) (#) ((#R (3 / 2)) * (f + exp_R)) is_differentiable_on Z & ( for x being Real st x in Z holds
(((2 / 3) (#) ((#R (3 / 2)) * (f + exp_R))) `| Z) . x = (exp_R . x) * ((1 + (exp_R . x)) #R (1 / 2)) ) )

proof end;

:: 37 f.x=(2/(3*lna))*((1+a |^x) ^ (3/2))

theorem :: FDIFF_6:37

for a being Real
for Z being open Subset of REAL
for f, f1 being PartFunc of REAL,REAL st Z c= dom ((2 / (3 * (log (number_e,a)))) (#) ((#R (3 / 2)) * (f + (exp_R * f1)))) & ( for x being Real st x in Z holds
( f . x = 1 & f1 . x = x * (log (number_e,a)) ) ) & a > 0 & a <> 1 holds
( (2 / (3 * (log (number_e,a)))) (#) ((#R (3 / 2)) * (f + (exp_R * f1))) is_differentiable_on Z & ( for x being Real st x in Z holds
(((2 / (3 * (log (number_e,a)))) (#) ((#R (3 / 2)) * (f + (exp_R * f1)))) `| Z) . x = (a #R x) * ((1 + (a #R x)) #R (1 / 2)) ) )

proof end;

:: 38 f.x=(-1/2)*cos(2*x)

theorem :: FDIFF_6:38

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

proof end;

theorem :: FDIFF_6:39

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

proof end;

theorem :: FDIFF_6:40

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

proof end;

Lm6: for Z being open Subset of REAL
for f1 being PartFunc of REAL,REAL st Z c= dom (f1 + (2 (#) sin)) & ( for x being Real st x in Z holds
f1 . x = 1 ) holds
( f1 + (2 (#) sin) is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 + (2 (#) sin)) `| Z) . x = 2 * (cos . x) ) )

proof end;

theorem :: FDIFF_6:41

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

proof end;

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

proof end;

theorem :: FDIFF_6:42

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

proof end;

:: 43 f.x=1/(4*a)*sin(2*a*x)

theorem Th43: :: FDIFF_6:43

for a being Real
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom ((1 / (4 * a)) (#) (sin * f)) & ( for x being Real st x in Z holds
f . x = (2 * a) * x ) & a <> 0 holds
( (1 / (4 * a)) (#) (sin * f) is_differentiable_on Z & ( for x being Real st x in Z holds
(((1 / (4 * a)) (#) (sin * f)) `| Z) . x = (1 / 2) * (cos ((2 * a) * x)) ) )

proof end;

:: 44 f.x=x/2-1/(4*a)*sin(2*a*x)

theorem :: FDIFF_6:44

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

proof end;

:: 45 f.x=x/2+1/(4*a)*sin(2*a*x)

theorem :: FDIFF_6:45

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

proof end;

:: 46 f.x=(1/n)*(cos.x ^ n)

theorem Th46: :: FDIFF_6:46

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

proof end;

:: 47 f.x=(1/3)*(cos.x ^ 3)-cos.x

theorem :: FDIFF_6:47

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

proof end;

:: 48 f.x=sin.x-(1/3)*(sin.x ^ 3)

theorem :: FDIFF_6:48

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

proof end;

:: 49 f.x=sin(ln x)

theorem :: FDIFF_6:49

for Z being open Subset of REAL st Z c= dom (sin * ln) holds
( sin * ln is_differentiable_on Z & ( for x being Real st x in Z holds
((sin * ln) `| Z) . x = (cos . (log (number_e,x))) / x ) )

proof end;

:: 50 f.x=-cos(ln x)

theorem :: FDIFF_6:50

for Z being open Subset of REAL st Z c= dom (- (cos * ln)) holds
( - (cos * ln) is_differentiable_on Z & ( for x being Real st x in Z holds
((- (cos * ln)) `| Z) . x = (sin . (log (number_e,x))) / x ) )

proof end;