let r be Real; :: thesis: for i being Integer st PI + ((2 * PI) * i) <= r & r <= ((3 * PI) / 2) + ((2 * PI) * i) & r / PI is rational & cos r is rational holds
r in {(PI + ((2 * PI) * i)),(((4 * PI) / 3) + ((2 * PI) * i)),(((3 * PI) / 2) + ((2 * PI) * i))}
let i be Integer; :: thesis: ( PI + ((2 * PI) * i) <= r & r <= ((3 * PI) / 2) + ((2 * PI) * i) & r / PI is rational & cos r is rational implies r in {(PI + ((2 * PI) * i)),(((4 * PI) / 3) + ((2 * PI) * i)),(((3 * PI) / 2) + ((2 * PI) * i))} )
set a = (2 * PI) * i;
set R = r - ((2 * PI) * i);
assume ( PI + ((2 * PI) * i) <= r & r <= ((3 * PI) / 2) + ((2 * PI) * i) ) ; :: thesis: ( not r / PI is rational or not cos r is rational or r in {(PI + ((2 * PI) * i)),(((4 * PI) / 3) + ((2 * PI) * i)),(((3 * PI) / 2) + ((2 * PI) * i))} )
then A1: ( (PI + ((2 * PI) * i)) - ((2 * PI) * i) <= r - ((2 * PI) * i) & r - ((2 * PI) * i) <= (((3 * PI) / 2) + ((2 * PI) * i)) - ((2 * PI) * i) ) by XREAL_1:9;
assume A2: ( r / PI is rational & cos r is rational ) ; :: thesis: r in {(PI + ((2 * PI) * i)),(((4 * PI) / 3) + ((2 * PI) * i)),(((3 * PI) / 2) + ((2 * PI) * i))}
((2 * PI) * i) / PI = ((2 * i) * PI) / PI
.= 2 * i by XCMPLX_1:89 ;
then A3: (r - ((2 * PI) * i)) / PI = (r / PI) - (2 * i) ;
r - ((2 * PI) * i) = ((2 * PI) * (- i)) + r ;
then cos r = cos (r - ((2 * PI) * i)) by COMPLEX2:9;
then r - ((2 * PI) * i) in {PI,((4 * PI) / 3),((3 * PI) / 2)} by A1, A2, A3, Th57;
then ( r - ((2 * PI) * i) = PI or r - ((2 * PI) * i) = (4 * PI) / 3 or r - ((2 * PI) * i) = (3 * PI) / 2 ) by ENUMSET1:def 1;
hence r in {(PI + ((2 * PI) * i)),(((4 * PI) / 3) + ((2 * PI) * i)),(((3 * PI) / 2) + ((2 * PI) * i))} by ENUMSET1:def 1; :: thesis: verum