let r be Real; :: thesis: for i being Integer st (PI / 2) + ((2 * PI) * i) < r & r <= (2 * PI) + ((2 * PI) * i) holds
sin r < 1
let i be Integer; :: thesis: ( (PI / 2) + ((2 * PI) * i) < r & r <= (2 * PI) + ((2 * PI) * i) implies sin r < 1 )
assume that
A1: ( (PI / 2) + H₁(i) < r & r <= (2 * PI) + H₁(i) ) and
A2: sin r >= 1 ; :: thesis: contradiction
A3: ( ((PI / 2) + H₁(i)) - H₁(i) < r - H₁(i) & r - H₁(i) <= ((2 * PI) + H₁(i)) - H₁(i) ) by A1, XREAL_1:9;
A4: sin r <= 1 by Th4;
sin (r - H₁(i)) = sin (r + H₁( - i))
.= sin r by COMPLEX2:8
.= 1 by A2, A4, XXREAL_0:1 ;
hence contradiction by A3, Th33; :: thesis: verum