theorem :: NUMBER10:61

for i being Integer holds
( (i ^2) mod 8 = 0 or (i ^2) mod 8 = 1 or (i ^2) mod 8 = 4 ) by Th59, Th60;