let Z be open Subset of REAL ; :: thesis: ( Z c= dom (arccot * ln ) & ( for x being Real st x in Z holds
( ln . x > - 1 & ln . x < 1 ) ) implies ( arccot * ln is_differentiable_on Z & ( for x being Real st x in Z holds
((arccot * ln ) `| Z) . x = - (1 / (x * (1 + ((ln . x) ^2 )))) ) ) )
assume that
A1: Z c= dom (arccot * ln ) and
A2: for x being Real st x in Z holds
( ln . x > - 1 & ln . x < 1 ) ; :: thesis: ( arccot * ln is_differentiable_on Z & ( for x being Real st x in Z holds
((arccot * ln ) `| Z) . x = - (1 / (x * (1 + ((ln . x) ^2 )))) ) )
A3: right_open_halfline 0 = { g where g is Real : 0 < g } by XXREAL_1:230;
dom (arccot * ln ) c= dom ln by RELAT_1:44;
then A4: Z c= dom ln by A1, XBOOLE_1:1;
A5: for x being Real st x in Z holds
x > 0

proof

let x be Real; :: thesis: ( x in Z implies x > 0 )
assume x in Z ; :: thesis: x > 0
then x in right_open_halfline 0 by A4, TAYLOR_1:18;
then ex g being Real st
( x = g & 0 < g ) by A3;
hence x > 0 ; :: thesis: verum

end;

A6: for x being Real st x in Z holds
arccot * ln is_differentiable_in x

proof

let x be Real; :: thesis: ( x in Z implies arccot * ln is_differentiable_in x )
assume A7: x in Z ; :: thesis: arccot * ln is_differentiable_in x
then x > 0 by A5;
then A8: ln is_differentiable_in x by TAYLOR_1:18;
( ln . x > - 1 & ln . x < 1 ) by A2, A7;
hence arccot * ln is_differentiable_in x by A8, Th84; :: thesis: verum

end;

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

proof

let x be Real; :: thesis: ( x in Z implies ((arccot * ln ) `| Z) . x = - (1 / (x * (1 + ((ln . x) ^2 )))) )
assume A9: x in Z ; :: thesis: ((arccot * ln ) `| Z) . x = - (1 / (x * (1 + ((ln . x) ^2 ))))
A10: x > 0 by A5, A9;
then A11: x in right_open_halfline 0 by A3;
A12: ln is_differentiable_in x by A10, TAYLOR_1:18;
A13: ( ln . x > - 1 & ln . x < 1 ) by A2, A9;
((arccot * ln ) `| Z) . x = diff (arccot * ln ),x by A8, A9, FDIFF_1:def 8
.= - ((diff ln ,x) / (1 + ((ln . x) ^2 ))) by A12, A13, Th84
.= - ((1 / x) / (1 + ((ln . x) ^2 ))) by A11, TAYLOR_1:18
.= - (1 / (x * (1 + ((ln . x) ^2 )))) by XCMPLX_1:79 ;
hence ((arccot * ln ) `| Z) . x = - (1 / (x * (1 + ((ln . x) ^2 )))) ; :: thesis: verum

end;

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