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

per cases then ( i mod (3 + 1) = 0 or i mod (3 + 1) = 1 or i mod (3 + 1) = 2 or i mod (3 + 1) = 3 ) ;

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

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

end;

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

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

end;

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

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

end;

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

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

end;

end;