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

begin

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

theorem :: FDIFF_4:11

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

theorem Th12: :: FDIFF_4:12

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

theorem Th13: :: FDIFF_4:13

for c, 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 + (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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

theorem :: FDIFF_4:32

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

theorem :: FDIFF_4:33

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

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;