now
let r1, r2 be Real; :: thesis: ( r1 in [.(- (PI / 2)),0 .[ /\ (dom cosec ) & r2 in [.(- (PI / 2)),0 .[ /\ (dom cosec ) & r1 < r2 implies cosec . r2 < cosec . r1 )
assume that
A1: r1 in [.(- (PI / 2)),0 .[ /\ (dom cosec ) and
A2: r2 in [.(- (PI / 2)),0 .[ /\ (dom cosec ) and
A3: r1 < r2 ; :: thesis: cosec . r2 < cosec . r1
A4: ( r1 in [.(- (PI / 2)),0 .[ & r1 in dom cosec & r2 in [.(- (PI / 2)),0 .[ & r2 in dom cosec ) by A1, A2, XBOOLE_0:def 4;
then A5: ( - (PI / 2) <= r1 & r1 < 0 & - (PI / 2) <= r2 & r2 < 0 ) by XXREAL_1:3;
now
per cases ( - (PI / 2) = r1 or - (PI / 2) < r1 ) by A5, XXREAL_0:1;
suppose A6: - (PI / 2) = r1 ; :: thesis: cosec . r2 < cosec . r1
A7: cosec . r1 = 1 / (sin . (- (PI / 2))) by A4, A6, RFUNCT_1:def 8
.= 1 / (- 1) by SIN_COS:33, SIN_COS:81
.= - 1 ;
A8: r2 in ].(- (PI / 2)),0 .[ by A3, A5, A6;
- (PI / 2) > - PI by COMPTRIG:21, XREAL_1:26;
then ].(- (PI / 2)),0 .[ c= ].(- PI ),0 .[ by XXREAL_1:46;
then ( - PI < r2 & r2 < 0 ) by A8, XXREAL_1:4;
then ( (- PI ) + (2 * PI ) < r2 + (2 * PI ) & r2 + (2 * PI ) < 0 + (2 * PI ) ) by XREAL_1:10;
then r2 + (2 * PI ) in ].PI ,(2 * PI ).[ ;
then sin . (r2 + (2 * PI )) < 0 by COMPTRIG:25;
then A9: sin . r2 < 0 by SIN_COS:83;
( ((3 / 2) * PI ) + ((2 * PI ) * (- 1)) < r2 & r2 < (2 * PI ) + ((2 * PI ) * (- 1)) ) by A3, A4, A6, XXREAL_1:3;
then sin r2 > - 1 by SIN_COS6:39;
then sin . r2 > - 1 by SIN_COS:def 21;
then (sin . r2) " < (- 1) " by A9, XREAL_1:89;
hence cosec . r2 < cosec . r1 by A4, A7, RFUNCT_1:def 8; :: thesis: verum
end;
end;
end;
hence cosec . r2 < cosec . r1 ; :: thesis: verum
end;
hence cosec | [.(- (PI / 2)),0 .[ is decreasing by RFUNCT_2:44; :: thesis: verum