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