let r be Real; ( (3 * PI) / 2 <= r & r <= 2 * PI & r / PI is rational & cos r is rational implies r in {((3 * PI) / 2),((5 * PI) / 3),(2 * PI)} )
set R = (2 * PI) - r;
assume
( (3 * PI) / 2 <= r & r <= 2 * PI )
; ( not r / PI is rational or not cos r is rational or r in {((3 * PI) / 2),((5 * PI) / 3),(2 * PI)} )
then A1:
( (2 * PI) - (2 * PI) <= (2 * PI) - r & (2 * PI) - r <= (2 * PI) - ((3 * PI) / 2) )
by XREAL_1:13;
assume A2:
( r / PI is rational & cos r is rational )
; r in {((3 * PI) / 2),((5 * PI) / 3),(2 * PI)}
A3: ((2 * PI) - r) / PI =
((2 * PI) / PI) - (r / PI)
.=
2 - (r / PI)
by XCMPLX_1:89
;
cos ((2 * PI) - r) = cos r
by EUCLID10:4;
then
(2 * PI) - r in {0,(PI / 3),(PI / 2)}
by A1, A2, A3, Th53;
then
( (2 * PI) - r = 0 or (2 * PI) - r = PI / 3 or (2 * PI) - r = PI / 2 )
by ENUMSET1:def 1;
hence
r in {((3 * PI) / 2),((5 * PI) / 3),(2 * PI)}
by ENUMSET1:def 1; verum