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