let r be Real; :: thesis: for i being Integer st (PI / 2) + ((2 * PI) * i) <= r & r <= ((3 / 2) * PI) + ((2 * PI) * i) holds
cos r <= 0
let i be Integer; :: thesis: ( (PI / 2) + ((2 * PI) * i) <= r & r <= ((3 / 2) * PI) + ((2 * PI) * i) implies cos r <= 0 )
assume ( (PI / 2) + ((2 * PI) * i) <= r & r <= ((3 / 2) * PI) + ((2 * PI) * i) ) ; :: thesis: cos r <= 0
then ( ( (PI / 2) + ((2 * PI) * i) < r & r < ((3 / 2) * PI) + ((2 * PI) * i) ) or (PI / 2) + ((2 * PI) * i) = r or r = ((3 / 2) * PI) + ((2 * PI) * i) ) by XXREAL_0:1;
hence cos r <= 0 by Th14, COMPLEX2:9, SIN_COS:77; :: thesis: verum