let Z be open Subset of REAL; ( Z c= ].(- 1),1.[ implies ( arccot ^ is_differentiable_on Z & ( for x being Real st x in Z holds
((arccot ^) `| Z) . x = 1 / (((arccot . x) ^2) * (1 + (x ^2))) ) ) )
assume A1:
Z c= ].(- 1),1.[
; ( arccot ^ is_differentiable_on Z & ( for x being Real st x in Z holds
((arccot ^) `| Z) . x = 1 / (((arccot . x) ^2) * (1 + (x ^2))) ) )
then A2:
arccot is_differentiable_on Z
by SIN_COS9:82;
A3:
for x being Real st x in Z holds
arccot . x <> 0
proof
PI in ].0,4.[
by SIN_COS:def 28;
then
PI > 0
by XXREAL_1:4;
then A4:
PI / 4
> 0 / 4
by XREAL_1:74;
let x be
Real;
( x in Z implies arccot . x <> 0 )
assume A5:
x in Z
;
arccot . x <> 0
assume A6:
arccot . x = 0
;
contradiction
].(- 1),1.[ c= [.(- 1),1.]
by XXREAL_1:25;
then
Z c= [.(- 1),1.]
by A1, XBOOLE_1:1;
then
x in [.(- 1),1.]
by A5;
then
0 in arccot .: [.(- 1),1.]
by A6, FUNCT_1:def 6, SIN_COS9:24;
then
0 in [.(PI / 4),((3 / 4) * PI).]
by RELAT_1:115, SIN_COS9:56;
hence
contradiction
by A4, XXREAL_1:1;
verum
end;
then A7:
arccot ^ is_differentiable_on Z
by A2, FDIFF_2:22;
for x being Real st x in Z holds
((arccot ^) `| Z) . x = 1 / (((arccot . x) ^2) * (1 + (x ^2)))
proof
let x be
Real;
( x in Z implies ((arccot ^) `| Z) . x = 1 / (((arccot . x) ^2) * (1 + (x ^2))) )
assume A8:
x in Z
;
((arccot ^) `| Z) . x = 1 / (((arccot . x) ^2) * (1 + (x ^2)))
then A9:
(
arccot . x <> 0 &
arccot is_differentiable_in x )
by A3, A2, FDIFF_1:9;
((arccot ^) `| Z) . x =
diff (
(arccot ^),
x)
by A7, A8, FDIFF_1:def 7
.=
- ((diff (arccot,x)) / ((arccot . x) ^2))
by A9, FDIFF_2:15
.=
- (((arccot `| Z) . x) / ((arccot . x) ^2))
by A2, A8, FDIFF_1:def 7
.=
- ((- (1 / (1 + (x ^2)))) / ((arccot . x) ^2))
by A1, A8, SIN_COS9:82
.=
(1 / (1 + (x ^2))) / ((arccot . x) ^2)
.=
1
/ (((arccot . x) ^2) * (1 + (x ^2)))
by XCMPLX_1:78
;
hence
((arccot ^) `| Z) . x = 1
/ (((arccot . x) ^2) * (1 + (x ^2)))
;
verum
end;
hence
( arccot ^ is_differentiable_on Z & ( for x being Real st x in Z holds
((arccot ^) `| Z) . x = 1 / (((arccot . x) ^2) * (1 + (x ^2))) ) )
by A3, A2, FDIFF_2:22; verum