let r be Real; :: thesis: ( r / PI is rational & sin r is rational implies sin 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 & sin r is rational ) ; :: thesis: sin 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 sin r = sin (r - ((2 * PI) * i)) by COMPLEX2:8;
hence sin r in {0,1,(- 1),(1 / 2),(- (1 / 2))} by A2, A3, A4, Lm5; :: thesis: verum