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

Proof

Step	Hyp	Ref	Expression
1		nnpw2blen	⊢ ( 𝑁 ∈ ℕ → ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ≤ 𝑁 ∧ 𝑁 < ( 2 ↑ ( #b ‘ 𝑁 ) ) ) )
2		nnz	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
3		2z	⊢ 2 ∈ ℤ
4		blennnelnn	⊢ ( 𝑁 ∈ ℕ → ( #b ‘ 𝑁 ) ∈ ℕ )
5		nnm1nn0	⊢ ( ( #b ‘ 𝑁 ) ∈ ℕ → ( ( #b ‘ 𝑁 ) − 1 ) ∈ ℕ0 )
6	4 5	syl	⊢ ( 𝑁 ∈ ℕ → ( ( #b ‘ 𝑁 ) − 1 ) ∈ ℕ0 )
7		zexpcl	⊢ ( ( 2 ∈ ℤ ∧ ( ( #b ‘ 𝑁 ) − 1 ) ∈ ℕ0 ) → ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ∈ ℤ )
8	3 6 7	sylancr	⊢ ( 𝑁 ∈ ℕ → ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ∈ ℤ )
9	4	nnnn0d	⊢ ( 𝑁 ∈ ℕ → ( #b ‘ 𝑁 ) ∈ ℕ0 )
10		zexpcl	⊢ ( ( 2 ∈ ℤ ∧ ( #b ‘ 𝑁 ) ∈ ℕ0 ) → ( 2 ↑ ( #b ‘ 𝑁 ) ) ∈ ℤ )
11	3 9 10	sylancr	⊢ ( 𝑁 ∈ ℕ → ( 2 ↑ ( #b ‘ 𝑁 ) ) ∈ ℤ )
12		elfzo	⊢ ( ( 𝑁 ∈ ℤ ∧ ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ∈ ℤ ∧ ( 2 ↑ ( #b ‘ 𝑁 ) ) ∈ ℤ ) → ( 𝑁 ∈ ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ..^ ( 2 ↑ ( #b ‘ 𝑁 ) ) ) ↔ ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ≤ 𝑁 ∧ 𝑁 < ( 2 ↑ ( #b ‘ 𝑁 ) ) ) ) )
13	2 8 11 12	syl3anc	⊢ ( 𝑁 ∈ ℕ → ( 𝑁 ∈ ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ..^ ( 2 ↑ ( #b ‘ 𝑁 ) ) ) ↔ ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ≤ 𝑁 ∧ 𝑁 < ( 2 ↑ ( #b ‘ 𝑁 ) ) ) ) )
14	1 13	mpbird	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ..^ ( 2 ↑ ( #b ‘ 𝑁 ) ) ) )