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