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 ( 𝐼 ∈ ℕ → ( ⌊ ‘ ( 2 logb ( ( 2 ↑ 𝐼 ) − 1 ) ) ) = ( 𝐼 − 1 ) )

Proof

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