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

begin

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;

theorem Th1: :: FDIFF_6:1

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

proof end;

theorem Th2: :: FDIFF_6:2

for a, x 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;

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;

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;

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;

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;

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;

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;

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;

theorem :: FDIFF_6:10

for Z being open Subset of REAL
for f2, f1 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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

theorem :: FDIFF_6:44

for a being Real
for Z being open Subset of REAL
for f1, f 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;

theorem :: FDIFF_6:45

for a being Real
for Z being open Subset of REAL
for f1, f 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;

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;

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;

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;

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;

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;