:: by Peng Wang and Bo Li

::

:: Received July 9, 2007

:: Copyright (c) 2007-2019 Association of Mizar Users

definition
end;

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) )

( 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)) )

( cosec is_differentiable_in x & diff (cosec,x) = - ((cos . x) / ((sin . x) ^2)) )

proof end;

:: 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 & ( for x being Real st x in Z holds

(sec `| Z) . x = (sin . x) / ((cos . x) ^2) ) )

( sec is_differentiable_on Z & ( for x being Real st x in Z holds

(sec `| Z) . x = (sin . x) / ((cos . x) ^2) ) )

proof end;

:: 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 & ( for x being Real st x in Z holds

(cosec `| Z) . x = - ((cos . x) / ((sin . x) ^2)) ) )

( cosec is_differentiable_on Z & ( for x being Real st x in Z holds

(cosec `| Z) . x = - ((cos . x) / ((sin . x) ^2)) ) )

proof end;

:: 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) & ( 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) ) )

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;

:: 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) & ( 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)) ) )

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;

:: f.x = sec.(1/x)

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))) ) )

( 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;

:: f.x = cosec.(1/x)

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)) ) )

( 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;

:: f.x = sec.(a+b*x+c*x^2)

theorem :: FDIFF_9:10

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

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;

:: f.x = cosec.(a+b*x+c*x^2)

theorem :: FDIFF_9:11

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

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;

:: 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 & ( 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) ) )

( 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;

:: 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 & ( 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)) ) )

( 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;

:: 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 & ( for x being Real st x in Z holds

((sec * ln) `| Z) . x = (sin . (ln . x)) / (x * ((cos . (ln . x)) ^2)) ) )

( 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;

:: 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 & ( for x being Real st x in Z holds

((cosec * ln) `| Z) . x = - ((cos . (ln . x)) / (x * ((sin . (ln . x)) ^2))) ) )

( 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;

:: 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 & ( for x being Real st x in Z holds

((exp_R * sec) `| Z) . x = ((exp_R . (sec . x)) * (sin . x)) / ((cos . x) ^2) ) )

( 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;

:: 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 & ( for x being Real st x in Z holds

((exp_R * cosec) `| Z) . x = - (((exp_R . (cosec . x)) * (cos . x)) / ((sin . x) ^2)) ) )

( 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;

:: 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 & ( for x being Real st x in Z holds

((ln * sec) `| Z) . x = (sin . x) / (cos . x) ) )

( 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;

:: 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 & ( for x being Real st x in Z holds

((ln * cosec) `| Z) . x = - ((cos . x) / (sin . x)) ) )

( 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;

:: 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) & 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)) ) )

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;

:: 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) & 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))) ) )

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;

:: 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 & ( for x being Real st x in Z holds

((sec - (id Z)) `| Z) . x = ((sin . x) - ((cos . x) ^2)) / ((cos . x) ^2) ) )

( 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;

:: 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 & ( for x being Real st x in Z holds

(((- cosec) - (id Z)) `| Z) . x = ((cos . x) - ((sin . x) ^2)) / ((sin . x) ^2) ) )

( (- 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;

:: 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 & ( 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)) ) )

( 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;

:: 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 & ( 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)) ) )

( 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;

:: 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)) & ( 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) ) )

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;

:: 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)) & ( 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) ) )

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;

:: 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) & ( 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)) ) )

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;

:: 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) & ( 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)) ) )

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;

:: 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 & ( for x being Real st x in Z holds

((ln (#) sec) `| Z) . x = ((1 / (cos . x)) / x) + (((ln . x) * (sin . x)) / ((cos . x) ^2)) ) )

( 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;

:: 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 & ( for x being Real st x in Z holds

((ln (#) cosec) `| Z) . x = ((1 / (sin . x)) / x) - (((ln . x) * (cos . x)) / ((sin . x) ^2)) ) )

( 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;

:: f.x = 1/x*sec.x

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)) ) )

( ((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;

:: f.x = 1/x*cosec.x

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)) ) )

( ((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;

:: 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 & ( for x being Real st x in Z holds

((sec * sin) `| Z) . x = ((cos . x) * (sin . (sin . x))) / ((cos . (sin . x)) ^2) ) )

( 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;

:: 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 & ( for x being Real st x in Z holds

((sec * cos) `| Z) . x = - (((sin . x) * (sin . (cos . x))) / ((cos . (cos . x)) ^2)) ) )

( 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;

:: 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 & ( for x being Real st x in Z holds

((cosec * sin) `| Z) . x = - (((cos . x) * (cos . (sin . x))) / ((sin . (sin . x)) ^2)) ) )

( 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;

:: 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 & ( for x being Real st x in Z holds

((cosec * cos) `| Z) . x = ((sin . x) * (cos . (cos . x))) / ((sin . (cos . x)) ^2) ) )

( 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;

:: 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 & ( for x being Real st x in Z holds

((sec * tan) `| Z) . x = ((sin . (tan . x)) / ((cos . x) ^2)) / ((cos . (tan . x)) ^2) ) )

( 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;

:: 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 & ( for x being Real st x in Z holds

((sec * cot) `| Z) . x = - (((sin . (cot . x)) / ((sin . x) ^2)) / ((cos . (cot . x)) ^2)) ) )

( 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;

:: 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 & ( for x being Real st x in Z holds

((cosec * tan) `| Z) . x = - (((cos . (tan . x)) / ((cos . x) ^2)) / ((sin . (tan . x)) ^2)) ) )

( 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;

:: 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 & ( for x being Real st x in Z holds

((cosec * cot) `| Z) . x = ((cos . (cot . x)) / ((sin . x) ^2)) / ((sin . (cot . x)) ^2) ) )

( 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;

:: 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 & ( 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)) ) )

( 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;

:: 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 & ( 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)) ) )

( 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;

:: 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 & ( 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)) ) )

( 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;

:: 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 & ( 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)) ) )

( 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;