let Z be open Subset of REAL; :: thesis: ( Z c= ].(- 1),1.[ implies ( arccot ^ is_differentiable_on Z & ( for x being Real st x in Z holds
((arccot ^) `| Z) . x = 1 / (((arccot . x) ^2) * (1 + (x ^2))) ) ) )
assume A1: Z c= ].(- 1),1.[ ; :: thesis: ( arccot ^ is_differentiable_on Z & ( for x being Real st x in Z holds
((arccot ^) `| Z) . x = 1 / (((arccot . x) ^2) * (1 + (x ^2))) ) )
then A2: arccot is_differentiable_on Z by SIN_COS9:82;
A3: for x being Real st x in Z holds
arccot . x <> 0
proof
PI in ].0,4.[ by SIN_COS:def 28;
then PI > 0 by XXREAL_1:4;
then A4: PI / 4 > 0 / 4 by XREAL_1:74;
let x be Real; :: thesis: ( x in Z implies arccot . x <> 0 )
assume A5: x in Z ; :: thesis: arccot . x <> 0
assume A6: arccot . x = 0 ; :: thesis: contradiction
].(- 1),1.[ c= [.(- 1),1.] by XXREAL_1:25;
then Z c= [.(- 1),1.] by A1, XBOOLE_1:1;
then x in [.(- 1),1.] by A5;
then 0 in arccot .: [.(- 1),1.] by A6, FUNCT_1:def 6, SIN_COS9:24;
then 0 in [.(PI / 4),((3 / 4) * PI).] by RELAT_1:115, SIN_COS9:56;
hence contradiction by A4, XXREAL_1:1; :: thesis: verum
end;
then A7: arccot ^ is_differentiable_on Z by A2, FDIFF_2:22;
for x being Real st x in Z holds
((arccot ^) `| Z) . x = 1 / (((arccot . x) ^2) * (1 + (x ^2)))
proof
let x be Real; :: thesis: ( x in Z implies ((arccot ^) `| Z) . x = 1 / (((arccot . x) ^2) * (1 + (x ^2))) )
assume A8: x in Z ; :: thesis: ((arccot ^) `| Z) . x = 1 / (((arccot . x) ^2) * (1 + (x ^2)))
then A9: ( arccot . x <> 0 & arccot is_differentiable_in x ) by A3, A2, FDIFF_1:9;
((arccot ^) `| Z) . x = diff ((arccot ^),x) by A7, A8, FDIFF_1:def 7
.= - ((diff (arccot,x)) / ((arccot . x) ^2)) by A9, FDIFF_2:15
.= - (((arccot `| Z) . x) / ((arccot . x) ^2)) by A2, A8, FDIFF_1:def 7
.= - ((- (1 / (1 + (x ^2)))) / ((arccot . x) ^2)) by A1, A8, SIN_COS9:82
.= (1 / (1 + (x ^2))) / ((arccot . x) ^2)
.= 1 / (((arccot . x) ^2) * (1 + (x ^2))) by XCMPLX_1:78 ;
hence ((arccot ^) `| Z) . x = 1 / (((arccot . x) ^2) * (1 + (x ^2))) ; :: thesis: verum
end;
hence ( arccot ^ is_differentiable_on Z & ( for x being Real st x in Z holds
((arccot ^) `| Z) . x = 1 / (((arccot . x) ^2) * (1 + (x ^2))) ) ) by A3, A2, FDIFF_2:22; :: thesis: verum