:: Several Differentiable Formulas of Special Functions
:: by Yan Zhang and Xiquan Liang
::
:: Received July 6, 2005
:: Copyright (c) 2005-2021 Association of Mizar Users
:: 1 $f.x=ln(a+x)$
theorem
Th1
:
:: FDIFF_4:1
for
a
being
Real
for
Z
being
open
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
st
Z
c=
dom
(
ln
*
f
)
& ( for
x
being
Real
st
x
in
Z
holds
(
f
.
x
=
a
+
x
&
f
.
x
>
0
) ) holds
(
ln
*
f
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
ln
*
f
)
`|
Z
)
.
x
=
1
/
(
a
+
x
)
) )
proof
end;
:: 2 $f.x=ln(x-a)$
theorem
Th2
:
:: FDIFF_4:2
for
a
being
Real
for
Z
being
open
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
st
Z
c=
dom
(
ln
*
f
)
& ( for
x
being
Real
st
x
in
Z
holds
(
f
.
x
=
x
-
a
&
f
.
x
>
0
) ) holds
(
ln
*
f
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
ln
*
f
)
`|
Z
)
.
x
=
1
/
(
x
-
a
)
) )
proof
end;
:: 3 $f.x=-ln(a-x)$
theorem
:: FDIFF_4:3
for
a
being
Real
for
Z
being
open
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
st
Z
c=
dom
(
-
(
ln
*
f
)
)
& ( for
x
being
Real
st
x
in
Z
holds
(
f
.
x
=
a
-
x
&
f
.
x
>
0
) ) holds
(
-
(
ln
*
f
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
-
(
ln
*
f
)
)
`|
Z
)
.
x
=
1
/
(
a
-
x
)
) )
proof
end;
:: 4 f.x=x-a*ln(a+x)
theorem
:: FDIFF_4:4
for
a
being
Real
for
Z
being
open
Subset
of
REAL
for
f
,
f1
being
PartFunc
of
REAL
,
REAL
st
Z
c=
dom
(
(
id
Z
)
-
(
a
(#)
f
)
)
&
f
=
ln
*
f1
& ( for
x
being
Real
st
x
in
Z
holds
(
f1
.
x
=
a
+
x
&
f1
.
x
>
0
) ) holds
(
(
id
Z
)
-
(
a
(#)
f
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
(
id
Z
)
-
(
a
(#)
f
)
)
`|
Z
)
.
x
=
x
/
(
a
+
x
)
) )
proof
end;
:: 5 f.x=(2*a)*ln(a+x)-x
theorem
:: FDIFF_4:5
for
a
being
Real
for
Z
being
open
Subset
of
REAL
for
f
,
f1
being
PartFunc
of
REAL
,
REAL
st
Z
c=
dom
(
(
(
2
*
a
)
(#)
f
)
-
(
id
Z
)
)
&
f
=
ln
*
f1
& ( for
x
being
Real
st
x
in
Z
holds
(
f1
.
x
=
a
+
x
&
f1
.
x
>
0
) ) holds
(
(
(
2
*
a
)
(#)
f
)
-
(
id
Z
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
(
(
2
*
a
)
(#)
f
)
-
(
id
Z
)
)
`|
Z
)
.
x
=
(
a
-
x
)
/
(
a
+
x
)
) )
proof
end;
:: 6 f.x=x-(2*a)*ln(x+a)
theorem
:: FDIFF_4:6
for
a
being
Real
for
Z
being
open
Subset
of
REAL
for
f
,
f1
being
PartFunc
of
REAL
,
REAL
st
Z
c=
dom
(
(
id
Z
)
-
(
(
2
*
a
)
(#)
f
)
)
&
f
=
ln
*
f1
& ( for
x
being
Real
st
x
in
Z
holds
(
f1
.
x
=
x
+
a
&
f1
.
x
>
0
) ) holds
(
(
id
Z
)
-
(
(
2
*
a
)
(#)
f
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
(
id
Z
)
-
(
(
2
*
a
)
(#)
f
)
)
`|
Z
)
.
x
=
(
x
-
a
)
/
(
x
+
a
)
) )
proof
end;
:: 7 f.x=x + (2*a)*ln(x-a)
theorem
:: FDIFF_4:7
for
a
being
Real
for
Z
being
open
Subset
of
REAL
for
f
,
f1
being
PartFunc
of
REAL
,
REAL
st
Z
c=
dom
(
(
id
Z
)
+
(
(
2
*
a
)
(#)
f
)
)
&
f
=
ln
*
f1
& ( for
x
being
Real
st
x
in
Z
holds
(
f1
.
x
=
x
-
a
&
f1
.
x
>
0
) ) holds
(
(
id
Z
)
+
(
(
2
*
a
)
(#)
f
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
(
id
Z
)
+
(
(
2
*
a
)
(#)
f
)
)
`|
Z
)
.
x
=
(
x
+
a
)
/
(
x
-
a
)
) )
proof
end;
:: 8 f.x=x+ (a-b)*ln(x+b)
theorem
:: FDIFF_4:8
for
a
,
b
being
Real
for
Z
being
open
Subset
of
REAL
for
f
,
f1
being
PartFunc
of
REAL
,
REAL
st
Z
c=
dom
(
(
id
Z
)
+
(
(
a
-
b
)
(#)
f
)
)
&
f
=
ln
*
f1
& ( for
x
being
Real
st
x
in
Z
holds
(
f1
.
x
=
x
+
b
&
f1
.
x
>
0
) ) holds
(
(
id
Z
)
+
(
(
a
-
b
)
(#)
f
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
(
id
Z
)
+
(
(
a
-
b
)
(#)
f
)
)
`|
Z
)
.
x
=
(
x
+
a
)
/
(
x
+
b
)
) )
proof
end;
:: 9 f.x=x+ (a+b)*ln(x-b)
theorem
:: FDIFF_4:9
for
a
,
b
being
Real
for
Z
being
open
Subset
of
REAL
for
f
,
f1
being
PartFunc
of
REAL
,
REAL
st
Z
c=
dom
(
(
id
Z
)
+
(
(
a
+
b
)
(#)
f
)
)
&
f
=
ln
*
f1
& ( for
x
being
Real
st
x
in
Z
holds
(
f1
.
x
=
x
-
b
&
f1
.
x
>
0
) ) holds
(
(
id
Z
)
+
(
(
a
+
b
)
(#)
f
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
(
id
Z
)
+
(
(
a
+
b
)
(#)
f
)
)
`|
Z
)
.
x
=
(
x
+
a
)
/
(
x
-
b
)
) )
proof
end;
:: 10 f.x=x- (a+b)*ln(x+b)
theorem
:: FDIFF_4:10
for
a
,
b
being
Real
for
Z
being
open
Subset
of
REAL
for
f
,
f1
being
PartFunc
of
REAL
,
REAL
st
Z
c=
dom
(
(
id
Z
)
-
(
(
a
+
b
)
(#)
f
)
)
&
f
=
ln
*
f1
& ( for
x
being
Real
st
x
in
Z
holds
(
f1
.
x
=
x
+
b
&
f1
.
x
>
0
) ) holds
(
(
id
Z
)
-
(
(
a
+
b
)
(#)
f
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
(
id
Z
)
-
(
(
a
+
b
)
(#)
f
)
)
`|
Z
)
.
x
=
(
x
-
a
)
/
(
x
+
b
)
) )
proof
end;
:: 11 f.x=x+ (b-a)*ln(x-b)
theorem
:: FDIFF_4:11
for
a
,
b
being
Real
for
Z
being
open
Subset
of
REAL
for
f
,
f1
being
PartFunc
of
REAL
,
REAL
st
Z
c=
dom
(
(
id
Z
)
+
(
(
b
-
a
)
(#)
f
)
)
&
f
=
ln
*
f1
& ( for
x
being
Real
st
x
in
Z
holds
(
f1
.
x
=
x
-
b
&
f1
.
x
>
0
) ) holds
(
(
id
Z
)
+
(
(
b
-
a
)
(#)
f
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
(
id
Z
)
+
(
(
b
-
a
)
(#)
f
)
)
`|
Z
)
.
x
=
(
x
-
a
)
/
(
x
-
b
)
) )
proof
end;
:: 12 f.x=a+b*x+c*x^2
theorem
Th12
:
:: FDIFF_4:12
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
(
f1
+
(
c
(#)
f2
)
)
& ( for
x
being
Real
st
x
in
Z
holds
f1
.
x
=
a
+
(
b
*
x
)
) &
f2
=
#Z
2 holds
(
f1
+
(
c
(#)
f2
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
f1
+
(
c
(#)
f2
)
)
`|
Z
)
.
x
=
b
+
(
(
2
*
c
)
*
x
)
) )
proof
end;
:: 13 f.x=ln(a+b*x+c*x^2)
theorem
Th13
:
:: FDIFF_4:13
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
(
ln
*
(
f1
+
(
c
(#)
f2
)
)
)
&
f2
=
#Z
2 & ( for
x
being
Real
st
x
in
Z
holds
(
f1
.
x
=
a
+
(
b
*
x
)
&
(
f1
+
(
c
(#)
f2
)
)
.
x
>
0
) ) holds
(
ln
*
(
f1
+
(
c
(#)
f2
)
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
ln
*
(
f1
+
(
c
(#)
f2
)
)
)
`|
Z
)
.
x
=
(
b
+
(
(
2
*
c
)
*
x
)
)
/
(
(
a
+
(
b
*
x
)
)
+
(
c
*
(
x
|^
2
)
)
)
) )
proof
end;
:: 14 f.x=1/(a+x)
theorem
Th14
:
:: FDIFF_4:14
for
a
being
Real
for
Z
being
open
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
st
Z
c=
dom
f
& ( for
x
being
Real
st
x
in
Z
holds
(
f
.
x
=
a
+
x
&
f
.
x
<>
0
) ) holds
(
f
^
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
f
^
)
`|
Z
)
.
x
=
-
(
1
/
(
(
a
+
x
)
^2
)
)
) )
proof
end;
:: 15 f.x=-1/(a+x)
theorem
:: FDIFF_4:15
for
a
being
Real
for
Z
being
open
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
st
Z
c=
dom
(
(
-
1
)
(#)
(
f
^
)
)
& ( for
x
being
Real
st
x
in
Z
holds
(
f
.
x
=
a
+
x
&
f
.
x
<>
0
) ) holds
(
(
-
1
)
(#)
(
f
^
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
(
-
1
)
(#)
(
f
^
)
)
`|
Z
)
.
x
=
1
/
(
(
a
+
x
)
^2
)
) )
proof
end;
:: 16 f.x=1/(a-x)
theorem
:: FDIFF_4:16
for
a
being
Real
for
Z
being
open
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
st
Z
c=
dom
f
& ( for
x
being
Real
st
x
in
Z
holds
(
f
.
x
=
a
-
x
&
f
.
x
<>
0
) ) holds
(
f
^
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
f
^
)
`|
Z
)
.
x
=
1
/
(
(
a
-
x
)
^2
)
) )
proof
end;
:: 17 f.x=a^2+x^2
theorem
Th17
:
:: FDIFF_4:17
for
a
being
Real
for
Z
being
open
Subset
of
REAL
for
f1
,
f2
being
PartFunc
of
REAL
,
REAL
st
Z
c=
dom
(
f1
+
f2
)
& ( for
x
being
Real
st
x
in
Z
holds
f1
.
x
=
a
^2
) &
f2
=
#Z
2 holds
(
f1
+
f2
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
f1
+
f2
)
`|
Z
)
.
x
=
2
*
x
) )
proof
end;
:: 18 f.x=ln(a^2+x^2)
theorem
:: FDIFF_4:18
for
a
being
Real
for
Z
being
open
Subset
of
REAL
for
f1
,
f2
being
PartFunc
of
REAL
,
REAL
st
Z
c=
dom
(
ln
*
(
f1
+
f2
)
)
&
f2
=
#Z
2 & ( for
x
being
Real
st
x
in
Z
holds
(
f1
.
x
=
a
^2
&
(
f1
+
f2
)
.
x
>
0
) ) holds
(
ln
*
(
f1
+
f2
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
ln
*
(
f1
+
f2
)
)
`|
Z
)
.
x
=
(
2
*
x
)
/
(
(
a
^2
)
+
(
x
|^
2
)
)
) )
proof
end;
:: 19 f.x=-ln(a^2-x^2)
theorem
:: FDIFF_4:19
for
a
being
Real
for
Z
being
open
Subset
of
REAL
for
f1
,
f2
being
PartFunc
of
REAL
,
REAL
st
Z
c=
dom
(
-
(
ln
*
(
f1
-
f2
)
)
)
&
f2
=
#Z
2 & ( for
x
being
Real
st
x
in
Z
holds
(
f1
.
x
=
a
^2
&
(
f1
-
f2
)
.
x
>
0
) ) holds
(
-
(
ln
*
(
f1
-
f2
)
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
-
(
ln
*
(
f1
-
f2
)
)
)
`|
Z
)
.
x
=
(
2
*
x
)
/
(
(
a
^2
)
-
(
x
|^
2
)
)
) )
proof
end;
:: 20 f.x=a+x^3
theorem
Th20
:
:: FDIFF_4:20
for
a
being
Real
for
Z
being
open
Subset
of
REAL
for
f1
,
f2
being
PartFunc
of
REAL
,
REAL
st
Z
c=
dom
(
f1
+
f2
)
& ( for
x
being
Real
st
x
in
Z
holds
f1
.
x
=
a
) &
f2
=
#Z
3 holds
(
f1
+
f2
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
f1
+
f2
)
`|
Z
)
.
x
=
3
*
(
x
|^
2
)
) )
proof
end;
:: 21 f.x=ln(a+x^3)
theorem
:: FDIFF_4:21
for
a
being
Real
for
Z
being
open
Subset
of
REAL
for
f1
,
f2
being
PartFunc
of
REAL
,
REAL
st
Z
c=
dom
(
ln
*
(
f1
+
f2
)
)
&
f2
=
#Z
3 & ( for
x
being
Real
st
x
in
Z
holds
(
f1
.
x
=
a
&
(
f1
+
f2
)
.
x
>
0
) ) holds
(
ln
*
(
f1
+
f2
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
ln
*
(
f1
+
f2
)
)
`|
Z
)
.
x
=
(
3
*
(
x
|^
2
)
)
/
(
a
+
(
x
|^
3
)
)
) )
proof
end;
:: 22 f.x=ln((a+x)/(a-x))
theorem
:: FDIFF_4:22
for
a
being
Real
for
Z
being
open
Subset
of
REAL
for
f1
,
f2
being
PartFunc
of
REAL
,
REAL
st
Z
c=
dom
(
ln
*
(
f1
/
f2
)
)
& ( for
x
being
Real
st
x
in
Z
holds
(
f1
.
x
=
a
+
x
&
f1
.
x
>
0
&
f2
.
x
=
a
-
x
&
f2
.
x
>
0
) ) holds
(
ln
*
(
f1
/
f2
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
ln
*
(
f1
/
f2
)
)
`|
Z
)
.
x
=
(
2
*
a
)
/
(
(
a
^2
)
-
(
x
^2
)
)
) )
proof
end;
:: 23 f.x=ln((x-a)/(x+a))
theorem
:: FDIFF_4:23
for
a
being
Real
for
Z
being
open
Subset
of
REAL
for
f1
,
f2
being
PartFunc
of
REAL
,
REAL
st
Z
c=
dom
(
ln
*
(
f1
/
f2
)
)
& ( for
x
being
Real
st
x
in
Z
holds
(
f1
.
x
=
x
-
a
&
f1
.
x
>
0
&
f2
.
x
=
x
+
a
&
f2
.
x
>
0
) ) holds
(
ln
*
(
f1
/
f2
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
ln
*
(
f1
/
f2
)
)
`|
Z
)
.
x
=
(
2
*
a
)
/
(
(
x
^2
)
-
(
a
^2
)
)
) )
proof
end;
:: 24 f.x=ln((x-a)/(x-b))
theorem
Th24
:
:: FDIFF_4:24
for
a
,
b
being
Real
for
Z
being
open
Subset
of
REAL
for
f1
,
f2
being
PartFunc
of
REAL
,
REAL
st
Z
c=
dom
(
ln
*
(
f1
/
f2
)
)
& ( for
x
being
Real
st
x
in
Z
holds
(
f1
.
x
=
x
-
a
&
f1
.
x
>
0
&
f2
.
x
=
x
-
b
&
f2
.
x
>
0
) ) holds
(
ln
*
(
f1
/
f2
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
ln
*
(
f1
/
f2
)
)
`|
Z
)
.
x
=
(
a
-
b
)
/
(
(
x
-
a
)
*
(
x
-
b
)
)
) )
proof
end;
:: 25 f.x=(1/(a-b))*ln((x-a)/(x-b))
theorem
:: FDIFF_4:25
for
a
,
b
being
Real
for
Z
being
open
Subset
of
REAL
for
f
,
f1
,
f2
being
PartFunc
of
REAL
,
REAL
st
Z
c=
dom
(
(
1
/
(
a
-
b
)
)
(#)
f
)
&
f
=
ln
*
(
f1
/
f2
)
& ( for
x
being
Real
st
x
in
Z
holds
(
f1
.
x
=
x
-
a
&
f1
.
x
>
0
&
f2
.
x
=
x
-
b
&
f2
.
x
>
0
&
a
-
b
<>
0
) ) holds
(
(
1
/
(
a
-
b
)
)
(#)
f
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
(
1
/
(
a
-
b
)
)
(#)
f
)
`|
Z
)
.
x
=
1
/
(
(
x
-
a
)
*
(
x
-
b
)
)
) )
proof
end;
:: 26 f.x=ln((x-a)/x^2)
theorem
:: FDIFF_4:26
for
a
being
Real
for
Z
being
open
Subset
of
REAL
for
f1
,
f2
being
PartFunc
of
REAL
,
REAL
st
Z
c=
dom
(
ln
*
(
f1
/
f2
)
)
&
f2
=
#Z
2 & ( for
x
being
Real
st
x
in
Z
holds
(
f1
.
x
=
x
-
a
&
f1
.
x
>
0
&
f2
.
x
>
0
&
x
<>
0
) ) holds
(
ln
*
(
f1
/
f2
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
ln
*
(
f1
/
f2
)
)
`|
Z
)
.
x
=
(
(
2
*
a
)
-
x
)
/
(
x
*
(
x
-
a
)
)
) )
proof
end;
:: irrational function
:: 27 f.x=(a+x) ^ (3/2)
theorem
Th27
:
:: FDIFF_4:27
for
a
being
Real
for
Z
being
open
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
st
Z
c=
dom
(
(
#R
(
3
/
2
)
)
*
f
)
& ( for
x
being
Real
st
x
in
Z
holds
(
f
.
x
=
a
+
x
&
f
.
x
>
0
) ) holds
(
(
#R
(
3
/
2
)
)
*
f
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
(
#R
(
3
/
2
)
)
*
f
)
`|
Z
)
.
x
=
(
3
/
2
)
*
(
(
a
+
x
)
#R
(
1
/
2
)
)
) )
proof
end;
:: 28 f.x=(a+x) ^ (2/3)
theorem
:: FDIFF_4:28
for
a
being
Real
for
Z
being
open
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
st
Z
c=
dom
(
(
2
/
3
)
(#)
(
(
#R
(
3
/
2
)
)
*
f
)
)
& ( for
x
being
Real
st
x
in
Z
holds
(
f
.
x
=
a
+
x
&
f
.
x
>
0
) ) holds
(
(
2
/
3
)
(#)
(
(
#R
(
3
/
2
)
)
*
f
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
(
2
/
3
)
(#)
(
(
#R
(
3
/
2
)
)
*
f
)
)
`|
Z
)
.
x
=
(
a
+
x
)
#R
(
1
/
2
)
) )
proof
end;
:: 29 f.x=(-2/3)*(a+x) ^ (2/3)
theorem
:: FDIFF_4:29
for
a
being
Real
for
Z
being
open
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
st
Z
c=
dom
(
(
-
(
2
/
3
)
)
(#)
(
(
#R
(
3
/
2
)
)
*
f
)
)
& ( for
x
being
Real
st
x
in
Z
holds
(
f
.
x
=
a
-
x
&
f
.
x
>
0
) ) holds
(
(
-
(
2
/
3
)
)
(#)
(
(
#R
(
3
/
2
)
)
*
f
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
(
-
(
2
/
3
)
)
(#)
(
(
#R
(
3
/
2
)
)
*
f
)
)
`|
Z
)
.
x
=
(
a
-
x
)
#R
(
1
/
2
)
) )
proof
end;
:: 30 f.x=2*(a+x) ^ (1/2)
theorem
:: FDIFF_4:30
for
a
being
Real
for
Z
being
open
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
st
Z
c=
dom
(
2
(#)
(
(
#R
(
1
/
2
)
)
*
f
)
)
& ( for
x
being
Real
st
x
in
Z
holds
(
f
.
x
=
a
+
x
&
f
.
x
>
0
) ) holds
( 2
(#)
(
(
#R
(
1
/
2
)
)
*
f
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
2
(#)
(
(
#R
(
1
/
2
)
)
*
f
)
)
`|
Z
)
.
x
=
(
a
+
x
)
#R
(
-
(
1
/
2
)
)
) )
proof
end;
:: 31 f.x=(-2)*(a-x) ^ (1/2)
theorem
:: FDIFF_4:31
for
a
being
Real
for
Z
being
open
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
st
Z
c=
dom
(
(
-
2
)
(#)
(
(
#R
(
1
/
2
)
)
*
f
)
)
& ( for
x
being
Real
st
x
in
Z
holds
(
f
.
x
=
a
-
x
&
f
.
x
>
0
) ) holds
(
(
-
2
)
(#)
(
(
#R
(
1
/
2
)
)
*
f
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
(
-
2
)
(#)
(
(
#R
(
1
/
2
)
)
*
f
)
)
`|
Z
)
.
x
=
(
a
-
x
)
#R
(
-
(
1
/
2
)
)
) )
proof
end;
:: 32 f.x=(2/(3*b))*((a+b*x) ^ (3/2))
theorem
:: FDIFF_4:32
for
a
,
b
being
Real
for
Z
being
open
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
st
Z
c=
dom
(
(
2
/
(
3
*
b
)
)
(#)
(
(
#R
(
3
/
2
)
)
*
f
)
)
& ( for
x
being
Real
st
x
in
Z
holds
(
f
.
x
=
a
+
(
b
*
x
)
&
b
<>
0
&
f
.
x
>
0
) ) holds
(
(
2
/
(
3
*
b
)
)
(#)
(
(
#R
(
3
/
2
)
)
*
f
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
(
2
/
(
3
*
b
)
)
(#)
(
(
#R
(
3
/
2
)
)
*
f
)
)
`|
Z
)
.
x
=
(
a
+
(
b
*
x
)
)
#R
(
1
/
2
)
) )
proof
end;
:: 33 f.x=(-2/(3*b))*((a-b*x) ^ (3/2))
theorem
:: FDIFF_4:33
for
a
,
b
being
Real
for
Z
being
open
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
st
Z
c=
dom
(
(
-
(
2
/
(
3
*
b
)
)
)
(#)
(
(
#R
(
3
/
2
)
)
*
f
)
)
& ( for
x
being
Real
st
x
in
Z
holds
(
f
.
x
=
a
-
(
b
*
x
)
&
b
<>
0
&
f
.
x
>
0
) ) holds
(
(
-
(
2
/
(
3
*
b
)
)
)
(#)
(
(
#R
(
3
/
2
)
)
*
f
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
(
-
(
2
/
(
3
*
b
)
)
)
(#)
(
(
#R
(
3
/
2
)
)
*
f
)
)
`|
Z
)
.
x
=
(
a
-
(
b
*
x
)
)
#R
(
1
/
2
)
) )
proof
end;
:: 34 f.x=(a^2+x|^2) ^ (1/2)
theorem
:: FDIFF_4:34
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
|^
2
)
)
#R
(
-
(
1
/
2
)
)
)
) )
proof
end;
:: 35 f.x=-(a^2-x|^2) ^ (1/2)
theorem
:: FDIFF_4:35
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
|^
2
)
)
#R
(
-
(
1
/
2
)
)
)
) )
proof
end;
:: 36 f.x=(x+x|^2) ^ (1/2)
theorem
:: FDIFF_4:36
for
Z
being
open
Subset
of
REAL
for
f
,
f1
,
f2
being
PartFunc
of
REAL
,
REAL
st
Z
c=
dom
(
2
(#)
(
(
#R
(
1
/
2
)
)
*
f
)
)
&
f
=
f1
+
f2
&
f2
=
#Z
2 & ( for
x
being
Real
st
x
in
Z
holds
(
f1
.
x
=
x
&
f
.
x
>
0
) ) holds
( 2
(#)
(
(
#R
(
1
/
2
)
)
*
f
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
2
(#)
(
(
#R
(
1
/
2
)
)
*
f
)
)
`|
Z
)
.
x
=
(
(
2
*
x
)
+
1
)
*
(
(
(
x
|^
2
)
+
x
)
#R
(
-
(
1
/
2
)
)
)
) )
proof
end;
:: trigonometric functions
:: 37 f.x=sin(a*x+b)
theorem
:: FDIFF_4:37
for
a
,
b
being
Real
for
Z
being
open
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
st
Z
c=
dom
(
sin
*
f
)
& ( for
x
being
Real
st
x
in
Z
holds
f
.
x
=
(
a
*
x
)
+
b
) holds
(
sin
*
f
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
sin
*
f
)
`|
Z
)
.
x
=
a
*
(
cos
.
(
(
a
*
x
)
+
b
)
)
) )
proof
end;
:: 38 f.x=sin(a*x+b)
theorem
:: FDIFF_4:38
for
a
,
b
being
Real
for
Z
being
open
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
st
Z
c=
dom
(
cos
*
f
)
& ( for
x
being
Real
st
x
in
Z
holds
f
.
x
=
(
a
*
x
)
+
b
) holds
(
cos
*
f
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
cos
*
f
)
`|
Z
)
.
x
=
-
(
a
*
(
sin
.
(
(
a
*
x
)
+
b
)
)
)
) )
proof
end;
:: 39 f.x=1/cos.x
theorem
:: FDIFF_4:39
for
Z
being
open
Subset
of
REAL
st ( for
x
being
Real
st
x
in
Z
holds
cos
.
x
<>
0
) holds
(
cos
^
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
cos
^
)
`|
Z
)
.
x
=
(
sin
.
x
)
/
(
(
cos
.
x
)
^2
)
) )
proof
end;
:: 40 f.x=1/sin.x
theorem
:: FDIFF_4:40
for
Z
being
open
Subset
of
REAL
st ( for
x
being
Real
st
x
in
Z
holds
sin
.
x
<>
0
) holds
(
sin
^
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
sin
^
)
`|
Z
)
.
x
=
-
(
(
cos
.
x
)
/
(
(
sin
.
x
)
^2
)
)
) )
proof
end;
:: 41 f.x=sin.x*cos.x
theorem
:: FDIFF_4:41
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
(
2
*
x
)
) )
proof
end;
:: 42 f.x=ln(cos.x)
theorem
:: FDIFF_4:42
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
ln
*
cos
)
& ( for
x
being
Real
st
x
in
Z
holds
cos
.
x
>
0
) holds
(
ln
*
cos
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
ln
*
cos
)
`|
Z
)
.
x
=
-
(
tan
x
)
) )
proof
end;
:: 43 f.x=ln(sin.x)
theorem
:: FDIFF_4:43
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
ln
*
sin
)
& ( for
x
being
Real
st
x
in
Z
holds
sin
.
x
>
0
) holds
(
ln
*
sin
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
ln
*
sin
)
`|
Z
)
.
x
=
cot
x
) )
proof
end;
:: 44 f.x=-x*cos.x
theorem
Th44
:
:: FDIFF_4:44
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
(
-
(
id
Z
)
)
(#)
cos
)
holds
(
(
-
(
id
Z
)
)
(#)
cos
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
(
-
(
id
Z
)
)
(#)
cos
)
`|
Z
)
.
x
=
(
-
(
cos
.
x
)
)
+
(
x
*
(
sin
.
x
)
)
) )
proof
end;
:: f.x=x*sin.x
theorem
Th45
:
:: FDIFF_4:45
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
(
id
Z
)
(#)
sin
)
holds
(
(
id
Z
)
(#)
sin
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
(
id
Z
)
(#)
sin
)
`|
Z
)
.
x
=
(
sin
.
x
)
+
(
x
*
(
cos
.
x
)
)
) )
proof
end;
:: 46 f.x=-x*cos.x+sin.x
theorem
:: FDIFF_4:46
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
(
(
-
(
id
Z
)
)
(#)
cos
)
+
sin
)
holds
(
(
(
-
(
id
Z
)
)
(#)
cos
)
+
sin
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
(
(
-
(
id
Z
)
)
(#)
cos
)
+
sin
)
`|
Z
)
.
x
=
x
*
(
sin
.
x
)
) )
proof
end;
:: 47 f.x=x*sin.x+cos.x
theorem
:: FDIFF_4:47
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
(
(
id
Z
)
(#)
sin
)
+
cos
)
holds
(
(
(
id
Z
)
(#)
sin
)
+
cos
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
(
(
id
Z
)
(#)
sin
)
+
cos
)
`|
Z
)
.
x
=
x
*
(
cos
.
x
)
) )
proof
end;
:: 48 f.x=2*(sin.x ^ (1/2))
theorem
:: FDIFF_4:48
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
2
(#)
(
(
#R
(
1
/
2
)
)
*
sin
)
)
& ( for
x
being
Real
st
x
in
Z
holds
sin
.
x
>
0
) holds
( 2
(#)
(
(
#R
(
1
/
2
)
)
*
sin
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
2
(#)
(
(
#R
(
1
/
2
)
)
*
sin
)
)
`|
Z
)
.
x
=
(
cos
.
x
)
*
(
(
sin
.
x
)
#R
(
-
(
1
/
2
)
)
)
) )
proof
end;
theorem
Th49
:
:: FDIFF_4:49
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
(
1
/
2
)
(#)
(
(
#Z
2
)
*
sin
)
)
holds
(
(
1
/
2
)
(#)
(
(
#Z
2
)
*
sin
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
(
1
/
2
)
(#)
(
(
#Z
2
)
*
sin
)
)
`|
Z
)
.
x
=
(
sin
.
x
)
*
(
cos
.
x
)
) )
proof
end;
:: 50 f.x=sin.x+(1/2)*(sin.x ^ 2)
theorem
:: FDIFF_4:50
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
sin
+
(
(
1
/
2
)
(#)
(
(
#Z
2
)
*
sin
)
)
)
& ( for
x
being
Real
st
x
in
Z
holds
(
sin
.
x
>
0
&
sin
.
x
<
1 ) ) holds
(
sin
+
(
(
1
/
2
)
(#)
(
(
#Z
2
)
*
sin
)
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
sin
+
(
(
1
/
2
)
(#)
(
(
#Z
2
)
*
sin
)
)
)
`|
Z
)
.
x
=
(
(
cos
.
x
)
|^
3
)
/
(
1
-
(
sin
.
x
)
)
) )
proof
end;
:: 51 f.x=(1/2)*(sin.x ^ 2)-cos.x
theorem
:: FDIFF_4:51
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
(
(
1
/
2
)
(#)
(
(
#Z
2
)
*
sin
)
)
-
cos
)
& ( for
x
being
Real
st
x
in
Z
holds
(
sin
.
x
>
0
&
cos
.
x
<
1 ) ) holds
(
(
(
1
/
2
)
(#)
(
(
#Z
2
)
*
sin
)
)
-
cos
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
(
(
1
/
2
)
(#)
(
(
#Z
2
)
*
sin
)
)
-
cos
)
`|
Z
)
.
x
=
(
(
sin
.
x
)
|^
3
)
/
(
1
-
(
cos
.
x
)
)
) )
proof
end;
:: 52 f.x=sin.x-(1/2)*(sin ^ 2)
theorem
:: FDIFF_4:52
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
sin
-
(
(
1
/
2
)
(#)
(
(
#Z
2
)
*
sin
)
)
)
& ( for
x
being
Real
st
x
in
Z
holds
(
sin
.
x
>
0
&
sin
.
x
>
-
1 ) ) holds
(
sin
-
(
(
1
/
2
)
(#)
(
(
#Z
2
)
*
sin
)
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
sin
-
(
(
1
/
2
)
(#)
(
(
#Z
2
)
*
sin
)
)
)
`|
Z
)
.
x
=
(
(
cos
.
x
)
|^
3
)
/
(
1
+
(
sin
.
x
)
)
) )
proof
end;
:: 53 f.x=-cos.x-(1/2)*(sin.x ^ 2)
theorem
:: FDIFF_4:53
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
(
-
cos
)
-
(
(
1
/
2
)
(#)
(
(
#Z
2
)
*
sin
)
)
)
& ( for
x
being
Real
st
x
in
Z
holds
(
sin
.
x
>
0
&
cos
.
x
>
-
1 ) ) holds
(
(
-
cos
)
-
(
(
1
/
2
)
(#)
(
(
#Z
2
)
*
sin
)
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
(
-
cos
)
-
(
(
1
/
2
)
(#)
(
(
#Z
2
)
*
sin
)
)
)
`|
Z
)
.
x
=
(
(
sin
.
x
)
|^
3
)
/
(
1
+
(
cos
.
x
)
)
) )
proof
end;
:: 54 f.x=(1/n)*(sin.x ^ n)
theorem
:: FDIFF_4:54
for
n
being
Element
of
NAT
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
(
1
/
n
)
(#)
(
(
#Z
n
)
*
sin
)
)
&
n
>
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
=
(
(
sin
.
x
)
#Z
(
n
-
1
)
)
*
(
cos
.
x
)
) )
proof
end;
:: exponential function
:: 55 f.x=exp.x*(x-1)
theorem
:: FDIFF_4:55
for
Z
being
open
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
st
Z
c=
dom
(
exp_R
(#)
f
)
& ( for
x
being
Real
st
x
in
Z
holds
f
.
x
=
x
-
1 ) holds
(
exp_R
(#)
f
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
exp_R
(#)
f
)
`|
Z
)
.
x
=
x
*
(
exp_R
.
x
)
) )
proof
end;
:: 56 f.x=ln(exp.x/(exp.x+1))
theorem
:: FDIFF_4:56
for
Z
being
open
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
st
Z
c=
dom
(
ln
*
(
exp_R
/
(
exp_R
+
f
)
)
)
& ( for
x
being
Real
st
x
in
Z
holds
f
.
x
=
1 ) holds
(
ln
*
(
exp_R
/
(
exp_R
+
f
)
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
ln
*
(
exp_R
/
(
exp_R
+
f
)
)
)
`|
Z
)
.
x
=
1
/
(
(
exp_R
.
x
)
+
1
)
) )
proof
end;
:: 57 f.x=ln((exp.x-1)/exp.x)
theorem
:: FDIFF_4:57
for
Z
being
open
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
st
Z
c=
dom
(
ln
*
(
(
exp_R
-
f
)
/
exp_R
)
)
& ( for
x
being
Real
st
x
in
Z
holds
(
f
.
x
=
1 &
(
exp_R
-
f
)
.
x
>
0
) ) holds
(
ln
*
(
(
exp_R
-
f
)
/
exp_R
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
ln
*
(
(
exp_R
-
f
)
/
exp_R
)
)
`|
Z
)
.
x
=
1
/
(
(
exp_R
.
x
)
-
1
)
) )
proof
end;