let x be set ; :: thesis: ( x in [.(- (sqrt 2)),(- 1).] implies arccosec1 . x in [.(- (PI / 2)),(- (PI / 4)).] )
A1: - (sqrt 2) < - 1 by SQUARE_1:19, XREAL_1:24;
assume x in [.(- (sqrt 2)),(- 1).] ; :: thesis: arccosec1 . x in [.(- (PI / 2)),(- (PI / 4)).]
then x in ].(- (sqrt 2)),(- 1).[ \/ {(- (sqrt 2)),(- 1)} by A1, XXREAL_1:128;
then A2: ( x in ].(- (sqrt 2)),(- 1).[ or x in {(- (sqrt 2)),(- 1)} ) by XBOOLE_0:def 3;
per cases ( x in ].(- (sqrt 2)),(- 1).[ or x = - (sqrt 2) or x = - 1 ) by A2, TARSKI:def 2;
suppose A3: x in ].(- (sqrt 2)),(- 1).[ ; :: thesis: arccosec1 . x in [.(- (PI / 2)),(- (PI / 4)).]
then A4: ( ].(- (sqrt 2)),(- 1).[ c= [.(- (sqrt 2)),(- 1).] & ex s being Real st
( s = x & - (sqrt 2) < s & s < - 1 ) ) by XXREAL_1:25;
A5: [.(- (sqrt 2)),(- 1).] /\ (dom arccosec1) = [.(- (sqrt 2)),(- 1).] by Th47, XBOOLE_1:28;
then - 1 in [.(- (sqrt 2)),(- 1).] /\ (dom arccosec1) by A1;
then A6: arccosec1 . x > - (PI / 2) by A3, A5, A4, Th75, Th83, RFUNCT_2:21;
- (sqrt 2) in [.(- (sqrt 2)),(- 1).] by A1;
then - (PI / 4) > arccosec1 . x by A3, A5, A4, Th75, Th83, RFUNCT_2:21;
hence arccosec1 . x in [.(- (PI / 2)),(- (PI / 4)).] by A6; :: thesis: verum
end;
suppose A7: x = - (sqrt 2) ; :: thesis: arccosec1 . x in [.(- (PI / 2)),(- (PI / 4)).]
- (PI / 2) <= - (PI / 4) by Lm7, XXREAL_1:3;
hence arccosec1 . x in [.(- (PI / 2)),(- (PI / 4)).] by A7, Th75; :: thesis: verum
end;
suppose A8: x = - 1 ; :: thesis: arccosec1 . x in [.(- (PI / 2)),(- (PI / 4)).]
- (PI / 2) <= - (PI / 4) by Lm7, XXREAL_1:3;
hence arccosec1 . x in [.(- (PI / 2)),(- (PI / 4)).] by A8, Th75; :: thesis: verum
end;
end;