let r be Real; :: thesis: ( 0 <= r & r <= 2 * PI & r / PI is rational & sin r is rational implies sin r in {0,1,(- 1),(1 / 2),(- (1 / 2))} )
assume A1: ( 0 <= r & r <= 2 * PI ) ; :: thesis: ( not r / PI is rational or not sin r is rational or sin r in {0,1,(- 1),(1 / 2),(- (1 / 2))} )
assume A2: ( r / PI is rational & sin r is rational ) ; :: thesis: sin r in {0,1,(- 1),(1 / 2),(- (1 / 2))}
per cases ( ( 0 <= r & r <= PI / 2 ) or ( PI / 2 <= r & r <= PI ) or ( PI <= r & r <= (3 * PI) / 2 ) or ( (3 * PI) / 2 <= r & r <= 2 * PI ) ) by A1;
suppose ( 0 <= r & r <= PI / 2 ) ; :: thesis: sin r in {0,1,(- 1),(1 / 2),(- (1 / 2))}
then r in {0,(PI / 6),(PI / 2)} by A2, Th62;
then ( r = 0 or r = PI / 6 or r = PI / 2 ) by ENUMSET1:def 1;
hence sin r in {0,1,(- 1),(1 / 2),(- (1 / 2))} by ENUMSET1:def 3, SIN_COS:31, SIN_COS:77, EUCLID10:17; :: thesis: verum
end;
suppose ( PI / 2 <= r & r <= PI ) ; :: thesis: sin r in {0,1,(- 1),(1 / 2),(- (1 / 2))}
then r in {(PI / 2),((5 * PI) / 6),PI} by A2, Th64;
then ( r = PI / 2 or r = (5 * PI) / 6 or r = PI ) by ENUMSET1:def 1;
hence sin r in {0,1,(- 1),(1 / 2),(- (1 / 2))} by ENUMSET1:def 3, Th5, SIN_COS:77; :: thesis: verum
end;
suppose ( PI <= r & r <= (3 * PI) / 2 ) ; :: thesis: sin r in {0,1,(- 1),(1 / 2),(- (1 / 2))}
then r in {PI,((7 * PI) / 6),((3 * PI) / 2)} by A2, Th66;
then ( r = PI or r = (7 * PI) / 6 or r = (3 * PI) / 2 ) by ENUMSET1:def 1;
hence sin r in {0,1,(- 1),(1 / 2),(- (1 / 2))} by ENUMSET1:def 3, Th7, SIN_COS:77; :: thesis: verum
end;
suppose ( (3 * PI) / 2 <= r & r <= 2 * PI ) ; :: thesis: sin r in {0,1,(- 1),(1 / 2),(- (1 / 2))}
then r in {((3 * PI) / 2),((11 * PI) / 6),(2 * PI)} by A2, Th68;
then ( r = (3 * PI) / 2 or r = (11 * PI) / 6 or r = 2 * PI ) by ENUMSET1:def 1;
hence sin r in {0,1,(- 1),(1 / 2),(- (1 / 2))} by ENUMSET1:def 3, Th9, SIN_COS:77; :: thesis: verum
end;
end;