theorem Th42: :: NUMBER13:42

for m, n being Nat st ( m is even or m = 2 * n ) holds
(2 |^ m) mod 3 = 1