:: Several Differentiation Formulas of Special Functions -- Part {III}
:: by Bo Li , Yan Zhang and Xiquan Liang
::
:: Received March 22, 2006
:: Copyright (c) 2006-2021 Association of Mizar Users
theorem
Th1
:
:: FDIFF_7:1
for
x
being
Real
holds
x
#Z
2
=
x
^2
proof
end;
theorem
Th2
:
:: FDIFF_7:2
for
x
being
Real
st
x
>
0
holds
x
#R
(
1
/
2
)
=
sqrt
x
proof
end;
theorem
Th3
:
:: FDIFF_7:3
for
x
being
Real
st
x
>
0
holds
x
#R
(
-
(
1
/
2
)
)
=
1
/
(
sqrt
x
)
proof
end;
Lm1
:
for
x
being
Real
holds 2
*
(
(
cos
.
(
x
/
2
)
)
^2
)
=
1
+
(
cos
.
x
)
proof
end;
Lm2
:
for
x
being
Real
holds 2
*
(
(
sin
.
(
x
/
2
)
)
^2
)
=
1
-
(
cos
.
x
)
proof
end;
::f.x=r*arcsinx
theorem
:: FDIFF_7:4
for
r
being
Real
for
Z
being
open
Subset
of
REAL
st
Z
c=
].
(
-
1
)
,1
.[
&
Z
c=
dom
(
r
(#)
arcsin
)
holds
(
r
(#)
arcsin
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
r
(#)
arcsin
)
`|
Z
)
.
x
=
r
/
(
sqrt
(
1
-
(
x
^2
)
)
)
) )
proof
end;
::f.x=r*arccosx
theorem
:: FDIFF_7:5
for
r
being
Real
for
Z
being
open
Subset
of
REAL
st
Z
c=
].
(
-
1
)
,1
.[
&
Z
c=
dom
(
r
(#)
arccos
)
holds
(
r
(#)
arccos
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
r
(#)
arccos
)
`|
Z
)
.
x
=
-
(
r
/
(
sqrt
(
1
-
(
x
^2
)
)
)
)
) )
proof
end;
theorem
Th6
:
:: FDIFF_7:6
for
x
being
Real
for
f
being
PartFunc
of
REAL
,
REAL
st
f
is_differentiable_in
x
&
f
.
x
>
-
1 &
f
.
x
<
1 holds
(
arcsin
*
f
is_differentiable_in
x
&
diff
(
(
arcsin
*
f
)
,
x
)
=
(
diff
(
f
,
x
)
)
/
(
sqrt
(
1
-
(
(
f
.
x
)
^2
)
)
)
)
proof
end;
theorem
Th7
:
:: FDIFF_7:7
for
x
being
Real
for
f
being
PartFunc
of
REAL
,
REAL
st
f
is_differentiable_in
x
&
f
.
x
>
-
1 &
f
.
x
<
1 holds
(
arccos
*
f
is_differentiable_in
x
&
diff
(
(
arccos
*
f
)
,
x
)
=
-
(
(
diff
(
f
,
x
)
)
/
(
sqrt
(
1
-
(
(
f
.
x
)
^2
)
)
)
)
)
proof
end;
::f.x=ln(arcsin.x)
theorem
:: FDIFF_7:8
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
ln
*
arcsin
)
&
Z
c=
].
(
-
1
)
,1
.[
& ( for
x
being
Real
st
x
in
Z
holds
arcsin
.
x
>
0
) holds
(
ln
*
arcsin
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
ln
*
arcsin
)
`|
Z
)
.
x
=
1
/
(
(
sqrt
(
1
-
(
x
^2
)
)
)
*
(
arcsin
.
x
)
)
) )
proof
end;
::f.x=ln(arccos.x)
theorem
:: FDIFF_7:9
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
ln
*
arccos
)
&
Z
c=
].
(
-
1
)
,1
.[
& ( for
x
being
Real
st
x
in
Z
holds
arccos
.
x
>
0
) holds
(
ln
*
arccos
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
ln
*
arccos
)
`|
Z
)
.
x
=
-
(
1
/
(
(
sqrt
(
1
-
(
x
^2
)
)
)
*
(
arccos
.
x
)
)
)
) )
proof
end;
::f.x=(arcsin)^n
theorem
Th10
:
:: FDIFF_7:10
for
n
being
Element
of
NAT
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
(
#Z
n
)
*
arcsin
)
&
Z
c=
].
(
-
1
)
,1
.[
holds
(
(
#Z
n
)
*
arcsin
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
(
#Z
n
)
*
arcsin
)
`|
Z
)
.
x
=
(
n
*
(
(
arcsin
.
x
)
#Z
(
n
-
1
)
)
)
/
(
sqrt
(
1
-
(
x
^2
)
)
)
) )
proof
end;
::f.x=(arccos)^n
theorem
Th11
:
:: FDIFF_7:11
for
n
being
Element
of
NAT
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
(
#Z
n
)
*
arccos
)
&
Z
c=
].
(
-
1
)
,1
.[
holds
(
(
#Z
n
)
*
arccos
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
(
#Z
n
)
*
arccos
)
`|
Z
)
.
x
=
-
(
(
n
*
(
(
arccos
.
x
)
#Z
(
n
-
1
)
)
)
/
(
sqrt
(
1
-
(
x
^2
)
)
)
)
) )
proof
end;
::f.x=(1/2)*(arcsin)^2
theorem
:: FDIFF_7:12
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
(
1
/
2
)
(#)
(
(
#Z
2
)
*
arcsin
)
)
&
Z
c=
].
(
-
1
)
,1
.[
holds
(
(
1
/
2
)
(#)
(
(
#Z
2
)
*
arcsin
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
(
1
/
2
)
(#)
(
(
#Z
2
)
*
arcsin
)
)
`|
Z
)
.
x
=
(
arcsin
.
x
)
/
(
sqrt
(
1
-
(
x
^2
)
)
)
) )
proof
end;
::f.x=(1/2)*(arccos)^2
theorem
:: FDIFF_7:13
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
(
1
/
2
)
(#)
(
(
#Z
2
)
*
arccos
)
)
&
Z
c=
].
(
-
1
)
,1
.[
holds
(
(
1
/
2
)
(#)
(
(
#Z
2
)
*
arccos
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
(
1
/
2
)
(#)
(
(
#Z
2
)
*
arccos
)
)
`|
Z
)
.
x
=
-
(
(
arccos
.
x
)
/
(
sqrt
(
1
-
(
x
^2
)
)
)
)
) )
proof
end;
::f.x=arcsin.(a*x+b)
theorem
Th14
:
:: FDIFF_7:14
for
a
,
b
being
Real
for
Z
being
open
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
st
Z
c=
dom
(
arcsin
*
f
)
& ( for
x
being
Real
st
x
in
Z
holds
(
f
.
x
=
(
a
*
x
)
+
b
&
f
.
x
>
-
1 &
f
.
x
<
1 ) ) holds
(
arcsin
*
f
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
arcsin
*
f
)
`|
Z
)
.
x
=
a
/
(
sqrt
(
1
-
(
(
(
a
*
x
)
+
b
)
^2
)
)
)
) )
proof
end;
::f.x=arccos.(a*x+b)
theorem
Th15
:
:: FDIFF_7:15
for
a
,
b
being
Real
for
Z
being
open
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
st
Z
c=
dom
(
arccos
*
f
)
& ( for
x
being
Real
st
x
in
Z
holds
(
f
.
x
=
(
a
*
x
)
+
b
&
f
.
x
>
-
1 &
f
.
x
<
1 ) ) holds
(
arccos
*
f
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
arccos
*
f
)
`|
Z
)
.
x
=
-
(
a
/
(
sqrt
(
1
-
(
(
(
a
*
x
)
+
b
)
^2
)
)
)
)
) )
proof
end;
::f.x=x*arcsin.x
theorem
Th16
:
:: FDIFF_7:16
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
(
id
Z
)
(#)
arcsin
)
&
Z
c=
].
(
-
1
)
,1
.[
holds
(
(
id
Z
)
(#)
arcsin
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
(
id
Z
)
(#)
arcsin
)
`|
Z
)
.
x
=
(
arcsin
.
x
)
+
(
x
/
(
sqrt
(
1
-
(
x
^2
)
)
)
)
) )
proof
end;
::f.x=x*arccos.x
theorem
Th17
:
:: FDIFF_7:17
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
(
id
Z
)
(#)
arccos
)
&
Z
c=
].
(
-
1
)
,1
.[
holds
(
(
id
Z
)
(#)
arccos
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
(
id
Z
)
(#)
arccos
)
`|
Z
)
.
x
=
(
arccos
.
x
)
-
(
x
/
(
sqrt
(
1
-
(
x
^2
)
)
)
)
) )
proof
end;
::f.x=(a*x+b)*arcsin.x
theorem
:: FDIFF_7:18
for
a
,
b
being
Real
for
Z
being
open
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
st
Z
c=
dom
(
f
(#)
arcsin
)
&
Z
c=
].
(
-
1
)
,1
.[
& ( for
x
being
Real
st
x
in
Z
holds
f
.
x
=
(
a
*
x
)
+
b
) holds
(
f
(#)
arcsin
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
f
(#)
arcsin
)
`|
Z
)
.
x
=
(
a
*
(
arcsin
.
x
)
)
+
(
(
(
a
*
x
)
+
b
)
/
(
sqrt
(
1
-
(
x
^2
)
)
)
)
) )
proof
end;
::f.x=(a*x+b)*arccos.x
theorem
:: FDIFF_7:19
for
a
,
b
being
Real
for
Z
being
open
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
st
Z
c=
dom
(
f
(#)
arccos
)
&
Z
c=
].
(
-
1
)
,1
.[
& ( for
x
being
Real
st
x
in
Z
holds
f
.
x
=
(
a
*
x
)
+
b
) holds
(
f
(#)
arccos
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
f
(#)
arccos
)
`|
Z
)
.
x
=
(
a
*
(
arccos
.
x
)
)
-
(
(
(
a
*
x
)
+
b
)
/
(
sqrt
(
1
-
(
x
^2
)
)
)
)
) )
proof
end;
::f.x=(1/2)*arcsin(2*x)
theorem
:: FDIFF_7:20
for
Z
being
open
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
st
Z
c=
dom
(
(
1
/
2
)
(#)
(
arcsin
*
f
)
)
& ( for
x
being
Real
st
x
in
Z
holds
(
f
.
x
=
2
*
x
&
f
.
x
>
-
1 &
f
.
x
<
1 ) ) holds
(
(
1
/
2
)
(#)
(
arcsin
*
f
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
(
1
/
2
)
(#)
(
arcsin
*
f
)
)
`|
Z
)
.
x
=
1
/
(
sqrt
(
1
-
(
(
2
*
x
)
^2
)
)
)
) )
proof
end;
::f.x=(1/2)*arccos(2*x)
theorem
:: FDIFF_7:21
for
Z
being
open
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
st
Z
c=
dom
(
(
1
/
2
)
(#)
(
arccos
*
f
)
)
& ( for
x
being
Real
st
x
in
Z
holds
(
f
.
x
=
2
*
x
&
f
.
x
>
-
1 &
f
.
x
<
1 ) ) holds
(
(
1
/
2
)
(#)
(
arccos
*
f
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
(
1
/
2
)
(#)
(
arccos
*
f
)
)
`|
Z
)
.
x
=
-
(
1
/
(
sqrt
(
1
-
(
(
2
*
x
)
^2
)
)
)
)
) )
proof
end;
::f.x=(1-x|^2) ^ (1/2)
theorem
Th22
:
:: FDIFF_7:22
for
Z
being
open
Subset
of
REAL
for
f
,
f1
,
f2
being
PartFunc
of
REAL
,
REAL
st
Z
c=
dom
(
(
#R
(
1
/
2
)
)
*
f
)
&
f
=
f1
-
f2
&
f2
=
#Z
2 & ( for
x
being
Real
st
x
in
Z
holds
(
f1
.
x
=
1 &
f
.
x
>
0
) ) holds
(
(
#R
(
1
/
2
)
)
*
f
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
(
#R
(
1
/
2
)
)
*
f
)
`|
Z
)
.
x
=
-
(
x
*
(
(
1
-
(
x
#Z
2
)
)
#R
(
-
(
1
/
2
)
)
)
)
) )
proof
end;
::f.x=x*arcsin.x+(1-x^2) ^ (1/2)
theorem
:: FDIFF_7:23
for
Z
being
open
Subset
of
REAL
for
f
,
f1
,
f2
being
PartFunc
of
REAL
,
REAL
st
Z
c=
dom
(
(
(
id
Z
)
(#)
arcsin
)
+
(
(
#R
(
1
/
2
)
)
*
f
)
)
&
Z
c=
].
(
-
1
)
,1
.[
&
f
=
f1
-
f2
&
f2
=
#Z
2 & ( for
x
being
Real
st
x
in
Z
holds
(
f1
.
x
=
1 &
f
.
x
>
0
&
x
<>
0
) ) holds
(
(
(
id
Z
)
(#)
arcsin
)
+
(
(
#R
(
1
/
2
)
)
*
f
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
(
(
id
Z
)
(#)
arcsin
)
+
(
(
#R
(
1
/
2
)
)
*
f
)
)
`|
Z
)
.
x
=
arcsin
.
x
) )
proof
end;
::f.x=x*arccos.x-(1-x^2) ^ (1/2)
theorem
:: FDIFF_7:24
for
Z
being
open
Subset
of
REAL
for
f
,
f1
,
f2
being
PartFunc
of
REAL
,
REAL
st
Z
c=
dom
(
(
(
id
Z
)
(#)
arccos
)
-
(
(
#R
(
1
/
2
)
)
*
f
)
)
&
Z
c=
].
(
-
1
)
,1
.[
&
f
=
f1
-
f2
&
f2
=
#Z
2 & ( for
x
being
Real
st
x
in
Z
holds
(
f1
.
x
=
1 &
f
.
x
>
0
&
x
<>
0
) ) holds
(
(
(
id
Z
)
(#)
arccos
)
-
(
(
#R
(
1
/
2
)
)
*
f
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
(
(
id
Z
)
(#)
arccos
)
-
(
(
#R
(
1
/
2
)
)
*
f
)
)
`|
Z
)
.
x
=
arccos
.
x
) )
proof
end;
::f.x=x*arcsin(x/a)
theorem
Th25
:
:: FDIFF_7:25
for
a
being
Real
for
Z
being
open
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
st
Z
c=
dom
(
(
id
Z
)
(#)
(
arcsin
*
f
)
)
& ( for
x
being
Real
st
x
in
Z
holds
(
f
.
x
=
x
/
a
&
f
.
x
>
-
1 &
f
.
x
<
1 ) ) holds
(
(
id
Z
)
(#)
(
arcsin
*
f
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
(
id
Z
)
(#)
(
arcsin
*
f
)
)
`|
Z
)
.
x
=
(
arcsin
.
(
x
/
a
)
)
+
(
x
/
(
a
*
(
sqrt
(
1
-
(
(
x
/
a
)
^2
)
)
)
)
)
) )
proof
end;
::f.x=x*arccos(x/a)
theorem
Th26
:
:: FDIFF_7:26
for
a
being
Real
for
Z
being
open
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
st
Z
c=
dom
(
(
id
Z
)
(#)
(
arccos
*
f
)
)
& ( for
x
being
Real
st
x
in
Z
holds
(
f
.
x
=
x
/
a
&
f
.
x
>
-
1 &
f
.
x
<
1 ) ) holds
(
(
id
Z
)
(#)
(
arccos
*
f
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
(
id
Z
)
(#)
(
arccos
*
f
)
)
`|
Z
)
.
x
=
(
arccos
.
(
x
/
a
)
)
-
(
x
/
(
a
*
(
sqrt
(
1
-
(
(
x
/
a
)
^2
)
)
)
)
)
) )
proof
end;
::f.x=(a^2-x^2) ^ (1/2)
theorem
Th27
:
:: FDIFF_7:27
for
a
being
Real
for
Z
being
open
Subset
of
REAL
for
f
,
f1
,
f2
being
PartFunc
of
REAL
,
REAL
st
Z
c=
dom
(
(
#R
(
1
/
2
)
)
*
f
)
&
f
=
f1
-
f2
&
f2
=
#Z
2 & ( for
x
being
Real
st
x
in
Z
holds
(
f1
.
x
=
a
^2
&
f
.
x
>
0
) ) holds
(
(
#R
(
1
/
2
)
)
*
f
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
(
#R
(
1
/
2
)
)
*
f
)
`|
Z
)
.
x
=
-
(
x
*
(
(
(
a
^2
)
-
(
x
#Z
2
)
)
#R
(
-
(
1
/
2
)
)
)
)
) )
proof
end;
::f.x=x*arcsin(x/a)+(a^2-x^2) ^ (1/2)
theorem
:: FDIFF_7:28
for
a
being
Real
for
Z
being
open
Subset
of
REAL
for
f
,
f1
,
f2
,
f3
being
PartFunc
of
REAL
,
REAL
st
Z
c=
dom
(
(
(
id
Z
)
(#)
(
arcsin
*
f3
)
)
+
(
(
#R
(
1
/
2
)
)
*
f
)
)
&
f
=
f1
-
f2
&
f2
=
#Z
2 & ( for
x
being
Real
st
x
in
Z
holds
(
f1
.
x
=
a
^2
&
f
.
x
>
0
&
f3
.
x
=
x
/
a
&
f3
.
x
>
-
1 &
f3
.
x
<
1 &
x
<>
0
&
a
>
0
) ) holds
(
(
(
id
Z
)
(#)
(
arcsin
*
f3
)
)
+
(
(
#R
(
1
/
2
)
)
*
f
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
(
(
id
Z
)
(#)
(
arcsin
*
f3
)
)
+
(
(
#R
(
1
/
2
)
)
*
f
)
)
`|
Z
)
.
x
=
arcsin
.
(
x
/
a
)
) )
proof
end;
::f.x=x*arccos(x/a)-(a^2-x^2) ^ (1/2)
theorem
:: FDIFF_7:29
for
a
being
Real
for
Z
being
open
Subset
of
REAL
for
f
,
f1
,
f2
,
f3
being
PartFunc
of
REAL
,
REAL
st
Z
c=
dom
(
(
(
id
Z
)
(#)
(
arccos
*
f3
)
)
-
(
(
#R
(
1
/
2
)
)
*
f
)
)
&
f
=
f1
-
f2
&
f2
=
#Z
2 & ( for
x
being
Real
st
x
in
Z
holds
(
f1
.
x
=
a
^2
&
f
.
x
>
0
&
f3
.
x
=
x
/
a
&
f3
.
x
>
-
1 &
f3
.
x
<
1 &
x
<>
0
&
a
>
0
) ) holds
(
(
(
id
Z
)
(#)
(
arccos
*
f3
)
)
-
(
(
#R
(
1
/
2
)
)
*
f
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
(
(
id
Z
)
(#)
(
arccos
*
f3
)
)
-
(
(
#R
(
1
/
2
)
)
*
f
)
)
`|
Z
)
.
x
=
arccos
.
(
x
/
a
)
) )
proof
end;
::f.x=-1/(n*(sin.x)^n)
theorem
:: FDIFF_7:30
for
n
being
Element
of
NAT
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
(
-
(
1
/
n
)
)
(#)
(
(
#Z
n
)
*
(
sin
^
)
)
)
&
n
>
0
& ( for
x
being
Real
st
x
in
Z
holds
sin
.
x
<>
0
) holds
(
(
-
(
1
/
n
)
)
(#)
(
(
#Z
n
)
*
(
sin
^
)
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
(
-
(
1
/
n
)
)
(#)
(
(
#Z
n
)
*
(
sin
^
)
)
)
`|
Z
)
.
x
=
(
cos
.
x
)
/
(
(
sin
.
x
)
#Z
(
n
+
1
)
)
) )
proof
end;
::f.x=1/(n*(cos.x)^n)
theorem
:: FDIFF_7:31
for
n
being
Element
of
NAT
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
(
1
/
n
)
(#)
(
(
#Z
n
)
*
(
cos
^
)
)
)
&
n
>
0
& ( for
x
being
Real
st
x
in
Z
holds
cos
.
x
<>
0
) holds
(
(
1
/
n
)
(#)
(
(
#Z
n
)
*
(
cos
^
)
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
(
1
/
n
)
(#)
(
(
#Z
n
)
*
(
cos
^
)
)
)
`|
Z
)
.
x
=
(
sin
.
x
)
/
(
(
cos
.
x
)
#Z
(
n
+
1
)
)
) )
proof
end;
Lm3
:
right_open_halfline
0
=
{
g
where
g
is
Real
:
0
<
g
}
by
XXREAL_1:230
;
::f.x=sin(ln.x)
theorem
:: FDIFF_7:32
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
sin
*
ln
)
& ( for
x
being
Real
st
x
in
Z
holds
x
>
0
) holds
(
sin
*
ln
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
sin
*
ln
)
`|
Z
)
.
x
=
(
cos
.
(
ln
.
x
)
)
/
x
) )
proof
end;
::f.x=cos(ln.x)
theorem
:: FDIFF_7:33
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
cos
*
ln
)
& ( for
x
being
Real
st
x
in
Z
holds
x
>
0
) holds
(
cos
*
ln
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
cos
*
ln
)
`|
Z
)
.
x
=
-
(
(
sin
.
(
ln
.
x
)
)
/
x
)
) )
proof
end;
::f.x=sin(exp.x)
theorem
:: FDIFF_7:34
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
sin
*
exp_R
)
holds
(
sin
*
exp_R
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
sin
*
exp_R
)
`|
Z
)
.
x
=
(
exp_R
.
x
)
*
(
cos
.
(
exp_R
.
x
)
)
) )
proof
end;
::f.x=cos(exp_R.x)
theorem
:: FDIFF_7:35
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
cos
*
exp_R
)
holds
(
cos
*
exp_R
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
cos
*
exp_R
)
`|
Z
)
.
x
=
-
(
(
exp_R
.
x
)
*
(
sin
.
(
exp_R
.
x
)
)
)
) )
proof
end;
::f.x=exp_R.(cos.x)
theorem
:: FDIFF_7:36
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
exp_R
*
cos
)
holds
(
exp_R
*
cos
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
exp_R
*
cos
)
`|
Z
)
.
x
=
-
(
(
exp_R
.
(
cos
.
x
)
)
*
(
sin
.
x
)
)
) )
proof
end;
::f.x=exp_R.(sin.x)
theorem
:: FDIFF_7:37
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
exp_R
*
sin
)
holds
(
exp_R
*
sin
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
exp_R
*
sin
)
`|
Z
)
.
x
=
(
exp_R
.
(
sin
.
x
)
)
*
(
cos
.
x
)
) )
proof
end;
::f.x=sin.x+cos.x
theorem
Th38
:
:: FDIFF_7:38
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
)
-
(
sin
.
x
)
) )
proof
end;
::f.x=sin.x-cos.x
theorem
Th39
:
:: FDIFF_7:39
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
)
+
(
sin
.
x
)
) )
proof
end;
::f.x=exp_R.x*(sin.x-cos.x)
theorem
:: FDIFF_7:40
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
exp_R
(#)
(
sin
-
cos
)
)
holds
(
exp_R
(#)
(
sin
-
cos
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
exp_R
(#)
(
sin
-
cos
)
)
`|
Z
)
.
x
=
(
2
*
(
exp_R
.
x
)
)
*
(
sin
.
x
)
) )
proof
end;
::f.x=exp_R.x*(sin.x+cos.x)
theorem
:: FDIFF_7:41
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
exp_R
(#)
(
sin
+
cos
)
)
holds
(
exp_R
(#)
(
sin
+
cos
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
exp_R
(#)
(
sin
+
cos
)
)
`|
Z
)
.
x
=
(
2
*
(
exp_R
.
x
)
)
*
(
cos
.
x
)
) )
proof
end;
::f.x=(sin.x+cos.x)/exp_R.x
theorem
:: FDIFF_7:42
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
(
sin
+
cos
)
/
exp_R
)
holds
(
(
sin
+
cos
)
/
exp_R
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
(
sin
+
cos
)
/
exp_R
)
`|
Z
)
.
x
=
-
(
(
2
*
(
sin
.
x
)
)
/
(
exp_R
.
x
)
)
) )
proof
end;
::f.x=(sin.x-cos.x)/exp_R.x
theorem
:: FDIFF_7:43
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
(
sin
-
cos
)
/
exp_R
)
holds
(
(
sin
-
cos
)
/
exp_R
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
(
sin
-
cos
)
/
exp_R
)
`|
Z
)
.
x
=
(
2
*
(
cos
.
x
)
)
/
(
exp_R
.
x
)
) )
proof
end;
::f.x=exp_R.x*sin.x
theorem
:: FDIFF_7:44
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
exp_R
(#)
sin
)
holds
(
exp_R
(#)
sin
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
exp_R
(#)
sin
)
`|
Z
)
.
x
=
(
exp_R
.
x
)
*
(
(
sin
.
x
)
+
(
cos
.
x
)
)
) )
proof
end;
::f.x=exp_R.x*cos.x
theorem
:: FDIFF_7:45
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
exp_R
(#)
cos
)
holds
(
exp_R
(#)
cos
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
exp_R
(#)
cos
)
`|
Z
)
.
x
=
(
exp_R
.
x
)
*
(
(
cos
.
x
)
-
(
sin
.
x
)
)
) )
proof
end;
:: f.x=tan.x
theorem
Th46
:
:: FDIFF_7:46
for
x
being
Real
st
cos
.
x
<>
0
holds
(
sin
/
cos
is_differentiable_in
x
&
diff
(
(
sin
/
cos
)
,
x
)
=
1
/
(
(
cos
.
x
)
^2
)
)
proof
end;
::f.x=cot.x
theorem
Th47
:
:: FDIFF_7:47
for
x
being
Real
st
sin
.
x
<>
0
holds
(
cos
/
sin
is_differentiable_in
x
&
diff
(
(
cos
/
sin
)
,
x
)
=
-
(
1
/
(
(
sin
.
x
)
^2
)
)
)
proof
end;
::f.x=(tan.x) ^ 2
theorem
:: FDIFF_7:48
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
(
#Z
2
)
*
(
sin
/
cos
)
)
& ( for
x
being
Real
st
x
in
Z
holds
cos
.
x
<>
0
) holds
(
(
#Z
2
)
*
(
sin
/
cos
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
(
#Z
2
)
*
(
sin
/
cos
)
)
`|
Z
)
.
x
=
(
2
*
(
sin
.
x
)
)
/
(
(
cos
.
x
)
#Z
3
)
) )
proof
end;
::f.x=(cot.x) ^ 2
theorem
:: FDIFF_7:49
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
(
#Z
2
)
*
(
cos
/
sin
)
)
& ( for
x
being
Real
st
x
in
Z
holds
sin
.
x
<>
0
) holds
(
(
#Z
2
)
*
(
cos
/
sin
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
(
#Z
2
)
*
(
cos
/
sin
)
)
`|
Z
)
.
x
=
-
(
(
2
*
(
cos
.
x
)
)
/
(
(
sin
.
x
)
#Z
3
)
)
) )
proof
end;
::f.x=tan.(x/2)
theorem
:: FDIFF_7:50
for
Z
being
open
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
st
Z
c=
dom
(
(
sin
/
cos
)
*
f
)
& ( for
x
being
Real
st
x
in
Z
holds
(
f
.
x
=
x
/
2 &
cos
.
(
f
.
x
)
<>
0
) ) holds
(
(
sin
/
cos
)
*
f
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
(
sin
/
cos
)
*
f
)
`|
Z
)
.
x
=
1
/
(
1
+
(
cos
.
x
)
)
) )
proof
end;
::f.x=cot.(x/2)
theorem
:: FDIFF_7:51
for
Z
being
open
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
st
Z
c=
dom
(
(
cos
/
sin
)
*
f
)
& ( for
x
being
Real
st
x
in
Z
holds
(
f
.
x
=
x
/
2 &
sin
.
(
f
.
x
)
<>
0
) ) holds
(
(
cos
/
sin
)
*
f
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
(
cos
/
sin
)
*
f
)
`|
Z
)
.
x
=
-
(
1
/
(
1
-
(
cos
.
x
)
)
)
) )
proof
end;