let r be Real; :: thesis: ( - 1 <= r & r <= 1 implies diff arccot ,r = - (1 / (1 + (r ^2 ))) )
set X = cot .: ].0 ,PI .[;
set g = arccot ;
set f = cot | ].0 ,PI .[;
set x = arccot . r;
assume that
A1: - 1 <= r and
A2: r <= 1 ; :: thesis: diff arccot ,r = - (1 / (1 + (r ^2 )))
A3: ((sin . (arccot . r)) ^2 ) + ((cos . (arccot . r)) ^2 ) = 1 by SIN_COS:31;
A4: cot | ].0 ,PI .[ is_differentiable_on ].0 ,PI .[ by Lm2, FDIFF_2:16;

A5: now

A6: 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 (sin . x0) ^2 > 0 by SQUARE_1:74;
then 1 / ((sin . x0) ^2 ) > 0 / ((sin . x0) ^2 ) by XREAL_1:76;
then - (1 / ((sin . x0) ^2 )) < - 0 by XREAL_1:26;
hence - (1 / ((sin . x0) ^2 )) < 0 ; :: thesis: verum

end;

let x0 be Real; :: thesis: ( x0 in ].0 ,PI .[ implies diff (cot | ].0 ,PI .[),x0 < 0 )
assume A7: x0 in ].0 ,PI .[ ; :: thesis: diff (cot | ].0 ,PI .[),x0 < 0
diff (cot | ].0 ,PI .[),x0 = ((cot | ].0 ,PI .[) `| ].0 ,PI .[) . x0 by A4, A7, FDIFF_1:def 8
.= (cot `| ].0 ,PI .[) . x0 by Lm2, FDIFF_2:16
.= diff cot ,x0 by A7, Lm2, FDIFF_1:def 8
.= - (1 / ((sin . x0) ^2 )) by A7, Lm4 ;
hence diff (cot | ].0 ,PI .[),x0 < 0 by A7, A6; :: thesis: verum

end;

A8: r in [.(- 1),1.] by A1, A2, XXREAL_1:1;
then A9: arccot . r in [.(PI / 4),((3 / 4) * PI ).] by Th50;
arccot . r = arccot r ;
then A10: r = cot (arccot . r) by A1, A2, Th52
.= (cos (arccot . r)) / (sin (arccot . r)) by SIN_COS4:def 2 ;
dom (cot | ].0 ,PI .[) = (dom cot ) /\ ].0 ,PI .[ by RELAT_1:90;
then A11: ].0 ,PI .[ c= dom (cot | ].0 ,PI .[) by Th2, XBOOLE_1:19;
A12: (cot | ].0 ,PI .[) | ].0 ,PI .[ = cot | ].0 ,PI .[ by RELAT_1:101;
A13: [.(PI / 4),((3 / 4) * PI ).] c= ].0 ,PI .[ by Lm9, Lm10, XXREAL_2:def 12;
then sin (arccot . r) <> 0 by A9, COMPTRIG:23;
then r * (sin (arccot . r)) = cos (arccot . r) by A10, XCMPLX_1:88;
then A14: 1 = ((sin (arccot . r)) ^2 ) * ((r ^2 ) + 1) by A3;
cot | ].0 ,PI .[ is_differentiable_on ].0 ,PI .[ by Lm2, FDIFF_2:16;
then diff (cot | ].0 ,PI .[),(arccot . r) = ((cot | ].0 ,PI .[) `| ].0 ,PI .[) . (arccot . r) by A9, A13, FDIFF_1:def 8
.= (cot `| ].0 ,PI .[) . (arccot . r) by Lm2, FDIFF_2:16
.= diff cot ,(arccot . r) by A9, A13, Lm2, FDIFF_1:def 8
.= - (1 / ((sin (arccot . r)) ^2 )) by A9, A13, Lm4 ;
then diff arccot ,r = 1 / (- (1 / ((sin (arccot . r)) ^2 ))) by A8, A4, A5, A12, A11, Th24, FDIFF_2:48
.= - (1 / (1 / ((sin (arccot . r)) ^2 ))) by XCMPLX_1:189
.= - (1 / ((r ^2 ) + 1)) by A14, XCMPLX_1:74 ;
hence diff arccot ,r = - (1 / (1 + (r ^2 ))) ; :: thesis: verum