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) + H₁(i) < r & r < ((3 / 2) * PI ) + H₁(i) ) ; :: thesis: cos r < 0
then ( ((PI / 2) + H₁(i)) + (PI / 2) < r + (PI / 2) & r + (PI / 2) < (((3 / 2) * PI ) + H₁(i)) + (PI / 2) ) by XREAL_1:8;
then A1: ( PI + H₁(i) < r + (PI / 2) & r + (PI / 2) < (2 * PI ) + H₁(i) ) ;
sin (r + (PI / 2)) = cos r by SIN_COS:84;
hence cos r < 0 by A1, Th12; :: thesis: verum