let n, k, l be Nat; ( not 2 |^ (k + l) divides (2 |^ (n + k)) - (2 |^ k) or l = 0 or n = 0 )
A0:
( 2 |^ (k + l) = (2 |^ k) * (2 |^ l) & 2 |^ (n + k) = (2 |^ n) * (2 |^ k) )
by NEWTON:8;
assume
2 |^ (k + l) divides (2 |^ (n + k)) - (2 |^ k)
; ( l = 0 or n = 0 )
then A2:
(2 |^ k) * (2 |^ l) divides (2 |^ k) * ((2 |^ n) - 1)
by A0;
reconsider a = (2 |^ n) - 1 as Element of NAT by INT_1:3;
reconsider b = 2 |^ l as Element of NAT by ORDINAL1:def 12;
reconsider c = 2 |^ k as Element of NAT by ORDINAL1:def 12;
A3:
( b divides a or c = 0 )
by A2, PYTHTRIP:7;
( 2 divides 2 |^ l or l = 0 )
by NAT_3:3;
hence
( l = 0 or n = 0 )
by Th88, INT_2:9, A3; verum