let r be Real; :: thesis: ( - 1 < r & r < 1 implies ( - (PI / 4) < arctan r & arctan r < PI / 4 ) )
A1: tan (PI / 4) = tan . (PI / 4) by Lm8, Th13
.= 1 by SIN_COS:def 28 ;
assume that
A2: - 1 < r and
A3: r < 1 ; :: thesis: ( - (PI / 4) < arctan r & arctan r < PI / 4 )
A4: arctan r <= PI / 4 by A2, A3, Th63;
- (PI / 4) <= arctan r by A2, A3, Th63;
then ( ( - (PI / 4) < arctan r & arctan r < PI / 4 ) or - (PI / 4) = arctan r or arctan r = PI / 4 ) by A4, XXREAL_0:1;
hence ( - (PI / 4) < arctan r & arctan r < PI / 4 ) by A2, A3, A1, Th17, Th51; :: thesis: verum