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