let n be Nat; :: thesis: ( (n ^2) mod 8 = 0 or (n ^2) mod 8 = 1 or (n ^2) mod 8 = 4 )
consider k being Nat such that
A1: ( n = 8 * k or n = (8 * k) + 1 or n = (8 * k) + 2 or n = (8 * k) + 3 or n = (8 * k) + 4 or n = (8 * k) + 5 or n = (8 * k) + 6 or n = (8 * k) + 7 ) by NUMBER02:28;
set a = n mod 8;
A2: (n ^2) mod 8 = ((n mod 8) * (n mod 8)) mod 8 by NAT_D:67;

per cases ( n = (8 * k) + 0 or n = (8 * k) + 1 or n = (8 * k) + 2 or n = (8 * k) + 3 or n = (8 * k) + 4 or n = (8 * k) + 5 or n = (8 * k) + 6 or n = (8 * k) + 7 ) by A1;

suppose n = (8 * k) + 0 ; :: thesis: ( (n ^2) mod 8 = 0 or (n ^2) mod 8 = 1 or (n ^2) mod 8 = 4 )

hence ( (n ^2) mod 8 = 0 or (n ^2) mod 8 = 1 or (n ^2) mod 8 = 4 ) by A2; :: thesis: verum

end;

suppose n = (8 * k) + 1 ; :: thesis: ( (n ^2) mod 8 = 0 or (n ^2) mod 8 = 1 or (n ^2) mod 8 = 4 )

then n mod 8 = 1 mod 8 by NAT_D:61
.= 1 by NAT_D:24 ;
hence ( (n ^2) mod 8 = 0 or (n ^2) mod 8 = 1 or (n ^2) mod 8 = 4 ) by A2; :: thesis: verum

end;

suppose n = (8 * k) + 2 ; :: thesis: ( (n ^2) mod 8 = 0 or (n ^2) mod 8 = 1 or (n ^2) mod 8 = 4 )

then n mod 8 = 2 mod 8 by NAT_D:61
.= 2 by NAT_D:24 ;
hence ( (n ^2) mod 8 = 0 or (n ^2) mod 8 = 1 or (n ^2) mod 8 = 4 ) by A2, NAT_D:24; :: thesis: verum

end;

suppose n = (8 * k) + 3 ; :: thesis: ( (n ^2) mod 8 = 0 or (n ^2) mod 8 = 1 or (n ^2) mod 8 = 4 )

then A3: n mod 8 = 3 mod 8 by NAT_D:61
.= 3 by NAT_D:24 ;
(1 + (1 * 8)) mod 8 = 1 mod 8 by NAT_D:61;
hence ( (n ^2) mod 8 = 0 or (n ^2) mod 8 = 1 or (n ^2) mod 8 = 4 ) by A2, A3, NAT_D:24; :: thesis: verum

end;

suppose n = (8 * k) + 4 ; :: thesis: ( (n ^2) mod 8 = 0 or (n ^2) mod 8 = 1 or (n ^2) mod 8 = 4 )

then A4: n mod 8 = 4 mod 8 by NAT_D:61
.= 4 by NAT_D:24 ;
(0 + (2 * 8)) mod 8 = 0 mod 8 ;
hence ( (n ^2) mod 8 = 0 or (n ^2) mod 8 = 1 or (n ^2) mod 8 = 4 ) by A2, A4; :: thesis: verum

end;

suppose n = (8 * k) + 5 ; :: thesis: ( (n ^2) mod 8 = 0 or (n ^2) mod 8 = 1 or (n ^2) mod 8 = 4 )

then A5: n mod 8 = 5 mod 8 by NAT_D:61
.= 5 by NAT_D:24 ;
(1 + (3 * 8)) mod 8 = 1 mod 8 by NAT_D:61;
hence ( (n ^2) mod 8 = 0 or (n ^2) mod 8 = 1 or (n ^2) mod 8 = 4 ) by A2, A5, NAT_D:24; :: thesis: verum

end;

suppose n = (8 * k) + 6 ; :: thesis: ( (n ^2) mod 8 = 0 or (n ^2) mod 8 = 1 or (n ^2) mod 8 = 4 )

then A6: n mod 8 = 6 mod 8 by NAT_D:61
.= 6 by NAT_D:24 ;
(4 + (4 * 8)) mod 8 = 4 mod 8 by NAT_D:61;
hence ( (n ^2) mod 8 = 0 or (n ^2) mod 8 = 1 or (n ^2) mod 8 = 4 ) by A2, A6, NAT_D:24; :: thesis: verum

end;

suppose n = (8 * k) + 7 ; :: thesis: ( (n ^2) mod 8 = 0 or (n ^2) mod 8 = 1 or (n ^2) mod 8 = 4 )

then A7: n mod 8 = 7 mod 8 by NAT_D:61
.= 7 by NAT_D:24 ;
(1 + (6 * 8)) mod 8 = 1 mod 8 by NAT_D:61;
hence ( (n ^2) mod 8 = 0 or (n ^2) mod 8 = 1 or (n ^2) mod 8 = 4 ) by A2, A7, NAT_D:24; :: thesis: verum

end;

end;