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

Proof

Step	Hyp	Ref	Expression
1		2nn	$$⊢2\in \mathbb{N}$$
2		nnexpcl	$$⊢\left(2\in \mathbb{N}\wedge I\in {\mathbb{N}}_0\right)\to 2^I\in \mathbb{N}$$
3	1 2	mpan	$$⊢I\in {\mathbb{N}}_0\to 2^I\in \mathbb{N}$$
4		blennn
5	3 4	syl
6		2z	$$⊢2\in \mathbb{Z}$$
7		uzid	$$⊢2\in \mathbb{Z}\to 2\in {\mathbb{Z}}_{\ge 2}$$
8	6 7	mp1i	$$⊢I\in {\mathbb{N}}_0\to 2\in {\mathbb{Z}}_{\ge 2}$$
9		nn0z	$$⊢I\in {\mathbb{N}}_0\to I\in \mathbb{Z}$$
10		nnlogbexp	$$⊢\left(2\in {\mathbb{Z}}_{\ge 2}\wedge I\in \mathbb{Z}\right)\to {\log }_2{2}^I=I$$
11	8 9 10	syl2anc	$$⊢I\in {\mathbb{N}}_0\to {\log }_2{2}^I=I$$
12	11	fveq2d	$$⊢I\in {\mathbb{N}}_0\to ⌊{\log }_2{2}^I⌋=⌊I⌋$$
13		flid	$$⊢I\in \mathbb{Z}\to ⌊I⌋=I$$
14	9 13	syl	$$⊢I\in {\mathbb{N}}_0\to ⌊I⌋=I$$
15	12 14	eqtrd	$$⊢I\in {\mathbb{N}}_0\to ⌊{\log }_2{2}^I⌋=I$$
16	15	oveq1d	$$⊢I\in {\mathbb{N}}_0\to ⌊{\log }_2{2}^I⌋+1=I+1$$
17	5 16	eqtrd