A1: cos is_differentiable_on ].PI ,(2 * PI ).[

proof

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

end;

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

proof

let x be Real; :: thesis: ( x in ].PI ,(2 * PI ).[ implies diff cos ,x > 0 )
assume x in ].PI ,(2 * PI ).[ ; :: thesis: diff cos ,x > 0
then 0 - (sin . x) > 0 by Th25, XREAL_1:52;
hence diff cos ,x > 0 by SIN_COS:72; :: thesis: verum

end;

hence cos | ].PI ,(2 * PI ).[ is increasing by A1, Lx3, ROLLE:9, SIN_COS:27; :: thesis: verum