theorem :: NEWTON02:187

for n, k, l being Nat holds
( not 2 |^ (k + l) divides (2 |^ (n + k)) - (2 |^ k) or l = 0 or n = 0 )