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	⊢ ( 𝑁 ∈ ℕ → ( 𝑁 = ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ∨ 𝑁 ∈ ( ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ..^ ( 2 ↑ ( #b ‘ 𝑁 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		nnpw2blenfzo	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ..^ ( 2 ↑ ( #b ‘ 𝑁 ) ) ) )
2		elfzolborelfzop1	⊢ ( 𝑁 ∈ ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ..^ ( 2 ↑ ( #b ‘ 𝑁 ) ) ) → ( 𝑁 = ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ∨ 𝑁 ∈ ( ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ..^ ( 2 ↑ ( #b ‘ 𝑁 ) ) ) ) )
3	1 2	syl	⊢ ( 𝑁 ∈ ℕ → ( 𝑁 = ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ∨ 𝑁 ∈ ( ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ..^ ( 2 ↑ ( #b ‘ 𝑁 ) ) ) ) )