let r be Real; :: thesis: ( (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 ) ; :: thesis: ( 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 ) ; :: thesis: 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; :: thesis: verum