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	⊢ ( 𝑁 ∈ ℕ → ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ≤ 𝑁 ∧ 𝑁 < ( 2 ↑ ( #b ‘ 𝑁 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		2rp	⊢ 2 ∈ ℝ+
2	1	a1i	⊢ ( 𝑁 ∈ ℕ → 2 ∈ ℝ+ )
3		nnrp	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ+ )
4		1ne2	⊢ 1 ≠ 2
5	4	necomi	⊢ 2 ≠ 1
6	5	a1i	⊢ ( 𝑁 ∈ ℕ → 2 ≠ 1 )
7		relogbcl	⊢ ( ( 2 ∈ ℝ+ ∧ 𝑁 ∈ ℝ+ ∧ 2 ≠ 1 ) → ( 2 logb 𝑁 ) ∈ ℝ )
8	2 3 6 7	syl3anc	⊢ ( 𝑁 ∈ ℕ → ( 2 logb 𝑁 ) ∈ ℝ )
9	8	flcld	⊢ ( 𝑁 ∈ ℕ → ( ⌊ ‘ ( 2 logb 𝑁 ) ) ∈ ℤ )
10	9	zcnd	⊢ ( 𝑁 ∈ ℕ → ( ⌊ ‘ ( 2 logb 𝑁 ) ) ∈ ℂ )
11		pncan1	⊢ ( ( ⌊ ‘ ( 2 logb 𝑁 ) ) ∈ ℂ → ( ( ( ⌊ ‘ ( 2 logb 𝑁 ) ) + 1 ) − 1 ) = ( ⌊ ‘ ( 2 logb 𝑁 ) ) )
12	10 11	syl	⊢ ( 𝑁 ∈ ℕ → ( ( ( ⌊ ‘ ( 2 logb 𝑁 ) ) + 1 ) − 1 ) = ( ⌊ ‘ ( 2 logb 𝑁 ) ) )
13	12	oveq2d	⊢ ( 𝑁 ∈ ℕ → ( 2 ↑ ( ( ( ⌊ ‘ ( 2 logb 𝑁 ) ) + 1 ) − 1 ) ) = ( 2 ↑ ( ⌊ ‘ ( 2 logb 𝑁 ) ) ) )
14		blennn	⊢ ( 𝑁 ∈ ℕ → ( #b ‘ 𝑁 ) = ( ( ⌊ ‘ ( 2 logb 𝑁 ) ) + 1 ) )
15	14	oveq1d	⊢ ( 𝑁 ∈ ℕ → ( ( #b ‘ 𝑁 ) − 1 ) = ( ( ( ⌊ ‘ ( 2 logb 𝑁 ) ) + 1 ) − 1 ) )
16	15	oveq2d	⊢ ( 𝑁 ∈ ℕ → ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) = ( 2 ↑ ( ( ( ⌊ ‘ ( 2 logb 𝑁 ) ) + 1 ) − 1 ) ) )
17		2cnd	⊢ ( 𝑁 ∈ ℕ → 2 ∈ ℂ )
18		2ne0	⊢ 2 ≠ 0
19	18	a1i	⊢ ( 𝑁 ∈ ℕ → 2 ≠ 0 )
20	17 19 9	cxpexpzd	⊢ ( 𝑁 ∈ ℕ → ( 2 ↑𝑐 ( ⌊ ‘ ( 2 logb 𝑁 ) ) ) = ( 2 ↑ ( ⌊ ‘ ( 2 logb 𝑁 ) ) ) )
21	13 16 20	3eqtr4d	⊢ ( 𝑁 ∈ ℕ → ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) = ( 2 ↑𝑐 ( ⌊ ‘ ( 2 logb 𝑁 ) ) ) )
22		flle	⊢ ( ( 2 logb 𝑁 ) ∈ ℝ → ( ⌊ ‘ ( 2 logb 𝑁 ) ) ≤ ( 2 logb 𝑁 ) )
23	8 22	syl	⊢ ( 𝑁 ∈ ℕ → ( ⌊ ‘ ( 2 logb 𝑁 ) ) ≤ ( 2 logb 𝑁 ) )
24		2re	⊢ 2 ∈ ℝ
25	24	a1i	⊢ ( 𝑁 ∈ ℕ → 2 ∈ ℝ )
26		1lt2	⊢ 1 < 2
27	26	a1i	⊢ ( 𝑁 ∈ ℕ → 1 < 2 )
28	9	zred	⊢ ( 𝑁 ∈ ℕ → ( ⌊ ‘ ( 2 logb 𝑁 ) ) ∈ ℝ )
29	25 27 28 8	cxpled	⊢ ( 𝑁 ∈ ℕ → ( ( ⌊ ‘ ( 2 logb 𝑁 ) ) ≤ ( 2 logb 𝑁 ) ↔ ( 2 ↑𝑐 ( ⌊ ‘ ( 2 logb 𝑁 ) ) ) ≤ ( 2 ↑𝑐 ( 2 logb 𝑁 ) ) ) )
30	23 29	mpbid	⊢ ( 𝑁 ∈ ℕ → ( 2 ↑𝑐 ( ⌊ ‘ ( 2 logb 𝑁 ) ) ) ≤ ( 2 ↑𝑐 ( 2 logb 𝑁 ) ) )
31		2cn	⊢ 2 ∈ ℂ
32		eldifpr	⊢ ( 2 ∈ ( ℂ ∖ { 0 , 1 } ) ↔ ( 2 ∈ ℂ ∧ 2 ≠ 0 ∧ 2 ≠ 1 ) )
33	31 18 5 32	mpbir3an	⊢ 2 ∈ ( ℂ ∖ { 0 , 1 } )
34		nncn	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
35		nnne0	⊢ ( 𝑁 ∈ ℕ → 𝑁 ≠ 0 )
36		eldifsn	⊢ ( 𝑁 ∈ ( ℂ ∖ { 0 } ) ↔ ( 𝑁 ∈ ℂ ∧ 𝑁 ≠ 0 ) )
37	34 35 36	sylanbrc	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ( ℂ ∖ { 0 } ) )
38		cxplogb	⊢ ( ( 2 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝑁 ∈ ( ℂ ∖ { 0 } ) ) → ( 2 ↑𝑐 ( 2 logb 𝑁 ) ) = 𝑁 )
39	33 37 38	sylancr	⊢ ( 𝑁 ∈ ℕ → ( 2 ↑𝑐 ( 2 logb 𝑁 ) ) = 𝑁 )
40	30 39	breqtrd	⊢ ( 𝑁 ∈ ℕ → ( 2 ↑𝑐 ( ⌊ ‘ ( 2 logb 𝑁 ) ) ) ≤ 𝑁 )
41	21 40	eqbrtrd	⊢ ( 𝑁 ∈ ℕ → ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ≤ 𝑁 )
42		flltp1	⊢ ( ( 2 logb 𝑁 ) ∈ ℝ → ( 2 logb 𝑁 ) < ( ( ⌊ ‘ ( 2 logb 𝑁 ) ) + 1 ) )
43	8 42	syl	⊢ ( 𝑁 ∈ ℕ → ( 2 logb 𝑁 ) < ( ( ⌊ ‘ ( 2 logb 𝑁 ) ) + 1 ) )
44	9	peano2zd	⊢ ( 𝑁 ∈ ℕ → ( ( ⌊ ‘ ( 2 logb 𝑁 ) ) + 1 ) ∈ ℤ )
45	44	zred	⊢ ( 𝑁 ∈ ℕ → ( ( ⌊ ‘ ( 2 logb 𝑁 ) ) + 1 ) ∈ ℝ )
46	25 27 8 45	cxpltd	⊢ ( 𝑁 ∈ ℕ → ( ( 2 logb 𝑁 ) < ( ( ⌊ ‘ ( 2 logb 𝑁 ) ) + 1 ) ↔ ( 2 ↑𝑐 ( 2 logb 𝑁 ) ) < ( 2 ↑𝑐 ( ( ⌊ ‘ ( 2 logb 𝑁 ) ) + 1 ) ) ) )
47	43 46	mpbid	⊢ ( 𝑁 ∈ ℕ → ( 2 ↑𝑐 ( 2 logb 𝑁 ) ) < ( 2 ↑𝑐 ( ( ⌊ ‘ ( 2 logb 𝑁 ) ) + 1 ) ) )
48	17 19 44	cxpexpzd	⊢ ( 𝑁 ∈ ℕ → ( 2 ↑𝑐 ( ( ⌊ ‘ ( 2 logb 𝑁 ) ) + 1 ) ) = ( 2 ↑ ( ( ⌊ ‘ ( 2 logb 𝑁 ) ) + 1 ) ) )
49	47 39 48	3brtr3d	⊢ ( 𝑁 ∈ ℕ → 𝑁 < ( 2 ↑ ( ( ⌊ ‘ ( 2 logb 𝑁 ) ) + 1 ) ) )
50	14	oveq2d	⊢ ( 𝑁 ∈ ℕ → ( 2 ↑ ( #b ‘ 𝑁 ) ) = ( 2 ↑ ( ( ⌊ ‘ ( 2 logb 𝑁 ) ) + 1 ) ) )
51	49 50	breqtrrd	⊢ ( 𝑁 ∈ ℕ → 𝑁 < ( 2 ↑ ( #b ‘ 𝑁 ) ) )
52	41 51	jca	⊢ ( 𝑁 ∈ ℕ → ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ≤ 𝑁 ∧ 𝑁 < ( 2 ↑ ( #b ‘ 𝑁 ) ) ) )