let i be Integer; :: thesis: ( i is even implies (i ^2 ) mod 4 = 0 )
assume i is even ; :: thesis: (i ^2 ) mod 4 = 0
then consider i9 being Integer such that
A1: i = 2 * i9 by ABIAN:def 1;
i ^2 = (4 * (i9 ^2 )) + 0 by A1;
hence (i ^2 ) mod 4 = 0 mod 4 by EULER_1:13
.= 0 by NAT_D:24 ;
:: thesis: verum