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 )
].(- 1),1.[ c= [.(- 1),1.] by XXREAL_1:25;
then A4: Z c= [.(- 1),1.] by A2, XBOOLE_1:1;
assume x in Z ; :: thesis: arccot . x > 0
then x in [.(- 1),1.] by A4;
then arccot . x in arccot .: [.(- 1),1.] by FUNCT_1:def 6, SIN_COS9:24;
then arccot . x in [.(PI / 4),((3 / 4) * PI).] by RELAT_1:115, SIN_COS9:56;
then arccot . x >= PI / 4 by XXREAL_1:1;
then A5: (arccot . x) + 0 > (PI / 4) + (- (PI / 4)) by XREAL_1:8;
assume arccot . x <= 0 ; :: thesis: contradiction
hence contradiction by A5; :: thesis: verum
end;
A6: 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 A7: x in Z ; :: thesis: (#R (1 / 2)) * arccot is_differentiable_in x
then A8: arccot . x > 0 by A3;
arccot is_differentiable_on Z by A2, SIN_COS9:82;
then arccot is_differentiable_in x by A7, FDIFF_1:9;
hence (#R (1 / 2)) * arccot is_differentiable_in x by A8, TAYLOR_1:22; :: thesis: verum
end;
Z c= dom ((#R (1 / 2)) * arccot) by A1, VALUED_1:def 5;
then A9: (#R (1 / 2)) * arccot is_differentiable_on Z by A6, FDIFF_1:9;
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 A10: x in Z ; :: thesis: ((2 (#) ((#R (1 / 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 (#) ((#R (1 / 2)) * arccot)) `| Z) . x = 2 * (diff (((#R (1 / 2)) * arccot),x)) by A1, A9, A10, FDIFF_1:20
.= 2 * (((1 / 2) * ((arccot . x) #R ((1 / 2) - 1))) * (diff (arccot,x))) by A13, A11, TAYLOR_1:22
.= 2 * (((1 / 2) * ((arccot . x) #R ((1 / 2) - 1))) * ((arccot `| Z) . x)) by A10, A12, FDIFF_1:def 7
.= 2 * (((1 / 2) * ((arccot . x) #R ((1 / 2) - 1))) * (- (1 / (1 + (x ^2))))) by A2, A10, 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, A9, FDIFF_1:20; :: thesis: verum