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