let r be Real; :: thesis: ( - 1 <= r & r <= 1 implies arctan r = - (arctan (- r)) )
assume ( - 1 <= r & r <= 1 ) ; :: thesis: arctan r = - (arctan (- r))
then A1: ( - (- 1) >= - r & - r >= - 1 ) by XREAL_1:26;
then A2: tan (arctan (- r)) = - r by Th49;
( - (PI / 4) <= arctan (- r) & arctan (- r) <= PI / 4 ) by A1, Th61;
then A4: arctan (- r) in [.(- (PI / 4)),(PI / 4).] by XXREAL_1:1;
[.(- (PI / 4)),(PI / 4).] c= ].(- (PI / 2)),(PI / 2).[ by Lm7, Lm8, XXREAL_2:def 12;
then A5: cos (arctan (- r)) <> 0 by A4, COMPTRIG:27;
A6: r = ((tan 0 ) - (tan (arctan (- r)))) / (1 + ((tan 0 ) * (tan (arctan (- r))))) by A2, Th39
.= tan (0 - (arctan (- r))) by A5, SIN_COS:34, SIN_COS4:12 ;
arctan (- r) <= PI / 4 by A1, Th61;
then A7: - (PI / 4) <= - (arctan (- r)) by XREAL_1:26;
- (PI / 4) <= arctan (- r) by A1, Th61;
then - (arctan (- r)) <= - (- (PI / 4)) by XREAL_1:26;
then A8: - (arctan (- r)) in [.(- (PI / 4)),(PI / 4).] by A7, XXREAL_1:1;
[.(- (PI / 4)),(PI / 4).] c= ].(- (PI / 2)),(PI / 2).[ by Lm7, Lm8, XXREAL_2:def 12;
then ( - (PI / 2) < - (arctan (- r)) & - (arctan (- r)) < PI / 2 ) by A8, XXREAL_1:4;
hence arctan r = - (arctan (- r)) by A6, Th33; :: thesis: verum