let Z be open Subset of REAL; ( Z c= dom (cos (#) arccot) & Z c= ].(- 1),1.[ implies ( 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))) ) ) )
assume that
A1:
Z c= dom (cos (#) arccot)
and
A2:
Z c= ].(- 1),1.[
; ( 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))) ) )
A3:
arccot is_differentiable_on Z
by A2, SIN_COS9:82;
A4:
for x being Real st x in Z holds
cos is_differentiable_in x
by SIN_COS:63;
Z c= (dom cos) /\ (dom arccot)
by A1, VALUED_1:def 4;
then
Z c= dom cos
by XBOOLE_1:18;
then A5:
cos is_differentiable_on Z
by A4, FDIFF_1:9;
for x being Real st x in Z holds
((cos (#) arccot) `| Z) . x = (- ((sin . x) * (arccot . x))) - ((cos . x) / (1 + (x ^2)))
proof
let x be
Real;
( x in Z implies ((cos (#) arccot) `| Z) . x = (- ((sin . x) * (arccot . x))) - ((cos . x) / (1 + (x ^2))) )
assume A6:
x in Z
;
((cos (#) arccot) `| Z) . x = (- ((sin . x) * (arccot . x))) - ((cos . x) / (1 + (x ^2)))
then ((cos (#) arccot) `| Z) . x =
((arccot . x) * (diff (cos,x))) + ((cos . x) * (diff (arccot,x)))
by A1, A5, A3, FDIFF_1:21
.=
((arccot . x) * (- (sin . x))) + ((cos . x) * (diff (arccot,x)))
by SIN_COS:63
.=
(- ((sin . x) * (arccot . x))) + ((cos . x) * ((arccot `| Z) . x))
by A3, A6, FDIFF_1:def 7
.=
(- ((sin . x) * (arccot . x))) + ((cos . x) * (- (1 / (1 + (x ^2)))))
by A2, A6, SIN_COS9:82
.=
(- ((sin . x) * (arccot . x))) - ((cos . x) / (1 + (x ^2)))
;
hence
((cos (#) arccot) `| Z) . x = (- ((sin . x) * (arccot . x))) - ((cos . x) / (1 + (x ^2)))
;
verum
end;
hence
( 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))) ) )
by A1, A5, A3, FDIFF_1:21; verum