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).]A4:
- 1
in [.(- 1),1.]
by XXREAL_1:1;
A5:
[.(- 1),1.] /\ (dom arctan ) = [.(- 1),1.]
by Th21, XBOOLE_1:28;
A7:
].(- 1),1.[ c= [.(- 1),1.]
by XXREAL_1:25;
x in { s where s is Real : ( - 1 < s & s < 1 ) }
by A2, RCOMP_1:def 2;
then A8:
ex
s being
Real st
(
s = x &
- 1
< s &
s < 1 )
;
then A9:
- (PI / 4) < arctan . x
by A2, A4, A5, A7, Th35, Th45, RFUNCT_2:43;
1
in [.(- 1),1.] /\ (dom arctan )
by A5, XXREAL_1:1;
then
arctan . x < PI / 4
by A2, A5, A7, A8, Th37, Th45, RFUNCT_2:43;
hence
arctan . x in [.(- (PI / 4)),(PI / 4).]
by A9, XXREAL_1:1;
:: thesis: verum end;