let Z be open Subset of REAL; ( Z c= dom (exp_R * arccot) & Z c= ].(- 1),1.[ implies ( - (exp_R * arccot) is_differentiable_on Z & ( for x being Real st x in Z holds
((- (exp_R * arccot)) `| Z) . x = (exp_R . (arccot . x)) / (1 + (x ^2)) ) ) )
assume A1:
( Z c= dom (exp_R * arccot) & Z c= ].(- 1),1.[ )
; ( - (exp_R * arccot) is_differentiable_on Z & ( for x being Real st x in Z holds
((- (exp_R * arccot)) `| Z) . x = (exp_R . (arccot . x)) / (1 + (x ^2)) ) )
then A2:
Z c= dom (- (exp_R * arccot))
by VALUED_1:8;
A3:
exp_R * arccot is_differentiable_on Z
by A1, SIN_COS9:120;
then A4:
(- 1) (#) (exp_R * arccot) is_differentiable_on Z
by A2, FDIFF_1:20;
for x being Real st x in Z holds
((- (exp_R * arccot)) `| Z) . x = (exp_R . (arccot . x)) / (1 + (x ^2))
proof
let x be
Real;
( x in Z implies ((- (exp_R * arccot)) `| Z) . x = (exp_R . (arccot . x)) / (1 + (x ^2)) )
assume A5:
x in Z
;
((- (exp_R * arccot)) `| Z) . x = (exp_R . (arccot . x)) / (1 + (x ^2))
A6:
arccot is_differentiable_on Z
by A1, SIN_COS9:82;
then A7:
arccot is_differentiable_in x
by A5, FDIFF_1:9;
A8:
exp_R is_differentiable_in arccot . x
by SIN_COS:65;
A9:
exp_R * arccot is_differentiable_in x
by A3, A5, FDIFF_1:9;
((- (exp_R * arccot)) `| Z) . x =
diff (
(- (exp_R * arccot)),
x)
by A4, A5, FDIFF_1:def 7
.=
(- 1) * (diff ((exp_R * arccot),x))
by A9, FDIFF_1:15
.=
(- 1) * ((diff (exp_R,(arccot . x))) * (diff (arccot,x)))
by A7, A8, FDIFF_2:13
.=
(- 1) * ((diff (exp_R,(arccot . x))) * ((arccot `| Z) . x))
by A5, A6, FDIFF_1:def 7
.=
(- 1) * ((diff (exp_R,(arccot . x))) * (- (1 / (1 + (x ^2)))))
by A5, A1, SIN_COS9:82
.=
(- 1) * (- ((diff (exp_R,(arccot . x))) * (1 / (1 + (x ^2)))))
.=
(exp_R . (arccot . x)) / (1 + (x ^2))
by SIN_COS:65
;
hence
((- (exp_R * arccot)) `| Z) . x = (exp_R . (arccot . x)) / (1 + (x ^2))
;
verum
end;
hence
( - (exp_R * arccot) is_differentiable_on Z & ( for x being Real st x in Z holds
((- (exp_R * arccot)) `| Z) . x = (exp_R . (arccot . x)) / (1 + (x ^2)) ) )
by A2, A3, FDIFF_1:20; verum