theorem P136a: :: NUMBER12:52

for k being Nat st k >= 1 holds
PrimeDivisors ((2 |^ k) * ((2 |^ k) - 2)) = {2} \/ (PrimeDivisors ((2 |^ (k -' 1)) - 1))