:: Several Differentiation Formulas of Special Functions -- Part {V}
:: by Bo Li and Pan Wang
::
:: Received September 19, 2007
:: Copyright (c) 2007-2021 Association of Mizar Users
::f.x=tan.(cot.x)
theorem
:: FDIFF_10:1
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
tan
*
cot
)
holds
(
tan
*
cot
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
tan
*
cot
)
`|
Z
)
.
x
=
(
1
/
(
(
cos
.
(
cot
.
x
)
)
^2
)
)
*
(
-
(
1
/
(
(
sin
.
x
)
^2
)
)
)
) )
proof
end;
::f.x=tan.(tan.x)
theorem
:: FDIFF_10:2
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
tan
*
tan
)
holds
(
tan
*
tan
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
tan
*
tan
)
`|
Z
)
.
x
=
(
1
/
(
(
cos
.
(
tan
.
x
)
)
^2
)
)
*
(
1
/
(
(
cos
.
x
)
^2
)
)
) )
proof
end;
::f.x=cot.(cot.x)
theorem
:: FDIFF_10:3
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
cot
*
cot
)
holds
(
cot
*
cot
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
cot
*
cot
)
`|
Z
)
.
x
=
(
1
/
(
(
sin
.
(
cot
.
x
)
)
^2
)
)
*
(
1
/
(
(
sin
.
x
)
^2
)
)
) )
proof
end;
::f.x=cot.(tan.x)
theorem
:: FDIFF_10:4
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
cot
*
tan
)
holds
(
cot
*
tan
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
cot
*
tan
)
`|
Z
)
.
x
=
(
-
(
1
/
(
(
sin
.
(
tan
.
x
)
)
^2
)
)
)
*
(
1
/
(
(
cos
.
x
)
^2
)
)
) )
proof
end;
::f.x= tan.x - cot.x
theorem
Th5
:
:: FDIFF_10:5
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
tan
-
cot
)
holds
(
tan
-
cot
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
tan
-
cot
)
`|
Z
)
.
x
=
(
1
/
(
(
cos
.
x
)
^2
)
)
+
(
1
/
(
(
sin
.
x
)
^2
)
)
) )
proof
end;
::f.x= tan.x + cot.x
theorem
Th6
:
:: FDIFF_10:6
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
tan
+
cot
)
holds
(
tan
+
cot
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
tan
+
cot
)
`|
Z
)
.
x
=
(
1
/
(
(
cos
.
x
)
^2
)
)
-
(
1
/
(
(
sin
.
x
)
^2
)
)
) )
proof
end;
::f.x=sin.(sin.x)
theorem
:: FDIFF_10:7
for
Z
being
open
Subset
of
REAL
holds
(
sin
*
sin
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
sin
*
sin
)
`|
Z
)
.
x
=
(
cos
.
(
sin
.
x
)
)
*
(
cos
.
x
)
) )
proof
end;
::f.x=sin.(cos.x)
theorem
:: FDIFF_10:8
for
Z
being
open
Subset
of
REAL
holds
(
sin
*
cos
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
sin
*
cos
)
`|
Z
)
.
x
=
-
(
(
cos
.
(
cos
.
x
)
)
*
(
sin
.
x
)
)
) )
proof
end;
::f.x=cos.(sin.x)
theorem
:: FDIFF_10:9
for
Z
being
open
Subset
of
REAL
holds
(
cos
*
sin
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
cos
*
sin
)
`|
Z
)
.
x
=
-
(
(
sin
.
(
sin
.
x
)
)
*
(
cos
.
x
)
)
) )
proof
end;
::f.x=cos.(cos.x)
theorem
:: FDIFF_10:10
for
Z
being
open
Subset
of
REAL
holds
(
cos
*
cos
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
cos
*
cos
)
`|
Z
)
.
x
=
(
sin
.
(
cos
.
x
)
)
*
(
sin
.
x
)
) )
proof
end;
:: f.x=cos.x * cot.x
theorem
:: FDIFF_10:11
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
cos
(#)
cot
)
holds
(
cos
(#)
cot
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
cos
(#)
cot
)
`|
Z
)
.
x
=
(
-
(
cos
.
x
)
)
-
(
(
cos
.
x
)
/
(
(
sin
.
x
)
^2
)
)
) )
proof
end;
:: f.x=sin.x * tan.x
theorem
:: FDIFF_10:12
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
sin
(#)
tan
)
holds
(
sin
(#)
tan
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
sin
(#)
tan
)
`|
Z
)
.
x
=
(
sin
.
x
)
+
(
(
sin
.
x
)
/
(
(
cos
.
x
)
^2
)
)
) )
proof
end;
:: f.x=sin.x * cot.x
theorem
:: FDIFF_10:13
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
sin
(#)
cot
)
holds
(
sin
(#)
cot
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
sin
(#)
cot
)
`|
Z
)
.
x
=
(
(
cos
.
x
)
*
(
cot
.
x
)
)
-
(
1
/
(
sin
.
x
)
)
) )
proof
end;
:: f.x=cos.x * tan.x
theorem
:: FDIFF_10:14
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
cos
(#)
tan
)
holds
(
cos
(#)
tan
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
cos
(#)
tan
)
`|
Z
)
.
x
=
(
-
(
(
(
sin
.
x
)
^2
)
/
(
cos
.
x
)
)
)
+
(
1
/
(
cos
.
x
)
)
) )
proof
end;
:: f.x=sin.x * cos.x
theorem
:: FDIFF_10:15
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
sin
(#)
cos
)
holds
(
sin
(#)
cos
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
sin
(#)
cos
)
`|
Z
)
.
x
=
(
(
cos
.
x
)
^2
)
-
(
(
sin
.
x
)
^2
)
) )
proof
end;
:: f.x=ln.x * sin.x
theorem
:: FDIFF_10:16
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
ln
(#)
sin
)
holds
(
ln
(#)
sin
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
ln
(#)
sin
)
`|
Z
)
.
x
=
(
(
sin
.
x
)
/
x
)
+
(
(
ln
.
x
)
*
(
cos
.
x
)
)
) )
proof
end;
:: f.x=ln.x * cos.x
theorem
:: FDIFF_10:17
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
ln
(#)
cos
)
holds
(
ln
(#)
cos
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
ln
(#)
cos
)
`|
Z
)
.
x
=
(
(
cos
.
x
)
/
x
)
-
(
(
ln
.
x
)
*
(
sin
.
x
)
)
) )
proof
end;
:: f.x=ln.x * exp_R.x
theorem
:: FDIFF_10:18
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
ln
(#)
exp_R
)
holds
(
ln
(#)
exp_R
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
ln
(#)
exp_R
)
`|
Z
)
.
x
=
(
(
exp_R
.
x
)
/
x
)
+
(
(
ln
.
x
)
*
(
exp_R
.
x
)
)
) )
proof
end;
::f.x=ln.(ln.x)
theorem
:: FDIFF_10:19
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
ln
*
ln
)
& ( for
x
being
Real
st
x
in
Z
holds
x
>
0
) holds
(
ln
*
ln
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
ln
*
ln
)
`|
Z
)
.
x
=
1
/
(
(
ln
.
x
)
*
x
)
) )
proof
end;
::f.x=exp_R.(exp_R.x)
theorem
:: FDIFF_10:20
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
exp_R
*
exp_R
)
holds
(
exp_R
*
exp_R
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
exp_R
*
exp_R
)
`|
Z
)
.
x
=
(
exp_R
.
(
exp_R
.
x
)
)
*
(
exp_R
.
x
)
) )
proof
end;
::f.x=sin.(tan.x)
theorem
:: FDIFF_10:21
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
sin
*
tan
)
holds
(
sin
*
tan
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
sin
*
tan
)
`|
Z
)
.
x
=
(
cos
(
tan
.
x
)
)
/
(
(
cos
.
x
)
^2
)
) )
proof
end;
::f.x=sin.(cot.x)
theorem
:: FDIFF_10:22
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
sin
*
cot
)
holds
(
sin
*
cot
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
sin
*
cot
)
`|
Z
)
.
x
=
-
(
(
cos
(
cot
.
x
)
)
/
(
(
sin
.
x
)
^2
)
)
) )
proof
end;
::f.x=cos.(tan.x)
theorem
:: FDIFF_10:23
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
cos
*
tan
)
holds
(
cos
*
tan
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
cos
*
tan
)
`|
Z
)
.
x
=
-
(
(
sin
(
tan
.
x
)
)
/
(
(
cos
.
x
)
^2
)
)
) )
proof
end;
::f.x=cos.(cot.x)
theorem
:: FDIFF_10:24
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
cos
*
cot
)
holds
(
cos
*
cot
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
cos
*
cot
)
`|
Z
)
.
x
=
(
sin
(
cot
.
x
)
)
/
(
(
sin
.
x
)
^2
)
) )
proof
end;
::f.x=sin.x*(tan.x+cot.x)
theorem
:: FDIFF_10:25
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
sin
(#)
(
tan
+
cot
)
)
holds
(
sin
(#)
(
tan
+
cot
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
sin
(#)
(
tan
+
cot
)
)
`|
Z
)
.
x
=
(
(
cos
.
x
)
*
(
(
tan
.
x
)
+
(
cot
.
x
)
)
)
+
(
(
sin
.
x
)
*
(
(
1
/
(
(
cos
.
x
)
^2
)
)
-
(
1
/
(
(
sin
.
x
)
^2
)
)
)
)
) )
proof
end;
::f.x=cos.x*(tan.x+cot.x)
theorem
:: FDIFF_10:26
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
cos
(#)
(
tan
+
cot
)
)
holds
(
cos
(#)
(
tan
+
cot
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
cos
(#)
(
tan
+
cot
)
)
`|
Z
)
.
x
=
(
-
(
(
sin
.
x
)
*
(
(
tan
.
x
)
+
(
cot
.
x
)
)
)
)
+
(
(
cos
.
x
)
*
(
(
1
/
(
(
cos
.
x
)
^2
)
)
-
(
1
/
(
(
sin
.
x
)
^2
)
)
)
)
) )
proof
end;
:: f.x=sin.x*(tan.x-cot.x)
theorem
:: FDIFF_10:27
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
sin
(#)
(
tan
-
cot
)
)
holds
(
sin
(#)
(
tan
-
cot
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
sin
(#)
(
tan
-
cot
)
)
`|
Z
)
.
x
=
(
(
cos
.
x
)
*
(
(
tan
.
x
)
-
(
cot
.
x
)
)
)
+
(
(
sin
.
x
)
*
(
(
1
/
(
(
cos
.
x
)
^2
)
)
+
(
1
/
(
(
sin
.
x
)
^2
)
)
)
)
) )
proof
end;
:: f.x=cos.x*(tan.x-cot.x)
theorem
:: FDIFF_10:28
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
cos
(#)
(
tan
-
cot
)
)
holds
(
cos
(#)
(
tan
-
cot
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
cos
(#)
(
tan
-
cot
)
)
`|
Z
)
.
x
=
(
-
(
(
sin
.
x
)
*
(
(
tan
.
x
)
-
(
cot
.
x
)
)
)
)
+
(
(
cos
.
x
)
*
(
(
1
/
(
(
cos
.
x
)
^2
)
)
+
(
1
/
(
(
sin
.
x
)
^2
)
)
)
)
) )
proof
end;
::f.x=exp_R.x*(tan.x + cot.x)
theorem
:: FDIFF_10:29
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
exp_R
(#)
(
tan
+
cot
)
)
holds
(
exp_R
(#)
(
tan
+
cot
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
exp_R
(#)
(
tan
+
cot
)
)
`|
Z
)
.
x
=
(
(
exp_R
.
x
)
*
(
(
tan
.
x
)
+
(
cot
.
x
)
)
)
+
(
(
exp_R
.
x
)
*
(
(
1
/
(
(
cos
.
x
)
^2
)
)
-
(
1
/
(
(
sin
.
x
)
^2
)
)
)
)
) )
proof
end;
::f.x=exp_R.x*(tan.x - cot.x)
theorem
:: FDIFF_10:30
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
exp_R
(#)
(
tan
-
cot
)
)
holds
(
exp_R
(#)
(
tan
-
cot
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
exp_R
(#)
(
tan
-
cot
)
)
`|
Z
)
.
x
=
(
(
exp_R
.
x
)
*
(
(
tan
.
x
)
-
(
cot
.
x
)
)
)
+
(
(
exp_R
.
x
)
*
(
(
1
/
(
(
cos
.
x
)
^2
)
)
+
(
1
/
(
(
sin
.
x
)
^2
)
)
)
)
) )
proof
end;
::f.x=sin.x*(sin.x+cos.x)
theorem
:: FDIFF_10:31
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
sin
(#)
(
sin
+
cos
)
)
holds
(
sin
(#)
(
sin
+
cos
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
sin
(#)
(
sin
+
cos
)
)
`|
Z
)
.
x
=
(
(
(
cos
.
x
)
^2
)
+
(
(
2
*
(
sin
.
x
)
)
*
(
cos
.
x
)
)
)
-
(
(
sin
.
x
)
^2
)
) )
proof
end;
::f.x=sin.x*(sin.x-cos.x)
theorem
:: FDIFF_10:32
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
sin
(#)
(
sin
-
cos
)
)
holds
(
sin
(#)
(
sin
-
cos
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
sin
(#)
(
sin
-
cos
)
)
`|
Z
)
.
x
=
(
(
(
sin
.
x
)
^2
)
+
(
(
2
*
(
sin
.
x
)
)
*
(
cos
.
x
)
)
)
-
(
(
cos
.
x
)
^2
)
) )
proof
end;
:: f.x=cos.x*(sin.x-cos.x)
theorem
:: FDIFF_10:33
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
cos
(#)
(
sin
-
cos
)
)
holds
(
cos
(#)
(
sin
-
cos
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
cos
(#)
(
sin
-
cos
)
)
`|
Z
)
.
x
=
(
(
(
cos
.
x
)
^2
)
+
(
(
2
*
(
sin
.
x
)
)
*
(
cos
.
x
)
)
)
-
(
(
sin
.
x
)
^2
)
) )
proof
end;
:: f.x=cos.x*(sin.x+cos.x)
theorem
:: FDIFF_10:34
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
cos
(#)
(
sin
+
cos
)
)
holds
(
cos
(#)
(
sin
+
cos
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
cos
(#)
(
sin
+
cos
)
)
`|
Z
)
.
x
=
(
(
(
cos
.
x
)
^2
)
-
(
(
2
*
(
sin
.
x
)
)
*
(
cos
.
x
)
)
)
-
(
(
sin
.
x
)
^2
)
) )
proof
end;
::f.x=sin.(tan.x+cot.x)
theorem
:: FDIFF_10:35
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
sin
*
(
tan
+
cot
)
)
holds
(
sin
*
(
tan
+
cot
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
sin
*
(
tan
+
cot
)
)
`|
Z
)
.
x
=
(
cos
.
(
(
tan
.
x
)
+
(
cot
.
x
)
)
)
*
(
(
1
/
(
(
cos
.
x
)
^2
)
)
-
(
1
/
(
(
sin
.
x
)
^2
)
)
)
) )
proof
end;
::f.x=sin.(tan.x-cot.x)
theorem
:: FDIFF_10:36
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
sin
*
(
tan
-
cot
)
)
holds
(
sin
*
(
tan
-
cot
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
sin
*
(
tan
-
cot
)
)
`|
Z
)
.
x
=
(
cos
.
(
(
tan
.
x
)
-
(
cot
.
x
)
)
)
*
(
(
1
/
(
(
cos
.
x
)
^2
)
)
+
(
1
/
(
(
sin
.
x
)
^2
)
)
)
) )
proof
end;
::f.x=cos.(tan.x-cot.x)
theorem
:: FDIFF_10:37
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
cos
*
(
tan
-
cot
)
)
holds
(
cos
*
(
tan
-
cot
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
cos
*
(
tan
-
cot
)
)
`|
Z
)
.
x
=
-
(
(
sin
.
(
(
tan
.
x
)
-
(
cot
.
x
)
)
)
*
(
(
1
/
(
(
cos
.
x
)
^2
)
)
+
(
1
/
(
(
sin
.
x
)
^2
)
)
)
)
) )
proof
end;
::f.x=cos.(tan.x+cot.x)
theorem
:: FDIFF_10:38
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
cos
*
(
tan
+
cot
)
)
holds
(
cos
*
(
tan
+
cot
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
cos
*
(
tan
+
cot
)
)
`|
Z
)
.
x
=
-
(
(
sin
.
(
(
tan
.
x
)
+
(
cot
.
x
)
)
)
*
(
(
1
/
(
(
cos
.
x
)
^2
)
)
-
(
1
/
(
(
sin
.
x
)
^2
)
)
)
)
) )
proof
end;
::f.x=exp_R.(tan.x + cot.x)
theorem
:: FDIFF_10:39
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
exp_R
*
(
tan
+
cot
)
)
holds
(
exp_R
*
(
tan
+
cot
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
exp_R
*
(
tan
+
cot
)
)
`|
Z
)
.
x
=
(
exp_R
.
(
(
tan
.
x
)
+
(
cot
.
x
)
)
)
*
(
(
1
/
(
(
cos
.
x
)
^2
)
)
-
(
1
/
(
(
sin
.
x
)
^2
)
)
)
) )
proof
end;
::f.x=exp_R.(tan.x - cot.x)
theorem
:: FDIFF_10:40
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
exp_R
*
(
tan
-
cot
)
)
holds
(
exp_R
*
(
tan
-
cot
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
exp_R
*
(
tan
-
cot
)
)
`|
Z
)
.
x
=
(
exp_R
.
(
(
tan
.
x
)
-
(
cot
.
x
)
)
)
*
(
(
1
/
(
(
cos
.
x
)
^2
)
)
+
(
1
/
(
(
sin
.
x
)
^2
)
)
)
) )
proof
end;
::f.x=(tan.x-cot.x)/exp_.x
theorem
:: FDIFF_10:41
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
(
tan
-
cot
)
/
exp_R
)
holds
(
(
tan
-
cot
)
/
exp_R
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
(
tan
-
cot
)
/
exp_R
)
`|
Z
)
.
x
=
(
(
(
(
1
/
(
(
cos
.
x
)
^2
)
)
+
(
1
/
(
(
sin
.
x
)
^2
)
)
)
-
(
tan
.
x
)
)
+
(
cot
.
x
)
)
/
(
exp_R
.
x
)
) )
proof
end;
::f.x=(tan.x+cot.x)/exp_.x
theorem
:: FDIFF_10:42
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
(
tan
+
cot
)
/
exp_R
)
holds
(
(
tan
+
cot
)
/
exp_R
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
(
tan
+
cot
)
/
exp_R
)
`|
Z
)
.
x
=
(
(
(
(
1
/
(
(
cos
.
x
)
^2
)
)
-
(
1
/
(
(
sin
.
x
)
^2
)
)
)
-
(
tan
.
x
)
)
-
(
cot
.
x
)
)
/
(
exp_R
.
x
)
) )
proof
end;
:: f.x = sin.(sec.x)
theorem
:: FDIFF_10:43
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
sin
*
sec
)
holds
(
sin
*
sec
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
sin
*
sec
)
`|
Z
)
.
x
=
(
(
cos
.
(
sec
.
x
)
)
*
(
sin
.
x
)
)
/
(
(
cos
.
x
)
^2
)
) )
proof
end;
:: f.x = cos.(sec.x)
theorem
:: FDIFF_10:44
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
cos
*
sec
)
holds
(
cos
*
sec
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
cos
*
sec
)
`|
Z
)
.
x
=
-
(
(
(
sin
.
(
sec
.
x
)
)
*
(
sin
.
x
)
)
/
(
(
cos
.
x
)
^2
)
)
) )
proof
end;
:: f.x = sin.(cosec.x)
theorem
:: FDIFF_10:45
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
sin
*
cosec
)
holds
(
sin
*
cosec
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
sin
*
cosec
)
`|
Z
)
.
x
=
-
(
(
(
cos
.
(
cosec
.
x
)
)
*
(
cos
.
x
)
)
/
(
(
sin
.
x
)
^2
)
)
) )
proof
end;
:: f.x = cos.(cose.x)
theorem
:: FDIFF_10:46
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
cos
*
cosec
)
holds
(
cos
*
cosec
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
cos
*
cosec
)
`|
Z
)
.
x
=
(
(
sin
.
(
cosec
.
x
)
)
*
(
cos
.
x
)
)
/
(
(
sin
.
x
)
^2
)
) )
proof
end;