let i be Integer; :: thesis: ( not i is even or (i ^2) mod 8 = 0 or (i ^2) mod 8 = 4 )
assume i is even ; :: thesis: ( (i ^2) mod 8 = 0 or (i ^2) mod 8 = 4 )
then ex j being Integer st i = 2 * j by ABIAN:11;
hence ( (i ^2) mod 8 = 0 or (i ^2) mod 8 = 4 ) by Lm15; :: thesis: verum