Theorem blen1

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

	Ref	Expression
Assertion	blen1

Proof

Step	Hyp	Ref	Expression
1		1nn	$$⊢1\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		logb1	$$⊢\left(2\in ℂ\wedge 2\ne 0\wedge 2\ne 1\right)\to {\log }_{2}1=0$$
8	3 4 6 7	mp3an	$$⊢{\log }_{2}1=0$$
9	8	fveq2i	$$⊢⌊{\log }_{2}1⌋=⌊0⌋$$
10		0z	$$⊢0\in \mathbb{Z}$$
11		flid	$$⊢0\in \mathbb{Z}\to ⌊0⌋=0$$
12	10 11	ax-mp	$$⊢⌊0⌋=0$$
13	9 12	eqtri	$$⊢⌊{\log }_{2}1⌋=0$$
14	13	a1i	$$⊢1\in \mathbb{N}\to ⌊{\log }_{2}1⌋=0$$
15	14	oveq1d	$$⊢1\in \mathbb{N}\to ⌊{\log }_{2}1⌋+1=0+1$$
16		0p1e1	$$⊢0+1=1$$
17	15 16	eqtrdi	$$⊢1\in \mathbb{N}\to ⌊{\log }_{2}1⌋+1=1$$
18	2 17	eqtrd
19	1 18	ax-mp