A1: sin is_differentiable_on ].PI ,((3 / 2) * PI ).[ by FDIFF_1:34, SIN_COS:73;
X: ].PI ,((3 / 2) * PI ).[ c= dom sin by SIN_COS:27;
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 A2: th in ].PI ,((3 / 2) * PI ).[ ; :: thesis: diff sin ,th < 0
A3: diff sin ,th = cos . (PI + (th - PI )) by SIN_COS:73
.= - (cos . (th - PI )) by SIN_COS:83 ;
( PI < th & th < (3 / 2) * PI ) by A2, XXREAL_1:4;
then ( PI - PI < th - PI & th - PI < ((3 / 2) * PI ) - PI ) by XREAL_1:11;
then th - PI in ].0 ,(PI / 2).[ by XXREAL_1:4;
then cos . (th - PI ) > 0 by SIN_COS:85;
then 0 - (cos . (th - PI )) < 0 ;
hence diff sin ,th < 0 by A3; :: thesis: verum

end;

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