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