theorem MersenneTh: :: NUMBER18:31
for n, k, m being Nat st n > 1 & m > 1 holds
Mersenne n <> k |^ m