let r be real number ; :: thesis: for i being integer number st PI + ((2 * PI ) * i) < r & r <= (2 * PI ) + ((2 * PI ) * i) holds
cos r > - 1
let i be integer number ; :: thesis: ( PI + ((2 * PI ) * i) < r & r <= (2 * PI ) + ((2 * PI ) * i) implies cos r > - 1 )
assume that
A1: ( PI + H₁(i) < r & r <= (2 * PI ) + H₁(i) ) and
A2: cos r <= - 1 ; :: thesis: contradiction
A3: ( (PI + H₁(i)) - H₁(i) < r - H₁(i) & r - H₁(i) <= ((2 * PI ) + H₁(i)) - H₁(i) ) by A1, XREAL_1:11;
A4: cos r >= - 1 by Th5;
cos (r - H₁(i)) = cos (r + H₁( - i))
.= cos r by COMPLEX2:10
.= - 1 by A2, A4, XXREAL_0:1 ;
hence contradiction by A3, Th36; :: thesis: verum