theorem :: NEWTON06:77

for i being Integer holds
( (i |^ 4) mod 5 = 0 or (i |^ 4) mod 5 = 1 )