theorem Th73: :: NUMBER08:73

for m, n being Nat holds
( not (3 |^ n) - (2 |^ m) = 1 or ( n = m & m = 1 ) or ( n = 2 & m = 3 ) )