let r be Real; for i being Integer st ((3 * PI) / 2) + ((2 * PI) * i) <= r & r <= (2 * PI) + ((2 * PI) * i) & r / PI is rational & cos r is rational holds
r in {(((3 * PI) / 2) + ((2 * PI) * i)),(((5 * PI) / 3) + ((2 * PI) * i)),((2 * PI) + ((2 * PI) * i))}
let i be Integer; ( ((3 * PI) / 2) + ((2 * PI) * i) <= r & r <= (2 * PI) + ((2 * PI) * i) & r / PI is rational & cos r is rational implies r in {(((3 * PI) / 2) + ((2 * PI) * i)),(((5 * PI) / 3) + ((2 * PI) * i)),((2 * PI) + ((2 * PI) * i))} )
set a = (2 * PI) * i;
set R = r - ((2 * PI) * i);
assume
( ((3 * PI) / 2) + ((2 * PI) * i) <= r & r <= (2 * PI) + ((2 * PI) * i) )
; ( not r / PI is rational or not cos r is rational or r in {(((3 * PI) / 2) + ((2 * PI) * i)),(((5 * PI) / 3) + ((2 * PI) * i)),((2 * PI) + ((2 * PI) * i))} )
then A1:
( (((3 * PI) / 2) + ((2 * PI) * i)) - ((2 * PI) * i) <= r - ((2 * PI) * i) & r - ((2 * PI) * i) <= ((2 * PI) + ((2 * PI) * i)) - ((2 * PI) * i) )
by XREAL_1:9;
assume A2:
( r / PI is rational & cos r is rational )
; r in {(((3 * PI) / 2) + ((2 * PI) * i)),(((5 * PI) / 3) + ((2 * PI) * i)),((2 * PI) + ((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 {((3 * PI) / 2),((5 * PI) / 3),(2 * PI)}
by A1, A2, A3, Th59;
then
( r - ((2 * PI) * i) = (3 * PI) / 2 or r - ((2 * PI) * i) = (5 * PI) / 3 or r - ((2 * PI) * i) = 2 * PI )
by ENUMSET1:def 1;
hence
r in {(((3 * PI) / 2) + ((2 * PI) * i)),(((5 * PI) / 3) + ((2 * PI) * i)),((2 * PI) + ((2 * PI) * i))}
by ENUMSET1:def 1; verum