Theorem blennnelnn

Description: The binary length of a positive integer is a positive integer. (Contributed by AV, 25-May-2020)

	Ref	Expression
Assertion	blennnelnn

Proof

Step	Hyp	Ref	Expression
1		blennn
2		2rp	$$⊢2\in {ℝ}^{+}$$
3	2	a1i	$$⊢N\in \mathbb{N}\to 2\in {ℝ}^{+}$$
4		nnrp	$$⊢N\in \mathbb{N}\to N\in {ℝ}^{+}$$
5		1ne2	$$⊢1\ne 2$$
6	5	necomi	$$⊢2\ne 1$$
7	6	a1i	$$⊢N\in \mathbb{N}\to 2\ne 1$$
8		relogbcl	$$⊢\left(2\in {ℝ}^{+}\wedge N\in {ℝ}^{+}\wedge 2\ne 1\right)\to {\log }_{2}N\in ℝ$$
9	3 4 7 8	syl3anc	$$⊢N\in \mathbb{N}\to {\log }_{2}N\in ℝ$$
10		2z	$$⊢2\in \mathbb{Z}$$
11		uzid	$$⊢2\in \mathbb{Z}\to 2\in {\mathbb{Z}}_{\ge 2}$$
12	10 11	mp1i	$$⊢N\in \mathbb{N}\to 2\in {\mathbb{Z}}_{\ge 2}$$
13		nnre	$$⊢N\in \mathbb{N}\to N\in ℝ$$
14		nnge1	$$⊢N\in \mathbb{N}\to 1\le N$$
15		1re	$$⊢1\in ℝ$$
16		elicopnf	$$⊢1\in ℝ\to \left(N\in \left[1,\mathrm{+\infty }\right)\leftrightarrow \left(N\in ℝ\wedge 1\le N\right)\right)$$
17	15 16	ax-mp	$$⊢N\in \left[1,\mathrm{+\infty }\right)\leftrightarrow \left(N\in ℝ\wedge 1\le N\right)$$
18	13 14 17	sylanbrc	$$⊢N\in \mathbb{N}\to N\in \left[1,\mathrm{+\infty }\right)$$
19		rege1logbzge0	$$⊢\left(2\in {\mathbb{Z}}_{\ge 2}\wedge N\in \left[1,\mathrm{+\infty }\right)\right)\to 0\le {\log }_{2}N$$
20	12 18 19	syl2anc	$$⊢N\in \mathbb{N}\to 0\le {\log }_{2}N$$
21		flge0nn0	$$⊢\left({\log }_{2}N\in ℝ\wedge 0\le {\log }_{2}N\right)\to ⌊{\log }_{2}N⌋\in {\mathbb{N}}_0$$
22	9 20 21	syl2anc	$$⊢N\in \mathbb{N}\to ⌊{\log }_{2}N⌋\in {\mathbb{N}}_0$$
23		nn0p1nn	$$⊢⌊{\log }_{2}N⌋\in {\mathbb{N}}_0\to ⌊{\log }_{2}N⌋+1\in \mathbb{N}$$
24	22 23	syl	$$⊢N\in \mathbb{N}\to ⌊{\log }_{2}N⌋+1\in \mathbb{N}$$
25	1 24	eqeltrd