Metamath Proof Explorer

Theorem nnpw2blenfzo2

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

Ref Expression
Assertion nnpw2blenfzo2 ⊢ N ∈ ℕ → N = 2 # b ⁡ N − 1 ∨ N ∈ 2 # b ⁡ N − 1 + 1 ..^ 2 # b ⁡ N

Proof

Step Hyp Ref Expression
1 nnpw2blenfzo ⊢ N ∈ ℕ → N ∈ 2 # b ⁡ N − 1 ..^ 2 # b ⁡ N
2 elfzolborelfzop1 ⊢ N ∈ 2 # b ⁡ N − 1 ..^ 2 # b ⁡ N → N = 2 # b ⁡ N − 1 ∨ N ∈ 2 # b ⁡ N − 1 + 1 ..^ 2 # b ⁡ N
3 1 2 syl ⊢ N ∈ ℕ → N = 2 # b ⁡ N − 1 ∨ N ∈ 2 # b ⁡ N − 1 + 1 ..^ 2 # b ⁡ N