let r be Real; :: thesis: for i being Integer st (2 * PI) * i <= r & r < (2 * PI) + ((2 * PI) * i) & cos r = 0 & not r = (PI / 2) + ((2 * PI) * i) holds
r = ((3 / 2) * PI) + ((2 * PI) * i)
let i be Integer; :: thesis: ( (2 * PI) * i <= r & r < (2 * PI) + ((2 * PI) * i) & cos r = 0 & not r = (PI / 2) + ((2 * PI) * i) implies r = ((3 / 2) * PI) + ((2 * PI) * i) )
assume that
A1: H₁(i) <= r and
A2: r < (2 * PI) + H₁(i) ; :: thesis: ( not cos r = 0 or r = (PI / 2) + ((2 * PI) * i) or r = ((3 / 2) * PI) + ((2 * PI) * i) )
A3: (- (PI / 2)) + H₁(i) < 0 + H₁(i) by XREAL_1:6;
assume A4: cos r = 0 ; :: thesis: ( r = (PI / 2) + ((2 * PI) * i) or r = ((3 / 2) * PI) + ((2 * PI) * i) )
then A5: ( (PI / 2) + H₁(i) >= r or r >= ((3 / 2) * PI) + H₁(i) ) by Th14;
( (- (PI / 2)) + H₁(i) >= r or r >= (PI / 2) + H₁(i) ) by A4, Th13;
then ( r = (PI / 2) + H₁(i) or r = ((3 / 2) * PI) + H₁(i) or r > ((3 / 2) * PI) + H₁(i) ) by A1, A5, A3, XXREAL_0:1, XXREAL_0:2;
hence ( r = (PI / 2) + ((2 * PI) * i) or r = ((3 / 2) * PI) + ((2 * PI) * i) ) by A2, A4, Th15; :: thesis: verum