:: Several Differentiation Formulas of Special Functions -- Part {IV}
:: by Bo Li and Peng Wang
::
:: Received September 29, 2006
:: Copyright (c) 2006-2011 Association of Mizar Users

begin

theorem Th1: :: FDIFF_8:1

for x being Real st x in dom tan holds
cos . x <> 0

proof end;

theorem Th2: :: FDIFF_8:2

for x being Real st x in dom cot holds
sin . x <> 0

proof end;

theorem Th3: :: FDIFF_8:3

for n being natural number
for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL,REAL st Z c= dom (f1 / f2) holds
for x being Real st x in Z holds
((f1 / f2) . x) #Z n = ((f1 . x) #Z n) / ((f2 . x) #Z n)

proof end;

theorem :: FDIFF_8:4

for a, b 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 = x + a & f2 . x = x - b ) ) holds
( f1 / f2 is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 / f2) `| Z) . x = ((- a) - b) / ((x - b) ^2) ) )

proof end;

Lm1: right_open_halfline 0 = { g where g is Real : 0 < g }
by XXREAL_1:230;

theorem :: FDIFF_8:5

for Z being open Subset of REAL st not 0 in Z & Z c= dom (ln * ((id Z) ^)) holds
( ln * ((id Z) ^) is_differentiable_on Z & ( for x being Real st x in Z holds
((ln * ((id Z) ^)) `| Z) . x = - (1 / x) ) )

proof end;

theorem Th6: :: FDIFF_8:6

for a, b being Real
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom (tan * f) & ( for x being Real st x in Z holds
f . x = (a * x) + b ) holds
( tan * f is_differentiable_on Z & ( for x being Real st x in Z holds
((tan * f) `| Z) . x = a / ((cos . ((a * x) + b)) ^2) ) )

proof end;

theorem Th7: :: FDIFF_8:7

for a, b being Real
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom (cot * f) & ( for x being Real st x in Z holds
f . x = (a * x) + b ) holds
( cot * f is_differentiable_on Z & ( for x being Real st x in Z holds
((cot * f) `| Z) . x = - (a / ((sin . ((a * x) + b)) ^2)) ) )

proof end;

theorem :: FDIFF_8:8

for Z being open Subset of REAL st not 0 in Z & Z c= dom (tan * ((id Z) ^)) holds
( tan * ((id Z) ^) is_differentiable_on Z & ( for x being Real st x in Z holds
((tan * ((id Z) ^)) `| Z) . x = - (1 / ((x ^2) * ((cos . (1 / x)) ^2))) ) )

proof end;

theorem :: FDIFF_8:9

for Z being open Subset of REAL st not 0 in Z & Z c= dom (cot * ((id Z) ^)) holds
( cot * ((id Z) ^) is_differentiable_on Z & ( for x being Real st x in Z holds
((cot * ((id Z) ^)) `| Z) . x = 1 / ((x ^2) * ((sin . (1 / x)) ^2)) ) )

proof end;

theorem :: FDIFF_8:10

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

proof end;

theorem :: FDIFF_8:11

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

proof end;

theorem :: FDIFF_8:12

for Z being open Subset of REAL st Z c= dom (tan * exp_R) holds
( tan * exp_R is_differentiable_on Z & ( for x being Real st x in Z holds
((tan * exp_R) `| Z) . x = (exp_R . x) / ((cos . (exp_R . x)) ^2) ) )

proof end;

theorem :: FDIFF_8:13

for Z being open Subset of REAL st Z c= dom (cot * exp_R) holds
( cot * exp_R is_differentiable_on Z & ( for x being Real st x in Z holds
((cot * exp_R) `| Z) . x = - ((exp_R . x) / ((sin . (exp_R . x)) ^2)) ) )

proof end;

theorem :: FDIFF_8:14

for Z being open Subset of REAL st Z c= dom (tan * ln) holds
( tan * ln is_differentiable_on Z & ( for x being Real st x in Z holds
((tan * ln) `| Z) . x = 1 / (x * ((cos . (ln . x)) ^2)) ) )

proof end;

theorem :: FDIFF_8:15

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

proof end;

theorem :: FDIFF_8:16

for Z being open Subset of REAL st Z c= dom (exp_R * tan) holds
( exp_R * tan is_differentiable_on Z & ( for x being Real st x in Z holds
((exp_R * tan) `| Z) . x = (exp_R . (tan . x)) / ((cos . x) ^2) ) )

