let m, n be Nat; :: thesis: ( ( not n mod 4 = 0 & not n mod 4 = 2 ) or (n * m) mod 4 = 0 or (n * m) mod 4 = 2 )
m = (2 * (m div 2)) + (m mod 2) by NAT_D:2;
then ( m = (2 * (m div 2)) + 0 or m = (2 * (m div 2)) + 1 ) by NAT_D:12;
then A1: ( 2 * m = (4 * (m div 2)) + 0 or 2 * m = (4 * (m div 2)) + (2 * 1) ) ;
assume ( n mod 4 = 0 or n mod 4 = 2 ) ; :: thesis: ( (n * m) mod 4 = 0 or (n * m) mod 4 = 2 )
then ( (m * n) mod 4 = (m * 0) mod 4 or (m * n) mod 4 = (m * 2) mod 4 ) by RADIX_2:3;
hence ( (n * m) mod 4 = 0 or (n * m) mod 4 = 2 ) by A1, NUMBER02:16; :: thesis: verum