Metamath Proof Explorer

Theorem logbpw2m1

Description: The floor of the binary logarithm of 2 to the power of a positive integer minus 1 is equal to the integer minus 1. (Contributed by AV, 31-May-2020)

Ref Expression
Assertion logbpw2m1 ⊢I∈ℕ→log22I−1=I−1

Proof

Step Hyp Ref Expression
1 2rp ⊢2∈ℝ+
2 1 a1i ⊢I∈ℕ→2∈ℝ+
3 2nn0 ⊢2∈ℕ0
4 3 a1i ⊢I∈ℕ→2∈ℕ0
5 nnnn0 ⊢I∈ℕ→I∈ℕ0
6 4 5 nn0expcld ⊢I∈ℕ→2I∈ℕ0
7 nnge1 ⊢I∈ℕ→1≤I
8 2re ⊢2∈ℝ
9 8 a1i ⊢I∈ℕ→2∈ℝ
10 1zzd ⊢I∈ℕ→1∈ℤ
11 nnz ⊢I∈ℕ→I∈ℤ
12 1lt2 ⊢1<2
13 12 a1i ⊢I∈ℕ→1<2
14 9 10 11 13 leexp2d ⊢I∈ℕ→1≤I↔21≤2I
15 2cn ⊢2∈ℂ
16 exp1 ⊢2∈ℂ→21=2
17 15 16 ax-mp ⊢21=2
18 17 a1i ⊢I∈ℕ→21=2
19 18 breq1d ⊢I∈ℕ→21≤2I↔2≤2I
20 14 19 bitrd ⊢I∈ℕ→1≤I↔2≤2I
21 7 20 mpbid ⊢I∈ℕ→2≤2I
22 nn0ge2m1nn ⊢2I∈ℕ0∧2≤2I→2I−1∈ℕ
23 6 21 22 syl2anc ⊢I∈ℕ→2I−1∈ℕ
24 23 nnrpd ⊢I∈ℕ→2I−1∈ℝ+
25 1ne2 ⊢1≠2
26 25 necomi ⊢2≠1
27 26 a1i ⊢I∈ℕ→2≠1
28 relogbcl ⊢2∈ℝ+∧2I−1∈ℝ+∧2≠1→log22I−1∈ℝ
29 2 24 27 28 syl3anc ⊢I∈ℕ→log22I−1∈ℝ
30 29 flcld ⊢I∈ℕ→log22I−1∈ℤ
31 peano2zm ⊢I∈ℤ→I−1∈ℤ
32 11 31 syl ⊢I∈ℕ→I−1∈ℤ
33 2z ⊢2∈ℤ
34 uzid ⊢2∈ℤ→2∈ℤ≥2
35 33 34 ax-mp ⊢2∈ℤ≥2
36 nnlogbexp ⊢2∈ℤ≥2∧I−1∈ℤ→log22I−1=I−1
37 35 32 36 sylancr ⊢I∈ℕ→log22I−1=I−1
38 37 fveq2d ⊢I∈ℕ→log22I−1=I−1
39 flid ⊢I−1∈ℤ→I−1=I−1
40 32 39 syl ⊢I∈ℕ→I−1=I−1
41 38 40 eqtrd ⊢I∈ℕ→log22I−1=I−1
42 2nn ⊢2∈ℕ
43 42 a1i ⊢I∈ℕ→2∈ℕ
44 nnm1nn0 ⊢I∈ℕ→I−1∈ℕ0
45 43 44 nnexpcld ⊢I∈ℕ→2I−1∈ℕ
46 45 nnrpd ⊢I∈ℕ→2I−1∈ℝ+
47 relogbcl ⊢2∈ℝ+∧2I−1∈ℝ+∧2≠1→log22I−1∈ℝ
48 2 46 27 47 syl3anc ⊢I∈ℕ→log22I−1∈ℝ
49 pw2m1lepw2m1 ⊢I∈ℕ→2I−1≤2I−1
50 35 a1i ⊢I∈ℕ→2∈ℤ≥2
51 logbleb ⊢2∈ℤ≥2∧2I−1∈ℝ+∧2I−1∈ℝ+→2I−1≤2I−1↔log22I−1≤log22I−1
52 50 46 24 51 syl3anc ⊢I∈ℕ→2I−1≤2I−1↔log22I−1≤log22I−1
53 49 52 mpbid ⊢I∈ℕ→log22I−1≤log22I−1
54 flwordi ⊢log22I−1∈ℝ∧log22I−1∈ℝ∧log22I−1≤log22I−1→log22I−1≤log22I−1
55 48 29 53 54 syl3anc ⊢I∈ℕ→log22I−1≤log22I−1
56 41 55 eqbrtrrd ⊢I∈ℕ→I−1≤log22I−1
57 43 5 nnexpcld ⊢I∈ℕ→2I∈ℕ
58 57 nnnn0d ⊢I∈ℕ→2I∈ℕ0
59 58 21 22 syl2anc ⊢I∈ℕ→2I−1∈ℕ
60 59 nnrpd ⊢I∈ℕ→2I−1∈ℝ+
61 2 60 27 28 syl3anc ⊢I∈ℕ→log22I−1∈ℝ
62 61 flcld ⊢I∈ℕ→log22I−1∈ℤ
63 62 zred ⊢I∈ℕ→log22I−1∈ℝ
64 nnre ⊢I∈ℕ→I∈ℝ
65 peano2rem ⊢I∈ℝ→I−1∈ℝ
66 64 65 syl ⊢I∈ℕ→I−1∈ℝ
67 peano2re ⊢I−1∈ℝ→I-1+1∈ℝ
68 66 67 syl ⊢I∈ℕ→I-1+1∈ℝ
69 flle ⊢log22I−1∈ℝ→log22I−1≤log22I−1
70 29 69 syl ⊢I∈ℕ→log22I−1≤log22I−1
71 57 nnrpd ⊢I∈ℕ→2I∈ℝ+
72 relogbcl ⊢2∈ℝ+∧2I∈ℝ+∧2≠1→log22I∈ℝ
73 2 71 27 72 syl3anc ⊢I∈ℕ→log22I∈ℝ
74 57 nnred ⊢I∈ℕ→2I∈ℝ
75 74 ltm1d ⊢I∈ℕ→2I−1<2I
76 logblt ⊢2∈ℤ≥2∧2I−1∈ℝ+∧2I∈ℝ+→2I−1<2I↔log22I−1<log22I
77 50 24 71 76 syl3anc ⊢I∈ℕ→2I−1<2I↔log22I−1<log22I
78 75 77 mpbid ⊢I∈ℕ→log22I−1<log22I
79 64 leidd ⊢I∈ℕ→I≤I
80 nnlogbexp ⊢2∈ℤ≥2∧I∈ℤ→log22I=I
81 35 11 80 sylancr ⊢I∈ℕ→log22I=I
82 nncn ⊢I∈ℕ→I∈ℂ
83 npcan1 ⊢I∈ℂ→I-1+1=I
84 82 83 syl ⊢I∈ℕ→I-1+1=I
85 79 81 84 3brtr4d ⊢I∈ℕ→log22I≤I-1+1
86 29 73 68 78 85 ltletrd ⊢I∈ℕ→log22I−1<I-1+1
87 63 29 68 70 86 lelttrd ⊢I∈ℕ→log22I−1<I-1+1
88 zgeltp1eq ⊢log22I−1∈ℤ∧I−1∈ℤ→I−1≤log22I−1∧log22I−1<I-1+1→log22I−1=I−1
89 88 imp ⊢log22I−1∈ℤ∧I−1∈ℤ∧I−1≤log22I−1∧log22I−1<I-1+1→log22I−1=I−1
90 30 32 56 87 89 syl22anc ⊢I∈ℕ→log22I−1=I−1