let r be Real; :: thesis: ( - 1 <= r & r <= 1 implies diff arccot ,r = - (1 / (1 + (r ^2 ))) )
set f = cot | ].0 ,PI .[;
set g = arccot ;
set x = arccot . r;
set X = cot .: ].0 ,PI .[;
assume A1: ( - 1 <= r & r <= 1 ) ; :: thesis: diff arccot ,r = - (1 / (1 + (r ^2 )))
then A2: r in [.(- 1),1.] by XXREAL_1:1;
then A3: arccot . r in [.(PI / 4),((3 / 4) * PI ).] by Th48;
A4: [.(PI / 4),((3 / 4) * PI ).] c= ].0 ,PI .[ by Lm9, Lm10, XXREAL_2:def 12;
A5: cot | ].0 ,PI .[ is_differentiable_on ].0 ,PI .[ by Lm2, FDIFF_2:16;
A6: diff (cot | ].0 ,PI .[),(arccot . r) = ((cot | ].0 ,PI .[) `| ].0 ,PI .[) . (arccot . r) by A3, A4, A5, FDIFF_1:def 8
.= (cot `| ].0 ,PI .[) . (arccot . r) by Lm2, FDIFF_2:16
.= diff cot ,(arccot . r) by A3, A4, Lm2, FDIFF_1:def 8
.= - (1 / ((sin (arccot . r)) ^2 )) by A3, A4, Lm4 ;
A7: sin (arccot . r) <> 0 by A3, A4, COMPTRIG:23;
B8: ((sin . (arccot . r)) ^2 ) + ((cos . (arccot . r)) ^2 ) = 1 by SIN_COS:31;
arccot . r = arccot r ;
then r = cot (arccot . r) by A1, Th50
.= (cos (arccot . r)) / (sin (arccot . r)) by SIN_COS4:def 2 ;
then r * (sin (arccot . r)) = cos (arccot . r) by A7, XCMPLX_1:88;
then A9: 1 = ((sin (arccot . r)) ^2 ) * ((r ^2 ) + 1) by B8;
A13: cot | ].0 ,PI .[ is_differentiable_on ].0 ,PI .[ by Lm2, FDIFF_2:16;

A14: now

let x0 be Real; :: thesis: ( x0 in ].0 ,PI .[ implies diff (cot | ].0 ,PI .[),x0 < 0 )
assume A15: x0 in ].0 ,PI .[ ; :: thesis: diff (cot | ].0 ,PI .[),x0 < 0
A16: diff (cot | ].0 ,PI .[),x0 = ((cot | ].0 ,PI .[) `| ].0 ,PI .[) . x0 by A13, A15, FDIFF_1:def 8
.= (cot `| ].0 ,PI .[) . x0 by Lm2, FDIFF_2:16
.= diff cot ,x0 by A15, Lm2, FDIFF_1:def 8
.= - (1 / ((sin . x0) ^2 )) by A15, Lm4 ;
for x0 being Real st x0 in ].0 ,PI .[ holds
- (1 / ((sin . x0) ^2 )) < 0

proof

let x0 be Real; :: thesis: ( x0 in ].0 ,PI .[ implies - (1 / ((sin . x0) ^2 )) < 0 )
assume x0 in ].0 ,PI .[ ; :: thesis: - (1 / ((sin . x0) ^2 )) < 0
then 0 < sin . x0 by COMPTRIG:23;
then A17: (sin . x0) ^2 > 0 by SQUARE_1:74;
1 / ((sin . x0) ^2 ) > 0 / ((sin . x0) ^2 ) by A17, XREAL_1:76;
then - (1 / ((sin . x0) ^2 )) < - 0 by XREAL_1:26;
hence - (1 / ((sin . x0) ^2 )) < 0 ; :: thesis: verum

end;

hence diff (cot | ].0 ,PI .[),x0 < 0 by A15, A16; :: thesis: verum

end;

A18: (cot | ].0 ,PI .[) | ].0 ,PI .[ = cot | ].0 ,PI .[ by RELAT_1:101;
dom (cot | ].0 ,PI .[) = (dom cot ) /\ ].0 ,PI .[ by RELAT_1:90;
then ].0 ,PI .[ c= dom (cot | ].0 ,PI .[) by Th2, XBOOLE_1:19;
then diff arccot ,r = 1 / (- (1 / ((sin (arccot . r)) ^2 ))) by A2, A6, A13, A14, A18, Th22, FDIFF_2:48
.= - (1 / (1 / ((sin (arccot . r)) ^2 ))) by XCMPLX_1:189
.= - (1 / ((r ^2 ) + 1)) by A9, XCMPLX_1:74 ;
hence diff arccot ,r = - (1 / (1 + (r ^2 ))) ; :: thesis: verum