let r be Real; ( - 1 <= r & r <= 1 implies arctan r = - (arctan (- r)) )
A1:
[.(- (PI / 4)),(PI / 4).] c= ].(- (PI / 2)),(PI / 2).[
by Lm7, Lm8, XXREAL_2:def 12;
assume that
A2:
- 1 <= r
and
A3:
r <= 1
; arctan r = - (arctan (- r))
A4:
- r >= - 1
by A3, XREAL_1:24;
A5:
- (- 1) >= - r
by A2, XREAL_1:24;
then A6:
arctan (- r) <= PI / 4
by A4, Th63;
- (PI / 4) <= arctan (- r)
by A5, A4, Th63;
then A7:
- (arctan (- r)) <= - (- (PI / 4))
by XREAL_1:24;
arctan (- r) <= PI / 4
by A5, A4, Th63;
then
- (PI / 4) <= - (arctan (- r))
by XREAL_1:24;
then A8:
- (arctan (- r)) in [.(- (PI / 4)),(PI / 4).]
by A7, XXREAL_1:1;
- (PI / 4) <= arctan (- r)
by A5, A4, Th63;
then
arctan (- r) in [.(- (PI / 4)),(PI / 4).]
by A6, XXREAL_1:1;
then A9:
cos (arctan (- r)) <> 0
by A1, COMPTRIG:11;
tan (arctan (- r)) = - r
by A5, A4, Th51;
then A10: r =
((tan 0) - (tan (arctan (- r)))) / (1 + ((tan 0) * (tan (arctan (- r)))))
by Th41
.=
tan (0 - (arctan (- r)))
by A9, SIN_COS:31, SIN_COS4:8
;
A11:
[.(- (PI / 4)),(PI / 4).] c= ].(- (PI / 2)),(PI / 2).[
by Lm7, Lm8, XXREAL_2:def 12;
then A12:
- (arctan (- r)) < PI / 2
by A8, XXREAL_1:4;
- (PI / 2) < - (arctan (- r))
by A8, A11, XXREAL_1:4;
hence
arctan r = - (arctan (- r))
by A10, A12, Th35; verum