let Z be open Subset of REAL; ( not 0 in Z & Z c= dom (((id Z) ^) (#) arccot) & Z c= ].(- 1),1.[ implies ( ((id Z) ^) (#) arccot is_differentiable_on Z & ( for x being Real st x in Z holds
((((id Z) ^) (#) arccot) `| Z) . x = (- ((arccot . x) / (x ^2))) - (1 / (x * (1 + (x ^2)))) ) ) )
set f = id Z;
assume that
A1:
not 0 in Z
and
A2:
Z c= dom (((id Z) ^) (#) arccot)
and
A3:
Z c= ].(- 1),1.[
; ( ((id Z) ^) (#) arccot is_differentiable_on Z & ( for x being Real st x in Z holds
((((id Z) ^) (#) arccot) `| Z) . x = (- ((arccot . x) / (x ^2))) - (1 / (x * (1 + (x ^2)))) ) )
A4:
(id Z) ^ is_differentiable_on Z
by A1, FDIFF_5:4;
A5:
arccot is_differentiable_on Z
by A3, Th82;
Z c= (dom ((id Z) ^)) /\ (dom arccot)
by A2, VALUED_1:def 4;
then A6:
Z c= dom ((id Z) ^)
by XBOOLE_1:18;
for x being Real st x in Z holds
((((id Z) ^) (#) arccot) `| Z) . x = (- ((arccot . x) / (x ^2))) - (1 / (x * (1 + (x ^2))))
proof
let x be
Real;
( x in Z implies ((((id Z) ^) (#) arccot) `| Z) . x = (- ((arccot . x) / (x ^2))) - (1 / (x * (1 + (x ^2)))) )
assume A7:
x in Z
;
((((id Z) ^) (#) arccot) `| Z) . x = (- ((arccot . x) / (x ^2))) - (1 / (x * (1 + (x ^2))))
then ((((id Z) ^) (#) arccot) `| Z) . x =
((arccot . x) * (diff (((id Z) ^),x))) + ((((id Z) ^) . x) * (diff (arccot,x)))
by A2, A4, A5, FDIFF_1:21
.=
((arccot . x) * ((((id Z) ^) `| Z) . x)) + ((((id Z) ^) . x) * (diff (arccot,x)))
by A4, A7, FDIFF_1:def 7
.=
((arccot . x) * (- (1 / (x ^2)))) + ((((id Z) ^) . x) * (diff (arccot,x)))
by A1, A7, FDIFF_5:4
.=
(- ((arccot . x) * (1 / (x ^2)))) + ((((id Z) ^) . x) * ((arccot `| Z) . x))
by A5, A7, FDIFF_1:def 7
.=
(- ((arccot . x) * (1 / (x ^2)))) + ((((id Z) ^) . x) * (- (1 / (1 + (x ^2)))))
by A3, A7, Th82
.=
(- (((arccot . x) * 1) / (x ^2))) - ((((id Z) ^) . x) * (1 / (1 + (x ^2))))
.=
(- ((arccot . x) / (x ^2))) - ((((id Z) . x) ") * (1 / (1 + (x ^2))))
by A6, A7, RFUNCT_1:def 2
.=
(- ((arccot . x) / (x ^2))) - ((1 / x) * (1 / (1 + (x ^2))))
by A7, FUNCT_1:18
.=
(- ((arccot . x) / (x ^2))) - ((1 * 1) / (x * (1 + (x ^2))))
by XCMPLX_1:76
.=
(- ((arccot . x) / (x ^2))) - (1 / (x * (1 + (x ^2))))
;
hence
((((id Z) ^) (#) arccot) `| Z) . x = (- ((arccot . x) / (x ^2))) - (1 / (x * (1 + (x ^2))))
;
verum
end;
hence
( ((id Z) ^) (#) arccot is_differentiable_on Z & ( for x being Real st x in Z holds
((((id Z) ^) (#) arccot) `| Z) . x = (- ((arccot . x) / (x ^2))) - (1 / (x * (1 + (x ^2)))) ) )
by A2, A4, A5, FDIFF_1:21; verum