let r be real number ; :: thesis: for i being integer number st ((3 / 2) * PI ) + ((2 * PI ) * i) < r & r < (2 * PI ) + ((2 * PI ) * i) holds
cos r > 0
let i be integer number ; :: thesis: ( ((3 / 2) * PI ) + ((2 * PI ) * i) < r & r < (2 * PI ) + ((2 * PI ) * i) implies cos r > 0 )
A1: PI + H₁(i) < ((3 / 2) * PI ) + H₁(i) by COMPTRIG:21, XREAL_1:8;
assume ( ((3 / 2) * PI ) + H₁(i) < r & r < (2 * PI ) + H₁(i) ) ; :: thesis: cos r > 0
then ( (((3 / 2) * PI ) + H₁(i)) - PI < r - PI & r - PI < ((2 * PI ) + H₁(i)) - PI ) by XREAL_1:11;
then A2: ( (PI / 2) + H₁(i) < r - PI & r - PI < ((3 / 2) * PI ) + H₁(i) ) by A1, XXREAL_0:2;
cos (r - PI ) = cos (- (PI - r))
.= cos (PI + (- r)) by SIN_COS:34
.= - (cos (- r)) by SIN_COS:84
.= - (cos r) by SIN_COS:34 ;
then - (cos r) < - 0 by A2, Th14;
hence cos r > 0 ; :: thesis: verum