A1: cos is_differentiable_on ].0 ,PI .[

proof

].0 ,PI .[ is open by RCOMP_1:25;
hence cos is_differentiable_on ].0 ,PI .[ by FDIFF_1:34, SIN_COS:72; :: thesis: verum

end;

for x being Real st x in ].0 ,PI .[ holds
diff cos ,x < 0

proof

let x be Real; :: thesis: ( x in ].0 ,PI .[ implies diff cos ,x < 0 )
assume x in ].0 ,PI .[ ; :: thesis: diff cos ,x < 0
then 0 < sin . x by Th23;
then 0 - (sin . x) < 0 ;
hence diff cos ,x < 0 by SIN_COS:72; :: thesis: verum

end;

hence cos | ].0 ,PI .[ is decreasing by A1, Lm0, ROLLE:10, SIN_COS:27; :: thesis: verum