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

proof

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

end;

hence cos | ].((3 / 2) * PI ),(2 * PI ).[ is increasing by FDIFF_1:34, ROLLE:9, SIN_COS:27, SIN_COS:72; :: thesis: verum