let r be Real; ( r / PI is rational & cos r is rational implies cos r in {0,1,(- 1),(1 / 2),(- (1 / 2))} )
consider i being Integer such that
A0:
( (2 * PI) * i <= r & r <= (2 * PI) * (i + 1) )
by Th16;
set a = (2 * PI) * i;
set R = r - ((2 * PI) * i);
A2:
( ((2 * PI) * i) - ((2 * PI) * i) <= r - ((2 * PI) * i) & r - ((2 * PI) * i) <= ((2 * PI) + ((2 * PI) * i)) - ((2 * PI) * i) )
by A0, XREAL_1:9;
assume A3:
( r / PI is rational & cos r is rational )
; cos r in {0,1,(- 1),(1 / 2),(- (1 / 2))}
((2 * PI) * i) / PI =
((2 * i) * PI) / PI
.=
2 * i
by XCMPLX_1:89
;
then A4:
(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;
hence
cos r in {0,1,(- 1),(1 / 2),(- (1 / 2))}
by A2, A3, A4, Lm4; verum