let x be set ; :: thesis: ( x in [.(- (PI / 4)),(PI / 4).] implies tan . x in [.(- 1),1.] )
assume x in [.(- (PI / 4)),(PI / 4).] ; :: thesis: 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).[ ; :: thesis: 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; :: thesis: verum
end;
suppose x = - (PI / 4) ; :: thesis: tan . x in [.(- 1),1.]
then tan . x in { s where s is Real : ( - 1 <= s & s <= 1 ) } by Th17;
hence tan . x in [.(- 1),1.] by RCOMP_1:def 1; :: thesis: verum
end;
suppose x = PI / 4 ; :: thesis: tan . x in [.(- 1),1.]
then tan . x = 1 by SIN_COS:def 28;
then tan . x in { s where s is Real : ( - 1 <= s & s <= 1 ) } ;
hence tan . x in [.(- 1),1.] by RCOMP_1:def 1; :: thesis: verum
end;
end;