let x be Nat; :: thesis: ( x <> 0 implies ex n being Nat st
( 2 to_power n <= x & x < 2 to_power (n + 1) ) )
assume x <> 0 ; :: thesis: ex n being Nat st
( 2 to_power n <= x & x < 2 to_power (n + 1) )
then P1: 1 <= x by NAT_1:25;
defpred S₁[ Nat] means x < 2 to_power $1;
A2: ex m being Nat st S₁[m] by LM000;
consider k being Nat such that
A3: ( S₁[k] & ( for n being Nat st S₁[n] holds
k <= n ) ) from NAT_1:sch 5(A2);
k <> 0 by P1, POWER:24, A3;
then 1 <= k by NAT_1:25;
then 0 <= k - 1 by XREAL_1:48;
then reconsider k1 = k - 1 as Nat by INT_1:3, ORDINAL1:def 12;
take k1 ; :: thesis: ( 2 to_power k1 <= x & x < 2 to_power (k1 + 1) )
thus 2 to_power k1 <= x :: thesis: x < 2 to_power (k1 + 1)

proof

assume ASP1: not 2 to_power k1 <= x ; :: thesis: contradiction
k - 1 < k - 0 by XREAL_1:15;
hence contradiction by A3, ASP1; :: thesis: verum

end;

thus x < 2 to_power (k1 + 1) by A3; :: thesis: verum