theorem :: NUMBER12:56

for k, m, n being Nat st k >= 1 & m = (2 |^ k) - 2 & n = (2 |^ k) * ((2 |^ k) - 2) holds
( PrimeDivisors m = PrimeDivisors n & PrimeDivisors (m + 1) = PrimeDivisors (n + 1) )