let b be Nat; :: thesis: ( b > 0 implies ex n being Nat st
( b >= 2 |^ n & b < 2 |^ (n + 1) ) )

assume b > 0 ; :: thesis: ex n being Nat st
( b >= 2 |^ n & b < 2 |^ (n + 1) )

then consider a being Nat such that
A0: b = 1 + a by ;
ex n being Nat st
( a + 1 >= 2 |^ n & a + 1 < 2 |^ (n + 1) )
proof
defpred S1[ Nat] means ex n being Nat st
( \$1 + 1 >= 2 |^ n & \$1 + 1 < 2 |^ (n + 1) );
( 0 + 1 >= 1 * (2 |^ 0) & 0 + 1 < 2 |^ (0 + 1) ) ;
then A1: S1[ 0 ] ;
A2: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume S1[k] ; :: thesis: S1[k + 1]
then consider n being Nat such that
B1: ( k + 1 >= 2 |^ n & k + 1 < 2 |^ (n + 1) ) ;
per cases ) + 1 < 2 |^ (n + 1) or (k + 1) + 1 >= 2 |^ (n + 1) ) ;
suppose C1: (k + 1) + 1 < 2 |^ (n + 1) ; :: thesis: S1[k + 1]
(k + 1) + 1 > (k + 1) + 0 by XREAL_1:6;
then (k + 1) + 1 >= 2 |^ n by ;
hence S1[k + 1] by C1; :: thesis: verum
end;
suppose C1: (k + 1) + 1 >= 2 |^ (n + 1) ; :: thesis: S1[k + 1]
2 * (k + 1) < 2 * (2 |^ (n + 1)) by ;
then C2: (2 * k) + 2 < 2 |^ ((n + 1) + 1) by NEWTON:6;
(k + 2) + 0 <= (k + 2) + k by XREAL_1:6;
then (k + 1) + 1 < 2 |^ ((n + 1) + 1) by ;
hence S1[k + 1] by C1; :: thesis: verum
end;
end;
end;
for c being Nat holds S1[c] from NAT_1:sch 2(A1, A2);
hence ex n being Nat st
( a + 1 >= 2 |^ n & a + 1 < 2 |^ (n + 1) ) ; :: thesis: verum
end;
hence ex n being Nat st
( b >= 2 |^ n & b < 2 |^ (n + 1) ) by A0; :: thesis: verum