let b be Nat; ( b > 0 implies ex n being Nat st
( b >= 2 |^ n & b < 2 |^ (n + 1) ) )
assume
b > 0
; 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 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;
( S1[k] implies S1[k + 1] )
assume
S1[
k]
;
S1[k + 1]
then consider n being
Nat such that B1:
(
k + 1
>= 2
|^ n &
k + 1
< 2
|^ (n + 1) )
;
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) )
;
verum
end;
hence
ex n being Nat st
( b >= 2 |^ n & b < 2 |^ (n + 1) )
by A0; verum