Theorem blenpw2

Description: The binary length of a power of 2 is the exponent plus 1. (Contributed by AV, 30-May-2020)

	Ref	Expression
Assertion	blenpw2	⊢ ( 𝐼 ∈ ℕ0 → ( #b ‘ ( 2 ↑ 𝐼 ) ) = ( 𝐼 + 1 ) )

Proof

Step	Hyp	Ref	Expression
1		2nn	⊢ 2 ∈ ℕ
2		nnexpcl	⊢ ( ( 2 ∈ ℕ ∧ 𝐼 ∈ ℕ0 ) → ( 2 ↑ 𝐼 ) ∈ ℕ )
3	1 2	mpan	⊢ ( 𝐼 ∈ ℕ0 → ( 2 ↑ 𝐼 ) ∈ ℕ )
4		blennn	⊢ ( ( 2 ↑ 𝐼 ) ∈ ℕ → ( #b ‘ ( 2 ↑ 𝐼 ) ) = ( ( ⌊ ‘ ( 2 logb ( 2 ↑ 𝐼 ) ) ) + 1 ) )
5	3 4	syl	⊢ ( 𝐼 ∈ ℕ0 → ( #b ‘ ( 2 ↑ 𝐼 ) ) = ( ( ⌊ ‘ ( 2 logb ( 2 ↑ 𝐼 ) ) ) + 1 ) )
6		2z	⊢ 2 ∈ ℤ
7		uzid	⊢ ( 2 ∈ ℤ → 2 ∈ ( ℤ≥ ‘ 2 ) )
8	6 7	mp1i	⊢ ( 𝐼 ∈ ℕ0 → 2 ∈ ( ℤ≥ ‘ 2 ) )
9		nn0z	⊢ ( 𝐼 ∈ ℕ0 → 𝐼 ∈ ℤ )
10		nnlogbexp	⊢ ( ( 2 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐼 ∈ ℤ ) → ( 2 logb ( 2 ↑ 𝐼 ) ) = 𝐼 )
11	8 9 10	syl2anc	⊢ ( 𝐼 ∈ ℕ0 → ( 2 logb ( 2 ↑ 𝐼 ) ) = 𝐼 )
12	11	fveq2d	⊢ ( 𝐼 ∈ ℕ0 → ( ⌊ ‘ ( 2 logb ( 2 ↑ 𝐼 ) ) ) = ( ⌊ ‘ 𝐼 ) )
13		flid	⊢ ( 𝐼 ∈ ℤ → ( ⌊ ‘ 𝐼 ) = 𝐼 )
14	9 13	syl	⊢ ( 𝐼 ∈ ℕ0 → ( ⌊ ‘ 𝐼 ) = 𝐼 )
15	12 14	eqtrd	⊢ ( 𝐼 ∈ ℕ0 → ( ⌊ ‘ ( 2 logb ( 2 ↑ 𝐼 ) ) ) = 𝐼 )
16	15	oveq1d	⊢ ( 𝐼 ∈ ℕ0 → ( ( ⌊ ‘ ( 2 logb ( 2 ↑ 𝐼 ) ) ) + 1 ) = ( 𝐼 + 1 ) )
17	5 16	eqtrd	⊢ ( 𝐼 ∈ ℕ0 → ( #b ‘ ( 2 ↑ 𝐼 ) ) = ( 𝐼 + 1 ) )