let r be real number ; :: thesis: for i being integer number 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 number ; :: 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) )
assume A3: cos r = 0 ; :: thesis: ( r = (PI / 2) + ((2 * PI ) * i) or r = ((3 / 2) * PI ) + ((2 * PI ) * i) )
then A4: ( ( (- (PI / 2)) + H₁(i) >= r or r >= (PI / 2) + H₁(i) ) & ( (PI / 2) + H₁(i) >= r or r >= ((3 / 2) * PI ) + H₁(i) ) ) by Th13, Th14;
(- (PI / 2)) + H₁(i) < 0 + H₁(i) by XREAL_1:8;
then ( r = (PI / 2) + H₁(i) or r = ((3 / 2) * PI ) + H₁(i) or r > ((3 / 2) * PI ) + H₁(i) ) by A1, A4, XXREAL_0:1, XXREAL_0:2;
hence ( r = (PI / 2) + ((2 * PI ) * i) or r = ((3 / 2) * PI ) + ((2 * PI ) * i) ) by A2, A3, Th15; :: thesis: verum