let x be set ; :: thesis: ( x in [.(- 1),1.] implies arctan . x in [.(- (PI / 4)),(PI / 4).] )
assume x in [.(- 1),1.] ; :: thesis: arctan . x in [.(- (PI / 4)),(PI / 4).]
then x in ].(- 1),1.[ \/ {(- 1),1} by XXREAL_1:128;
then A1: ( x in ].(- 1),1.[ or x in {(- 1),1} ) by XBOOLE_0:def 3;
per cases ( x in ].(- 1),1.[ or x = - 1 or x = 1 ) by A1, TARSKI:def 2;
suppose A2: x in ].(- 1),1.[ ; :: thesis: arctan . x in [.(- (PI / 4)),(PI / 4).]
then x in { s where s is Real : ( - 1 < s & s < 1 ) } by RCOMP_1:def 2;
then A3: ex s being Real st
( s = x & - 1 < s & s < 1 ) ;
A4: ].(- 1),1.[ c= [.(- 1),1.] by XXREAL_1:25;
A5: [.(- 1),1.] /\ (dom arctan) = [.(- 1),1.] by Th23, XBOOLE_1:28;
then 1 in [.(- 1),1.] /\ (dom arctan) by XXREAL_1:1;
then A6: arctan . x < PI / 4 by A2, A5, A4, A3, Th39, Th47, RFUNCT_2:20;
- 1 in [.(- 1),1.] by XXREAL_1:1;
then - (PI / 4) < arctan . x by A2, A5, A4, A3, Th37, Th47, RFUNCT_2:20;
hence arctan . x in [.(- (PI / 4)),(PI / 4).] by A6, XXREAL_1:1; :: thesis: verum
end;
suppose x = - 1 ; :: thesis: arctan . x in [.(- (PI / 4)),(PI / 4).]
hence arctan . x in [.(- (PI / 4)),(PI / 4).] by Th37, XXREAL_1:1; :: thesis: verum
end;
suppose x = 1 ; :: thesis: arctan . x in [.(- (PI / 4)),(PI / 4).]
hence arctan . x in [.(- (PI / 4)),(PI / 4).] by Th39, XXREAL_1:1; :: thesis: verum
end;
end;