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

begin

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 st not 0 in Z & 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 . (1 / x)) / ((x ^2) * ((cos . (1 / x)) ^2))) ) )

proof end;

theorem :: FDIFF_9:9

for Z being open Subset of REAL st not 0 in Z & 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 . (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 st not 0 in Z & Z c= dom (((id Z) ^) (#) sec) holds
( ((id Z) ^) (#) sec is_differentiable_on Z & ( for x being Real st x in Z holds
((((id Z) ^) (#) 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 st not 0 in Z & Z c= dom (((id Z) ^) (#) cosec) holds
( ((id Z) ^) (#) cosec is_differentiable_on Z & ( for x being Real st x in Z holds
((((id Z) ^) (#) 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;