Theorem nnpw2blen

Description: A positive integer is between 2 to the power of its binary length minus 1 and 2 to the power of its binary length. (Contributed by AV, 31-May-2020)

	Ref	Expression
Assertion	nnpw2blen

Proof

Step	Hyp	Ref	Expression
1		2rp	$$⊢2\in {ℝ}^{+}$$
2	1	a1i	$$⊢N\in \mathbb{N}\to 2\in {ℝ}^{+}$$
3		nnrp	$$⊢N\in \mathbb{N}\to N\in {ℝ}^{+}$$
4		1ne2	$$⊢1\ne 2$$
5	4	necomi	$$⊢2\ne 1$$
6	5	a1i	$$⊢N\in \mathbb{N}\to 2\ne 1$$
7		relogbcl	$$⊢\left(2\in {ℝ}^{+}\wedge N\in {ℝ}^{+}\wedge 2\ne 1\right)\to {\log }_{2}N\in ℝ$$
8	2 3 6 7	syl3anc	$$⊢N\in \mathbb{N}\to {\log }_{2}N\in ℝ$$
9	8	flcld	$$⊢N\in \mathbb{N}\to ⌊{\log }_{2}N⌋\in \mathbb{Z}$$
10	9	zcnd	$$⊢N\in \mathbb{N}\to ⌊{\log }_{2}N⌋\in ℂ$$
11		pncan1	$$⊢⌊{\log }_{2}N⌋\in ℂ\to ⌊{\log }_{2}N⌋+1-1=⌊{\log }_{2}N⌋$$
12	10 11	syl	$$⊢N\in \mathbb{N}\to ⌊{\log }_{2}N⌋+1-1=⌊{\log }_{2}N⌋$$
13	12	oveq2d	$$⊢N\in \mathbb{N}\to 2^{⌊{\log }_{2}N⌋+1-1}=2^{⌊{\log }_{2}N⌋}$$
14		blennn
15	14	oveq1d
16	15	oveq2d
17		2cnd	$$⊢N\in \mathbb{N}\to 2\in ℂ$$
18		2ne0	$$⊢2\ne 0$$
19	18	a1i	$$⊢N\in \mathbb{N}\to 2\ne 0$$
20	17 19 9	cxpexpzd	$$⊢N\in \mathbb{N}\to 2^{⌊{\log }_{2}N⌋}=2^{⌊{\log }_{2}N⌋}$$
21	13 16 20	3eqtr4d
22		flle	$$⊢{\log }_{2}N\in ℝ\to ⌊{\log }_{2}N⌋\le {\log }_{2}N$$
23	8 22	syl	$$⊢N\in \mathbb{N}\to ⌊{\log }_{2}N⌋\le {\log }_{2}N$$
24		2re	$$⊢2\in ℝ$$
25	24	a1i	$$⊢N\in \mathbb{N}\to 2\in ℝ$$
26		1lt2	$$⊢1<2$$
27	26	a1i	$$⊢N\in \mathbb{N}\to 1<2$$
28	9	zred	$$⊢N\in \mathbb{N}\to ⌊{\log }_{2}N⌋\in ℝ$$
29	25 27 28 8	cxpled	$$⊢N\in \mathbb{N}\to \left(⌊{\log }_{2}N⌋\le {\log }_{2}N\leftrightarrow 2^{⌊{\log }_{2}N⌋}\le 2^{{\log }_{2}N}\right)$$
30	23 29	mpbid	$$⊢N\in \mathbb{N}\to 2^{⌊{\log }_{2}N⌋}\le 2^{{\log }_{2}N}$$
31		2cn	$$⊢2\in ℂ$$
32		eldifpr	$$⊢2\in \left(ℂ\setminus \left\{0,1\right\}\right)\leftrightarrow \left(2\in ℂ\wedge 2\ne 0\wedge 2\ne 1\right)$$
33	31 18 5 32	mpbir3an	$$⊢2\in \left(ℂ\setminus \left\{0,1\right\}\right)$$
34		nncn	$$⊢N\in \mathbb{N}\to N\in ℂ$$
35		nnne0	$$⊢N\in \mathbb{N}\to N\ne 0$$
36		eldifsn	$$⊢N\in \left(ℂ\setminus \left\{0\right\}\right)\leftrightarrow \left(N\in ℂ\wedge N\ne 0\right)$$
37	34 35 36	sylanbrc	$$⊢N\in \mathbb{N}\to N\in \left(ℂ\setminus \left\{0\right\}\right)$$
38		cxplogb	$$⊢\left(2\in \left(ℂ\setminus \left\{0,1\right\}\right)\wedge N\in \left(ℂ\setminus \left\{0\right\}\right)\right)\to 2^{{\log }_{2}N}=N$$
39	33 37 38	sylancr	$$⊢N\in \mathbb{N}\to 2^{{\log }_{2}N}=N$$
40	30 39	breqtrd	$$⊢N\in \mathbb{N}\to 2^{⌊{\log }_{2}N⌋}\le N$$
41	21 40	eqbrtrd
42		flltp1	$$⊢{\log }_{2}N\in ℝ\to {\log }_{2}N<⌊{\log }_{2}N⌋+1$$
43	8 42	syl	$$⊢N\in \mathbb{N}\to {\log }_{2}N<⌊{\log }_{2}N⌋+1$$
44	9	peano2zd	$$⊢N\in \mathbb{N}\to ⌊{\log }_{2}N⌋+1\in \mathbb{Z}$$
45	44	zred	$$⊢N\in \mathbb{N}\to ⌊{\log }_{2}N⌋+1\in ℝ$$
46	25 27 8 45	cxpltd	$$⊢N\in \mathbb{N}\to \left({\log }_{2}N<⌊{\log }_{2}N⌋+1\leftrightarrow 2^{{\log }_{2}N}<2^{⌊{\log }_{2}N⌋+1}\right)$$
47	43 46	mpbid	$$⊢N\in \mathbb{N}\to 2^{{\log }_{2}N}<2^{⌊{\log }_{2}N⌋+1}$$
48	17 19 44	cxpexpzd	$$⊢N\in \mathbb{N}\to 2^{⌊{\log }_{2}N⌋+1}=2^{⌊{\log }_{2}N⌋+1}$$
49	47 39 48	3brtr3d	$$⊢N\in \mathbb{N}\to N<2^{⌊{\log }_{2}N⌋+1}$$
50	14	oveq2d
51	49 50	breqtrrd
52	41 51	jca