let r be Real; :: thesis: ( PI <= r & r <= (3 * PI) / 2 & r / PI is rational & sin r is rational implies r in {PI,((7 * PI) / 6),((3 * PI) / 2)} )
set R = r - PI;
assume ( PI <= r & r <= (3 * PI) / 2 ) ; :: thesis: ( not r / PI is rational or not sin r is rational or r in {PI,((7 * PI) / 6),((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 & sin r is rational ) ; :: thesis: r in {PI,((7 * PI) / 6),((3 * PI) / 2)}
A3: (r - PI) / PI = (r / PI) - (PI / PI)
.= (r / PI) - 1 by XCMPLX_1:60 ;
sin (r - PI) = sin (- (PI - r))
.= - (sin (PI - r)) by SIN_COS:31
.= - (sin r) by EUCLID10:1 ;
then r - PI in {0,(PI / 6),(PI / 2)} by A1, A2, A3, Th62;
then ( r - PI = 0 or r - PI = PI / 6 or r - PI = PI / 2 ) by ENUMSET1:def 1;
hence r in {PI,((7 * PI) / 6),((3 * PI) / 2)} by ENUMSET1:def 1; :: thesis: verum