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

per cases then ( i mod (7 + 1) = 0 or i mod (7 + 1) = 1 or i mod (7 + 1) = 2 or i mod (7 + 1) = 3 or i mod (7 + 1) = 4 or i mod (7 + 1) = 5 or i mod (7 + 1) = 6 or i mod (7 + 1) = 7 ) ;

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

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

end;

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

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

end;

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

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

end;

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

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

end;

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

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

end;

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

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

end;

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

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

end;

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

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

end;

end;