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 )
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:11;
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:21, XREAL_1:8, XREAL_1:11;
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:34
.= - (cos (- r)) by SIN_COS:84
.= - (cos r) by SIN_COS:34 ;
hence cos r > 0 by A3, A4, Th14; :: thesis: verum