:: Several Differentiation Formulas of Special Functions -- Part {V}
:: by Peng Wang and Bo Li
::
:: Received July 9, 2007
:: Copyright (c) 2007-2012 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 &amp; diff (sec,x) = (sin . x) / ((cos . x) ^2) )
proofend;

theorem Th2: :: FDIFF_9:2
for x being Real st sin . x <> 0 holds
( cosec is_differentiable_in x &amp; diff (cosec,x) = - ((cos . x) / ((sin . x) ^2)) )
proofend;

theorem Th3: :: FDIFF_9:3
for x being Real
for n being Nat holds (1 / x) #Z n = 1 / (x #Z n)
proofend;

:: f.x=sec.x
theorem :: FDIFF_9:4
for Z being open Subset of REAL st Z c= dom sec holds
( sec is_differentiable_on Z &amp; ( for x being Real st x in Z holds
(sec `| Z) . x = (sin . x) / ((cos . x) ^2) ) )
proofend;

:: f.x=cosec.x
theorem :: FDIFF_9:5
for Z being open Subset of REAL st Z c= dom cosec holds
( cosec is_differentiable_on Z &amp; ( for x being Real st x in Z holds
(cosec `| Z) . x = - ((cos . x) / ((sin . x) ^2)) ) )
proofend;

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

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

:: f.x = sec.(1/x)
theorem :: FDIFF_9:8
for Z being open Subset of REAL st not 0 in Z &amp; Z c= dom (sec * ((id Z) ^)) holds
( sec * ((id Z) ^) is_differentiable_on Z &amp; ( for x being Real st x in Z holds
((sec * ((id Z) ^)) `| Z) . x = - ((sin . (1 / x)) / ((x ^2) * ((cos . (1 / x)) ^2))) ) )
proofend;

:: f.x = cosec.(1/x)
theorem :: FDIFF_9:9
for Z being open Subset of REAL st not 0 in Z &amp; Z c= dom (cosec * ((id Z) ^)) holds
( cosec * ((id Z) ^) is_differentiable_on Z &amp; ( for x being Real st x in Z holds
((cosec * ((id Z) ^)) `| Z) . x = (cos . (1 / x)) / ((x ^2) * ((sin . (1 / x)) ^2)) ) )
proofend;

:: f.x = sec.(a+b*x+c*x^2)
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))) &amp; f2 = #Z 2 &amp; ( for x being Real st x in Z holds
f1 . x = a + (b * x) ) holds
( sec * (f1 + (c (#) f2)) is_differentiable_on Z &amp; ( 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) ) )
proofend;

:: f.x = cosec.(a+b*x+c*x^2)
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))) &amp; f2 = #Z 2 &amp; ( for x being Real st x in Z holds
f1 . x = a + (b * x) ) holds
( cosec * (f1 + (c (#) f2)) is_differentiable_on Z &amp; ( 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)) ) )
proofend;

:: f.x = sec.(exp_R.x)
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 &amp; ( 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) ) )
proofend;

:: f.x = cosec.(exp_R.x)
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 &amp; ( 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)) ) )
proofend;

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

:: f.x = sec.(ln.x)
theorem :: FDIFF_9:14
for Z being open Subset of REAL st Z c= dom (sec * ln) holds
( sec * ln is_differentiable_on Z &amp; ( for x being Real st x in Z holds
((sec * ln) `| Z) . x = (sin . (ln . x)) / (x * ((cos . (ln . x)) ^2)) ) )
proofend;

:: f.x = cosec.(ln.x)
theorem :: FDIFF_9:15
for Z being open Subset of REAL st Z c= dom (cosec * ln) holds
( cosec * ln is_differentiable_on Z &amp; ( for x being Real st x in Z holds
((cosec * ln) `| Z) . x = - ((cos . (ln . x)) / (x * ((sin . (ln . x)) ^2))) ) )
proofend;

