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