for th being Real st th in ].PI,((3 / 2) * PI).[ holds
diff (sin,th) < 0

proof

let th be Real; :: thesis: ( th in ].PI,((3 / 2) * PI).[ implies diff (sin,th) < 0 )
assume A1: th in ].PI,((3 / 2) * PI).[ ; :: thesis: diff (sin,th) < 0
th < (3 / 2) * PI by A1, XXREAL_1:4;
then A2: th - PI < ((3 / 2) * PI) - PI by XREAL_1:9;
PI < th by A1, XXREAL_1:4;
then PI - PI < th - PI by XREAL_1:9;
then th - PI in ].0,(PI / 2).[ by A2, XXREAL_1:4;
then cos . (th - PI) > 0 by SIN_COS:80;
then A3: 0 - (cos . (th - PI)) < 0 ;
diff (sin,th) = cos . (PI + (th - PI)) by SIN_COS:68
.= - (cos . (th - PI)) by SIN_COS:78 ;
hence diff (sin,th) < 0 by A3; :: thesis: verum

end;

hence sin | ].PI,((3 / 2) * PI).[ is decreasing by FDIFF_1:26, ROLLE:10, SIN_COS:24, SIN_COS:68; :: thesis: verum