Metamath Proof Explorer

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 ⊢N∈ℕ→2#b ⁡ N − 1 ≤ N ∧ N<2#b ⁡N

Proof

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