let x be set ; :: thesis: ( x in [.(- (PI / 2)),(- (PI / 4)).] implies cosec . x in [.(- (sqrt 2)),(- 1).] )
assume A1:
x in [.(- (PI / 2)),(- (PI / 4)).]
; :: thesis: cosec . x in [.(- (sqrt 2)),(- 1).]
PI / 4 < PI / 2
by XREAL_1:78;
then A3:
- (PI / 2) < - (PI / 4)
by XREAL_1:26;
then
x in ].(- (PI / 2)),(- (PI / 4)).[ \/ {(- (PI / 2)),(- (PI / 4))}
by A1, XXREAL_1:128;
then A4:
( x in ].(- (PI / 2)),(- (PI / 4)).[ or x in {(- (PI / 2)),(- (PI / 4))} )
by XBOOLE_0:def 3;
per cases
( x in ].(- (PI / 2)),(- (PI / 4)).[ or x = - (PI / 2) or x = - (PI / 4) )
by A4, TARSKI:def 2;
suppose A5:
x in ].(- (PI / 2)),(- (PI / 4)).[
;
:: thesis: cosec . x in [.(- (sqrt 2)),(- 1).]A6:
- (PI / 2) in [.(- (PI / 2)),0 .[
;
- (PI / 4) in [.(- (PI / 2)),0 .[
by A3;
then A7:
[.(- (PI / 2)),(- (PI / 4)).] c= [.(- (PI / 2)),0 .[
by A6, XXREAL_2:def 12;
then A8:
cosec | [.(- (PI / 2)),(- (PI / 4)).] is
decreasing
by Th19, RFUNCT_2:61;
A9:
- (PI / 2) in [.(- (PI / 2)),(- (PI / 4)).]
by A3;
A10:
[.(- (PI / 2)),(- (PI / 4)).] /\ (dom cosec ) = [.(- (PI / 2)),(- (PI / 4)).]
by A7, Th3, XBOOLE_1:1, XBOOLE_1:28;
A11:
].(- (PI / 2)),(- (PI / 4)).[ c= [.(- (PI / 2)),(- (PI / 4)).]
by XXREAL_1:25;
x in { s where s is Real : ( - (PI / 2) < s & s < - (PI / 4) ) }
by A5;
then
ex
s being
Real st
(
s = x &
- (PI / 2) < s &
s < - (PI / 4) )
;
then A12:
- 1
> cosec . x
by A5, A8, A9, A10, A11, Th32, RFUNCT_2:44;
- (PI / 4) in { s where s is Real : ( - (PI / 2) <= s & s <= - (PI / 4) ) }
by A3;
then A13:
- (PI / 4) in [.(- (PI / 2)),(- (PI / 4)).] /\ (dom cosec )
by A10;
x in { s where s is Real : ( - (PI / 2) < s & s < - (PI / 4) ) }
by A5;
then
ex
s being
Real st
(
s = x &
- (PI / 2) < s &
s < - (PI / 4) )
;
then
cosec . x > - (sqrt 2)
by A5, A8, A10, A11, A13, Th32, RFUNCT_2:44;
then A14:
cosec . x in ].(- (sqrt 2)),(- 1).[
by A12;
].(- (sqrt 2)),(- 1).[ c= [.(- (sqrt 2)),(- 1).]
by XXREAL_1:25;
hence
cosec . x in [.(- (sqrt 2)),(- 1).]
by A14;
:: thesis: verum end;