Proof of Theorem log2ublem2
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | log2ublem2.1 | . 2
⊢
(((3↑7) · (5 · 7)) · Σ𝑛 ∈ (0...𝐾)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ≤ (2 · 𝐵) | 
| 2 |  | fzfid 14014 | . . . 4
⊢ (⊤
→ (0...𝐾) ∈
Fin) | 
| 3 |  | elfznn0 13660 | . . . . . 6
⊢ (𝑛 ∈ (0...𝐾) → 𝑛 ∈ ℕ0) | 
| 4 | 3 | adantl 481 | . . . . 5
⊢
((⊤ ∧ 𝑛
∈ (0...𝐾)) →
𝑛 ∈
ℕ0) | 
| 5 |  | 2re 12340 | . . . . . 6
⊢ 2 ∈
ℝ | 
| 6 |  | 3nn 12345 | . . . . . . . 8
⊢ 3 ∈
ℕ | 
| 7 |  | 2nn0 12543 | . . . . . . . . . 10
⊢ 2 ∈
ℕ0 | 
| 8 |  | nn0mulcl 12562 | . . . . . . . . . 10
⊢ ((2
∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → (2
· 𝑛) ∈
ℕ0) | 
| 9 | 7, 8 | mpan 690 | . . . . . . . . 9
⊢ (𝑛 ∈ ℕ0
→ (2 · 𝑛)
∈ ℕ0) | 
| 10 |  | nn0p1nn 12565 | . . . . . . . . 9
⊢ ((2
· 𝑛) ∈
ℕ0 → ((2 · 𝑛) + 1) ∈ ℕ) | 
| 11 | 9, 10 | syl 17 | . . . . . . . 8
⊢ (𝑛 ∈ ℕ0
→ ((2 · 𝑛) + 1)
∈ ℕ) | 
| 12 |  | nnmulcl 12290 | . . . . . . . 8
⊢ ((3
∈ ℕ ∧ ((2 · 𝑛) + 1) ∈ ℕ) → (3 · ((2
· 𝑛) + 1)) ∈
ℕ) | 
| 13 | 6, 11, 12 | sylancr 587 | . . . . . . 7
⊢ (𝑛 ∈ ℕ0
→ (3 · ((2 · 𝑛) + 1)) ∈ ℕ) | 
| 14 |  | 9nn 12364 | . . . . . . . 8
⊢ 9 ∈
ℕ | 
| 15 |  | nnexpcl 14115 | . . . . . . . 8
⊢ ((9
∈ ℕ ∧ 𝑛
∈ ℕ0) → (9↑𝑛) ∈ ℕ) | 
| 16 | 14, 15 | mpan 690 | . . . . . . 7
⊢ (𝑛 ∈ ℕ0
→ (9↑𝑛) ∈
ℕ) | 
| 17 | 13, 16 | nnmulcld 12319 | . . . . . 6
⊢ (𝑛 ∈ ℕ0
→ ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)) ∈ ℕ) | 
| 18 |  | nndivre 12307 | . . . . . 6
⊢ ((2
∈ ℝ ∧ ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)) ∈ ℕ) → (2 / ((3 ·
((2 · 𝑛) + 1))
· (9↑𝑛)))
∈ ℝ) | 
| 19 | 5, 17, 18 | sylancr 587 | . . . . 5
⊢ (𝑛 ∈ ℕ0
→ (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ ℝ) | 
| 20 | 4, 19 | syl 17 | . . . 4
⊢
((⊤ ∧ 𝑛
∈ (0...𝐾)) → (2 /
((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ ℝ) | 
| 21 | 2, 20 | fsumrecl 15770 | . . 3
⊢ (⊤
→ Σ𝑛 ∈
(0...𝐾)(2 / ((3 ·
((2 · 𝑛) + 1))
· (9↑𝑛)))
∈ ℝ) | 
| 22 | 21 | mptru 1547 | . 2
⊢
Σ𝑛 ∈
(0...𝐾)(2 / ((3 ·
((2 · 𝑛) + 1))
· (9↑𝑛)))
∈ ℝ | 
| 23 |  | log2ublem2.4 | . . . . . 6
⊢ 𝑁 ∈
ℕ0 | 
| 24 | 7, 23 | nn0mulcli 12564 | . . . . 5
⊢ (2
· 𝑁) ∈
ℕ0 | 
| 25 |  | nn0p1nn 12565 | . . . . 5
⊢ ((2
· 𝑁) ∈
ℕ0 → ((2 · 𝑁) + 1) ∈ ℕ) | 
| 26 | 24, 25 | ax-mp 5 | . . . 4
⊢ ((2
· 𝑁) + 1) ∈
ℕ | 
| 27 | 6, 26 | nnmulcli 12291 | . . 3
⊢ (3
· ((2 · 𝑁) +
1)) ∈ ℕ | 
| 28 |  | nnexpcl 14115 | . . . 4
⊢ ((9
∈ ℕ ∧ 𝑁
∈ ℕ0) → (9↑𝑁) ∈ ℕ) | 
| 29 | 14, 23, 28 | mp2an 692 | . . 3
⊢
(9↑𝑁) ∈
ℕ | 
| 30 | 27, 29 | nnmulcli 12291 | . 2
⊢ ((3
· ((2 · 𝑁) +
1)) · (9↑𝑁))
∈ ℕ | 
| 31 |  | log2ublem2.2 | . . 3
⊢ 𝐵 ∈
ℕ0 | 
| 32 | 7, 31 | nn0mulcli 12564 | . 2
⊢ (2
· 𝐵) ∈
ℕ0 | 
| 33 |  | log2ublem2.3 | . . 3
⊢ 𝐹 ∈
ℕ0 | 
| 34 | 7, 33 | nn0mulcli 12564 | . 2
⊢ (2
· 𝐹) ∈
ℕ0 | 
| 35 |  | nn0uz 12920 | . . . . . . 7
⊢
ℕ0 = (ℤ≥‘0) | 
| 36 | 23, 35 | eleqtri 2839 | . . . . . 6
⊢ 𝑁 ∈
(ℤ≥‘0) | 
| 37 | 36 | a1i 11 | . . . . 5
⊢ (⊤
→ 𝑁 ∈
(ℤ≥‘0)) | 
| 38 |  | elfznn0 13660 | . . . . . . 7
⊢ (𝑛 ∈ (0...𝑁) → 𝑛 ∈ ℕ0) | 
| 39 | 38 | adantl 481 | . . . . . 6
⊢
((⊤ ∧ 𝑛
∈ (0...𝑁)) →
𝑛 ∈
ℕ0) | 
| 40 | 19 | recnd 11289 | . . . . . 6
⊢ (𝑛 ∈ ℕ0
→ (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ ℂ) | 
| 41 | 39, 40 | syl 17 | . . . . 5
⊢
((⊤ ∧ 𝑛
∈ (0...𝑁)) → (2 /
((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ ℂ) | 
| 42 |  | oveq2 7439 | . . . . . . . . 9
⊢ (𝑛 = 𝑁 → (2 · 𝑛) = (2 · 𝑁)) | 
| 43 | 42 | oveq1d 7446 | . . . . . . . 8
⊢ (𝑛 = 𝑁 → ((2 · 𝑛) + 1) = ((2 · 𝑁) + 1)) | 
| 44 | 43 | oveq2d 7447 | . . . . . . 7
⊢ (𝑛 = 𝑁 → (3 · ((2 · 𝑛) + 1)) = (3 · ((2
· 𝑁) +
1))) | 
| 45 |  | oveq2 7439 | . . . . . . 7
⊢ (𝑛 = 𝑁 → (9↑𝑛) = (9↑𝑁)) | 
| 46 | 44, 45 | oveq12d 7449 | . . . . . 6
⊢ (𝑛 = 𝑁 → ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)) = ((3 · ((2 ·
𝑁) + 1)) ·
(9↑𝑁))) | 
| 47 | 46 | oveq2d 7447 | . . . . 5
⊢ (𝑛 = 𝑁 → (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) = (2 / ((3 · ((2
· 𝑁) + 1)) ·
(9↑𝑁)))) | 
| 48 | 37, 41, 47 | fsumm1 15787 | . . . 4
⊢ (⊤
→ Σ𝑛 ∈
(0...𝑁)(2 / ((3 ·
((2 · 𝑛) + 1))
· (9↑𝑛))) =
(Σ𝑛 ∈
(0...(𝑁 − 1))(2 / ((3
· ((2 · 𝑛) +
1)) · (9↑𝑛))) +
(2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑁))))) | 
| 49 | 48 | mptru 1547 | . . 3
⊢
Σ𝑛 ∈
(0...𝑁)(2 / ((3 ·
((2 · 𝑛) + 1))
· (9↑𝑛))) =
(Σ𝑛 ∈
(0...(𝑁 − 1))(2 / ((3
· ((2 · 𝑛) +
1)) · (9↑𝑛))) +
(2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑁)))) | 
| 50 |  | log2ublem2.5 | . . . . . 6
⊢ (𝑁 − 1) = 𝐾 | 
| 51 | 50 | oveq2i 7442 | . . . . 5
⊢
(0...(𝑁 − 1))
= (0...𝐾) | 
| 52 | 51 | sumeq1i 15733 | . . . 4
⊢
Σ𝑛 ∈
(0...(𝑁 − 1))(2 / ((3
· ((2 · 𝑛) +
1)) · (9↑𝑛))) =
Σ𝑛 ∈ (0...𝐾)(2 / ((3 · ((2 ·
𝑛) + 1)) ·
(9↑𝑛))) | 
| 53 | 52 | oveq1i 7441 | . . 3
⊢
(Σ𝑛 ∈
(0...(𝑁 − 1))(2 / ((3
· ((2 · 𝑛) +
1)) · (9↑𝑛))) +
(2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑁)))) = (Σ𝑛 ∈ (0...𝐾)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) + (2 / ((3 · ((2
· 𝑁) + 1)) ·
(9↑𝑁)))) | 
| 54 | 49, 53 | eqtri 2765 | . 2
⊢
Σ𝑛 ∈
(0...𝑁)(2 / ((3 ·
((2 · 𝑛) + 1))
· (9↑𝑛))) =
(Σ𝑛 ∈ (0...𝐾)(2 / ((3 · ((2 ·
𝑛) + 1)) ·
(9↑𝑛))) + (2 / ((3
· ((2 · 𝑁) +
1)) · (9↑𝑁)))) | 
| 55 |  | 2cn 12341 | . . . 4
⊢ 2 ∈
ℂ | 
| 56 | 31 | nn0cni 12538 | . . . 4
⊢ 𝐵 ∈ ℂ | 
| 57 | 33 | nn0cni 12538 | . . . 4
⊢ 𝐹 ∈ ℂ | 
| 58 | 55, 56, 57 | adddii 11273 | . . 3
⊢ (2
· (𝐵 + 𝐹)) = ((2 · 𝐵) + (2 · 𝐹)) | 
| 59 |  | log2ublem2.6 | . . . 4
⊢ (𝐵 + 𝐹) = 𝐺 | 
| 60 | 59 | oveq2i 7442 | . . 3
⊢ (2
· (𝐵 + 𝐹)) = (2 · 𝐺) | 
| 61 | 58, 60 | eqtr3i 2767 | . 2
⊢ ((2
· 𝐵) + (2 ·
𝐹)) = (2 · 𝐺) | 
| 62 |  | 7nn 12358 | . . . . . . . . 9
⊢ 7 ∈
ℕ | 
| 63 | 62 | nnnn0i 12534 | . . . . . . . 8
⊢ 7 ∈
ℕ0 | 
| 64 |  | nnexpcl 14115 | . . . . . . . 8
⊢ ((3
∈ ℕ ∧ 7 ∈ ℕ0) → (3↑7) ∈
ℕ) | 
| 65 | 6, 63, 64 | mp2an 692 | . . . . . . 7
⊢
(3↑7) ∈ ℕ | 
| 66 |  | 5nn 12352 | . . . . . . . 8
⊢ 5 ∈
ℕ | 
| 67 | 66, 62 | nnmulcli 12291 | . . . . . . 7
⊢ (5
· 7) ∈ ℕ | 
| 68 | 65, 67 | nnmulcli 12291 | . . . . . 6
⊢
((3↑7) · (5 · 7)) ∈ ℕ | 
| 69 | 68 | nnrei 12275 | . . . . 5
⊢
((3↑7) · (5 · 7)) ∈ ℝ | 
| 70 | 69, 5 | remulcli 11277 | . . . 4
⊢
(((3↑7) · (5 · 7)) · 2) ∈
ℝ | 
| 71 | 70 | leidi 11797 | . . 3
⊢
(((3↑7) · (5 · 7)) · 2) ≤ (((3↑7)
· (5 · 7)) · 2) | 
| 72 | 6 | nnnn0i 12534 | . . . . . . . . . . . 12
⊢ 3 ∈
ℕ0 | 
| 73 |  | nnexpcl 14115 | . . . . . . . . . . . 12
⊢ ((9
∈ ℕ ∧ 3 ∈ ℕ0) → (9↑3) ∈
ℕ) | 
| 74 | 14, 72, 73 | mp2an 692 | . . . . . . . . . . 11
⊢
(9↑3) ∈ ℕ | 
| 75 | 74 | nncni 12276 | . . . . . . . . . 10
⊢
(9↑3) ∈ ℂ | 
| 76 | 67 | nncni 12276 | . . . . . . . . . 10
⊢ (5
· 7) ∈ ℂ | 
| 77 | 75, 76 | mulcomi 11269 | . . . . . . . . 9
⊢
((9↑3) · (5 · 7)) = ((5 · 7) ·
(9↑3)) | 
| 78 |  | log2ublem2.8 | . . . . . . . . . . . . 13
⊢ (𝑀 + 𝑁) = 3 | 
| 79 |  | log2ublem2.7 | . . . . . . . . . . . . . . 15
⊢ 𝑀 ∈
ℕ0 | 
| 80 | 79 | nn0cni 12538 | . . . . . . . . . . . . . 14
⊢ 𝑀 ∈ ℂ | 
| 81 | 23 | nn0cni 12538 | . . . . . . . . . . . . . 14
⊢ 𝑁 ∈ ℂ | 
| 82 | 80, 81 | addcomi 11452 | . . . . . . . . . . . . 13
⊢ (𝑀 + 𝑁) = (𝑁 + 𝑀) | 
| 83 | 78, 82 | eqtr3i 2767 | . . . . . . . . . . . 12
⊢ 3 =
(𝑁 + 𝑀) | 
| 84 | 83 | oveq2i 7442 | . . . . . . . . . . 11
⊢
(9↑3) = (9↑(𝑁 + 𝑀)) | 
| 85 | 14 | nncni 12276 | . . . . . . . . . . . 12
⊢ 9 ∈
ℂ | 
| 86 |  | expadd 14145 | . . . . . . . . . . . 12
⊢ ((9
∈ ℂ ∧ 𝑁
∈ ℕ0 ∧ 𝑀 ∈ ℕ0) →
(9↑(𝑁 + 𝑀)) = ((9↑𝑁) · (9↑𝑀))) | 
| 87 | 85, 23, 79, 86 | mp3an 1463 | . . . . . . . . . . 11
⊢
(9↑(𝑁 + 𝑀)) = ((9↑𝑁) · (9↑𝑀)) | 
| 88 | 84, 87 | eqtri 2765 | . . . . . . . . . 10
⊢
(9↑3) = ((9↑𝑁) · (9↑𝑀)) | 
| 89 | 88 | oveq2i 7442 | . . . . . . . . 9
⊢ ((5
· 7) · (9↑3)) = ((5 · 7) · ((9↑𝑁) · (9↑𝑀))) | 
| 90 | 29 | nncni 12276 | . . . . . . . . . 10
⊢
(9↑𝑁) ∈
ℂ | 
| 91 |  | nnexpcl 14115 | . . . . . . . . . . . 12
⊢ ((9
∈ ℕ ∧ 𝑀
∈ ℕ0) → (9↑𝑀) ∈ ℕ) | 
| 92 | 14, 79, 91 | mp2an 692 | . . . . . . . . . . 11
⊢
(9↑𝑀) ∈
ℕ | 
| 93 | 92 | nncni 12276 | . . . . . . . . . 10
⊢
(9↑𝑀) ∈
ℂ | 
| 94 | 76, 90, 93 | mul12i 11456 | . . . . . . . . 9
⊢ ((5
· 7) · ((9↑𝑁) · (9↑𝑀))) = ((9↑𝑁) · ((5 · 7) ·
(9↑𝑀))) | 
| 95 | 77, 89, 94 | 3eqtri 2769 | . . . . . . . 8
⊢
((9↑3) · (5 · 7)) = ((9↑𝑁) · ((5 · 7) ·
(9↑𝑀))) | 
| 96 |  | log2ublem2.9 | . . . . . . . . 9
⊢ ((5
· 7) · (9↑𝑀)) = (((2 · 𝑁) + 1) · 𝐹) | 
| 97 | 96 | oveq2i 7442 | . . . . . . . 8
⊢
((9↑𝑁) ·
((5 · 7) · (9↑𝑀))) = ((9↑𝑁) · (((2 · 𝑁) + 1) · 𝐹)) | 
| 98 | 95, 97 | eqtri 2765 | . . . . . . 7
⊢
((9↑3) · (5 · 7)) = ((9↑𝑁) · (((2 · 𝑁) + 1) · 𝐹)) | 
| 99 | 98 | oveq2i 7442 | . . . . . 6
⊢ (3
· ((9↑3) · (5 · 7))) = (3 · ((9↑𝑁) · (((2 · 𝑁) + 1) · 𝐹))) | 
| 100 |  | df-7 12334 | . . . . . . . . . 10
⊢ 7 = (6 +
1) | 
| 101 | 100 | oveq2i 7442 | . . . . . . . . 9
⊢
(3↑7) = (3↑(6 + 1)) | 
| 102 |  | 3cn 12347 | . . . . . . . . . . 11
⊢ 3 ∈
ℂ | 
| 103 |  | 6nn0 12547 | . . . . . . . . . . 11
⊢ 6 ∈
ℕ0 | 
| 104 |  | expp1 14109 | . . . . . . . . . . 11
⊢ ((3
∈ ℂ ∧ 6 ∈ ℕ0) → (3↑(6 + 1)) =
((3↑6) · 3)) | 
| 105 | 102, 103,
104 | mp2an 692 | . . . . . . . . . 10
⊢
(3↑(6 + 1)) = ((3↑6) · 3) | 
| 106 |  | expmul 14148 | . . . . . . . . . . . . 13
⊢ ((3
∈ ℂ ∧ 2 ∈ ℕ0 ∧ 3 ∈
ℕ0) → (3↑(2 · 3)) =
((3↑2)↑3)) | 
| 107 | 102, 7, 72, 106 | mp3an 1463 | . . . . . . . . . . . 12
⊢
(3↑(2 · 3)) = ((3↑2)↑3) | 
| 108 | 55, 102 | mulcomi 11269 | . . . . . . . . . . . . . 14
⊢ (2
· 3) = (3 · 2) | 
| 109 |  | 3t2e6 12432 | . . . . . . . . . . . . . 14
⊢ (3
· 2) = 6 | 
| 110 | 108, 109 | eqtri 2765 | . . . . . . . . . . . . 13
⊢ (2
· 3) = 6 | 
| 111 | 110 | oveq2i 7442 | . . . . . . . . . . . 12
⊢
(3↑(2 · 3)) = (3↑6) | 
| 112 |  | sq3 14237 | . . . . . . . . . . . . 13
⊢
(3↑2) = 9 | 
| 113 | 112 | oveq1i 7441 | . . . . . . . . . . . 12
⊢
((3↑2)↑3) = (9↑3) | 
| 114 | 107, 111,
113 | 3eqtr3i 2773 | . . . . . . . . . . 11
⊢
(3↑6) = (9↑3) | 
| 115 | 114 | oveq1i 7441 | . . . . . . . . . 10
⊢
((3↑6) · 3) = ((9↑3) · 3) | 
| 116 | 105, 115 | eqtri 2765 | . . . . . . . . 9
⊢
(3↑(6 + 1)) = ((9↑3) · 3) | 
| 117 | 75, 102 | mulcomi 11269 | . . . . . . . . 9
⊢
((9↑3) · 3) = (3 · (9↑3)) | 
| 118 | 101, 116,
117 | 3eqtri 2769 | . . . . . . . 8
⊢
(3↑7) = (3 · (9↑3)) | 
| 119 | 118 | oveq1i 7441 | . . . . . . 7
⊢
((3↑7) · (5 · 7)) = ((3 · (9↑3)) ·
(5 · 7)) | 
| 120 | 102, 75, 76 | mulassi 11272 | . . . . . . 7
⊢ ((3
· (9↑3)) · (5 · 7)) = (3 · ((9↑3)
· (5 · 7))) | 
| 121 | 119, 120 | eqtri 2765 | . . . . . 6
⊢
((3↑7) · (5 · 7)) = (3 · ((9↑3) ·
(5 · 7))) | 
| 122 | 26 | nncni 12276 | . . . . . . . . 9
⊢ ((2
· 𝑁) + 1) ∈
ℂ | 
| 123 | 102, 122,
90 | mul32i 11457 | . . . . . . . 8
⊢ ((3
· ((2 · 𝑁) +
1)) · (9↑𝑁)) =
((3 · (9↑𝑁))
· ((2 · 𝑁) +
1)) | 
| 124 | 123 | oveq1i 7441 | . . . . . . 7
⊢ (((3
· ((2 · 𝑁) +
1)) · (9↑𝑁))
· 𝐹) = (((3 ·
(9↑𝑁)) · ((2
· 𝑁) + 1)) ·
𝐹) | 
| 125 | 102, 90 | mulcli 11268 | . . . . . . . 8
⊢ (3
· (9↑𝑁)) ∈
ℂ | 
| 126 | 125, 122,
57 | mulassi 11272 | . . . . . . 7
⊢ (((3
· (9↑𝑁))
· ((2 · 𝑁) +
1)) · 𝐹) = ((3
· (9↑𝑁))
· (((2 · 𝑁) +
1) · 𝐹)) | 
| 127 | 122, 57 | mulcli 11268 | . . . . . . . 8
⊢ (((2
· 𝑁) + 1) ·
𝐹) ∈
ℂ | 
| 128 | 102, 90, 127 | mulassi 11272 | . . . . . . 7
⊢ ((3
· (9↑𝑁))
· (((2 · 𝑁) +
1) · 𝐹)) = (3
· ((9↑𝑁)
· (((2 · 𝑁) +
1) · 𝐹))) | 
| 129 | 124, 126,
128 | 3eqtri 2769 | . . . . . 6
⊢ (((3
· ((2 · 𝑁) +
1)) · (9↑𝑁))
· 𝐹) = (3 ·
((9↑𝑁) · (((2
· 𝑁) + 1) ·
𝐹))) | 
| 130 | 99, 121, 129 | 3eqtr4i 2775 | . . . . 5
⊢
((3↑7) · (5 · 7)) = (((3 · ((2 · 𝑁) + 1)) · (9↑𝑁)) · 𝐹) | 
| 131 | 130 | oveq2i 7442 | . . . 4
⊢ (2
· ((3↑7) · (5 · 7))) = (2 · (((3 · ((2
· 𝑁) + 1)) ·
(9↑𝑁)) · 𝐹)) | 
| 132 | 65 | nncni 12276 | . . . . . 6
⊢
(3↑7) ∈ ℂ | 
| 133 | 132, 76 | mulcli 11268 | . . . . 5
⊢
((3↑7) · (5 · 7)) ∈ ℂ | 
| 134 | 133, 55 | mulcomi 11269 | . . . 4
⊢
(((3↑7) · (5 · 7)) · 2) = (2 ·
((3↑7) · (5 · 7))) | 
| 135 | 30 | nncni 12276 | . . . . 5
⊢ ((3
· ((2 · 𝑁) +
1)) · (9↑𝑁))
∈ ℂ | 
| 136 | 135, 55, 57 | mul12i 11456 | . . . 4
⊢ (((3
· ((2 · 𝑁) +
1)) · (9↑𝑁))
· (2 · 𝐹)) =
(2 · (((3 · ((2 · 𝑁) + 1)) · (9↑𝑁)) · 𝐹)) | 
| 137 | 131, 134,
136 | 3eqtr4i 2775 | . . 3
⊢
(((3↑7) · (5 · 7)) · 2) = (((3 · ((2
· 𝑁) + 1)) ·
(9↑𝑁)) · (2
· 𝐹)) | 
| 138 | 71, 137 | breqtri 5168 | . 2
⊢
(((3↑7) · (5 · 7)) · 2) ≤ (((3 · ((2
· 𝑁) + 1)) ·
(9↑𝑁)) · (2
· 𝐹)) | 
| 139 | 1, 22, 7, 30, 32, 34, 54, 61, 138 | log2ublem1 26989 | 1
⊢
(((3↑7) · (5 · 7)) · Σ𝑛 ∈ (0...𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ≤ (2 · 𝐺) |