let m, n be Nat; :: thesis: ( not (n * m) mod 4 = 1 or n mod 4 = 1 or n mod 4 = 3 )
assume that
A1: (n * m) mod 4 = 1 and
A2: ( n mod 4 <> 1 & n mod 4 <> 3 ) ; :: thesis: contradiction
not not n mod (3 + 1) = 0 & ... & not n mod (3 + 1) = 3 by NUMBER03:11;
hence contradiction by A1, A2, Th5; :: thesis: verum