let r be Real; :: thesis: for i being Integer st ((3 / 2) * PI) + ((2 * PI) * i) <= r & r <= (2 * PI) + ((2 * PI) * i) holds
cos r >= 0
let i be Integer; :: thesis: ( ((3 / 2) * PI) + ((2 * PI) * i) <= r & r <= (2 * PI) + ((2 * PI) * i) implies cos r >= 0 )
assume A1: ( ((3 / 2) * PI) + ((2 * PI) * i) <= r & r <= (2 * PI) + ((2 * PI) * i) ) ; :: thesis: cos r >= 0

per cases ( ( ((3 / 2) * PI) + ((2 * PI) * i) < r & r < (2 * PI) + ((2 * PI) * i) ) or ((3 / 2) * PI) + ((2 * PI) * i) = r or r = (2 * PI) + ((2 * PI) * i) ) by A1, XXREAL_0:1;

suppose ( ((3 / 2) * PI) + ((2 * PI) * i) < r & r < (2 * PI) + ((2 * PI) * i) ) ; :: thesis: cos r >= 0

hence cos r >= 0 by Th15; :: thesis: verum

end;

suppose ((3 / 2) * PI) + ((2 * PI) * i) = r ; :: thesis: cos r >= 0

hence cos r >= 0 by COMPLEX2:9, SIN_COS:77; :: thesis: verum

end;

suppose r = (2 * PI) + ((2 * PI) * i) ; :: thesis: cos r >= 0

hence cos r >= 0 by COMPLEX2:9, SIN_COS:77; :: thesis: verum

end;

end;