Theorem blen2

Description: The binary length of 2. (Contributed by AV, 21-May-2020)

	Ref	Expression
Assertion	blen2

Proof

Step	Hyp	Ref	Expression
1		2nn	$$⊢2\in \mathbb{N}$$
2		blennn
3		2cn	$$⊢2\in ℂ$$
4		2ne0	$$⊢2\ne 0$$
5		1ne2	$$⊢1\ne 2$$
6	5	necomi	$$⊢2\ne 1$$
7		logbid1	$$⊢\left(2\in ℂ\wedge 2\ne 0\wedge 2\ne 1\right)\to {\log }_{2}2=1$$
8	3 4 6 7	mp3an	$$⊢{\log }_{2}2=1$$
9	8	fveq2i	$$⊢⌊{\log }_{2}2⌋=⌊1⌋$$
10		1z	$$⊢1\in \mathbb{Z}$$
11		flid	$$⊢1\in \mathbb{Z}\to ⌊1⌋=1$$
12	10 11	ax-mp	$$⊢⌊1⌋=1$$
13	9 12	eqtri	$$⊢⌊{\log }_{2}2⌋=1$$
14	13	a1i	$$⊢2\in \mathbb{N}\to ⌊{\log }_{2}2⌋=1$$
15	14	oveq1d	$$⊢2\in \mathbb{N}\to ⌊{\log }_{2}2⌋+1=1+1$$
16		1p1e2	$$⊢1+1=2$$
17	16	a1i	$$⊢2\in \mathbb{N}\to 1+1=2$$
18	2 15 17	3eqtrd
19	1 18	ax-mp