let x be set ; :: thesis: ( x in [.0 ,(PI / 4).] implies sec . x in [.1,(sqrt 2).] )
assume A1:
x in [.0 ,(PI / 4).]
; :: thesis: sec . x in [.1,(sqrt 2).]
x in ].0 ,(PI / 4).[ \/ {0 ,(PI / 4)}
by A1, XXREAL_1:128;
then A4:
( x in ].0 ,(PI / 4).[ or x in {0 ,(PI / 4)} )
by XBOOLE_0:def 3;
per cases
( x in ].0 ,(PI / 4).[ or x = 0 or x = PI / 4 )
by A4, TARSKI:def 2;
suppose A5:
x in ].0 ,(PI / 4).[
;
:: thesis: sec . x in [.1,(sqrt 2).]A6:
0 in [.0 ,(PI / 2).[
;
PI / 4
< PI / 2
by XREAL_1:78;
then
PI / 4
in [.0 ,(PI / 2).[
;
then A7:
[.0 ,(PI / 4).] c= [.0 ,(PI / 2).[
by A6, XXREAL_2:def 12;
then A8:
sec | [.0 ,(PI / 4).] is
increasing
by Th17, RFUNCT_2:60;
A9:
0 in [.0 ,(PI / 4).]
by XXREAL_1:1;
A10:
[.0 ,(PI / 4).] /\ (dom sec ) = [.0 ,(PI / 4).]
by A7, Th1, XBOOLE_1:1, XBOOLE_1:28;
A11:
].0 ,(PI / 4).[ c= [.0 ,(PI / 4).]
by XXREAL_1:25;
x in { s where s is Real : ( 0 < s & s < PI / 4 ) }
by A5, RCOMP_1:def 2;
then
ex
s being
Real st
(
s = x &
0 < s &
s < PI / 4 )
;
then A12:
1
< sec . x
by A5, A8, A9, A10, A11, Th31, RFUNCT_2:43;
PI / 4
in { s where s is Real : ( 0 <= s & s <= PI / 4 ) }
;
then A13:
PI / 4
in [.0 ,(PI / 4).] /\ (dom sec )
by A10, RCOMP_1:def 1;
x in { s where s is Real : ( 0 < s & s < PI / 4 ) }
by A5, RCOMP_1:def 2;
then
ex
s being
Real st
(
s = x &
0 < s &
s < PI / 4 )
;
then
sec . x < sqrt 2
by A5, A8, A10, A11, A13, Th31, RFUNCT_2:43;
then A14:
sec . x in ].1,(sqrt 2).[
by A12, XXREAL_1:4;
].1,(sqrt 2).[ c= [.1,(sqrt 2).]
by XXREAL_1:25;
hence
sec . x in [.1,(sqrt 2).]
by A14;
:: thesis: verum end;