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 that
A1: (PI / 2) + H₁(i) < r and
A2: r < ((3 / 2) * PI) + H₁(i) ; :: thesis: cos r < 0
((PI / 2) + H₁(i)) + (PI / 2) < r + (PI / 2) by A1, XREAL_1:6;
then A3: PI + H₁(i) < r + (PI / 2) ;
r + (PI / 2) < (((3 / 2) * PI) + H₁(i)) + (PI / 2) by A2, XREAL_1:6;
then A4: r + (PI / 2) < (2 * PI) + H₁(i) ;
sin (r + (PI / 2)) = cos r by SIN_COS:79;
hence cos r < 0 by A3, A4, Th12; :: thesis: verum