let r be Real; ( - 1 <= r & r <= 1 implies diff (arccot,r) = - (1 / (1 + (r ^2))) )
set g = arccot ;
set f = cot | ].0,PI.[;
set x = arccot . r;
assume that
A1:
- 1 <= r
and
A2:
r <= 1
; diff (arccot,r) = - (1 / (1 + (r ^2)))
A3:
((sin . (arccot . r)) ^2) + ((cos . (arccot . r)) ^2) = 1
by SIN_COS:28;
A4:
cot | ].0,PI.[ is_differentiable_on ].0,PI.[
by Lm2, FDIFF_2:16;
A5:
now for x0 being Real st x0 in ].0,PI.[ holds
diff ((cot | ].0,PI.[),x0) < 0 A6:
for
x0 being
Real st
x0 in ].0,PI.[ holds
- (1 / ((sin . x0) ^2)) < 0
let x0 be
Real;
( x0 in ].0,PI.[ implies diff ((cot | ].0,PI.[),x0) < 0 )assume A7:
x0 in ].0,PI.[
;
diff ((cot | ].0,PI.[),x0) < 0 diff (
(cot | ].0,PI.[),
x0) =
((cot | ].0,PI.[) `| ].0,PI.[) . x0
by A4, A7, FDIFF_1:def 7
.=
(cot `| ].0,PI.[) . x0
by Lm2, FDIFF_2:16
.=
diff (
cot,
x0)
by A7, Lm2, FDIFF_1:def 7
.=
- (1 / ((sin . x0) ^2))
by A7, Lm4
;
hence
diff (
(cot | ].0,PI.[),
x0)
< 0
by A7, A6;
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:61;
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:72;
A13:
[.(PI / 4),((3 / 4) * PI).] c= ].0,PI.[
by Lm9, Lm10, XXREAL_2:def 12;
then
sin (arccot . r) <> 0
by A9, COMPTRIG:7;
then
r * (sin (arccot . r)) = cos (arccot . r)
by A10, XCMPLX_1:87;
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 7
.=
(cot `| ].0,PI.[) . (arccot . r)
by Lm2, FDIFF_2:16
.=
diff (cot,(arccot . r))
by A9, A13, Lm2, FDIFF_1:def 7
.=
- (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:188
.=
- (1 / ((r ^2) + 1))
by A14, XCMPLX_1:73
;
hence
diff (arccot,r) = - (1 / (1 + (r ^2)))
; verum