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