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) )

( b >= 2 |^ n & b < 2 |^ (n + 1) ) by A0; :: thesis: verum

( 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

hence
ex n being Nat st
defpred S_{1}[ 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_{1}[ 0 ]
;

A2: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
_{1}[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;( $1 + 1 >= 2 |^ n & $1 + 1 < 2 |^ (n + 1) );

( 0 + 1 >= 1 * (2 |^ 0) & 0 + 1 < 2 |^ (0 + 1) ) ;

then A1: S

A2: for k being Nat st S

S

proof

for c being Nat holds S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume S_{1}[k]
; :: thesis: S_{1}[k + 1]

then consider n being Nat such that

B1: ( k + 1 >= 2 |^ n & k + 1 < 2 |^ (n + 1) ) ;

end;assume S

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) )
;

end;

suppose C1:
(k + 1) + 1 < 2 |^ (n + 1)
; :: thesis: S_{1}[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_{1}[k + 1]
by C1; :: thesis: verum

end;then (k + 1) + 1 >= 2 |^ n by B1, XXREAL_0:2;

hence S

suppose C1:
(k + 1) + 1 >= 2 |^ (n + 1)
; :: thesis: S_{1}[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_{1}[k + 1]
by C1; :: thesis: verum

end;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

hence ex n being Nat st

( a + 1 >= 2 |^ n & a + 1 < 2 |^ (n + 1) ) ; :: thesis: verum

( b >= 2 |^ n & b < 2 |^ (n + 1) ) by A0; :: thesis: verum