let i be Integer; :: thesis: ( i is even implies (i |^ 3) mod 8 = 0 )
assume i is even ; :: thesis: (i |^ 3) mod 8 = 0
then consider j being Integer such that
A1: i = 2 * j by ABIAN:11;
thus (i |^ 3) mod 8 = ((2 |^ 3) * (j |^ 3)) mod 8 by A1, NEWTON:7
.= (((2 * 2) * 2) * (j |^ 3)) mod 8 by POLYEQ_5:2
.= 0 by BINARI_4:20 ; :: thesis: verum