Proof of Theorem logbpw2m1
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 2rp 13039 | . . . . 5
⊢ 2 ∈
ℝ+ | 
| 2 | 1 | a1i 11 | . . . 4
⊢ (𝐼 ∈ ℕ → 2 ∈
ℝ+) | 
| 3 |  | 2nn0 12543 | . . . . . . . 8
⊢ 2 ∈
ℕ0 | 
| 4 | 3 | a1i 11 | . . . . . . 7
⊢ (𝐼 ∈ ℕ → 2 ∈
ℕ0) | 
| 5 |  | nnnn0 12533 | . . . . . . 7
⊢ (𝐼 ∈ ℕ → 𝐼 ∈
ℕ0) | 
| 6 | 4, 5 | nn0expcld 14285 | . . . . . 6
⊢ (𝐼 ∈ ℕ →
(2↑𝐼) ∈
ℕ0) | 
| 7 |  | nnge1 12294 | . . . . . . 7
⊢ (𝐼 ∈ ℕ → 1 ≤
𝐼) | 
| 8 |  | 2re 12340 | . . . . . . . . . 10
⊢ 2 ∈
ℝ | 
| 9 | 8 | a1i 11 | . . . . . . . . 9
⊢ (𝐼 ∈ ℕ → 2 ∈
ℝ) | 
| 10 |  | 1zzd 12648 | . . . . . . . . 9
⊢ (𝐼 ∈ ℕ → 1 ∈
ℤ) | 
| 11 |  | nnz 12634 | . . . . . . . . 9
⊢ (𝐼 ∈ ℕ → 𝐼 ∈
ℤ) | 
| 12 |  | 1lt2 12437 | . . . . . . . . . 10
⊢ 1 <
2 | 
| 13 | 12 | a1i 11 | . . . . . . . . 9
⊢ (𝐼 ∈ ℕ → 1 <
2) | 
| 14 | 9, 10, 11, 13 | leexp2d 14291 | . . . . . . . 8
⊢ (𝐼 ∈ ℕ → (1 ≤
𝐼 ↔ (2↑1) ≤
(2↑𝐼))) | 
| 15 |  | 2cn 12341 | . . . . . . . . . . 11
⊢ 2 ∈
ℂ | 
| 16 |  | exp1 14108 | . . . . . . . . . . 11
⊢ (2 ∈
ℂ → (2↑1) = 2) | 
| 17 | 15, 16 | ax-mp 5 | . . . . . . . . . 10
⊢
(2↑1) = 2 | 
| 18 | 17 | a1i 11 | . . . . . . . . 9
⊢ (𝐼 ∈ ℕ →
(2↑1) = 2) | 
| 19 | 18 | breq1d 5153 | . . . . . . . 8
⊢ (𝐼 ∈ ℕ →
((2↑1) ≤ (2↑𝐼)
↔ 2 ≤ (2↑𝐼))) | 
| 20 | 14, 19 | bitrd 279 | . . . . . . 7
⊢ (𝐼 ∈ ℕ → (1 ≤
𝐼 ↔ 2 ≤
(2↑𝐼))) | 
| 21 | 7, 20 | mpbid 232 | . . . . . 6
⊢ (𝐼 ∈ ℕ → 2 ≤
(2↑𝐼)) | 
| 22 |  | nn0ge2m1nn 12596 | . . . . . 6
⊢
(((2↑𝐼) ∈
ℕ0 ∧ 2 ≤ (2↑𝐼)) → ((2↑𝐼) − 1) ∈
ℕ) | 
| 23 | 6, 21, 22 | syl2anc 584 | . . . . 5
⊢ (𝐼 ∈ ℕ →
((2↑𝐼) − 1)
∈ ℕ) | 
| 24 | 23 | nnrpd 13075 | . . . 4
⊢ (𝐼 ∈ ℕ →
((2↑𝐼) − 1)
∈ ℝ+) | 
| 25 |  | 1ne2 12474 | . . . . . 6
⊢ 1 ≠
2 | 
| 26 | 25 | necomi 2995 | . . . . 5
⊢ 2 ≠
1 | 
| 27 | 26 | a1i 11 | . . . 4
⊢ (𝐼 ∈ ℕ → 2 ≠
1) | 
| 28 |  | relogbcl 26816 | . . . 4
⊢ ((2
∈ ℝ+ ∧ ((2↑𝐼) − 1) ∈ ℝ+
∧ 2 ≠ 1) → (2 logb ((2↑𝐼) − 1)) ∈
ℝ) | 
| 29 | 2, 24, 27, 28 | syl3anc 1373 | . . 3
⊢ (𝐼 ∈ ℕ → (2
logb ((2↑𝐼)
− 1)) ∈ ℝ) | 
| 30 | 29 | flcld 13838 | . 2
⊢ (𝐼 ∈ ℕ →
(⌊‘(2 logb ((2↑𝐼) − 1))) ∈
ℤ) | 
| 31 |  | peano2zm 12660 | . . 3
⊢ (𝐼 ∈ ℤ → (𝐼 − 1) ∈
ℤ) | 
| 32 | 11, 31 | syl 17 | . 2
⊢ (𝐼 ∈ ℕ → (𝐼 − 1) ∈
ℤ) | 
| 33 |  | 2z 12649 | . . . . . . 7
⊢ 2 ∈
ℤ | 
| 34 |  | uzid 12893 | . . . . . . 7
⊢ (2 ∈
ℤ → 2 ∈ (ℤ≥‘2)) | 
| 35 | 33, 34 | ax-mp 5 | . . . . . 6
⊢ 2 ∈
(ℤ≥‘2) | 
| 36 |  | nnlogbexp 26824 | . . . . . 6
⊢ ((2
∈ (ℤ≥‘2) ∧ (𝐼 − 1) ∈ ℤ) → (2
logb (2↑(𝐼
− 1))) = (𝐼 −
1)) | 
| 37 | 35, 32, 36 | sylancr 587 | . . . . 5
⊢ (𝐼 ∈ ℕ → (2
logb (2↑(𝐼
− 1))) = (𝐼 −
1)) | 
| 38 | 37 | fveq2d 6910 | . . . 4
⊢ (𝐼 ∈ ℕ →
(⌊‘(2 logb (2↑(𝐼 − 1)))) = (⌊‘(𝐼 − 1))) | 
| 39 |  | flid 13848 | . . . . 5
⊢ ((𝐼 − 1) ∈ ℤ
→ (⌊‘(𝐼
− 1)) = (𝐼 −
1)) | 
| 40 | 32, 39 | syl 17 | . . . 4
⊢ (𝐼 ∈ ℕ →
(⌊‘(𝐼 −
1)) = (𝐼 −
1)) | 
| 41 | 38, 40 | eqtrd 2777 | . . 3
⊢ (𝐼 ∈ ℕ →
(⌊‘(2 logb (2↑(𝐼 − 1)))) = (𝐼 − 1)) | 
| 42 |  | 2nn 12339 | . . . . . . . 8
⊢ 2 ∈
ℕ | 
| 43 | 42 | a1i 11 | . . . . . . 7
⊢ (𝐼 ∈ ℕ → 2 ∈
ℕ) | 
| 44 |  | nnm1nn0 12567 | . . . . . . 7
⊢ (𝐼 ∈ ℕ → (𝐼 − 1) ∈
ℕ0) | 
| 45 | 43, 44 | nnexpcld 14284 | . . . . . 6
⊢ (𝐼 ∈ ℕ →
(2↑(𝐼 − 1))
∈ ℕ) | 
| 46 | 45 | nnrpd 13075 | . . . . 5
⊢ (𝐼 ∈ ℕ →
(2↑(𝐼 − 1))
∈ ℝ+) | 
| 47 |  | relogbcl 26816 | . . . . 5
⊢ ((2
∈ ℝ+ ∧ (2↑(𝐼 − 1)) ∈ ℝ+
∧ 2 ≠ 1) → (2 logb (2↑(𝐼 − 1))) ∈
ℝ) | 
| 48 | 2, 46, 27, 47 | syl3anc 1373 | . . . 4
⊢ (𝐼 ∈ ℕ → (2
logb (2↑(𝐼
− 1))) ∈ ℝ) | 
| 49 |  | pw2m1lepw2m1 48437 | . . . . 5
⊢ (𝐼 ∈ ℕ →
(2↑(𝐼 − 1)) ≤
((2↑𝐼) −
1)) | 
| 50 | 35 | a1i 11 | . . . . . 6
⊢ (𝐼 ∈ ℕ → 2 ∈
(ℤ≥‘2)) | 
| 51 |  | logbleb 26826 | . . . . . 6
⊢ ((2
∈ (ℤ≥‘2) ∧ (2↑(𝐼 − 1)) ∈ ℝ+
∧ ((2↑𝐼) −
1) ∈ ℝ+) → ((2↑(𝐼 − 1)) ≤ ((2↑𝐼) − 1) ↔ (2 logb
(2↑(𝐼 − 1)))
≤ (2 logb ((2↑𝐼) − 1)))) | 
| 52 | 50, 46, 24, 51 | syl3anc 1373 | . . . . 5
⊢ (𝐼 ∈ ℕ →
((2↑(𝐼 − 1))
≤ ((2↑𝐼) − 1)
↔ (2 logb (2↑(𝐼 − 1))) ≤ (2 logb
((2↑𝐼) −
1)))) | 
| 53 | 49, 52 | mpbid 232 | . . . 4
⊢ (𝐼 ∈ ℕ → (2
logb (2↑(𝐼
− 1))) ≤ (2 logb ((2↑𝐼) − 1))) | 
| 54 |  | flwordi 13852 | . . . 4
⊢ (((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 1373 | . . 3
⊢ (𝐼 ∈ ℕ →
(⌊‘(2 logb (2↑(𝐼 − 1)))) ≤ (⌊‘(2
logb ((2↑𝐼)
− 1)))) | 
| 56 | 41, 55 | eqbrtrrd 5167 | . 2
⊢ (𝐼 ∈ ℕ → (𝐼 − 1) ≤
(⌊‘(2 logb ((2↑𝐼) − 1)))) | 
| 57 | 43, 5 | nnexpcld 14284 | . . . . . . . . 9
⊢ (𝐼 ∈ ℕ →
(2↑𝐼) ∈
ℕ) | 
| 58 | 57 | nnnn0d 12587 | . . . . . . . 8
⊢ (𝐼 ∈ ℕ →
(2↑𝐼) ∈
ℕ0) | 
| 59 | 58, 21, 22 | syl2anc 584 | . . . . . . 7
⊢ (𝐼 ∈ ℕ →
((2↑𝐼) − 1)
∈ ℕ) | 
| 60 | 59 | nnrpd 13075 | . . . . . 6
⊢ (𝐼 ∈ ℕ →
((2↑𝐼) − 1)
∈ ℝ+) | 
| 61 | 2, 60, 27, 28 | syl3anc 1373 | . . . . 5
⊢ (𝐼 ∈ ℕ → (2
logb ((2↑𝐼)
− 1)) ∈ ℝ) | 
| 62 | 61 | flcld 13838 | . . . 4
⊢ (𝐼 ∈ ℕ →
(⌊‘(2 logb ((2↑𝐼) − 1))) ∈
ℤ) | 
| 63 | 62 | zred 12722 | . . 3
⊢ (𝐼 ∈ ℕ →
(⌊‘(2 logb ((2↑𝐼) − 1))) ∈
ℝ) | 
| 64 |  | nnre 12273 | . . . . 5
⊢ (𝐼 ∈ ℕ → 𝐼 ∈
ℝ) | 
| 65 |  | peano2rem 11576 | . . . . 5
⊢ (𝐼 ∈ ℝ → (𝐼 − 1) ∈
ℝ) | 
| 66 | 64, 65 | syl 17 | . . . 4
⊢ (𝐼 ∈ ℕ → (𝐼 − 1) ∈
ℝ) | 
| 67 |  | peano2re 11434 | . . . 4
⊢ ((𝐼 − 1) ∈ ℝ
→ ((𝐼 − 1) + 1)
∈ ℝ) | 
| 68 | 66, 67 | syl 17 | . . 3
⊢ (𝐼 ∈ ℕ → ((𝐼 − 1) + 1) ∈
ℝ) | 
| 69 |  | flle 13839 | . . . 4
⊢ ((2
logb ((2↑𝐼)
− 1)) ∈ ℝ → (⌊‘(2 logb
((2↑𝐼) − 1)))
≤ (2 logb ((2↑𝐼) − 1))) | 
| 70 | 29, 69 | syl 17 | . . 3
⊢ (𝐼 ∈ ℕ →
(⌊‘(2 logb ((2↑𝐼) − 1))) ≤ (2 logb
((2↑𝐼) −
1))) | 
| 71 | 57 | nnrpd 13075 | . . . . 5
⊢ (𝐼 ∈ ℕ →
(2↑𝐼) ∈
ℝ+) | 
| 72 |  | relogbcl 26816 | . . . . 5
⊢ ((2
∈ ℝ+ ∧ (2↑𝐼) ∈ ℝ+ ∧ 2 ≠ 1)
→ (2 logb (2↑𝐼)) ∈ ℝ) | 
| 73 | 2, 71, 27, 72 | syl3anc 1373 | . . . 4
⊢ (𝐼 ∈ ℕ → (2
logb (2↑𝐼))
∈ ℝ) | 
| 74 | 57 | nnred 12281 | . . . . . 6
⊢ (𝐼 ∈ ℕ →
(2↑𝐼) ∈
ℝ) | 
| 75 | 74 | ltm1d 12200 | . . . . 5
⊢ (𝐼 ∈ ℕ →
((2↑𝐼) − 1) <
(2↑𝐼)) | 
| 76 |  | logblt 26827 | . . . . . 6
⊢ ((2
∈ (ℤ≥‘2) ∧ ((2↑𝐼) − 1) ∈ ℝ+
∧ (2↑𝐼) ∈
ℝ+) → (((2↑𝐼) − 1) < (2↑𝐼) ↔ (2 logb ((2↑𝐼) − 1)) < (2
logb (2↑𝐼)))) | 
| 77 | 50, 24, 71, 76 | syl3anc 1373 | . . . . 5
⊢ (𝐼 ∈ ℕ →
(((2↑𝐼) − 1)
< (2↑𝐼) ↔ (2
logb ((2↑𝐼)
− 1)) < (2 logb (2↑𝐼)))) | 
| 78 | 75, 77 | mpbid 232 | . . . 4
⊢ (𝐼 ∈ ℕ → (2
logb ((2↑𝐼)
− 1)) < (2 logb (2↑𝐼))) | 
| 79 | 64 | leidd 11829 | . . . . 5
⊢ (𝐼 ∈ ℕ → 𝐼 ≤ 𝐼) | 
| 80 |  | nnlogbexp 26824 | . . . . . 6
⊢ ((2
∈ (ℤ≥‘2) ∧ 𝐼 ∈ ℤ) → (2 logb
(2↑𝐼)) = 𝐼) | 
| 81 | 35, 11, 80 | sylancr 587 | . . . . 5
⊢ (𝐼 ∈ ℕ → (2
logb (2↑𝐼))
= 𝐼) | 
| 82 |  | nncn 12274 | . . . . . 6
⊢ (𝐼 ∈ ℕ → 𝐼 ∈
ℂ) | 
| 83 |  | npcan1 11688 | . . . . . 6
⊢ (𝐼 ∈ ℂ → ((𝐼 − 1) + 1) = 𝐼) | 
| 84 | 82, 83 | syl 17 | . . . . 5
⊢ (𝐼 ∈ ℕ → ((𝐼 − 1) + 1) = 𝐼) | 
| 85 | 79, 81, 84 | 3brtr4d 5175 | . . . 4
⊢ (𝐼 ∈ ℕ → (2
logb (2↑𝐼))
≤ ((𝐼 − 1) +
1)) | 
| 86 | 29, 73, 68, 78, 85 | ltletrd 11421 | . . 3
⊢ (𝐼 ∈ ℕ → (2
logb ((2↑𝐼)
− 1)) < ((𝐼
− 1) + 1)) | 
| 87 | 63, 29, 68, 70, 86 | lelttrd 11419 | . 2
⊢ (𝐼 ∈ ℕ →
(⌊‘(2 logb ((2↑𝐼) − 1))) < ((𝐼 − 1) + 1)) | 
| 88 |  | zgeltp1eq 47321 | . . 3
⊢
(((⌊‘(2 logb ((2↑𝐼) − 1))) ∈ ℤ ∧ (𝐼 − 1) ∈ ℤ)
→ (((𝐼 − 1) ≤
(⌊‘(2 logb ((2↑𝐼) − 1))) ∧ (⌊‘(2
logb ((2↑𝐼)
− 1))) < ((𝐼
− 1) + 1)) → (⌊‘(2 logb ((2↑𝐼) − 1))) = (𝐼 − 1))) | 
| 89 | 88 | imp 406 | . 2
⊢
((((⌊‘(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 839 | 1
⊢ (𝐼 ∈ ℕ →
(⌊‘(2 logb ((2↑𝐼) − 1))) = (𝐼 − 1)) |