:: Several Differentiation Formulas of Special Functions -- Part {VII}
:: by Fuguo Ge and Bing Xie
::
:: Received September 23, 2008
:: Copyright (c) 2008-2012 Association of Mizar Users
begin
::f.x=arctan.(sin.x)
theorem
:: FDIFF_11:1
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
arctan
*
sin
)
& ( for
x
being
Real
st
x
in
Z
holds
(
sin
.
x
>
-
1 &
sin
.
x
<
1 ) ) holds
(
arctan
*
sin
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
arctan
*
sin
)
`|
Z
)
.
x
=
(
cos
.
x
)
/
(
1
+
(
(
sin
.
x
)
^2
)
)
) )
proof
end;
::f.x=arccot.(sin.x)
theorem
:: FDIFF_11:2
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
arccot
*
sin
)
& ( for
x
being
Real
st
x
in
Z
holds
(
sin
.
x
>
-
1 &
sin
.
x
<
1 ) ) holds
(
arccot
*
sin
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
arccot
*
sin
)
`|
Z
)
.
x
=
-
(
(
cos
.
x
)
/
(
1
+
(
(
sin
.
x
)
^2
)
)
)
) )
proof
end;
::f.x=arctan.(cos.x)
theorem
:: FDIFF_11:3
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
arctan
*
cos
)
& ( for
x
being
Real
st
x
in
Z
holds
(
cos
.
x
>
-
1 &
cos
.
x
<
1 ) ) holds
(
arctan
*
cos
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
arctan
*
cos
)
`|
Z
)
.
x
=
-
(
(
sin
.
x
)
/
(
1
+
(
(
cos
.
x
)
^2
)
)
)
) )
proof
end;
::f.x=arccot.(cos.x)
theorem
:: FDIFF_11:4
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
arccot
*
cos
)
& ( for
x
being
Real
st
x
in
Z
holds
(
cos
.
x
>
-
1 &
cos
.
x
<
1 ) ) holds
(
arccot
*
cos
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
arccot
*
cos
)
`|
Z
)
.
x
=
(
sin
.
x
)
/
(
1
+
(
(
cos
.
x
)
^2
)
)
) )
proof
end;
::f.x=arctan.(tan.x)
theorem
:: FDIFF_11:5
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
arctan
*
tan
)
& ( for
x
being
Real
st
x
in
Z
holds
(
tan
.
x
>
-
1 &
tan
.
x
<
1 ) ) holds
(
arctan
*
tan
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
arctan
*
tan
)
`|
Z
)
.
x
=
1 ) )
proof
end;
::f.x=arccot.(tan.x)
theorem
:: FDIFF_11:6
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
arccot
*
tan
)
& ( for
x
being
Real
st
x
in
Z
holds
(
tan
.
x
>
-
1 &
tan
.
x
<
1 ) ) holds
(
arccot
*
tan
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
arccot
*
tan
)
`|
Z
)
.
x
=
-
1 ) )
proof
end;
::f.x=arctan.(cot.x)
theorem
:: FDIFF_11:7
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
arctan
*
cot
)
& ( for
x
being
Real
st
x
in
Z
holds
(
cot
.
x
>
-
1 &
cot
.
x
<
1 ) ) holds
(
arctan
*
cot
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
arctan
*
cot
)
`|
Z
)
.
x
=
-
1 ) )
proof
end;
::f.x=arccot.(cot.x)
theorem
:: FDIFF_11:8
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
arccot
*
cot
)
& ( for
x
being
Real
st
x
in
Z
holds
(
cot
.
x
>
-
1 &
cot
.
x
<
1 ) ) holds
(
arccot
*
cot
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
arccot
*
cot
)
`|
Z
)
.
x
=
1 ) )
proof
end;
::f.x=arctan.(arctan.x)
theorem
:: FDIFF_11:9
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
arctan
*
arctan
)
&
Z
c=
].
(
-
1
)
,1
.[
& ( for
x
being
Real
st
x
in
Z
holds
(
arctan
.
x
>
-
1 &
arctan
.
x
<
1 ) ) holds
(
arctan
*
arctan
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
arctan
*
arctan
)
`|
Z
)
.
x
=
1
/
(
(
1
+
(
x
^2
)
)
*
(
1
+
(
(
arctan
.
x
)
^2
)
)
)
) )
proof
end;
::f.x=arccot.(arctan.x)
theorem
:: FDIFF_11:10
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
arccot
*
arctan
)
&
Z
c=
].
(
-
1
)
,1
.[
& ( for
x
being
Real
st
x
in
Z
holds
(
arctan
.
x
>
-
1 &
arctan
.
x
<
1 ) ) holds
(
arccot
*
arctan
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
arccot
*
arctan
)
`|
Z
)
.
x
=
-
(
1
/
(
(
1
+
(
x
^2
)
)
*
(
1
+
(
(
arctan
.
x
)
^2
)
)
)
)
) )
proof
end;
::f.x=arctan.(arccot.x)
theorem
:: FDIFF_11:11
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
arctan
*
arccot
)
&
Z
c=
].
(
-
1
)
,1
.[
& ( for
x
being
Real
st
x
in
Z
holds
(
arccot
.
x
>
-
1 &
arccot
.
x
<
1 ) ) holds
(
arctan
*
arccot
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
arctan
*
arccot
)
`|
Z
)
.
x
=
-
(
1
/
(
(
1
+
(
x
^2
)
)
*
(
1
+
(
(
arccot
.
x
)
^2
)
)
)
)
) )
proof
end;
::f.x=arccot.(arccot.x)
theorem
:: FDIFF_11:12
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
arccot
*
arccot
)
&
Z
c=
].
(
-
1
)
,1
.[
& ( for
x
being
Real
st
x
in
Z
holds
(
arccot
.
x
>
-
1 &
arccot
.
x
<
1 ) ) holds
(
arccot
*
arccot
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
arccot
*
arccot
)
`|
Z
)
.
x
=
1
/
(
(
1
+
(
x
^2
)
)
*
(
1
+
(
(
arccot
.
x
)
^2
)
)
)
) )
proof
end;
::f.x=sin.(arctan.x)
theorem
:: FDIFF_11:13
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
sin
*
arctan
)
&
Z
c=
].
(
-
1
)
,1
.[
holds
(
sin
*
arctan
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
sin
*
arctan
)
`|
Z
)
.
x
=
(
cos
.
(
arctan
.
x
)
)
/
(
1
+
(
x
^2
)
)
) )
proof
end;
::f.x=sin.(arccot.x)
theorem
:: FDIFF_11:14
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
sin
*
arccot
)
&
Z
c=
].
(
-
1
)
,1
.[
holds
(
sin
*
arccot
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
sin
*
arccot
)
`|
Z
)
.
x
=
-
(
(
cos
.
(
arccot
.
x
)
)
/
(
1
+
(
x
^2
)
)
)
) )
proof
end;
::f.x=cos.(arctan.x)
theorem
:: FDIFF_11:15
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
cos
*
arctan
)
&
Z
c=
].
(
-
1
)
,1
.[
holds
(
cos
*
arctan
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
cos
*
arctan
)
`|
Z
)
.
x
=
-
(
(
sin
.
(
arctan
.
x
)
)
/
(
1
+
(
x
^2
)
)
)
) )
proof
end;
::f.x=cos.(arccot.x)
theorem
:: FDIFF_11:16
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
cos
*
arccot
)
&
Z
c=
].
(
-
1
)
,1
.[
holds
(
cos
*
arccot
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
cos
*
arccot
)
`|
Z
)
.
x
=
(
sin
.
(
arccot
.
x
)
)
/
(
1
+
(
x
^2
)
)
) )
proof
end;
::f.x=tan.(arctan.x)
theorem
:: FDIFF_11:17
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
tan
*
arctan
)
&
Z
c=
].
(
-
1
)
,1
.[
holds
(
tan
*
arctan
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
tan
*
arctan
)
`|
Z
)
.
x
=
1
/
(
(
(
cos
.
(
arctan
.
x
)
)
^2
)
*
(
1
+
(
x
^2
)
)
)
) )
proof
end;
::f.x=tan.(arccot.x)
theorem
:: FDIFF_11:18
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
tan
*
arccot
)
&
Z
c=
].
(
-
1
)
,1
.[
holds
(
tan
*
arccot
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
tan
*
arccot
)
`|
Z
)
.
x
=
-
(
1
/
(
(
(
cos
.
(
arccot
.
x
)
)
^2
)
*
(
1
+
(
x
^2
)
)
)
)
) )
proof
end;
::f.x=cot.(arctan.x)
theorem
:: FDIFF_11:19
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
cot
*
arctan
)
&
Z
c=
].
(
-
1
)
,1
.[
holds
(
cot
*
arctan
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
cot
*
arctan
)
`|
Z
)
.
x
=
-
(
1
/
(
(
(
sin
.
(
arctan
.
x
)
)
^2
)
*
(
1
+
(
x
^2
)
)
)
)
) )
proof
end;
::f.x=cot.(arccot.x)
theorem
:: FDIFF_11:20
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
cot
*
arccot
)
&
Z
c=
].
(
-
1
)
,1
.[
holds
(
cot
*
arccot
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
cot
*
arccot
)
`|
Z
)
.
x
=
1
/
(
(
(
sin
.
(
arccot
.
x
)
)
^2
)
*
(
1
+
(
x
^2
)
)
)
) )
proof
end;
::f.x=sec.(arctan.x)
theorem
:: FDIFF_11:21
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
sec
*
arctan
)
&
Z
c=
].
(
-
1
)
,1
.[
holds
(
sec
*
arctan
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
sec
*
arctan
)
`|
Z
)
.
x
=
(
sin
.
(
arctan
.
x
)
)
/
(
(
(
cos
.
(
arctan
.
x
)
)
^2
)
*
(
1
+
(
x
^2
)
)
)
) )
proof
end;
::f.x=sec.(arccot.x)
theorem
:: FDIFF_11:22
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
sec
*
arccot
)
&
Z
c=
].
(
-
1
)
,1
.[
holds
(
sec
*
arccot
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
sec
*
arccot
)
`|
Z
)
.
x
=
-
(
(
sin
.
(
arccot
.
x
)
)
/
(
(
(
cos
.
(
arccot
.
x
)
)
^2
)
*
(
1
+
(
x
^2
)
)
)
)
) )
proof
end;
::f.x=cosec.(arctan.x)
theorem
:: FDIFF_11:23
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
cosec
*
arctan
)
&
Z
c=
].
(
-
1
)
,1
.[
holds
(
cosec
*
arctan
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
cosec
*
arctan
)
`|
Z
)
.
x
=
-
(
(
cos
.
(
arctan
.
x
)
)
/
(
(
(
sin
.
(
arctan
.
x
)
)
^2
)
*
(
1
+
(
x
^2
)
)
)
)
) )
proof
end;
::f.x=cosec.(arccot.x)
theorem
:: FDIFF_11:24
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
cosec
*
arccot
)
&
Z
c=
].
(
-
1
)
,1
.[
holds
(
cosec
*
arccot
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
cosec
*
arccot
)
`|
Z
)
.
x
=
(
cos
.
(
arccot
.
x
)
)
/
(
(
(
sin
.
(
arccot
.
x
)
)
^2
)
*
(
1
+
(
x
^2
)
)
)
) )
proof
end;
::f.x=sin.x*arctan.x
theorem
:: FDIFF_11:25
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
sin
(#)
arctan
)
&
Z
c=
].
(
-
1
)
,1
.[
holds
(
sin
(#)
arctan
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
sin
(#)
arctan
)
`|
Z
)
.
x
=
(
(
cos
.
x
)
*
(
arctan
.
x
)
)
+
(
(
sin
.
x
)
/
(
1
+
(
x
^2
)
)
)
) )
proof
end;
::f.x=sin.x*arccot.x
theorem
:: FDIFF_11:26
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
sin
(#)
arccot
)
&
Z
c=
].
(
-
1
)
,1
.[
holds
(
sin
(#)
arccot
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
sin
(#)
arccot
)
`|
Z
)
.
x
=
(
(
cos
.
x
)
*
(
arccot
.
x
)
)
-
(
(
sin
.
x
)
/
(
1
+
(
x
^2
)
)
)
) )
proof
end;
::f.x=cos.x*arctan.x
theorem
:: FDIFF_11:27
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
cos
(#)
arctan
)
&
Z
c=
].
(
-
1
)
,1
.[
holds
(
cos
(#)
arctan
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
cos
(#)
arctan
)
`|
Z
)
.
x
=
(
-
(
(
sin
.
x
)
*
(
arctan
.
x
)
)
)
+
(
(
cos
.
x
)
/
(
1
+
(
x
^2
)
)
)
) )
proof
end;
::f.x=cos.x*arccot.x
theorem
:: FDIFF_11:28
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
cos
(#)
arccot
)
&
Z
c=
].
(
-
1
)
,1
.[
holds
(
cos
(#)
arccot
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
cos
(#)
arccot
)
`|
Z
)
.
x
=
(
-
(
(
sin
.
x
)
*
(
arccot
.
x
)
)
)
-
(
(
cos
.
x
)
/
(
1
+
(
x
^2
)
)
)
) )
proof
end;
::f.x=tan.x*arctan.x
theorem
:: FDIFF_11:29
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
tan
(#)
arctan
)
&
Z
c=
].
(
-
1
)
,1
.[
holds
(
tan
(#)
arctan
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
tan
(#)
arctan
)
`|
Z
)
.
x
=
(
(
arctan
.
x
)
/
(
(
cos
.
x
)
^2
)
)
+
(
(
tan
.
x
)
/
(
1
+
(
x
^2
)
)
)
) )
proof
end;
::f.x=tan.x*arccot.x
theorem
:: FDIFF_11:30
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
tan
(#)
arccot
)
&
Z
c=
].
(
-
1
)
,1
.[
holds
(
tan
(#)
arccot
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
tan
(#)
arccot
)
`|
Z
)
.
x
=
(
(
arccot
.
x
)
/
(
(
cos
.
x
)
^2
)
)
-
(
(
tan
.
x
)
/
(
1
+
(
x
^2
)
)
)
) )
proof
end;
::f.x=cot.x*arctan.x
theorem
:: FDIFF_11:31
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
cot
(#)
arctan
)
&
Z
c=
].
(
-
1
)
,1
.[
holds
(
cot
(#)
arctan
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
cot
(#)
arctan
)
`|
Z
)
.
x
=
(
-
(
(
arctan
.
x
)
/
(
(
sin
.
x
)
^2
)
)
)
+
(
(
cot
.
x
)
/
(
1
+
(
x
^2
)
)
)
) )
proof
end;
::f.x=cot.x*arccot.x
theorem
:: FDIFF_11:32
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
cot
(#)
arccot
)
&
Z
c=
].
(
-
1
)
,1
.[
holds
(
cot
(#)
arccot
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
cot
(#)
arccot
)
`|
Z
)
.
x
=
(
-
(
(
arccot
.
x
)
/
(
(
sin
.
x
)
^2
)
)
)
-
(
(
cot
.
x
)
/
(
1
+
(
x
^2
)
)
)
) )
proof
end;
::f.x=sec.x*arctan.x
theorem
:: FDIFF_11:33
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
sec
(#)
arctan
)
&
Z
c=
].
(
-
1
)
,1
.[
holds
(
sec
(#)
arctan
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
sec
(#)
arctan
)
`|
Z
)
.
x
=
(
(
(
sin
.
x
)
*
(
arctan
.
x
)
)
/
(
(
cos
.
x
)
^2
)
)
+
(
1
/
(
(
cos
.
x
)
*
(
1
+
(
x
^2
)
)
)
)
) )
proof
end;
::f.x=sec.x*arccot.x
theorem
:: FDIFF_11:34
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
sec
(#)
arccot
)
&
Z
c=
].
(
-
1
)
,1
.[
holds
(
sec
(#)
arccot
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
sec
(#)
arccot
)
`|
Z
)
.
x
=
(
(
(
sin
.
x
)
*
(
arccot
.
x
)
)
/
(
(
cos
.
x
)
^2
)
)
-
(
1
/
(
(
cos
.
x
)
*
(
1
+
(
x
^2
)
)
)
)
) )
proof
end;
::f.x=cosec.x*arctan.x
theorem
:: FDIFF_11:35
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
cosec
(#)
arctan
)
&
Z
c=
].
(
-
1
)
,1
.[
holds
(
cosec
(#)
arctan
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
cosec
(#)
arctan
)
`|
Z
)
.
x
=
(
-
(
(
(
cos
.
x
)
*
(
arctan
.
x
)
)
/
(
(
sin
.
x
)
^2
)
)
)
+
(
1
/
(
(
sin
.
x
)
*
(
1
+
(
x
^2
)
)
)
)
) )
proof
end;
::f.x=cosec.x*arccot.x
theorem
:: FDIFF_11:36
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
cosec
(#)
arccot
)
&
Z
c=
].
(
-
1
)
,1
.[
holds
(
cosec
(#)
arccot
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
cosec
(#)
arccot
)
`|
Z
)
.
x
=
(
-
(
(
(
cos
.
x
)
*
(
arccot
.
x
)
)
/
(
(
sin
.
x
)
^2
)
)
)
-
(
1
/
(
(
sin
.
x
)
*
(
1
+
(
x
^2
)
)
)
)
) )
proof
end;
::f.x=arctan.x+arccot.x
theorem
Th37
:
:: FDIFF_11:37
for
Z
being
open
Subset
of
REAL
st
Z
c=
].
(
-
1
)
,1
.[
holds
(
arctan
+
arccot
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
arctan
+
arccot
)
`|
Z
)
.
x
=
0
) )
proof
end;
::f.x=arctan.x-arccot.x
theorem
Th38
:
:: FDIFF_11:38
for
Z
being
open
Subset
of
REAL
st
Z
c=
].
(
-
1
)
,1
.[
holds
(
arctan
-
arccot
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
arctan
-
arccot
)
`|
Z
)
.
x
=
2
/
(
1
+
(
x
^2
)
)
) )
proof
end;
::f.x=sin.x*(arctan.x+arccot.x)
theorem
:: FDIFF_11:39
for
Z
being
open
Subset
of
REAL
st
Z
c=
].
(
-
1
)
,1
.[
holds
(
sin
(#)
(
arctan
+
arccot
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
sin
(#)
(
arctan
+
arccot
)
)
`|
Z
)
.
x
=
(
cos
.
x
)
*
(
(
arctan
.
x
)
+
(
arccot
.
x
)
)
) )
proof
end;
::f.x=sin.x*(arctan.x-arccot.x)
theorem
:: FDIFF_11:40
for
Z
being
open
Subset
of
REAL
st
Z
c=
].
(
-
1
)
,1
.[
holds
(
sin
(#)
(
arctan
-
arccot
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
sin
(#)
(
arctan
-
arccot
)
)
`|
Z
)
.
x
=
(
(
cos
.
x
)
*
(
(
arctan
.
x
)
-
(
arccot
.
x
)
)
)
+
(
(
2
*
(
sin
.
x
)
)
/
(
1
+
(
x
^2
)
)
)
) )
proof
end;
::f.x=cos.x*(arctan.x+arccot.x)
theorem
:: FDIFF_11:41
for
Z
being
open
Subset
of
REAL
st
Z
c=
].
(
-
1
)
,1
.[
holds
(
cos
(#)
(
arctan
+
arccot
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
cos
(#)
(
arctan
+
arccot
)
)
`|
Z
)
.
x
=
-
(
(
sin
.
x
)
*
(
(
arctan
.
x
)
+
(
arccot
.
x
)
)
)
) )
proof
end;
::f.x=cos.x*(arctan.x-arccot.x)
theorem
:: FDIFF_11:42
for
Z
being
open
Subset
of
REAL
st
Z
c=
].
(
-
1
)
,1
.[
holds
(
cos
(#)
(
arctan
-
arccot
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
cos
(#)
(
arctan
-
arccot
)
)
`|
Z
)
.
x
=
(
-
(
(
sin
.
x
)
*
(
(
arctan
.
x
)
-
(
arccot
.
x
)
)
)
)
+
(
(
2
*
(
cos
.
x
)
)
/
(
1
+
(
x
^2
)
)
)
) )
proof
end;
::f.x=tan.x*(arctan.x+arccot.x)
theorem
:: FDIFF_11:43
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
tan
&
Z
c=
].
(
-
1
)
,1
.[
holds
(
tan
(#)
(
arctan
+
arccot
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
tan
(#)
(
arctan
+
arccot
)
)
`|
Z
)
.
x
=
(
(
arctan
.
x
)
+
(
arccot
.
x
)
)
/
(
(
cos
.
x
)
^2
)
) )
proof
end;
::f.x=tan.x*(arctan.x-arccot.x)
theorem
:: FDIFF_11:44
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
tan
&
Z
c=
].
(
-
1
)
,1
.[
holds
(
tan
(#)
(
arctan
-
arccot
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
tan
(#)
(
arctan
-
arccot
)
)
`|
Z
)
.
x
=
(
(
(
arctan
.
x
)
-
(
arccot
.
x
)
)
/
(
(
cos
.
x
)
^2
)
)
+
(
(
2
*
(
tan
.
x
)
)
/
(
1
+
(
x
^2
)
)
)
) )
proof
end;
::f.x=cot.x*(arctan.x+arccot.x)
theorem
:: FDIFF_11:45
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
cot
&
Z
c=
].
(
-
1
)
,1
.[
holds
(
cot
(#)
(
arctan
+
arccot
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
cot
(#)
(
arctan
+
arccot
)
)
`|
Z
)
.
x
=
-
(
(
(
arctan
.
x
)
+
(
arccot
.
x
)
)
/
(
(
sin
.
x
)
^2
)
)
) )
proof
end;
::f.x=cot.x*(arctan.x-arccot.x)
theorem
:: FDIFF_11:46
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
cot
&
Z
c=
].
(
-
1
)
,1
.[
holds
(
cot
(#)
(
arctan
-
arccot
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
cot
(#)
(
arctan
-
arccot
)
)
`|
Z
)
.
x
=
(
-
(
(
(
arctan
.
x
)
-
(
arccot
.
x
)
)
/
(
(
sin
.
x
)
^2
)
)
)
+
(
(
2
*
(
cot
.
x
)
)
/
(
1
+
(
x
^2
)
)
)
) )
proof
end;
::f.x=sec.x*(arctan.x+arccot.x)
theorem
:: FDIFF_11:47
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
sec
&
Z
c=
].
(
-
1
)
,1
.[
holds
(
sec
(#)
(
arctan
+
arccot
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
sec
(#)
(
arctan
+
arccot
)
)
`|
Z
)
.
x
=
(
(
(
arctan
.
x
)
+
(
arccot
.
x
)
)
*
(
sin
.
x
)
)
/
(
(
cos
.
x
)
^2
)
) )
proof
end;
::f.x=sec.x*(arctan.x-arccot.x)
theorem
:: FDIFF_11:48
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
sec
&
Z
c=
].
(
-
1
)
,1
.[
holds
(
sec
(#)
(
arctan
-
arccot
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
sec
(#)
(
arctan
-
arccot
)
)
`|
Z
)
.
x
=
(
(
(
(
arctan
.
x
)
-
(
arccot
.
x
)
)
*
(
sin
.
x
)
)
/
(
(
cos
.
x
)
^2
)
)
+
(
(
2
*
(
sec
.
x
)
)
/
(
1
+
(
x
^2
)
)
)
) )
proof
end;
::f.x=cosec.x*(arctan.x+arccot.x)
theorem
:: FDIFF_11:49
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
cosec
&
Z
c=
].
(
-
1
)
,1
.[
holds
(
cosec
(#)
(
arctan
+
arccot
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
cosec
(#)
(
arctan
+
arccot
)
)
`|
Z
)
.
x
=
-
(
(
(
(
arctan
.
x
)
+
(
arccot
.
x
)
)
*
(
cos
.
x
)
)
/
(
(
sin
.
x
)
^2
)
)
) )
proof
end;
::f.x=cosec.x*(arctan.x-arccot.x)
theorem
:: FDIFF_11:50
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
cosec
&
Z
c=
].
(
-
1
)
,1
.[
holds
(
cosec
(#)
(
arctan
-
arccot
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
cosec
(#)
(
arctan
-
arccot
)
)
`|
Z
)
.
x
=
(
-
(
(
(
(
arctan
.
x
)
-
(
arccot
.
x
)
)
*
(
cos
.
x
)
)
/
(
(
sin
.
x
)
^2
)
)
)
+
(
(
2
*
(
cosec
.
x
)
)
/
(
1
+
(
x
^2
)
)
)
) )
proof
end;
::f.x=exp_R.x*(arctan.x+arccot.x)
theorem
:: FDIFF_11:51
for
Z
being
open
Subset
of
REAL
st
Z
c=
].
(
-
1
)
,1
.[
holds
(
exp_R
(#)
(
arctan
+
arccot
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
exp_R
(#)
(
arctan
+
arccot
)
)
`|
Z
)
.
x
=
(
exp_R
.
x
)
*
(
(
arctan
.
x
)
+
(
arccot
.
x
)
)
) )
proof
end;
::f.x=exp_R.x*(arctan.x-arccot.x)
theorem
:: FDIFF_11:52
for
Z
being
open
Subset
of
REAL
st
Z
c=
].
(
-
1
)
,1
.[
holds
(
exp_R
(#)
(
arctan
-
arccot
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
exp_R
(#)
(
arctan
-
arccot
)
)
`|
Z
)
.
x
=
(
(
exp_R
.
x
)
*
(
(
arctan
.
x
)
-
(
arccot
.
x
)
)
)
+
(
(
2
*
(
exp_R
.
x
)
)
/
(
1
+
(
x
^2
)
)
)
) )
proof
end;
::f.x=(arctan.x+arccot.x)/exp_R.x
theorem
:: FDIFF_11:53
for
Z
being
open
Subset
of
REAL
st
Z
c=
].
(
-
1
)
,1
.[
holds
(
(
arctan
+
arccot
)
/
exp_R
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
(
arctan
+
arccot
)
/
exp_R
)
`|
Z
)
.
x
=
-
(
(
(
arctan
.
x
)
+
(
arccot
.
x
)
)
/
(
exp_R
.
x
)
)
) )
proof
end;
::f.x=(arctan.x-arccot.x)/exp_R.x
theorem
:: FDIFF_11:54
for
Z
being
open
Subset
of
REAL
st
Z
c=
].
(
-
1
)
,1
.[
holds
(
(
arctan
-
arccot
)
/
exp_R
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
(
arctan
-
arccot
)
/
exp_R
)
`|
Z
)
.
x
=
(
(
(
2
/
(
1
+
(
x
^2
)
)
)
-
(
arctan
.
x
)
)
+
(
arccot
.
x
)
)
/
(
exp_R
.
x
)
) )
proof
end;
::f.x=exp_R.(arctan.x+arccot.x)
theorem
:: FDIFF_11:55
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
exp_R
*
(
arctan
+
arccot
)
)
&
Z
c=
].
(
-
1
)
,1
.[
holds
(
exp_R
*
(
arctan
+
arccot
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
exp_R
*
(
arctan
+
arccot
)
)
`|
Z
)
.
x
=
0
) )
proof
end;
::f.x=exp_R.(arctan.x-arccot.x)
theorem
:: FDIFF_11:56
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
exp_R
*
(
arctan
-
arccot
)
)
&
Z
c=
].
(
-
1
)
,1
.[
holds
(
exp_R
*
(
arctan
-
arccot
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
exp_R
*
(
arctan
-
arccot
)
)
`|
Z
)
.
x
=
(
2
*
(
exp_R
.
(
(
arctan
.
x
)
-
(
arccot
.
x
)
)
)
)
/
(
1
+
(
x
^2
)
)
) )
proof
end;
::f.x=sin.(arctan.x+arccot.x)
theorem
:: FDIFF_11:57
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
sin
*
(
arctan
+
arccot
)
)
&
Z
c=
].
(
-
1
)
,1
.[
holds
(
sin
*
(
arctan
+
arccot
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
sin
*
(
arctan
+
arccot
)
)
`|
Z
)
.
x
=
0
) )
proof
end;
::f.x=sin.(arctan.x-arccot.x)
theorem
:: FDIFF_11:58
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
sin
*
(
arctan
-
arccot
)
)
&
Z
c=
].
(
-
1
)
,1
.[
holds
(
sin
*
(
arctan
-
arccot
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
sin
*
(
arctan
-
arccot
)
)
`|
Z
)
.
x
=
(
2
*
(
cos
.
(
(
arctan
.
x
)
-
(
arccot
.
x
)
)
)
)
/
(
1
+
(
x
^2
)
)
) )
proof
end;
::f.x=cos.(arctan.x+arccot.x)
theorem
:: FDIFF_11:59
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
cos
*
(
arctan
+
arccot
)
)
&
Z
c=
].
(
-
1
)
,1
.[
holds
(
cos
*
(
arctan
+
arccot
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
cos
*
(
arctan
+
arccot
)
)
`|
Z
)
.
x
=
0
) )
proof
end;
::f.x=cos.(arctan.x-arccot.x)
theorem
:: FDIFF_11:60
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
cos
*
(
arctan
-
arccot
)
)
&
Z
c=
].
(
-
1
)
,1
.[
holds
(
cos
*
(
arctan
-
arccot
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
cos
*
(
arctan
-
arccot
)
)
`|
Z
)
.
x
=
-
(
(
2
*
(
sin
.
(
(
arctan
.
x
)
-
(
arccot
.
x
)
)
)
)
/
(
1
+
(
x
^2
)
)
)
) )
proof
end;
::f.x=arctan.x*arccot.x
theorem
:: FDIFF_11:61
for
Z
being
open
Subset
of
REAL
st
Z
c=
].
(
-
1
)
,1
.[
holds
(
arctan
(#)
arccot
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
arctan
(#)
arccot
)
`|
Z
)
.
x
=
(
(
arccot
.
x
)
-
(
arctan
.
x
)
)
/
(
1
+
(
x
^2
)
)
) )
proof
end;
::f.x=arctan.(1/x)*arccot.(1/x)
theorem
:: FDIFF_11:62
for
Z
being
open
Subset
of
REAL
st not
0
in
Z
&
Z
c=
dom
(
(
arctan
*
(
(
id
Z
)
^
)
)
(#)
(
arccot
*
(
(
id
Z
)
^
)
)
)
& ( for
x
being
Real
st
x
in
Z
holds
(
(
(
id
Z
)
^
)
.
x
>
-
1 &
(
(
id
Z
)
^
)
.
x
<
1 ) ) holds
(
(
arctan
*
(
(
id
Z
)
^
)
)
(#)
(
arccot
*
(
(
id
Z
)
^
)
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
(
arctan
*
(
(
id
Z
)
^
)
)
(#)
(
arccot
*
(
(
id
Z
)
^
)
)
)
`|
Z
)
.
x
=
(
(
arctan
.
(
1
/
x
)
)
-
(
arccot
.
(
1
/
x
)
)
)
/
(
1
+
(
x
^2
)
)
) )
proof
end;
::f.x=x*arctan(1/x)
theorem
:: FDIFF_11:63
for
Z
being
open
Subset
of
REAL
st not
0
in
Z
&
Z
c=
dom
(
(
id
Z
)
(#)
(
arctan
*
(
(
id
Z
)
^
)
)
)
& ( for
x
being
Real
st
x
in
Z
holds
(
(
(
id
Z
)
^
)
.
x
>
-
1 &
(
(
id
Z
)
^
)
.
x
<
1 ) ) holds
(
(
id
Z
)
(#)
(
arctan
*
(
(
id
Z
)
^
)
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
(
id
Z
)
(#)
(
arctan
*
(
(
id
Z
)
^
)
)
)
`|
Z
)
.
x
=
(
arctan
.
(
1
/
x
)
)
-
(
x
/
(
1
+
(
x
^2
)
)
)
) )
proof
end;
::f.x=x*arccot(1/x)
theorem
:: FDIFF_11:64
for
Z
being
open
Subset
of
REAL
st not
0
in
Z
&
Z
c=
dom
(
(
id
Z
)
(#)
(
arccot
*
(
(
id
Z
)
^
)
)
)
& ( for
x
being
Real
st
x
in
Z
holds
(
(
(
id
Z
)
^
)
.
x
>
-
1 &
(
(
id
Z
)
^
)
.
x
<
1 ) ) holds
(
(
id
Z
)
(#)
(
arccot
*
(
(
id
Z
)
^
)
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
(
id
Z
)
(#)
(
arccot
*
(
(
id
Z
)
^
)
)
)
`|
Z
)
.
x
=
(
arccot
.
(
1
/
x
)
)
+
(
x
/
(
1
+
(
x
^2
)
)
)
) )
proof
end;
::f.x=x^2*arctan(1/x)
theorem
:: FDIFF_11:65
for
Z
being
open
Subset
of
REAL
for
g
being
PartFunc
of
REAL
,
REAL
st not
0
in
Z
&
Z
c=
dom
(
g
(#)
(
arctan
*
(
(
id
Z
)
^
)
)
)
&
g
=
#Z
2 & ( for
x
being
Real
st
x
in
Z
holds
(
(
(
id
Z
)
^
)
.
x
>
-
1 &
(
(
id
Z
)
^
)
.
x
<
1 ) ) holds
(
g
(#)
(
arctan
*
(
(
id
Z
)
^
)
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
g
(#)
(
arctan
*
(
(
id
Z
)
^
)
)
)
`|
Z
)
.
x
=
(
(
2
*
x
)
*
(
arctan
.
(
1
/
x
)
)
)
-
(
(
x
^2
)
/
(
1
+
(
x
^2
)
)
)
) )
proof
end;
::f.x=x^2*arccot(1/x)
theorem
:: FDIFF_11:66
for
Z
being
open
Subset
of
REAL
for
g
being
PartFunc
of
REAL
,
REAL
st not
0
in
Z
&
Z
c=
dom
(
g
(#)
(
arccot
*
(
(
id
Z
)
^
)
)
)
&
g
=
#Z
2 & ( for
x
being
Real
st
x
in
Z
holds
(
(
(
id
Z
)
^
)
.
x
>
-
1 &
(
(
id
Z
)
^
)
.
x
<
1 ) ) holds
(
g
(#)
(
arccot
*
(
(
id
Z
)
^
)
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
g
(#)
(
arccot
*
(
(
id
Z
)
^
)
)
)
`|
Z
)
.
x
=
(
(
2
*
x
)
*
(
arccot
.
(
1
/
x
)
)
)
+
(
(
x
^2
)
/
(
1
+
(
x
^2
)
)
)
) )
proof
end;
::f.x=1/arctan.x
theorem
Th67
:
:: FDIFF_11:67
for
Z
being
open
Subset
of
REAL
st
Z
c=
].
(
-
1
)
,1
.[
& ( for
x
being
Real
st
x
in
Z
holds
arctan
.
x
<>
0
) holds
(
arctan
^
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
arctan
^
)
`|
Z
)
.
x
=
-
(
1
/
(
(
(
arctan
.
x
)
^2
)
*
(
1
+
(
x
^2
)
)
)
)
) )
proof
end;
::f.x=1/arccot.x
theorem
Th68
:
:: FDIFF_11:68
for
Z
being
open
Subset
of
REAL
st
Z
c=
].
(
-
1
)
,1
.[
holds
(
arccot
^
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
arccot
^
)
`|
Z
)
.
x
=
1
/
(
(
(
arccot
.
x
)
^2
)
*
(
1
+
(
x
^2
)
)
)
) )
proof
end;
::f.x=1/(n*(arctan.x)|^n)
theorem
:: FDIFF_11:69
for
n
being
Element
of
NAT
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
(
1
/
n
)
(#)
(
(
#Z
n
)
*
(
arctan
^
)
)
)
&
Z
c=
].
(
-
1
)
,1
.[
&
n
>
0
& ( for
x
being
Real
st
x
in
Z
holds
arctan
.
x
<>
0
) holds
(
(
1
/
n
)
(#)
(
(
#Z
n
)
*
(
arctan
^
)
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
(
1
/
n
)
(#)
(
(
#Z
n
)
*
(
arctan
^
)
)
)
`|
Z
)
.
x
=
-
(
1
/
(
(
(
arctan
.
x
)
#Z
(
n
+
1
)
)
*
(
1
+
(
x
^2
)
)
)
)
) )
proof
end;
::f.x=1/(n*(arccot.x)|^n)
theorem
:: FDIFF_11:70
for
n
being
Element
of
NAT
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
(
1
/
n
)
(#)
(
(
#Z
n
)
*
(
arccot
^
)
)
)
&
Z
c=
].
(
-
1
)
,1
.[
&
n
>
0
holds
(
(
1
/
n
)
(#)
(
(
#Z
n
)
*
(
arccot
^
)
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
(
1
/
n
)
(#)
(
(
#Z
n
)
*
(
arccot
^
)
)
)
`|
Z
)
.
x
=
1
/
(
(
(
arccot
.
x
)
#Z
(
n
+
1
)
)
*
(
1
+
(
x
^2
)
)
)
) )
proof
end;
::f.x=2*(arctan #R (1/2))
theorem
:: FDIFF_11:71
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
2
(#)
(
(
#R
(
1
/
2
)
)
*
arctan
)
)
&
Z
c=
].
(
-
1
)
,1
.[
& ( for
x
being
Real
st
x
in
Z
holds
arctan
.
x
>
0
) holds
( 2
(#)
(
(
#R
(
1
/
2
)
)
*
arctan
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
2
(#)
(
(
#R
(
1
/
2
)
)
*
arctan
)
)
`|
Z
)
.
x
=
(
(
arctan
.
x
)
#R
(
-
(
1
/
2
)
)
)
/
(
1
+
(
x
^2
)
)
) )
proof
end;
::f.x=2*(arccot #R (1/2))
theorem
:: FDIFF_11:72
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
2
(#)
(
(
#R
(
1
/
2
)
)
*
arccot
)
)
&
Z
c=
].
(
-
1
)
,1
.[
holds
( 2
(#)
(
(
#R
(
1
/
2
)
)
*
arccot
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
2
(#)
(
(
#R
(
1
/
2
)
)
*
arccot
)
)
`|
Z
)
.
x
=
-
(
(
(
arccot
.
x
)
#R
(
-
(
1
/
2
)
)
)
/
(
1
+
(
x
^2
)
)
)
) )
proof
end;
::f.x=(2/3)*(arctan #R (3/2))
theorem
:: FDIFF_11:73
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
(
2
/
3
)
(#)
(
(
#R
(
3
/
2
)
)
*
arctan
)
)
&
Z
c=
].
(
-
1
)
,1
.[
& ( for
x
being
Real
st
x
in
Z
holds
arctan
.
x
>
0
) holds
(
(
2
/
3
)
(#)
(
(
#R
(
3
/
2
)
)
*
arctan
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
(
2
/
3
)
(#)
(
(
#R
(
3
/
2
)
)
*
arctan
)
)
`|
Z
)
.
x
=
(
(
arctan
.
x
)
#R
(
1
/
2
)
)
/
(
1
+
(
x
^2
)
)
) )
proof
end;
::f.x=(2/3)*(arccot #R (3/2))
theorem
:: FDIFF_11:74
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
(
2
/
3
)
(#)
(
(
#R
(
3
/
2
)
)
*
arccot
)
)
&
Z
c=
].
(
-
1
)
,1
.[
holds
(
(
2
/
3
)
(#)
(
(
#R
(
3
/
2
)
)
*
arccot
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
(
2
/
3
)
(#)
(
(
#R
(
3
/
2
)
)
*
arccot
)
)
`|
Z
)
.
x
=
-
(
(
(
arccot
.
x
)
#R
(
1
/
2
)
)
/
(
1
+
(
x
^2
)
)
)
) )
proof
end;