let x be set ; :: thesis: ( x in [.((3 / 4) * PI),PI.] implies sec . x in [.(- (sqrt 2)),(- 1).] )
A1: PI / 4 < PI / 2 by XREAL_1:76;
then A2: (PI / 4) + (PI / 2) < (PI / 2) + (PI / 2) by XREAL_1:8;
assume x in [.((3 / 4) * PI),PI.] ; :: thesis: sec . x in [.(- (sqrt 2)),(- 1).]
then x in ].((3 / 4) * PI),PI.[ \/ {((3 / 4) * PI),PI} by A2, XXREAL_1:128;
then A3: ( 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 A3, TARSKI:def 2;
suppose A4: x in ].((3 / 4) * PI),PI.[ ; :: thesis: sec . x in [.(- (sqrt 2)),(- 1).]
(PI / 4) + (PI / 4) < (PI / 2) + (PI / 4) by A1, XREAL_1:8;
then A5: (3 / 4) * PI in ].(PI / 2),PI.] by A2;
PI in ].(PI / 2),PI.] by COMPTRIG:5;
then A6: [.((3 / 4) * PI),PI.] c= ].(PI / 2),PI.] by A5, XXREAL_2:def 12;
then A7: sec | [.((3 / 4) * PI),PI.] is increasing by Th18, RFUNCT_2:28;
A8: ex s being Real st
( s = x & (3 / 4) * PI < s & s < PI ) by A4;
A9: ex s being Real st
( s = x & (3 / 4) * PI < s & s < PI ) by A4;
A10: ].((3 / 4) * PI),PI.[ c= [.((3 / 4) * PI),PI.] by XXREAL_1:25;
A11: [.((3 / 4) * PI),PI.] /\ (dom sec) = [.((3 / 4) * PI),PI.] by A6, Th2, XBOOLE_1:1, XBOOLE_1:28;
then PI in [.((3 / 4) * PI),PI.] /\ (dom sec) by A2;
then A12: sec . x < - 1 by A4, A7, A11, A10, A9, Th31, RFUNCT_2:20;
(3 / 4) * PI in [.((3 / 4) * PI),PI.] by A2;
then - (sqrt 2) < sec . x by A4, A7, A11, A10, A8, Th31, RFUNCT_2:20;
hence sec . x in [.(- (sqrt 2)),(- 1).] by A12; :: thesis: verum
end;
suppose A13: x = (3 / 4) * PI ; :: thesis: sec . x in [.(- (sqrt 2)),(- 1).]
- (sqrt 2) < - 1 by SQUARE_1:19, XREAL_1:24;
hence sec . x in [.(- (sqrt 2)),(- 1).] by A13, Th31; :: thesis: verum
end;
suppose A14: x = PI ; :: thesis: sec . x in [.(- (sqrt 2)),(- 1).]
- (sqrt 2) < - 1 by SQUARE_1:19, XREAL_1:24;
hence sec . x in [.(- (sqrt 2)),(- 1).] by A14, Th31; :: thesis: verum
end;
end;