theorem P136b: :: NUMBER12:53

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