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