:: Several Differentiation Formulas of Special Functions -- Part {V}
:: by Peng Wang and Bo Li
::
:: Received July 9, 2007
:: Copyright (c) 2007-2021 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
Nat
holds
(
1
/
x
)
#Z
n
=
1
/
(
x
#Z
n
)
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
)
) )
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
)
)
) )
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
)
) )
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
)
)
) )
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
)
)
)
) )
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
)
)
) )
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
)
) )
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
)
)
) )
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
)
) )
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
)
)
) )
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
)
)
) )
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
)
)
)
) )
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
)
) )
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
)
)
) )
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
)
) )
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
)
)
) )
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
)
)
) )
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
)
)
)
) )
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
)
) )
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
)
) )
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
)
)
) )
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
)
)
) )
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
)
) )
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
)
) )
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
)
)
) )
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
)
)
) )
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
)
)
) )
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
)
)
) )
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
)
)
) )
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
)
)
) )
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
)
) )
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
)
)
) )
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
)
)
) )
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
)
) )
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
)
) )
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
)
)
) )
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
)
)
) )
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
)
) )
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
)
)
) )
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
)
)
) )
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
)
)
) )
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
)
)
) )
proof
end;