let r be Real; ( - 1 <= r & r <= 1 implies arccot r = PI - (arccot (- r)) )
set x = arccot (- r);
assume that
A1:
- 1 <= r
and
A2:
r <= 1
; arccot r = PI - (arccot (- r))
A3:
- r >= - 1
by A2, XREAL_1:24;
A4:
- (- 1) >= - r
by A1, XREAL_1:24;
then
- r = cot (arccot (- r))
by A3, Th52;
then A5: r =
- (cot (arccot (- r)))
.=
- ((cos (arccot (- r))) / (sin (arccot (- r))))
by SIN_COS4:def 2
.=
(cos (arccot (- r))) / (- (sin (arccot (- r))))
by XCMPLX_1:188
.=
(cos (arccot (- r))) / (sin (- (arccot (- r))))
by SIN_COS:31
.=
(cos (- (arccot (- r)))) / (sin (- (arccot (- r))))
by SIN_COS:31
.=
cot (- (arccot (- r)))
by SIN_COS4:def 2
;
- r in [.(- 1),1.]
by A4, A3, XXREAL_1:1;
then A6:
arccot (- r) in [.(PI / 4),((3 / 4) * PI).]
by Th50;
then
arccot (- r) <= (3 / 4) * PI
by XXREAL_1:1;
then
- (arccot (- r)) >= - ((3 / 4) * PI)
by XREAL_1:24;
then A7:
PI + (- (arccot (- r))) >= PI + (- ((3 / 4) * PI))
by XREAL_1:6;
PI / 4 <= arccot (- r)
by A6, XXREAL_1:1;
then
- (PI / 4) >= - (arccot (- r))
by XREAL_1:24;
then
PI + (- (PI / 4)) >= PI + (- (arccot (- r)))
by XREAL_1:6;
then A8:
PI + (- (arccot (- r))) in [.(PI / 4),((3 / 4) * PI).]
by A7, XXREAL_1:1;
A9:
[.(PI / 4),((3 / 4) * PI).] c= ].0,PI.[
by Lm9, Lm10, XXREAL_2:def 12;
then A10:
PI + (- (arccot (- r))) < PI
by A8, XXREAL_1:4;
A11: cot (PI + (- (arccot (- r)))) =
(cos (PI + (- (arccot (- r))))) / (sin (PI + (- (arccot (- r)))))
by SIN_COS4:def 2
.=
(- (cos (- (arccot (- r))))) / (sin (PI + (- (arccot (- r)))))
by SIN_COS:79
.=
(- (cos (- (arccot (- r))))) / (- (sin (- (arccot (- r)))))
by SIN_COS:79
.=
(cos (- (arccot (- r)))) / (sin (- (arccot (- r))))
by XCMPLX_1:191
.=
cot (- (arccot (- r)))
by SIN_COS4:def 2
;
0 < PI + (- (arccot (- r)))
by A8, A9, XXREAL_1:4;
hence
arccot r = PI - (arccot (- r))
by A5, A10, A11, Th36; verum