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 ) )