let m, n be Nat; :: thesis: ( not (n * m) mod 4 = 3 or ( n mod 4 = 1 & m mod 4 = 3 ) or ( n mod 4 = 3 & m mod 4 = 1 ) )
assume A1: (n * m) mod 4 = 3 ; :: thesis: ( ( n mod 4 = 1 & m mod 4 = 3 ) or ( n mod 4 = 3 & m mod 4 = 1 ) )
A2: not not m mod (3 + 1) = 0 & ... & not m mod (3 + 1) = 3 by NUMBER03:11;
not not n mod (3 + 1) = 0 & ... & not n mod (3 + 1) = 3 by NUMBER03:11;

per cases then ( n mod (3 + 1) = 1 or n mod (3 + 1) = 3 ) by A1, Th5;

suppose A3: n mod (3 + 1) = 1 ; :: thesis: ( ( n mod 4 = 1 & m mod 4 = 3 ) or ( n mod 4 = 3 & m mod 4 = 1 ) )

m mod (3 + 1) = 3

proof

assume m mod (3 + 1) <> 3 ; :: thesis: contradiction
then (n * m) mod 4 = (1 * n) mod 4 by A2, A1, Th5, RADIX_2:3;
hence contradiction by A1, A3; :: thesis: verum

end;

hence ( ( n mod 4 = 1 & m mod 4 = 3 ) or ( n mod 4 = 3 & m mod 4 = 1 ) ) by A3; :: thesis: verum

end;

suppose A4: n mod (3 + 1) = 3 ; :: thesis: ( ( n mod 4 = 1 & m mod 4 = 3 ) or ( n mod 4 = 3 & m mod 4 = 1 ) )

m mod (3 + 1) = 1

proof

A5: 3 * 3 = (4 * 2) + 1 ;
assume m mod (3 + 1) <> 1 ; :: thesis: contradiction
then (n * m) mod 4 = (3 * n) mod 4 by A2, A1, Th5, RADIX_2:3;
then (n * m) mod 4 = (3 * 3) mod 4 by A4, RADIX_2:3;
hence contradiction by A1, A5, NUMBER02:16; :: thesis: verum

end;

hence ( ( n mod 4 = 1 & m mod 4 = 3 ) or ( n mod 4 = 3 & m mod 4 = 1 ) ) by A4; :: thesis: verum

end;

end;