let Z be open Subset of REAL ; :: thesis: ( Z c= dom (2 (#) ((#R (1 / 2)) * arccot )) & Z c= ].(- 1),1.[ implies ( 2 (#) ((#R (1 / 2)) * arccot ) is_differentiable_on Z & ( for x being Real st x in Z holds
((2 (#) ((#R (1 / 2)) * arccot )) `| Z) . x = - (((arccot . x) #R (- (1 / 2))) / (1 + (x ^2 ))) ) ) )
assume that
A1: Z c= dom (2 (#) ((#R (1 / 2)) * arccot )) and
A2: Z c= ].(- 1),1.[ ; :: thesis: ( 2 (#) ((#R (1 / 2)) * arccot ) is_differentiable_on Z & ( for x being Real st x in Z holds
((2 (#) ((#R (1 / 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

proof

let x be Real; :: thesis: ( x in Z implies arccot . x > 0 )
assume A4: x in Z ; :: thesis: arccot . x > 0
assume A5: arccot . x <= 0 ; :: thesis: contradiction
].(- 1),1.[ c= [.(- 1),1.] by XXREAL_1:25;
then Z c= [.(- 1),1.] by A2, XBOOLE_1:1;
then x in [.(- 1),1.] by A4;
then arccot . x in arccot .: [.(- 1),1.] by SIN_COS9:24, FUNCT_1:def 12;
then arccot . x in [.(PI / 4),((3 / 4) * PI ).] by SIN_COS9:56, RELAT_1:148;
then A7: arccot . x >= PI / 4 by XXREAL_1:1;
(arccot . x) + 0 > (PI / 4) + (- (PI / 4)) by A7, XREAL_1:10;
hence contradiction by A5; :: thesis: verum

end;

A8: Z c= dom ((#R (1 / 2)) * arccot ) by A1, VALUED_1:def 5;
for x being Real st x in Z holds
(#R (1 / 2)) * arccot is_differentiable_in x

proof

let x be Real; :: thesis: ( x in Z implies (#R (1 / 2)) * arccot is_differentiable_in x )
assume A9: x in Z ; :: thesis: (#R (1 / 2)) * arccot is_differentiable_in x
arccot is_differentiable_on Z by A2, SIN_COS9:82;
then A10: arccot is_differentiable_in x by A9, FDIFF_1:16;
arccot . x > 0 by A3, A9;
hence (#R (1 / 2)) * arccot is_differentiable_in x by A10, TAYLOR_1:22; :: thesis: verum

end;

then A11: (#R (1 / 2)) * arccot is_differentiable_on Z by A8, FDIFF_1:16;
for x being Real st x in Z holds
((2 (#) ((#R (1 / 2)) * arccot )) `| Z) . x = - (((arccot . x) #R (- (1 / 2))) / (1 + (x ^2 )))

proof

let x be Real; :: thesis: ( x in Z implies ((2 (#) ((#R (1 / 2)) * arccot )) `| Z) . x = - (((arccot . x) #R (- (1 / 2))) / (1 + (x ^2 ))) )
assume A13: x in Z ; :: thesis: ((2 (#) ((#R (1 / 2)) * arccot )) `| Z) . x = - (((arccot . x) #R (- (1 / 2))) / (1 + (x ^2 )))
A14: arccot is_differentiable_on Z by A2, SIN_COS9:82;
then A15: arccot is_differentiable_in x by A13, FDIFF_1:16;
A16: arccot . x > 0 by A3, A13;
((2 (#) ((#R (1 / 2)) * arccot )) `| Z) . x = 2 * (diff ((#R (1 / 2)) * arccot ),x) by A1, A11, A13, FDIFF_1:28
.= 2 * (((1 / 2) * ((arccot . x) #R ((1 / 2) - 1))) * (diff arccot ,x)) by A15, A16, TAYLOR_1:22
.= 2 * (((1 / 2) * ((arccot . x) #R ((1 / 2) - 1))) * ((arccot `| Z) . x)) by A13, A14, FDIFF_1:def 8
.= 2 * (((1 / 2) * ((arccot . x) #R ((1 / 2) - 1))) * (- (1 / (1 + (x ^2 ))))) by A2, A13, SIN_COS9:82
.= - (((arccot . x) #R (- (1 / 2))) / (1 + (x ^2 ))) ;
hence ((2 (#) ((#R (1 / 2)) * arccot )) `| Z) . x = - (((arccot . x) #R (- (1 / 2))) / (1 + (x ^2 ))) ; :: thesis: verum

end;

hence ( 2 (#) ((#R (1 / 2)) * arccot ) is_differentiable_on Z & ( for x being Real st x in Z holds
((2 (#) ((#R (1 / 2)) * arccot )) `| Z) . x = - (((arccot . x) #R (- (1 / 2))) / (1 + (x ^2 ))) ) ) by A1, A11, FDIFF_1:28; :: thesis: verum