A1: sin is_differentiable_on ].((3 / 2) * PI ),(2 * PI ).[ by FDIFF_1:34, SIN_COS:73;
X: ].((3 / 2) * PI ),(2 * PI ).[ c= dom sin by SIN_COS:27;
for th being Real st th in ].((3 / 2) * PI ),(2 * PI ).[ holds
diff sin ,th > 0

proof

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

end;

hence sin | ].((3 / 2) * PI ),(2 * PI ).[ is increasing by A1, Lm1, X, ROLLE:9; :: thesis: verum