theorem PreProb53: :: NUMBER18:18
for n being non zero Nat
for k, t being Nat st k >= 1 & n = ((2 |^ k) * t) + (2 |^ (k -' 1)) holds
k divides card (NatDivisors n)