now for r1, r2 being Real st r1 in ].0,(PI / 2).] /\ (dom cosec) & r2 in ].0,(PI / 2).] /\ (dom cosec) & r1 < r2 holds
cosec . r2 < cosec . r1let r1,
r2 be
Real;
( r1 in ].0,(PI / 2).] /\ (dom cosec) & r2 in ].0,(PI / 2).] /\ (dom cosec) & r1 < r2 implies cosec . r2 < cosec . r1 )assume that A1:
r1 in ].0,(PI / 2).] /\ (dom cosec)
and A2:
r2 in ].0,(PI / 2).] /\ (dom cosec)
and A3:
r1 < r2
;
cosec . r2 < cosec . r1A4:
r1 in dom cosec
by A1, XBOOLE_0:def 4;
A5:
r2 in ].0,(PI / 2).]
by A2, XBOOLE_0:def 4;
then A6:
r2 <= PI / 2
by XXREAL_1:2;
A7:
r2 in dom cosec
by A2, XBOOLE_0:def 4;
A8:
r1 in ].0,(PI / 2).]
by A1, XBOOLE_0:def 4;
then A9:
0 < r1
by XXREAL_1:2;
A10:
0 < r2
by A5, XXREAL_1:2;
now cosec . r2 < cosec . r1per cases
( r2 < PI / 2 or r2 = PI / 2 )
by A6, XXREAL_0:1;
suppose A11:
r2 < PI / 2
;
cosec . r2 < cosec . r1then
r1 < PI / 2
by A3, XXREAL_0:2;
then
r1 in ].0,(PI / 2).[
by A9;
then A12:
r1 in ].0,(PI / 2).[ /\ (dom cosec)
by A4, XBOOLE_0:def 4;
r2 in ].0,(PI / 2).[
by A10, A11;
then
r2 in ].0,(PI / 2).[ /\ (dom cosec)
by A7, XBOOLE_0:def 4;
hence
cosec . r2 < cosec . r1
by A3, A12, Th16, RFUNCT_2:21;
verum end; suppose A13:
r2 = PI / 2
;
cosec . r2 < cosec . r1then
sin r1 < 1
by A3, A9, SIN_COS6:30;
then A14:
sin . r1 < 1
by SIN_COS:def 17;
sin . r1 > 0
by A8, Lm4, COMPTRIG:7;
then A15:
1
/ 1
< 1
/ (sin . r1)
by A14, XREAL_1:76;
cosec . r2 =
1
/ 1
by A7, A13, RFUNCT_1:def 2, SIN_COS:76
.=
1
;
hence
cosec . r2 < cosec . r1
by A4, A15, RFUNCT_1:def 2;
verum end; hence
cosec . r2 < cosec . r1
;
verum end;
hence
cosec | ].0,(PI / 2).] is decreasing
by RFUNCT_2:21; verum