let r be real number ; :: thesis: for i being integer number st (PI / 2) + ((2 * PI ) * i) <= r & r <= ((3 / 2) * PI ) + ((2 * PI ) * i) holds
cos r <= 0
let i be integer number ; :: 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:10, SIN_COS:82; :: thesis: verum