let Z be open Subset of REAL; ( Z c= dom ((2 / 3) (#) ((#R (3 / 2)) * arccot)) & Z c= ].(- 1),1.[ implies ( (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))) ) ) )
assume that
A1:
Z c= dom ((2 / 3) (#) ((#R (3 / 2)) * arccot))
and
A2:
Z c= ].(- 1),1.[
; ( (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))) ) )
A3:
for x being Real st x in Z holds
arccot . x > 0
A6:
for x being Real st x in Z holds
(#R (3 / 2)) * arccot is_differentiable_in x
Z c= dom ((#R (3 / 2)) * arccot)
by A1, VALUED_1:def 5;
then A9:
(#R (3 / 2)) * arccot is_differentiable_on Z
by A6, FDIFF_1:9;
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
let x be
Real;
( x in Z implies (((2 / 3) (#) ((#R (3 / 2)) * arccot)) `| Z) . x = - (((arccot . x) #R (1 / 2)) / (1 + (x ^2))) )
assume A10:
x in Z
;
(((2 / 3) (#) ((#R (3 / 2)) * arccot)) `| Z) . x = - (((arccot . x) #R (1 / 2)) / (1 + (x ^2)))
then A11:
arccot . x > 0
by A3;
A12:
arccot is_differentiable_on Z
by A2, SIN_COS9:82;
then A13:
arccot is_differentiable_in x
by A10, FDIFF_1:9;
(((2 / 3) (#) ((#R (3 / 2)) * arccot)) `| Z) . x =
(2 / 3) * (diff (((#R (3 / 2)) * arccot),x))
by A1, A9, A10, FDIFF_1:20
.=
(2 / 3) * (((3 / 2) * ((arccot . x) #R ((3 / 2) - 1))) * (diff (arccot,x)))
by A13, A11, TAYLOR_1:22
.=
(2 / 3) * (((3 / 2) * ((arccot . x) #R ((3 / 2) - 1))) * ((arccot `| Z) . x))
by A10, A12, FDIFF_1:def 7
.=
(2 / 3) * (((3 / 2) * ((arccot . x) #R ((3 / 2) - 1))) * (- (1 / (1 + (x ^2)))))
by A2, A10, SIN_COS9:82
.=
- (((arccot . x) #R (1 / 2)) / (1 + (x ^2)))
;
hence
(((2 / 3) (#) ((#R (3 / 2)) * arccot)) `| Z) . x = - (((arccot . x) #R (1 / 2)) / (1 + (x ^2)))
;
verum
end;
hence
( (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))) ) )
by A1, A9, FDIFF_1:20; verum