let m, n be Nat; :: thesis: ( 2 |^ m divides 2 |^ n implies m <= n )
( not m <= n implies not 2 |^ m divides 2 |^ n )
proof
assume A1: not m <= n ; :: thesis: not 2 |^ m divides 2 |^ n
not 2 |^ m divides 2 |^ n
proof
(2 |^ n) div (2 |^ m) = 0 by A1, Lm9, NAT_D:27;
then A2: 2 |^ n > (2 |^ m) * ((2 |^ n) div (2 |^ m)) by PREPOWER:6;
assume 2 |^ m divides 2 |^ n ; :: thesis: contradiction
hence contradiction by A2, NAT_D:3; :: thesis: verum
end;
hence not 2 |^ m divides 2 |^ n ; :: thesis: verum
end;
hence ( 2 |^ m divides 2 |^ n implies m <= n ) ; :: thesis: verum