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 NAT_1:10, NAT_1:14;
ex n being Nat st
( a + 1 >= 2 |^ n & a + 1 < 2 |^ (n + 1) )

proof

defpred S₁[ 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: S₁[ 0 ] ;
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume S₁[k] ; :: thesis: S₁[k + 1]
then consider n being Nat such that
B1: ( k + 1 >= 2 |^ n & k + 1 < 2 |^ (n + 1) ) ;

per cases ( (k + 1) + 1 < 2 |^ (n + 1) or (k + 1) + 1 >= 2 |^ (n + 1) ) ;

suppose C1: (k + 1) + 1 < 2 |^ (n + 1) ; :: thesis: S₁[k + 1]

(k + 1) + 1 > (k + 1) + 0 by XREAL_1:6;
then (k + 1) + 1 >= 2 |^ n by B1, XXREAL_0:2;
hence S₁[k + 1] by C1; :: thesis: verum

end;

suppose C1: (k + 1) + 1 >= 2 |^ (n + 1) ; :: thesis: S₁[k + 1]

2 * (k + 1) < 2 * (2 |^ (n + 1)) by B1, XREAL_1:68;
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 C2, XXREAL_0:2;
hence S₁[k + 1] by C1; :: thesis: verum

end;

end;

end;

for c being Nat holds S₁[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