let i be Integer; :: thesis: ( (i |^ 4) mod 8 = 0 or (i |^ 4) mod 8 = 1 )
A1: (i |^ (2 + 2)) mod 8 = ((i |^ 2) * (i |^ 2)) mod 8 by NEWTON:8
.= (((i |^ 2) mod 8) * ((i |^ 2) mod 8)) mod 8 by NAT_D:67 ;

per cases ( (i |^ 2) mod 8 = 0 or (i |^ 2) mod 8 = 1 or (i |^ 2) mod 8 = 4 ) by MOS8;

suppose (i |^ 2) mod 8 = 0 ; :: thesis: ( (i |^ 4) mod 8 = 0 or (i |^ 4) mod 8 = 1 )

hence ( (i |^ 4) mod 8 = 0 or (i |^ 4) mod 8 = 1 ) by A1; :: thesis: verum

end;

suppose (i |^ 2) mod 8 = 1 ; :: thesis: ( (i |^ 4) mod 8 = 0 or (i |^ 4) mod 8 = 1 )

hence ( (i |^ 4) mod 8 = 0 or (i |^ 4) mod 8 = 1 ) by A1; :: thesis: verum

end;

suppose (i |^ 2) mod 8 = 4 ; :: thesis: ( (i |^ 4) mod 8 = 0 or (i |^ 4) mod 8 = 1 )

then (i |^ (2 + 2)) mod 8 = ((2 * 8) + 0) mod 8 by A1
.= 0 ;
hence ( (i |^ 4) mod 8 = 0 or (i |^ 4) mod 8 = 1 ) ; :: thesis: verum

end;

end;