:: f.x = exp_R.(sec.x)
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 &amp; ( for x being Real st x in Z holds
((exp_R * sec) `| Z) . x = ((exp_R . (sec . x)) * (sin . x)) / ((cos . x) ^2) ) )
proofend;

:: f.x = exp_R.(cosec.x)
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 &amp; ( for x being Real st x in Z holds
((exp_R * cosec) `| Z) . x = - (((exp_R . (cosec . x)) * (cos . x)) / ((sin . x) ^2)) ) )
proofend;

:: f.x = ln.(sec.x)
theorem :: FDIFF_9:18
for Z being open Subset of REAL st Z c= dom (ln * sec) holds
( ln * sec is_differentiable_on Z &amp; ( for x being Real st x in Z holds
((ln * sec) `| Z) . x = (sin . x) / (cos . x) ) )
proofend;

:: f.x = ln.(cosec.x)
theorem :: FDIFF_9:19
for Z being open Subset of REAL st Z c= dom (ln * cosec) holds
( ln * cosec is_differentiable_on Z &amp; ( for x being Real st x in Z holds
((ln * cosec) `| Z) . x = - ((cos . x) / (sin . x)) ) )
proofend;

:: f.x=(sec.x) #Z n
theorem :: FDIFF_9:20
for n being Nat
for Z being open Subset of REAL st Z c= dom ((#Z n) * sec) &amp; 1 <= n holds
( (#Z n) * sec is_differentiable_on Z &amp; ( for x being Real st x in Z holds
(((#Z n) * sec) `| Z) . x = (n * (sin . x)) / ((cos . x) #Z (n + 1)) ) )
proofend;

:: f.x=(cosec.x) #Z n
theorem :: FDIFF_9:21
for n being Nat
for Z being open Subset of REAL st Z c= dom ((#Z n) * cosec) &amp; 1 <= n holds
( (#Z n) * cosec is_differentiable_on Z &amp; ( for x being Real st x in Z holds
(((#Z n) * cosec) `| Z) . x = - ((n * (cos . x)) / ((sin . x) #Z (n + 1))) ) )
proofend;

:: f.x = sec.x-x
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 &amp; ( for x being Real st x in Z holds
((sec - (id Z)) `| Z) . x = ((sin . x) - ((cos . x) ^2)) / ((cos . x) ^2) ) )
proofend;

:: f.x = -cosec.x-x
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 &amp; ( for x being Real st x in Z holds
(((- cosec) - (id Z)) `| Z) . x = ((cos . x) - ((sin . x) ^2)) / ((sin . x) ^2) ) )
proofend;

:: f.x = exp_R.x*sec.x
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 &amp; ( 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)) ) )
proofend;

:: f.x = exp_R.x*cosec.x
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 &amp; ( 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)) ) )
proofend;

:: f.x = (1/a)*sec.(a*x)-x
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)) &amp; ( for x being Real st x in Z holds
( f . x = a * x &amp; a <> 0 ) ) holds
( ((1 / a) (#) (sec * f)) - (id Z) is_differentiable_on Z &amp; ( 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) ) )
proofend;

:: f.x = (-1/a)*cosec.(a*x)-x
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)) &amp; ( for x being Real st x in Z holds
( f . x = a * x &amp; a <> 0 ) ) holds
( ((- (1 / a)) (#) (cosec * f)) - (id Z) is_differentiable_on Z &amp; ( 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) ) )
proofend;

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

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

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

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

:: f.x = 1/x*sec.x
theorem :: FDIFF_9:32
for Z being open Subset of REAL st not 0 in Z &amp; Z c= dom (((id Z) ^) (#) sec) holds
( ((id Z) ^) (#) sec is_differentiable_on Z &amp; ( 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)) ) )
proofend;

:: f.x = 1/x*cosec.x
theorem :: FDIFF_9:33
for Z being open Subset of REAL st not 0 in Z &amp; Z c= dom (((id Z) ^) (#) cosec) holds
( ((id Z) ^) (#) cosec is_differentiable_on Z &amp; ( 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)) ) )
proofend;

:: f.x = sec.(sin.x)
theorem :: FDIFF_9:34
for Z being open Subset of REAL st Z c= dom (sec * sin) holds
( sec * sin is_differentiable_on Z &amp; ( for x being Real st x in Z holds
((sec * sin) `| Z) . x = ((cos . x) * (sin . (sin . x))) / ((cos . (sin . x)) ^2) ) )
proofend;

:: f.x = sec.(cos.x)
theorem :: FDIFF_9:35
for Z being open Subset of REAL st Z c= dom (sec * cos) holds
( sec * cos is_differentiable_on Z &amp; ( for x being Real st x in Z holds
((sec * cos) `| Z) . x = - (((sin . x) * (sin . (cos . x))) / ((cos . (cos . x)) ^2)) ) )
proofend;

:: f.x = cosec.(sin.x)
theorem :: FDIFF_9:36
for Z being open Subset of REAL st Z c= dom (cosec * sin) holds
( cosec * sin is_differentiable_on Z &amp; ( for x being Real st x in Z holds
((cosec * sin) `| Z) . x = - (((cos . x) * (cos . (sin . x))) / ((sin . (sin . x)) ^2)) ) )
proofend;

:: f.x = cosec.(cos.x)
theorem :: FDIFF_9:37
for Z being open Subset of REAL st Z c= dom (cosec * cos) holds
( cosec * cos is_differentiable_on Z &amp; ( for x being Real st x in Z holds
((cosec * cos) `| Z) . x = ((sin . x) * (cos . (cos . x))) / ((sin . (cos . x)) ^2) ) )
proofend;

:: f.x = sec.(tan.x)
theorem :: FDIFF_9:38
for Z being open Subset of REAL st Z c= dom (sec * tan) holds
( sec * tan is_differentiable_on Z &amp; ( for x being Real st x in Z holds
((sec * tan) `| Z) . x = ((sin . (tan . x)) / ((cos . x) ^2)) / ((cos . (tan . x)) ^2) ) )
proofend;

:: f.x = sec.(cot.x)
theorem :: FDIFF_9:39
for Z being open Subset of REAL st Z c= dom (sec * cot) holds
( sec * cot is_differentiable_on Z &amp; ( for x being Real st x in Z holds
((sec * cot) `| Z) . x = - (((sin . (cot . x)) / ((sin . x) ^2)) / ((cos . (cot . x)) ^2)) ) )
proofend;

:: f.x = cosec.(tan.x)
theorem :: FDIFF_9:40
for Z being open Subset of REAL st Z c= dom (cosec * tan) holds
( cosec * tan is_differentiable_on Z &amp; ( for x being Real st x in Z holds
((cosec * tan) `| Z) . x = - (((cos . (tan . x)) / ((cos . x) ^2)) / ((sin . (tan . x)) ^2)) ) )
proofend;

:: f.x = cosec.(cot.x)
theorem :: FDIFF_9:41
for Z being open Subset of REAL st Z c= dom (cosec * cot) holds
( cosec * cot is_differentiable_on Z &amp; ( for x being Real st x in Z holds
((cosec * cot) `| Z) . x = ((cos . (cot . x)) / ((sin . x) ^2)) / ((sin . (cot . x)) ^2) ) )
proofend;

:: f.x = tan.x*sec.x
theorem :: FDIFF_9:42
for Z being open Subset of REAL st Z c= dom (tan (#) sec) holds
( tan (#) sec is_differentiable_on Z &amp; ( 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)) ) )
proofend;

:: f.x = cot.x*sec.x
theorem :: FDIFF_9:43
for Z being open Subset of REAL st Z c= dom (cot (#) sec) holds
( cot (#) sec is_differentiable_on Z &amp; ( 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)) ) )
proofend;

:: f.x = tan.x*cosec.x
theorem :: FDIFF_9:44
for Z being open Subset of REAL st Z c= dom (tan (#) cosec) holds
( tan (#) cosec is_differentiable_on Z &amp; ( 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)) ) )
proofend;

:: f.x = cot.x*cosec.x
theorem :: FDIFF_9:45
for Z being open Subset of REAL st Z c= dom (cot (#) cosec) holds
( cot (#) cosec is_differentiable_on Z &amp; ( 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)) ) )
proofend;