let i be Integer; :: thesis: cos ((PI / 2) + (PI * i)) = 0

per cases ( i is even or i is odd ) ;

suppose i is even ; :: thesis: cos ((PI / 2) + (PI * i)) = 0

then consider j being Integer such that
A1: i = 2 * j by INT_1:def 3, ABIAN:def 1;
thus cos ((PI / 2) + (PI * i)) = cos ((PI / 2) + ((2 * PI) * j)) by A1
.= cos (PI / 2) by COMPLEX2:9
.= 0 by SIN_COS:76 ; :: thesis: verum

end;

suppose i is odd ; :: thesis: cos ((PI / 2) + (PI * i)) = 0

then consider j being Integer such that
A2: i = (2 * j) + 1 by ABIAN:1;
thus cos ((PI / 2) + (PI * i)) = cos ((PI + (PI / 2)) + ((2 * PI) * j)) by A2
.= cos (PI + (PI / 2)) by COMPLEX2:9
.= 0 by SIN_COS:76 ; :: thesis: verum

end;

end;