Metamath Proof Explorer


Theorem nnpw2blenfzo

Description: A positive integer is between 2 to the power of the binary length of the integer minus 1, and 2 to the power of the binary length of the integer. (Contributed by AV, 2-Jun-2020)

Ref Expression
Assertion nnpw2blenfzo N N 2 # b N 1 ..^ 2 # b N

Proof

Step Hyp Ref Expression
1 nnpw2blen N 2 # b N 1 N N < 2 # b N
2 nnz N N
3 2z 2
4 blennnelnn N # b N
5 nnm1nn0 # b N # b N 1 0
6 4 5 syl N # b N 1 0
7 zexpcl 2 # b N 1 0 2 # b N 1
8 3 6 7 sylancr N 2 # b N 1
9 4 nnnn0d N # b N 0
10 zexpcl 2 # b N 0 2 # b N
11 3 9 10 sylancr N 2 # b N
12 elfzo N 2 # b N 1 2 # b N N 2 # b N 1 ..^ 2 # b N 2 # b N 1 N N < 2 # b N
13 2 8 11 12 syl3anc N N 2 # b N 1 ..^ 2 # b N 2 # b N 1 N N < 2 # b N
14 1 13 mpbird N N 2 # b N 1 ..^ 2 # b N