let i be Integer; :: thesis: sin (PI * i) = 0
per cases ( i is even or i is odd ) ;
suppose i is even ; :: thesis: sin (PI * i) = 0
then consider j being Integer such that
A1: i = 2 * j by INT_1:def 3, ABIAN:def 1;
thus sin (PI * i) = sin (((2 * PI) * j) + 0) by A1
.= 0 by SIN_COS:31, COMPLEX2:8 ; :: thesis: verum
end;
suppose i is odd ; :: thesis: sin (PI * i) = 0
then consider j being Integer such that
A2: i = (2 * j) + 1 by ABIAN:1;
thus sin (PI * i) = sin (((2 * PI) * j) + PI) by A2
.= 0 by SIN_COS:77, COMPLEX2:8 ; :: thesis: verum
end;
end;