:: Several Differentiation Formulas of Special Functions -- Part {V}
:: by Peng Wang and Bo Li
::
:: Received July 9, 2007
:: Copyright (c) 2007 Association of Mizar Users

definition

func sec -> PartFunc of REAL , REAL equals :: FDIFF_9:def 1
cos ^ ;
coherence
cos ^ is PartFunc of REAL , REAL ;
func cosec -> PartFunc of REAL , REAL equals :: FDIFF_9:def 2
sin ^ ;
coherence
sin ^ is PartFunc of REAL , REAL ;

end;

:: deftheorem defines sec FDIFF_9:def 1 :

sec = cos ^ ;

:: deftheorem defines cosec FDIFF_9:def 2 :

cosec = sin ^ ;

theorem Th1: :: FDIFF_9:1

for x being Real st cos . x <> 0 holds
( sec is_differentiable_in x & diff sec ,x = (sin . x) / ((cos . x) ^2 ) )

proof end;

theorem Th2: :: FDIFF_9:2

for x being Real st sin . x <> 0 holds
( cosec is_differentiable_in x & diff cosec ,x = - ((cos . x) / ((sin . x) ^2 )) )

proof end;

theorem Th3: :: FDIFF_9:3

for x being Real
for n being natural number holds (1 / x) #Z n = 1 / (x #Z n)

proof end;

theorem :: FDIFF_9:4

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

proof end;

theorem :: FDIFF_9:5

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

proof end;

theorem Th6: :: FDIFF_9:6

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

proof end;

theorem Th7: :: FDIFF_9:7

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

proof end;

theorem :: FDIFF_9:8

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

proof end;

theorem :: FDIFF_9:9

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

proof end;

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

proof end;

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

proof end;

theorem :: FDIFF_9:12

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

proof end;

theorem :: FDIFF_9:13

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

proof end;

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

theorem :: FDIFF_9:14

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

proof end;

theorem :: FDIFF_9:15

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

proof end;

theorem :: FDIFF_9:16

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

proof end;

theorem :: FDIFF_9:17

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

proof end;

theorem :: FDIFF_9:18

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

proof end;

theorem :: FDIFF_9:19

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

proof end;

theorem :: FDIFF_9:20

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

proof end;

theorem :: FDIFF_9:21

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

proof end;

theorem :: FDIFF_9:22

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

proof end;

theorem :: FDIFF_9:23

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

proof end;

theorem :: FDIFF_9:24

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

proof end;

theorem :: FDIFF_9:25

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

proof end;

theorem :: FDIFF_9: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) (#) (sec * f)) - (id Z)) & ( for x being Real st x in Z holds
( f . x = a * x & a <> 0 ) ) holds
( ((1 / a) (#) (sec * f)) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds
((((1 / a) (#) (sec * f)) - (id Z)) `| Z) . x = ((sin . (a * x)) - ((cos . (a * x)) ^2 )) / ((cos . (a * x)) ^2 ) ) )

proof end;

theorem :: FDIFF_9: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)) (#) (cosec * f)) - (id Z)) & ( for x being Real st x in Z holds
( f . x = a * x & a <> 0 ) ) holds
( ((- (1 / a)) (#) (cosec * f)) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds
((((- (1 / a)) (#) (cosec * f)) - (id Z)) `| Z) . x = ((cos . (a * x)) - ((sin . (a * x)) ^2 )) / ((sin . (a * x)) ^2 ) ) )

proof end;

theorem :: FDIFF_9: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 (#) sec ) & ( for x being Real st x in Z holds
f . x = (a * x) + b ) holds
( f (#) sec is_differentiable_on Z & ( for x being Real st x in Z holds
((f (#) sec ) `| Z) . x = (a / (cos . x)) + ((((a * x) + b) * (sin . x)) / ((cos . x) ^2 )) ) )

proof end;

theorem :: FDIFF_9: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 (#) cosec ) & ( for x being Real st x in Z holds
f . x = (a * x) + b ) holds
( f (#) cosec is_differentiable_on Z & ( for x being Real st x in Z holds
((f (#) cosec ) `| Z) . x = (a / (sin . x)) - ((((a * x) + b) * (cos . x)) / ((sin . x) ^2 )) ) )

proof end;

theorem :: FDIFF_9:30

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

proof end;

theorem :: FDIFF_9:31

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

proof end;

theorem :: FDIFF_9:32

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

proof end;

theorem :: FDIFF_9:33

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

proof end;

theorem :: FDIFF_9:34

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

proof end;

theorem :: FDIFF_9:35

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

proof end;

theorem :: FDIFF_9:36

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

proof end;

theorem :: FDIFF_9:37

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

proof end;

theorem :: FDIFF_9:38

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

proof end;

theorem :: FDIFF_9:39

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

proof end;

theorem :: FDIFF_9:40

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

proof end;

theorem :: FDIFF_9:41

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

proof end;

theorem :: FDIFF_9:42

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

proof end;

theorem :: FDIFF_9:43

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

proof end;

theorem :: FDIFF_9:44

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

proof end;

theorem :: FDIFF_9:45

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

proof end;