now

let r1, r2 be Real; :: thesis: ( r1 in [.PI ,(2 * PI ).] /\ (dom cos ) & r2 in [.PI ,(2 * PI ).] /\ (dom cos ) & r1 < r2 implies cos . r2 > cos . r1 )
assume that
A1: r1 in [.PI ,(2 * PI ).] /\ (dom cos ) and
A2: r2 in [.PI ,(2 * PI ).] /\ (dom cos ) and
A3: r1 < r2 ; :: thesis: cos . r2 > cos . r1
A4: r1 in dom cos by A1, XBOOLE_0:def 4;
set r3 = (r1 + r2) / 2;
r1 in [.PI ,(2 * PI ).] by A1, XBOOLE_0:def 4;
then A5: PI <= r1 by XXREAL_1:1;
abs (cos ((r1 + r2) / 2)) <= 1 by SIN_COS:30;
then A6: abs (cos . ((r1 + r2) / 2)) <= 1 by SIN_COS:def 23;
then A7: cos . ((r1 + r2) / 2) <= 1 by ABSVALUE:12;
r2 in [.PI ,(2 * PI ).] by A2, XBOOLE_0:def 4;
then A8: r2 <= 2 * PI by XXREAL_1:1;
A9: r1 < (r1 + r2) / 2 by A3, XREAL_1:228;
then A10: PI < (r1 + r2) / 2 by A5, XXREAL_0:2;
A11: (r1 + r2) / 2 < r2 by A3, XREAL_1:228;
then (r1 + r2) / 2 < 2 * PI by A8, XXREAL_0:2;
then (r1 + r2) / 2 in ].PI ,(2 * PI ).[ by A10, XXREAL_1:4;
then A12: (r1 + r2) / 2 in ].PI ,(2 * PI ).[ /\ (dom cos ) by SIN_COS:27, XBOOLE_0:def 4;
abs (cos r2) <= 1 by SIN_COS:30;
then abs (cos . r2) <= 1 by SIN_COS:def 23;
then A13: cos . r2 >= - 1 by ABSVALUE:12;
A14: r2 in dom cos by A2, XBOOLE_0:def 4;
A15: cos . ((r1 + r2) / 2) >= - 1 by A6, ABSVALUE:12;

now

per cases ( PI < r1 or PI = r1 ) by A5, XXREAL_0:1;

suppose A16: PI < r1 ; :: thesis: cos . r2 > cos . r1

then A17: PI < r2 by A3, XXREAL_0:2;

now

per cases ( r2 < 2 * PI or r2 = 2 * PI ) by A8, XXREAL_0:1;

suppose A18: r2 < 2 * PI ; :: thesis: cos . r2 > cos . r1

then r1 < 2 * PI by A3, XXREAL_0:2;
then r1 in ].PI ,(2 * PI ).[ by A16, XXREAL_1:4;
then A19: r1 in ].PI ,(2 * PI ).[ /\ (dom cos ) by A4, XBOOLE_0:def 4;
r2 in ].PI ,(2 * PI ).[ by A17, A18, XXREAL_1:4;
then r2 in ].PI ,(2 * PI ).[ /\ (dom cos ) by A14, XBOOLE_0:def 4;
hence cos . r2 > cos . r1 by A3, A19, Th38, RFUNCT_2:43; :: thesis: verum

end;

suppose A20: r2 = 2 * PI ; :: thesis: not cos . r2 <= cos . r1

then r1 in ].PI ,(2 * PI ).[ by A3, A16, XXREAL_1:4;
then r1 in ].PI ,(2 * PI ).[ /\ (dom cos ) by A4, XBOOLE_0:def 4;
then A21: cos . ((r1 + r2) / 2) > cos . r1 by A9, A12, Th38, RFUNCT_2:43;
assume cos . r2 <= cos . r1 ; :: thesis: contradiction
hence contradiction by A7, A20, A21, SIN_COS:81, XXREAL_0:2; :: thesis: verum

end;

end;

end;

hence cos . r2 > cos . r1 ; :: thesis: verum

end;

suppose A22: PI = r1 ; :: thesis: cos . r2 > cos . r1

now

per cases ( r2 < 2 * PI or r2 = 2 * PI ) by A8, XXREAL_0:1;

suppose r2 < 2 * PI ; :: thesis: not cos . r2 <= cos . r1

then r2 in ].PI ,(2 * PI ).[ by A3, A22, XXREAL_1:4;
then r2 in ].PI ,(2 * PI ).[ /\ (dom cos ) by A14, XBOOLE_0:def 4;
then A23: cos . r2 > cos . ((r1 + r2) / 2) by A11, A12, Th38, RFUNCT_2:43;
assume cos . r2 <= cos . r1 ; :: thesis: contradiction
hence contradiction by A15, A13, A22, A23, SIN_COS:81, XXREAL_0:1; :: thesis: verum

end;

suppose r2 = 2 * PI ; :: thesis: cos . r2 > cos . r1

hence cos . r2 > cos . r1 by A22, SIN_COS:81; :: thesis: verum

end;

end;

end;

hence cos . r2 > cos . r1 ; :: thesis: verum

end;

end;

end;

hence cos . r2 > cos . r1 ; :: thesis: verum

end;

hence cos | [.PI ,(2 * PI ).] is increasing by RFUNCT_2:43; :: thesis: verum