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

Proof

Step	Hyp	Ref	Expression
1		2nn0	$$⊢2\in {\mathbb{N}}_0$$
2	1	a1i	$$⊢I\in \mathbb{N}\to 2\in {\mathbb{N}}_0$$
3		nnnn0	$$⊢I\in \mathbb{N}\to I\in {\mathbb{N}}_0$$
4	2 3	nn0expcld	$$⊢I\in \mathbb{N}\to 2^I\in {\mathbb{N}}_0$$
5		nnge1	$$⊢I\in \mathbb{N}\to 1\le I$$
6		2cnd	$$⊢I\in \mathbb{N}\to 2\in ℂ$$
7	6	exp1d	$$⊢I\in \mathbb{N}\to 2^1=2$$
8	7	eqcomd	$$⊢I\in \mathbb{N}\to 2=2^1$$
9	8	breq1d	$$⊢I\in \mathbb{N}\to \left(2\le 2^I\leftrightarrow 2^1\le 2^I\right)$$
10		2re	$$⊢2\in ℝ$$
11	10	a1i	$$⊢I\in \mathbb{N}\to 2\in ℝ$$
12		1zzd	$$⊢I\in \mathbb{N}\to 1\in \mathbb{Z}$$
13		nnz	$$⊢I\in \mathbb{N}\to I\in \mathbb{Z}$$
14		1lt2	$$⊢1<2$$
15	14	a1i	$$⊢I\in \mathbb{N}\to 1<2$$
16	11 12 13 15	leexp2d	$$⊢I\in \mathbb{N}\to \left(1\le I\leftrightarrow 2^1\le 2^I\right)$$
17	9 16	bitr4d	$$⊢I\in \mathbb{N}\to \left(2\le 2^I\leftrightarrow 1\le I\right)$$
18	5 17	mpbird	$$⊢I\in \mathbb{N}\to 2\le 2^I$$
19		nn0ge2m1nn	$$⊢\left(2^I\in {\mathbb{N}}_0\wedge 2\le 2^I\right)\to 2^I-1\in \mathbb{N}$$
20	4 18 19	syl2anc	$$⊢I\in \mathbb{N}\to 2^I-1\in \mathbb{N}$$
21		blennn
22	20 21	syl
23		logbpw2m1	$$⊢I\in \mathbb{N}\to ⌊{\log }_2\left(2^I-1\right)⌋=I-1$$
24	23	oveq1d	$$⊢I\in \mathbb{N}\to ⌊{\log }_2\left(2^I-1\right)⌋+1=I-1+1$$
25		nncn	$$⊢I\in \mathbb{N}\to I\in ℂ$$
26		npcan1	$$⊢I\in ℂ\to I-1+1=I$$
27	25 26	syl	$$⊢I\in \mathbb{N}\to I-1+1=I$$
28	22 24 27	3eqtrd