Theorem blenpw2m1

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

	Ref	Expression
Assertion	blenpw2m1	⊢ ( 𝐼 ∈ ℕ → ( #b ‘ ( ( 2 ↑ 𝐼 ) − 1 ) ) = 𝐼 )

Proof

Step	Hyp	Ref	Expression
1		2nn0	⊢ 2 ∈ ℕ0
2	1	a1i	⊢ ( 𝐼 ∈ ℕ → 2 ∈ ℕ0 )
3		nnnn0	⊢ ( 𝐼 ∈ ℕ → 𝐼 ∈ ℕ0 )
4	2 3	nn0expcld	⊢ ( 𝐼 ∈ ℕ → ( 2 ↑ 𝐼 ) ∈ ℕ0 )
5		nnge1	⊢ ( 𝐼 ∈ ℕ → 1 ≤ 𝐼 )
6		2cnd	⊢ ( 𝐼 ∈ ℕ → 2 ∈ ℂ )
7	6	exp1d	⊢ ( 𝐼 ∈ ℕ → ( 2 ↑ 1 ) = 2 )
8	7	eqcomd	⊢ ( 𝐼 ∈ ℕ → 2 = ( 2 ↑ 1 ) )
9	8	breq1d	⊢ ( 𝐼 ∈ ℕ → ( 2 ≤ ( 2 ↑ 𝐼 ) ↔ ( 2 ↑ 1 ) ≤ ( 2 ↑ 𝐼 ) ) )
10		2re	⊢ 2 ∈ ℝ
11	10	a1i	⊢ ( 𝐼 ∈ ℕ → 2 ∈ ℝ )
12		1zzd	⊢ ( 𝐼 ∈ ℕ → 1 ∈ ℤ )
13		nnz	⊢ ( 𝐼 ∈ ℕ → 𝐼 ∈ ℤ )
14		1lt2	⊢ 1 < 2
15	14	a1i	⊢ ( 𝐼 ∈ ℕ → 1 < 2 )
16	11 12 13 15	leexp2d	⊢ ( 𝐼 ∈ ℕ → ( 1 ≤ 𝐼 ↔ ( 2 ↑ 1 ) ≤ ( 2 ↑ 𝐼 ) ) )
17	9 16	bitr4d	⊢ ( 𝐼 ∈ ℕ → ( 2 ≤ ( 2 ↑ 𝐼 ) ↔ 1 ≤ 𝐼 ) )
18	5 17	mpbird	⊢ ( 𝐼 ∈ ℕ → 2 ≤ ( 2 ↑ 𝐼 ) )
19		nn0ge2m1nn	⊢ ( ( ( 2 ↑ 𝐼 ) ∈ ℕ0 ∧ 2 ≤ ( 2 ↑ 𝐼 ) ) → ( ( 2 ↑ 𝐼 ) − 1 ) ∈ ℕ )
20	4 18 19	syl2anc	⊢ ( 𝐼 ∈ ℕ → ( ( 2 ↑ 𝐼 ) − 1 ) ∈ ℕ )
21		blennn	⊢ ( ( ( 2 ↑ 𝐼 ) − 1 ) ∈ ℕ → ( #b ‘ ( ( 2 ↑ 𝐼 ) − 1 ) ) = ( ( ⌊ ‘ ( 2 logb ( ( 2 ↑ 𝐼 ) − 1 ) ) ) + 1 ) )
22	20 21	syl	⊢ ( 𝐼 ∈ ℕ → ( #b ‘ ( ( 2 ↑ 𝐼 ) − 1 ) ) = ( ( ⌊ ‘ ( 2 logb ( ( 2 ↑ 𝐼 ) − 1 ) ) ) + 1 ) )
23		logbpw2m1	⊢ ( 𝐼 ∈ ℕ → ( ⌊ ‘ ( 2 logb ( ( 2 ↑ 𝐼 ) − 1 ) ) ) = ( 𝐼 − 1 ) )
24	23	oveq1d	⊢ ( 𝐼 ∈ ℕ → ( ( ⌊ ‘ ( 2 logb ( ( 2 ↑ 𝐼 ) − 1 ) ) ) + 1 ) = ( ( 𝐼 − 1 ) + 1 ) )
25		nncn	⊢ ( 𝐼 ∈ ℕ → 𝐼 ∈ ℂ )
26		npcan1	⊢ ( 𝐼 ∈ ℂ → ( ( 𝐼 − 1 ) + 1 ) = 𝐼 )
27	25 26	syl	⊢ ( 𝐼 ∈ ℕ → ( ( 𝐼 − 1 ) + 1 ) = 𝐼 )
28	22 24 27	3eqtrd	⊢ ( 𝐼 ∈ ℕ → ( #b ‘ ( ( 2 ↑ 𝐼 ) − 1 ) ) = 𝐼 )