let x be set ; ( x in [.(- (PI / 4)),(PI / 4).] implies tan . x in [.(- 1),1.] )
assume
x in [.(- (PI / 4)),(PI / 4).]
; tan . x in [.(- 1),1.]
then
x in ].(- (PI / 4)),(PI / 4).[ \/ {(- (PI / 4)),(PI / 4)}
by XXREAL_1:128;
then A1:
( x in ].(- (PI / 4)),(PI / 4).[ or x in {(- (PI / 4)),(PI / 4)} )
by XBOOLE_0:def 3;
per cases
( x in ].(- (PI / 4)),(PI / 4).[ or x = - (PI / 4) or x = PI / 4 )
by A1, TARSKI:def 2;
suppose A2:
x in ].(- (PI / 4)),(PI / 4).[
;
tan . x in [.(- 1),1.]then
x in { s where s is Real : ( - (PI / 4) < s & s < PI / 4 ) }
by RCOMP_1:def 2;
then A3:
ex
s being
Real st
(
s = x &
- (PI / 4) < s &
s < PI / 4 )
;
A4:
].(- (PI / 4)),(PI / 4).[ c= [.(- (PI / 4)),(PI / 4).]
by XXREAL_1:25;
- (PI / 4) in { s where s is Real : ( - (PI / 4) <= s & s <= PI / 4 ) }
;
then A5:
- (PI / 4) in [.(- (PI / 4)),(PI / 4).]
by RCOMP_1:def 1;
A6:
[.(- (PI / 4)),(PI / 4).] c= ].(- (PI / 2)),(PI / 2).[
by Lm7, Lm8, XXREAL_2:def 12;
then A7:
tan | [.(- (PI / 4)),(PI / 4).] is
increasing
by Th7, RFUNCT_2:28;
A8:
[.(- (PI / 4)),(PI / 4).] /\ (dom tan) = [.(- (PI / 4)),(PI / 4).]
by A6, Th1, XBOOLE_1:1, XBOOLE_1:28;
PI / 4
in { s where s is Real : ( - (PI / 4) <= s & s <= PI / 4 ) }
;
then
PI / 4
in [.(- (PI / 4)),(PI / 4).] /\ (dom tan)
by A8, RCOMP_1:def 1;
then
tan . x < tan . (PI / 4)
by A2, A7, A8, A4, A3, RFUNCT_2:20;
then A9:
tan . x < 1
by SIN_COS:def 28;
x in { s where s is Real : ( - (PI / 4) < s & s < PI / 4 ) }
by A2, RCOMP_1:def 2;
then
ex
s being
Real st
(
s = x &
- (PI / 4) < s &
s < PI / 4 )
;
then
- 1
< tan . x
by A2, A7, A5, A8, A4, Th17, RFUNCT_2:20;
then
tan . x in { s where s is Real : ( - 1 < s & s < 1 ) }
by A9;
then A10:
tan . x in ].(- 1),1.[
by RCOMP_1:def 2;
].(- 1),1.[ c= [.(- 1),1.]
by XXREAL_1:25;
hence
tan . x in [.(- 1),1.]
by A10;
verum end;