Theorem blennnt2

Description: The binary length of a positive integer, doubled and increased by 1, is the binary length of the integer plus 1. (Contributed by AV, 30-May-2010)

	Ref	Expression
Assertion	blennnt2

Proof

Step	Hyp	Ref	Expression
1		2nn	$$⊢2\in \mathbb{N}$$
2	1	a1i	$$⊢N\in \mathbb{N}\to 2\in \mathbb{N}$$
3		id	$$⊢N\in \mathbb{N}\to N\in \mathbb{N}$$
4	2 3	nnmulcld	$$⊢N\in \mathbb{N}\to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in \mathbb{N}$$
5		blennn
6	4 5	syl
7		2cn	$$⊢2\in ℂ$$
8	7	a1i	$$⊢N\in \mathbb{N}\to 2\in ℂ$$
9		nncn	$$⊢N\in \mathbb{N}\to N\in ℂ$$
10	8 9	mulcomd	$$⊢N\in \mathbb{N}\to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=\mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot 2$$
11	10	oveq2d	$$⊢N\in \mathbb{N}\to {\log }_{2}2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}={\log }_2\mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot 2$$
12		2z	$$⊢2\in \mathbb{Z}$$
13		uzid	$$⊢2\in \mathbb{Z}\to 2\in {\mathbb{Z}}_{\ge 2}$$
14	12 13	ax-mp	$$⊢2\in {\mathbb{Z}}_{\ge 2}$$
15		eluz2cnn0n1	$$⊢2\in {\mathbb{Z}}_{\ge 2}\to 2\in \left(ℂ\setminus \left\{0,1\right\}\right)$$
16	14 15	mp1i	$$⊢N\in \mathbb{N}\to 2\in \left(ℂ\setminus \left\{0,1\right\}\right)$$
17		nnrp	$$⊢N\in \mathbb{N}\to N\in {ℝ}^{+}$$
18		2rp	$$⊢2\in {ℝ}^{+}$$
19	18	a1i	$$⊢N\in \mathbb{N}\to 2\in {ℝ}^{+}$$
20		relogbmul	$$⊢\left(2\in \left(ℂ\setminus \left\{0,1\right\}\right)\wedge \left(N\in {ℝ}^{+}\wedge 2\in {ℝ}^{+}\right)\right)\to {\log }_2\mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot 2={\log }_{2}N+{\log }_{2}2$$
21	16 17 19 20	syl12anc	$$⊢N\in \mathbb{N}\to {\log }_2\mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot 2={\log }_{2}N+{\log }_{2}2$$
22		2ne0	$$⊢2\ne 0$$
23		1ne2	$$⊢1\ne 2$$
24	23	necomi	$$⊢2\ne 1$$
25	7 22 24	3pm3.2i	$$⊢\left(2\in ℂ\wedge 2\ne 0\wedge 2\ne 1\right)$$
26		logbid1	$$⊢\left(2\in ℂ\wedge 2\ne 0\wedge 2\ne 1\right)\to {\log }_{2}2=1$$
27	25 26	mp1i	$$⊢N\in \mathbb{N}\to {\log }_{2}2=1$$
28	27	oveq2d	$$⊢N\in \mathbb{N}\to {\log }_{2}N+{\log }_{2}2={\log }_{2}N+1$$
29	11 21 28	3eqtrd	$$⊢N\in \mathbb{N}\to {\log }_{2}2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}={\log }_{2}N+1$$
30	29	fveq2d	$$⊢N\in \mathbb{N}\to ⌊{\log }_{2}2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}⌋=⌊{\log }_{2}N+1⌋$$
31	24	a1i	$$⊢N\in \mathbb{N}\to 2\ne 1$$
32		relogbcl	$$⊢\left(2\in {ℝ}^{+}\wedge N\in {ℝ}^{+}\wedge 2\ne 1\right)\to {\log }_{2}N\in ℝ$$
33	19 17 31 32	syl3anc	$$⊢N\in \mathbb{N}\to {\log }_{2}N\in ℝ$$
34		1zzd	$$⊢N\in \mathbb{N}\to 1\in \mathbb{Z}$$
35		fladdz	$$⊢\left({\log }_{2}N\in ℝ\wedge 1\in \mathbb{Z}\right)\to ⌊{\log }_{2}N+1⌋=⌊{\log }_{2}N⌋+1$$
36	33 34 35	syl2anc	$$⊢N\in \mathbb{N}\to ⌊{\log }_{2}N+1⌋=⌊{\log }_{2}N⌋+1$$
37	30 36	eqtrd	$$⊢N\in \mathbb{N}\to ⌊{\log }_{2}2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}⌋=⌊{\log }_{2}N⌋+1$$
38	37	oveq1d	$$⊢N\in \mathbb{N}\to ⌊{\log }_{2}2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}⌋+1=⌊{\log }_{2}N⌋+1+1$$
39		blennn
40	39	eqcomd
41	40	oveq1d
42	6 38 41	3eqtrd