let n, k, l be Nat; :: thesis: ( 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) ; :: thesis: ( 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; :: thesis: verum

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) ; :: thesis: ( 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; :: thesis: verum