proof end;

theorem :: FDIFF_8:17

for Z being open Subset of REAL st Z c= dom (exp_R * cot) holds
( exp_R * cot is_differentiable_on Z & ( for x being Real st x in Z holds
((exp_R * cot) `| Z) . x = - ((exp_R . (cot . x)) / ((sin . x) ^2)) ) )

proof end;

theorem :: FDIFF_8:18

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

proof end;

theorem :: FDIFF_8:19

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

proof end;

theorem :: FDIFF_8:20

for n being natural number
for Z being open Subset of REAL st Z c= dom ((#Z n) * tan) & 1 <= n holds
( (#Z n) * tan is_differentiable_on Z & ( for x being Real st x in Z holds
(((#Z n) * tan) `| Z) . x = (n * ((sin . x) #Z (n - 1))) / ((cos . x) #Z (n + 1)) ) )

proof end;

theorem :: FDIFF_8:21

for n being natural number
for Z being open Subset of REAL st Z c= dom ((#Z n) * cot) & 1 <= n holds
( (#Z n) * cot is_differentiable_on Z & ( for x being Real st x in Z holds
(((#Z n) * cot) `| Z) . x = - ((n * ((cos . x) #Z (n - 1))) / ((sin . x) #Z (n + 1))) ) )

proof end;

theorem :: FDIFF_8:22

for Z being open Subset of REAL st Z c= dom (tan + (cos ^)) & ( for x being Real st x in Z holds
( 1 + (sin . x) <> 0 & 1 - (sin . x) <> 0 ) ) holds
( tan + (cos ^) is_differentiable_on Z & ( for x being Real st x in Z holds
((tan + (cos ^)) `| Z) . x = 1 / (1 - (sin . x)) ) )

proof end;

theorem :: FDIFF_8:23

for Z being open Subset of REAL st Z c= dom (tan - (cos ^)) & ( for x being Real st x in Z holds
( 1 - (sin . x) <> 0 & 1 + (sin . x) <> 0 ) ) holds
( tan - (cos ^) is_differentiable_on Z & ( for x being Real st x in Z holds
((tan - (cos ^)) `| Z) . x = 1 / (1 + (sin . x)) ) )

proof end;

theorem :: FDIFF_8:24

for Z being open Subset of REAL st Z c= dom (tan - (id Z)) holds
( tan - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds
((tan - (id Z)) `| Z) . x = ((sin . x) ^2) / ((cos . x) ^2) ) )

proof end;

theorem :: FDIFF_8:25

for Z being open Subset of REAL st Z c= dom ((- cot) - (id Z)) holds
( (- cot) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds
(((- cot) - (id Z)) `| Z) . x = ((cos . x) ^2) / ((sin . x) ^2) ) )

proof end;

theorem :: FDIFF_8:26

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

proof end;

theorem :: FDIFF_8:27

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

proof end;

theorem :: FDIFF_8:28

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

proof end;

theorem :: FDIFF_8:29

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

proof end;

theorem :: FDIFF_8:30

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

proof end;

theorem :: FDIFF_8:31

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

proof end;

theorem :: FDIFF_8:32

for Z being open Subset of REAL st Z c= dom (ln (#) tan) holds
( ln (#) tan is_differentiable_on Z & ( for x being Real st x in Z holds
((ln (#) tan) `| Z) . x = (((sin . x) / (cos . x)) / x) + ((ln . x) / ((cos . x) ^2)) ) )

proof end;

theorem :: FDIFF_8:33

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

proof end;

theorem :: FDIFF_8:34

for Z being open Subset of REAL st not 0 in Z & Z c= dom (((id Z) ^) (#) tan) holds
( ((id Z) ^) (#) tan is_differentiable_on Z & ( for x being Real st x in Z holds
((((id Z) ^) (#) tan) `| Z) . x = (- (((sin . x) / (cos . x)) / (x ^2))) + ((1 / x) / ((cos . x) ^2)) ) )

proof end;

theorem :: FDIFF_8:35

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

proof end;