let r be real number ; :: thesis: for i being integer number 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 number ; :: 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 that
A1: H₁(i) <= r and
A2: r < (2 * PI ) + H₁(i) ; :: thesis: ( not sin r = 0 or r = (2 * PI ) * i or r = PI + ((2 * PI ) * i) )
assume sin r = 0 ; :: thesis: ( r = (2 * PI ) * i or r = PI + ((2 * PI ) * i) )
then ( ( r <= H₁(i) or r >= PI + H₁(i) ) & ( r <= PI + H₁(i) or (2 * PI ) + H₁(i) <= r ) ) by Th11, Th12;
hence ( r = (2 * PI ) * i or r = PI + ((2 * PI ) * i) ) by A1, A2, XXREAL_0:1; :: thesis: verum