let i be Integer; :: thesis: ( ((2 * i) ^2) mod 8 = 0 or ((2 * i) ^2) mod 8 = 4 )

per cases ( i >= 0 or i < 0 ) ;

suppose i >= 0 ; :: thesis: ( ((2 * i) ^2) mod 8 = 0 or ((2 * i) ^2) mod 8 = 4 )

then i in NAT by INT_1:3;
hence ( ((2 * i) ^2) mod 8 = 0 or ((2 * i) ^2) mod 8 = 4 ) by Lm14; :: thesis: verum

end;

suppose i < 0 ; :: thesis: ( ((2 * i) ^2) mod 8 = 0 or ((2 * i) ^2) mod 8 = 4 )

then A1: - i in NAT by INT_1:3;
(2 * i) ^2 = (2 * (- i)) ^2 ;
hence ( ((2 * i) ^2) mod 8 = 0 or ((2 * i) ^2) mod 8 = 4 ) by A1, Lm14; :: thesis: verum

end;

end;