let r be Real; :: thesis: ( - 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 ; :: thesis: 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; :: thesis: verum