let r be Real; :: thesis: for i being Integer st ((3 / 2) * PI) + ((2 * PI) * i) < r & r < (2 * PI) + ((2 * PI) * i) holds
cos r > 0
let i be Integer; :: thesis: ( ((3 / 2) * PI) + ((2 * PI) * i) < r & r < (2 * PI) + ((2 * PI) * i) implies cos r > 0 )
assume that
A1: ((3 / 2) * PI) + H₁(i) < r and
A2: r < (2 * PI) + H₁(i) ; :: thesis: cos r > 0
(((3 / 2) * PI) + H₁(i)) - PI < r - PI by A1, XREAL_1:9;
then A3: (PI / 2) + H₁(i) < r - PI ;
( PI + H₁(i) < ((3 / 2) * PI) + H₁(i) & r - PI < ((2 * PI) + H₁(i)) - PI ) by A2, COMPTRIG:5, XREAL_1:6, XREAL_1:9;
then A4: r - PI < ((3 / 2) * PI) + H₁(i) by XXREAL_0:2;
cos (r - PI) = cos (- (PI - r))
.= cos (PI + (- r)) by SIN_COS:31
.= - (cos (- r)) by SIN_COS:79
.= - (cos r) by SIN_COS:31 ;
hence cos r > 0 by A3, A4, Th14; :: thesis: verum