let r be Real; :: thesis: for i being Integer st (2 * PI) * i <= r & r < (2 * PI) + ((2 * PI) * i) & sin r = 0 & not r = (2 * PI) * i holds
r = PI + ((2 * PI) * i)
let i be Integer; :: thesis: ( (2 * PI) * i <= r & r < (2 * PI) + ((2 * PI) * i) & sin r = 0 & not r = (2 * PI) * i implies r = PI + ((2 * PI) * i) )
assume A1: ( H₁(i) <= r & r < (2 * PI) + H₁(i) ) ; :: thesis: ( not sin r = 0 or r = (2 * PI) * i or r = PI + ((2 * PI) * i) )
assume A2: sin r = 0 ; :: thesis: ( r = (2 * PI) * i or r = PI + ((2 * PI) * i) )
then A3: ( r <= PI + H₁(i) or (2 * PI) + H₁(i) <= r ) by Th12;
( r <= H₁(i) or r >= PI + H₁(i) ) by A2, Th11;
hence ( r = (2 * PI) * i or r = PI + ((2 * PI) * i) ) by A1, A3, XXREAL_0:1; :: thesis: verum