now

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

now

per cases ( 0 < r1 or 0 = r1 ) by A4, XXREAL_1:1;

suppose A11: 0 < r1 ; :: thesis: cos . r2 < cos . r1

now

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

suppose A12: r2 < PI ; :: thesis: cos . r2 < cos . r1

then r1 < PI by A3, XXREAL_0:2;
then ( r1 in ].0 ,PI .[ & r2 in ].0 ,PI .[ ) by A3, A11, A12, XXREAL_1:4;
then ( r1 in ].0 ,PI .[ /\ (dom cos ) & r2 in ].0 ,PI .[ /\ (dom cos ) ) by A4, XBOOLE_0:def 4;
hence cos . r2 < cos . r1 by A3, Th37, RFUNCT_2:44; :: thesis: verum

end;

suppose A13: r2 = PI ; :: thesis: not cos . r2 >= cos . r1

then r1 in ].0 ,PI .[ by A3, A11, XXREAL_1:4;
then r1 in ].0 ,PI .[ /\ (dom cos ) by A4, XBOOLE_0:def 4;
then A14: cos . ((r1 + r2) / 2) < cos . r1 by A9, A10, Th37, RFUNCT_2:44;
assume cos . r2 >= cos . r1 ; :: thesis: contradiction
hence contradiction by A6, A7, A13, A14, SIN_COS:81, XXREAL_0:1; :: thesis: verum

end;

end;

end;

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

end;

suppose A15: 0 = r1 ; :: thesis: cos . r2 < cos . r1

now

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

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

then r2 in ].0 ,PI .[ by A3, A15, XXREAL_1:4;
then r2 in ].0 ,PI .[ /\ (dom cos ) by A4, XBOOLE_0:def 4;
then A16: cos . r2 < cos . ((r1 + r2) / 2) by A9, A10, Th37, RFUNCT_2:44;
assume cos . r2 >= cos . r1 ; :: thesis: contradiction
hence contradiction by A7, A8, A15, A16, SIN_COS:33, XXREAL_0:1; :: thesis: verum

end;

suppose r2 = PI ; :: thesis: cos . r2 < cos . r1

hence cos . r2 < cos . r1 by A15, SIN_COS:33, 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 | [.0 ,PI .] is decreasing by RFUNCT_2:44; :: thesis: verum