MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  log2tlbnd Structured version   Visualization version   GIF version

Theorem log2tlbnd 24585
Description: Bound the error term in the series of log2cnv 24584. (Contributed by Mario Carneiro, 7-Apr-2015.)
Assertion
Ref Expression
log2tlbnd (𝑁 ∈ ℕ0 → ((log‘2) − Σ𝑛 ∈ (0...(𝑁 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ∈ (0[,](3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁)))))
Distinct variable group:   𝑛,𝑁

Proof of Theorem log2tlbnd
Dummy variable 𝑘 is distinct from all other variables.
StepHypRef Expression
1 nn0uz 11673 . . . . . 6 0 = (ℤ‘0)
2 0zd 11340 . . . . . 6 (𝑁 ∈ ℕ0 → 0 ∈ ℤ)
3 oveq2 6618 . . . . . . . . . . . 12 (𝑘 = 𝑛 → (2 · 𝑘) = (2 · 𝑛))
43oveq1d 6625 . . . . . . . . . . 11 (𝑘 = 𝑛 → ((2 · 𝑘) + 1) = ((2 · 𝑛) + 1))
54oveq2d 6626 . . . . . . . . . 10 (𝑘 = 𝑛 → (3 · ((2 · 𝑘) + 1)) = (3 · ((2 · 𝑛) + 1)))
6 oveq2 6618 . . . . . . . . . 10 (𝑘 = 𝑛 → (9↑𝑘) = (9↑𝑛))
75, 6oveq12d 6628 . . . . . . . . 9 (𝑘 = 𝑛 → ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘)) = ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))
87oveq2d 6626 . . . . . . . 8 (𝑘 = 𝑛 → (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))) = (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))))
9 eqid 2621 . . . . . . . 8 (𝑘 ∈ ℕ0 ↦ (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘)))) = (𝑘 ∈ ℕ0 ↦ (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))))
10 ovex 6638 . . . . . . . 8 (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ V
118, 9, 10fvmpt 6244 . . . . . . 7 (𝑛 ∈ ℕ0 → ((𝑘 ∈ ℕ0 ↦ (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))))‘𝑛) = (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))))
1211adantl 482 . . . . . 6 ((𝑁 ∈ ℕ0𝑛 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))))‘𝑛) = (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))))
13 2re 11041 . . . . . . . 8 2 ∈ ℝ
14 3nn 11137 . . . . . . . . . 10 3 ∈ ℕ
15 2nn0 11260 . . . . . . . . . . . 12 2 ∈ ℕ0
16 simpr 477 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ0𝑛 ∈ ℕ0) → 𝑛 ∈ ℕ0)
17 nn0mulcl 11280 . . . . . . . . . . . 12 ((2 ∈ ℕ0𝑛 ∈ ℕ0) → (2 · 𝑛) ∈ ℕ0)
1815, 16, 17sylancr 694 . . . . . . . . . . 11 ((𝑁 ∈ ℕ0𝑛 ∈ ℕ0) → (2 · 𝑛) ∈ ℕ0)
19 nn0p1nn 11283 . . . . . . . . . . 11 ((2 · 𝑛) ∈ ℕ0 → ((2 · 𝑛) + 1) ∈ ℕ)
2018, 19syl 17 . . . . . . . . . 10 ((𝑁 ∈ ℕ0𝑛 ∈ ℕ0) → ((2 · 𝑛) + 1) ∈ ℕ)
21 nnmulcl 10994 . . . . . . . . . 10 ((3 ∈ ℕ ∧ ((2 · 𝑛) + 1) ∈ ℕ) → (3 · ((2 · 𝑛) + 1)) ∈ ℕ)
2214, 20, 21sylancr 694 . . . . . . . . 9 ((𝑁 ∈ ℕ0𝑛 ∈ ℕ0) → (3 · ((2 · 𝑛) + 1)) ∈ ℕ)
23 9nn 11143 . . . . . . . . . 10 9 ∈ ℕ
24 nnexpcl 12820 . . . . . . . . . 10 ((9 ∈ ℕ ∧ 𝑛 ∈ ℕ0) → (9↑𝑛) ∈ ℕ)
2523, 16, 24sylancr 694 . . . . . . . . 9 ((𝑁 ∈ ℕ0𝑛 ∈ ℕ0) → (9↑𝑛) ∈ ℕ)
2622, 25nnmulcld 11019 . . . . . . . 8 ((𝑁 ∈ ℕ0𝑛 ∈ ℕ0) → ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)) ∈ ℕ)
27 nndivre 11007 . . . . . . . 8 ((2 ∈ ℝ ∧ ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)) ∈ ℕ) → (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ ℝ)
2813, 26, 27sylancr 694 . . . . . . 7 ((𝑁 ∈ ℕ0𝑛 ∈ ℕ0) → (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ ℝ)
2928recnd 10019 . . . . . 6 ((𝑁 ∈ ℕ0𝑛 ∈ ℕ0) → (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ ℂ)
309log2cnv 24584 . . . . . . 7 seq0( + , (𝑘 ∈ ℕ0 ↦ (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))))) ⇝ (log‘2)
3130a1i 11 . . . . . 6 (𝑁 ∈ ℕ0 → seq0( + , (𝑘 ∈ ℕ0 ↦ (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))))) ⇝ (log‘2))
321, 2, 12, 29, 31isumclim 14423 . . . . 5 (𝑁 ∈ ℕ0 → Σ𝑛 ∈ ℕ0 (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) = (log‘2))
33 eqid 2621 . . . . . 6 (ℤ𝑁) = (ℤ𝑁)
34 id 22 . . . . . 6 (𝑁 ∈ ℕ0𝑁 ∈ ℕ0)
35 seqex 12750 . . . . . . . 8 seq0( + , (𝑘 ∈ ℕ0 ↦ (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))))) ∈ V
36 fvex 6163 . . . . . . . 8 (log‘2) ∈ V
3735, 36breldm 5294 . . . . . . 7 (seq0( + , (𝑘 ∈ ℕ0 ↦ (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))))) ⇝ (log‘2) → seq0( + , (𝑘 ∈ ℕ0 ↦ (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))))) ∈ dom ⇝ )
3830, 37mp1i 13 . . . . . 6 (𝑁 ∈ ℕ0 → seq0( + , (𝑘 ∈ ℕ0 ↦ (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))))) ∈ dom ⇝ )
391, 33, 34, 12, 29, 38isumsplit 14504 . . . . 5 (𝑁 ∈ ℕ0 → Σ𝑛 ∈ ℕ0 (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) = (Σ𝑛 ∈ (0...(𝑁 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) + Σ𝑛 ∈ (ℤ𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))))
4032, 39eqtr3d 2657 . . . 4 (𝑁 ∈ ℕ0 → (log‘2) = (Σ𝑛 ∈ (0...(𝑁 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) + Σ𝑛 ∈ (ℤ𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))))
4140oveq1d 6625 . . 3 (𝑁 ∈ ℕ0 → ((log‘2) − Σ𝑛 ∈ (0...(𝑁 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) = ((Σ𝑛 ∈ (0...(𝑁 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) + Σ𝑛 ∈ (ℤ𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) − Σ𝑛 ∈ (0...(𝑁 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))))
42 fzfid 12719 . . . . 5 (𝑁 ∈ ℕ0 → (0...(𝑁 − 1)) ∈ Fin)
43 elfznn0 12381 . . . . . 6 (𝑛 ∈ (0...(𝑁 − 1)) → 𝑛 ∈ ℕ0)
4443, 29sylan2 491 . . . . 5 ((𝑁 ∈ ℕ0𝑛 ∈ (0...(𝑁 − 1))) → (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ ℂ)
4542, 44fsumcl 14404 . . . 4 (𝑁 ∈ ℕ0 → Σ𝑛 ∈ (0...(𝑁 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ ℂ)
46 nn0z 11351 . . . . . 6 (𝑁 ∈ ℕ0𝑁 ∈ ℤ)
47 eluznn0 11708 . . . . . . 7 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → 𝑛 ∈ ℕ0)
4847, 11syl 17 . . . . . 6 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → ((𝑘 ∈ ℕ0 ↦ (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))))‘𝑛) = (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))))
4947, 28syldan 487 . . . . . 6 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ ℝ)
5012, 29eqeltrd 2698 . . . . . . . 8 ((𝑁 ∈ ℕ0𝑛 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))))‘𝑛) ∈ ℂ)
511, 34, 50iserex 14328 . . . . . . 7 (𝑁 ∈ ℕ0 → (seq0( + , (𝑘 ∈ ℕ0 ↦ (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))))) ∈ dom ⇝ ↔ seq𝑁( + , (𝑘 ∈ ℕ0 ↦ (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))))) ∈ dom ⇝ ))
5238, 51mpbid 222 . . . . . 6 (𝑁 ∈ ℕ0 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))))) ∈ dom ⇝ )
5333, 46, 48, 49, 52isumrecl 14431 . . . . 5 (𝑁 ∈ ℕ0 → Σ𝑛 ∈ (ℤ𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ ℝ)
5453recnd 10019 . . . 4 (𝑁 ∈ ℕ0 → Σ𝑛 ∈ (ℤ𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ ℂ)
5545, 54pncan2d 10345 . . 3 (𝑁 ∈ ℕ0 → ((Σ𝑛 ∈ (0...(𝑁 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) + Σ𝑛 ∈ (ℤ𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) − Σ𝑛 ∈ (0...(𝑁 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) = Σ𝑛 ∈ (ℤ𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))))
5641, 55eqtrd 2655 . 2 (𝑁 ∈ ℕ0 → ((log‘2) − Σ𝑛 ∈ (0...(𝑁 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) = Σ𝑛 ∈ (ℤ𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))))
5713a1i 11 . . . . . 6 ((𝑁 ∈ ℕ0𝑛 ∈ ℕ0) → 2 ∈ ℝ)
58 0le2 11062 . . . . . . 7 0 ≤ 2
5958a1i 11 . . . . . 6 ((𝑁 ∈ ℕ0𝑛 ∈ ℕ0) → 0 ≤ 2)
6026nnred 10986 . . . . . 6 ((𝑁 ∈ ℕ0𝑛 ∈ ℕ0) → ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)) ∈ ℝ)
6126nngt0d 11015 . . . . . 6 ((𝑁 ∈ ℕ0𝑛 ∈ ℕ0) → 0 < ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))
62 divge0 10843 . . . . . 6 (((2 ∈ ℝ ∧ 0 ≤ 2) ∧ (((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)) ∈ ℝ ∧ 0 < ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) → 0 ≤ (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))))
6357, 59, 60, 61, 62syl22anc 1324 . . . . 5 ((𝑁 ∈ ℕ0𝑛 ∈ ℕ0) → 0 ≤ (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))))
6447, 63syldan 487 . . . 4 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → 0 ≤ (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))))
6533, 46, 48, 49, 52, 64isumge0 14432 . . 3 (𝑁 ∈ ℕ0 → 0 ≤ Σ𝑛 ∈ (ℤ𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))))
66 oveq2 6618 . . . . . . . . . 10 (𝑘 = 𝑛 → ((1 / 9)↑𝑘) = ((1 / 9)↑𝑛))
6766oveq2d 6626 . . . . . . . . 9 (𝑘 = 𝑛 → ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑘)) = ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑛)))
68 eqid 2621 . . . . . . . . 9 (𝑘 ∈ ℕ0 ↦ ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑘))) = (𝑘 ∈ ℕ0 ↦ ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑘)))
69 ovex 6638 . . . . . . . . 9 ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑛)) ∈ V
7067, 68, 69fvmpt 6244 . . . . . . . 8 (𝑛 ∈ ℕ0 → ((𝑘 ∈ ℕ0 ↦ ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑘)))‘𝑛) = ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑛)))
7170adantl 482 . . . . . . 7 ((𝑁 ∈ ℕ0𝑛 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑘)))‘𝑛) = ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑛)))
72 9cn 11059 . . . . . . . . . . 11 9 ∈ ℂ
7372a1i 11 . . . . . . . . . 10 ((𝑁 ∈ ℕ0𝑛 ∈ ℕ0) → 9 ∈ ℂ)
7423nnne0i 11006 . . . . . . . . . . 11 9 ≠ 0
7574a1i 11 . . . . . . . . . 10 ((𝑁 ∈ ℕ0𝑛 ∈ ℕ0) → 9 ≠ 0)
76 nn0z 11351 . . . . . . . . . . 11 (𝑛 ∈ ℕ0𝑛 ∈ ℤ)
7776adantl 482 . . . . . . . . . 10 ((𝑁 ∈ ℕ0𝑛 ∈ ℕ0) → 𝑛 ∈ ℤ)
7873, 75, 77exprecd 12963 . . . . . . . . 9 ((𝑁 ∈ ℕ0𝑛 ∈ ℕ0) → ((1 / 9)↑𝑛) = (1 / (9↑𝑛)))
7978oveq2d 6626 . . . . . . . 8 ((𝑁 ∈ ℕ0𝑛 ∈ ℕ0) → ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑛)) = ((2 / (3 · ((2 · 𝑁) + 1))) · (1 / (9↑𝑛))))
80 nn0mulcl 11280 . . . . . . . . . . . . . . 15 ((2 ∈ ℕ0𝑁 ∈ ℕ0) → (2 · 𝑁) ∈ ℕ0)
8115, 80mpan 705 . . . . . . . . . . . . . 14 (𝑁 ∈ ℕ0 → (2 · 𝑁) ∈ ℕ0)
82 nn0p1nn 11283 . . . . . . . . . . . . . 14 ((2 · 𝑁) ∈ ℕ0 → ((2 · 𝑁) + 1) ∈ ℕ)
8381, 82syl 17 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ0 → ((2 · 𝑁) + 1) ∈ ℕ)
84 nnmulcl 10994 . . . . . . . . . . . . 13 ((3 ∈ ℕ ∧ ((2 · 𝑁) + 1) ∈ ℕ) → (3 · ((2 · 𝑁) + 1)) ∈ ℕ)
8514, 83, 84sylancr 694 . . . . . . . . . . . 12 (𝑁 ∈ ℕ0 → (3 · ((2 · 𝑁) + 1)) ∈ ℕ)
86 nndivre 11007 . . . . . . . . . . . 12 ((2 ∈ ℝ ∧ (3 · ((2 · 𝑁) + 1)) ∈ ℕ) → (2 / (3 · ((2 · 𝑁) + 1))) ∈ ℝ)
8713, 85, 86sylancr 694 . . . . . . . . . . 11 (𝑁 ∈ ℕ0 → (2 / (3 · ((2 · 𝑁) + 1))) ∈ ℝ)
8887recnd 10019 . . . . . . . . . 10 (𝑁 ∈ ℕ0 → (2 / (3 · ((2 · 𝑁) + 1))) ∈ ℂ)
8988adantr 481 . . . . . . . . 9 ((𝑁 ∈ ℕ0𝑛 ∈ ℕ0) → (2 / (3 · ((2 · 𝑁) + 1))) ∈ ℂ)
9025nncnd 10987 . . . . . . . . 9 ((𝑁 ∈ ℕ0𝑛 ∈ ℕ0) → (9↑𝑛) ∈ ℂ)
9125nnne0d 11016 . . . . . . . . 9 ((𝑁 ∈ ℕ0𝑛 ∈ ℕ0) → (9↑𝑛) ≠ 0)
9289, 90, 91divrecd 10755 . . . . . . . 8 ((𝑁 ∈ ℕ0𝑛 ∈ ℕ0) → ((2 / (3 · ((2 · 𝑁) + 1))) / (9↑𝑛)) = ((2 / (3 · ((2 · 𝑁) + 1))) · (1 / (9↑𝑛))))
93 2cnd 11044 . . . . . . . . 9 ((𝑁 ∈ ℕ0𝑛 ∈ ℕ0) → 2 ∈ ℂ)
9485adantr 481 . . . . . . . . . 10 ((𝑁 ∈ ℕ0𝑛 ∈ ℕ0) → (3 · ((2 · 𝑁) + 1)) ∈ ℕ)
9594nncnd 10987 . . . . . . . . 9 ((𝑁 ∈ ℕ0𝑛 ∈ ℕ0) → (3 · ((2 · 𝑁) + 1)) ∈ ℂ)
9694nnne0d 11016 . . . . . . . . 9 ((𝑁 ∈ ℕ0𝑛 ∈ ℕ0) → (3 · ((2 · 𝑁) + 1)) ≠ 0)
9793, 95, 90, 96, 91divdiv1d 10783 . . . . . . . 8 ((𝑁 ∈ ℕ0𝑛 ∈ ℕ0) → ((2 / (3 · ((2 · 𝑁) + 1))) / (9↑𝑛)) = (2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛))))
9879, 92, 973eqtr2d 2661 . . . . . . 7 ((𝑁 ∈ ℕ0𝑛 ∈ ℕ0) → ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑛)) = (2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛))))
9971, 98eqtrd 2655 . . . . . 6 ((𝑁 ∈ ℕ0𝑛 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑘)))‘𝑛) = (2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛))))
10047, 99syldan 487 . . . . 5 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → ((𝑘 ∈ ℕ0 ↦ ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑘)))‘𝑛) = (2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛))))
10194, 25nnmulcld 11019 . . . . . . 7 ((𝑁 ∈ ℕ0𝑛 ∈ ℕ0) → ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛)) ∈ ℕ)
102 nndivre 11007 . . . . . . 7 ((2 ∈ ℝ ∧ ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛)) ∈ ℕ) → (2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛))) ∈ ℝ)
10313, 101, 102sylancr 694 . . . . . 6 ((𝑁 ∈ ℕ0𝑛 ∈ ℕ0) → (2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛))) ∈ ℝ)
10447, 103syldan 487 . . . . 5 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → (2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛))) ∈ ℝ)
10581adantr 481 . . . . . . . . . 10 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → (2 · 𝑁) ∈ ℕ0)
106105nn0red 11303 . . . . . . . . 9 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → (2 · 𝑁) ∈ ℝ)
10715, 47, 17sylancr 694 . . . . . . . . . 10 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → (2 · 𝑛) ∈ ℕ0)
108107nn0red 11303 . . . . . . . . 9 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → (2 · 𝑛) ∈ ℝ)
109 1red 10006 . . . . . . . . 9 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → 1 ∈ ℝ)
110 eluzle 11651 . . . . . . . . . . 11 (𝑛 ∈ (ℤ𝑁) → 𝑁𝑛)
111110adantl 482 . . . . . . . . . 10 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → 𝑁𝑛)
112 nn0re 11252 . . . . . . . . . . . 12 (𝑁 ∈ ℕ0𝑁 ∈ ℝ)
113112adantr 481 . . . . . . . . . . 11 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → 𝑁 ∈ ℝ)
11447nn0red 11303 . . . . . . . . . . 11 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → 𝑛 ∈ ℝ)
11513a1i 11 . . . . . . . . . . 11 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → 2 ∈ ℝ)
116 2pos 11063 . . . . . . . . . . . 12 0 < 2
117116a1i 11 . . . . . . . . . . 11 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → 0 < 2)
118 lemul2 10827 . . . . . . . . . . 11 ((𝑁 ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (𝑁𝑛 ↔ (2 · 𝑁) ≤ (2 · 𝑛)))
119113, 114, 115, 117, 118syl112anc 1327 . . . . . . . . . 10 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → (𝑁𝑛 ↔ (2 · 𝑁) ≤ (2 · 𝑛)))
120111, 119mpbid 222 . . . . . . . . 9 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → (2 · 𝑁) ≤ (2 · 𝑛))
121106, 108, 109, 120leadd1dd 10592 . . . . . . . 8 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → ((2 · 𝑁) + 1) ≤ ((2 · 𝑛) + 1))
12283adantr 481 . . . . . . . . . 10 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → ((2 · 𝑁) + 1) ∈ ℕ)
123122nnred 10986 . . . . . . . . 9 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → ((2 · 𝑁) + 1) ∈ ℝ)
12447, 20syldan 487 . . . . . . . . . 10 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → ((2 · 𝑛) + 1) ∈ ℕ)
125124nnred 10986 . . . . . . . . 9 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → ((2 · 𝑛) + 1) ∈ ℝ)
126 3re 11045 . . . . . . . . . 10 3 ∈ ℝ
127126a1i 11 . . . . . . . . 9 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → 3 ∈ ℝ)
128 3pos 11065 . . . . . . . . . 10 0 < 3
129128a1i 11 . . . . . . . . 9 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → 0 < 3)
130 lemul2 10827 . . . . . . . . 9 ((((2 · 𝑁) + 1) ∈ ℝ ∧ ((2 · 𝑛) + 1) ∈ ℝ ∧ (3 ∈ ℝ ∧ 0 < 3)) → (((2 · 𝑁) + 1) ≤ ((2 · 𝑛) + 1) ↔ (3 · ((2 · 𝑁) + 1)) ≤ (3 · ((2 · 𝑛) + 1))))
131123, 125, 127, 129, 130syl112anc 1327 . . . . . . . 8 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → (((2 · 𝑁) + 1) ≤ ((2 · 𝑛) + 1) ↔ (3 · ((2 · 𝑁) + 1)) ≤ (3 · ((2 · 𝑛) + 1))))
132121, 131mpbid 222 . . . . . . 7 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → (3 · ((2 · 𝑁) + 1)) ≤ (3 · ((2 · 𝑛) + 1)))
13385adantr 481 . . . . . . . . 9 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → (3 · ((2 · 𝑁) + 1)) ∈ ℕ)
134133nnred 10986 . . . . . . . 8 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → (3 · ((2 · 𝑁) + 1)) ∈ ℝ)
13547, 22syldan 487 . . . . . . . . 9 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → (3 · ((2 · 𝑛) + 1)) ∈ ℕ)
136135nnred 10986 . . . . . . . 8 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → (3 · ((2 · 𝑛) + 1)) ∈ ℝ)
13723, 47, 24sylancr 694 . . . . . . . . 9 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → (9↑𝑛) ∈ ℕ)
138137nnred 10986 . . . . . . . 8 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → (9↑𝑛) ∈ ℝ)
139137nngt0d 11015 . . . . . . . 8 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → 0 < (9↑𝑛))
140 lemul1 10826 . . . . . . . 8 (((3 · ((2 · 𝑁) + 1)) ∈ ℝ ∧ (3 · ((2 · 𝑛) + 1)) ∈ ℝ ∧ ((9↑𝑛) ∈ ℝ ∧ 0 < (9↑𝑛))) → ((3 · ((2 · 𝑁) + 1)) ≤ (3 · ((2 · 𝑛) + 1)) ↔ ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛)) ≤ ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))))
141134, 136, 138, 139, 140syl112anc 1327 . . . . . . 7 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → ((3 · ((2 · 𝑁) + 1)) ≤ (3 · ((2 · 𝑛) + 1)) ↔ ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛)) ≤ ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))))
142132, 141mpbid 222 . . . . . 6 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛)) ≤ ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))
14347, 101syldan 487 . . . . . . . 8 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛)) ∈ ℕ)
144143nnred 10986 . . . . . . 7 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛)) ∈ ℝ)
145143nngt0d 11015 . . . . . . 7 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → 0 < ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛)))
14647, 60syldan 487 . . . . . . 7 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)) ∈ ℝ)
14747, 61syldan 487 . . . . . . 7 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → 0 < ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))
148 lediv2 10864 . . . . . . 7 (((((3 · ((2 · 𝑁) + 1)) · (9↑𝑛)) ∈ ℝ ∧ 0 < ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛))) ∧ (((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)) ∈ ℝ ∧ 0 < ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∧ (2 ∈ ℝ ∧ 0 < 2)) → (((3 · ((2 · 𝑁) + 1)) · (9↑𝑛)) ≤ ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)) ↔ (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ≤ (2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛)))))
149144, 145, 146, 147, 115, 117, 148syl222anc 1339 . . . . . 6 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → (((3 · ((2 · 𝑁) + 1)) · (9↑𝑛)) ≤ ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)) ↔ (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ≤ (2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛)))))
150142, 149mpbid 222 . . . . 5 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ≤ (2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛))))
151 9re 11058 . . . . . . . . . . . 12 9 ∈ ℝ
152151, 74rereccli 10741 . . . . . . . . . . 11 (1 / 9) ∈ ℝ
153152recni 10003 . . . . . . . . . 10 (1 / 9) ∈ ℂ
154153a1i 11 . . . . . . . . 9 (𝑁 ∈ ℕ0 → (1 / 9) ∈ ℂ)
155 0re 9991 . . . . . . . . . . . . 13 0 ∈ ℝ
156 9pos 11073 . . . . . . . . . . . . . 14 0 < 9
157151, 156recgt0ii 10880 . . . . . . . . . . . . 13 0 < (1 / 9)
158155, 152, 157ltleii 10111 . . . . . . . . . . . 12 0 ≤ (1 / 9)
159 absid 13977 . . . . . . . . . . . 12 (((1 / 9) ∈ ℝ ∧ 0 ≤ (1 / 9)) → (abs‘(1 / 9)) = (1 / 9))
160152, 158, 159mp2an 707 . . . . . . . . . . 11 (abs‘(1 / 9)) = (1 / 9)
161 1lt9 11180 . . . . . . . . . . . . 13 1 < 9
162 recgt1i 10871 . . . . . . . . . . . . 13 ((9 ∈ ℝ ∧ 1 < 9) → (0 < (1 / 9) ∧ (1 / 9) < 1))
163151, 161, 162mp2an 707 . . . . . . . . . . . 12 (0 < (1 / 9) ∧ (1 / 9) < 1)
164163simpri 478 . . . . . . . . . . 11 (1 / 9) < 1
165160, 164eqbrtri 4639 . . . . . . . . . 10 (abs‘(1 / 9)) < 1
166165a1i 11 . . . . . . . . 9 (𝑁 ∈ ℕ0 → (abs‘(1 / 9)) < 1)
167 eqid 2621 . . . . . . . . . . 11 (𝑘 ∈ ℕ0 ↦ ((1 / 9)↑𝑘)) = (𝑘 ∈ ℕ0 ↦ ((1 / 9)↑𝑘))
168 ovex 6638 . . . . . . . . . . 11 ((1 / 9)↑𝑛) ∈ V
16966, 167, 168fvmpt 6244 . . . . . . . . . 10 (𝑛 ∈ ℕ0 → ((𝑘 ∈ ℕ0 ↦ ((1 / 9)↑𝑘))‘𝑛) = ((1 / 9)↑𝑛))
17047, 169syl 17 . . . . . . . . 9 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → ((𝑘 ∈ ℕ0 ↦ ((1 / 9)↑𝑘))‘𝑛) = ((1 / 9)↑𝑛))
171154, 166, 34, 170geolim2 14534 . . . . . . . 8 (𝑁 ∈ ℕ0 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((1 / 9)↑𝑘))) ⇝ (((1 / 9)↑𝑁) / (1 − (1 / 9))))
17272a1i 11 . . . . . . . . . . 11 (𝑁 ∈ ℕ0 → 9 ∈ ℂ)
17374a1i 11 . . . . . . . . . . 11 (𝑁 ∈ ℕ0 → 9 ≠ 0)
174172, 173, 46exprecd 12963 . . . . . . . . . 10 (𝑁 ∈ ℕ0 → ((1 / 9)↑𝑁) = (1 / (9↑𝑁)))
17572, 74dividi 10709 . . . . . . . . . . . . 13 (9 / 9) = 1
176175oveq1i 6620 . . . . . . . . . . . 12 ((9 / 9) − (1 / 9)) = (1 − (1 / 9))
177 ax-1cn 9945 . . . . . . . . . . . . . 14 1 ∈ ℂ
17872, 74pm3.2i 471 . . . . . . . . . . . . . 14 (9 ∈ ℂ ∧ 9 ≠ 0)
179 divsubdir 10672 . . . . . . . . . . . . . 14 ((9 ∈ ℂ ∧ 1 ∈ ℂ ∧ (9 ∈ ℂ ∧ 9 ≠ 0)) → ((9 − 1) / 9) = ((9 / 9) − (1 / 9)))
18072, 177, 178, 179mp3an 1421 . . . . . . . . . . . . 13 ((9 − 1) / 9) = ((9 / 9) − (1 / 9))
181 df-9 11037 . . . . . . . . . . . . . . . 16 9 = (8 + 1)
182181oveq1i 6620 . . . . . . . . . . . . . . 15 (9 − 1) = ((8 + 1) − 1)
183 8cn 11057 . . . . . . . . . . . . . . . 16 8 ∈ ℂ
184183, 177pncan3oi 10248 . . . . . . . . . . . . . . 15 ((8 + 1) − 1) = 8
185182, 184eqtri 2643 . . . . . . . . . . . . . 14 (9 − 1) = 8
186185oveq1i 6620 . . . . . . . . . . . . 13 ((9 − 1) / 9) = (8 / 9)
187180, 186eqtr3i 2645 . . . . . . . . . . . 12 ((9 / 9) − (1 / 9)) = (8 / 9)
188176, 187eqtr3i 2645 . . . . . . . . . . 11 (1 − (1 / 9)) = (8 / 9)
189188a1i 11 . . . . . . . . . 10 (𝑁 ∈ ℕ0 → (1 − (1 / 9)) = (8 / 9))
190174, 189oveq12d 6628 . . . . . . . . 9 (𝑁 ∈ ℕ0 → (((1 / 9)↑𝑁) / (1 − (1 / 9))) = ((1 / (9↑𝑁)) / (8 / 9)))
191177a1i 11 . . . . . . . . . 10 (𝑁 ∈ ℕ0 → 1 ∈ ℂ)
192 nnexpcl 12820 . . . . . . . . . . . 12 ((9 ∈ ℕ ∧ 𝑁 ∈ ℕ0) → (9↑𝑁) ∈ ℕ)
19323, 192mpan 705 . . . . . . . . . . 11 (𝑁 ∈ ℕ0 → (9↑𝑁) ∈ ℕ)
194193nncnd 10987 . . . . . . . . . 10 (𝑁 ∈ ℕ0 → (9↑𝑁) ∈ ℂ)
195183, 72, 74divcli 10718 . . . . . . . . . . 11 (8 / 9) ∈ ℂ
196195a1i 11 . . . . . . . . . 10 (𝑁 ∈ ℕ0 → (8 / 9) ∈ ℂ)
197193nnne0d 11016 . . . . . . . . . 10 (𝑁 ∈ ℕ0 → (9↑𝑁) ≠ 0)
198 8nn 11142 . . . . . . . . . . . . 13 8 ∈ ℕ
199198nnne0i 11006 . . . . . . . . . . . 12 8 ≠ 0
200183, 72, 199, 74divne0i 10724 . . . . . . . . . . 11 (8 / 9) ≠ 0
201200a1i 11 . . . . . . . . . 10 (𝑁 ∈ ℕ0 → (8 / 9) ≠ 0)
202191, 194, 196, 197, 201divdiv32d 10777 . . . . . . . . 9 (𝑁 ∈ ℕ0 → ((1 / (9↑𝑁)) / (8 / 9)) = ((1 / (8 / 9)) / (9↑𝑁)))
203 recdiv 10682 . . . . . . . . . . . 12 (((8 ∈ ℂ ∧ 8 ≠ 0) ∧ (9 ∈ ℂ ∧ 9 ≠ 0)) → (1 / (8 / 9)) = (9 / 8))
204183, 199, 72, 74, 203mp4an 708 . . . . . . . . . . 11 (1 / (8 / 9)) = (9 / 8)
205204oveq1i 6620 . . . . . . . . . 10 ((1 / (8 / 9)) / (9↑𝑁)) = ((9 / 8) / (9↑𝑁))
206183a1i 11 . . . . . . . . . . 11 (𝑁 ∈ ℕ0 → 8 ∈ ℂ)
207199a1i 11 . . . . . . . . . . 11 (𝑁 ∈ ℕ0 → 8 ≠ 0)
208172, 206, 194, 207, 197divdiv1d 10783 . . . . . . . . . 10 (𝑁 ∈ ℕ0 → ((9 / 8) / (9↑𝑁)) = (9 / (8 · (9↑𝑁))))
209205, 208syl5eq 2667 . . . . . . . . 9 (𝑁 ∈ ℕ0 → ((1 / (8 / 9)) / (9↑𝑁)) = (9 / (8 · (9↑𝑁))))
210190, 202, 2093eqtrd 2659 . . . . . . . 8 (𝑁 ∈ ℕ0 → (((1 / 9)↑𝑁) / (1 − (1 / 9))) = (9 / (8 · (9↑𝑁))))
211171, 210breqtrd 4644 . . . . . . 7 (𝑁 ∈ ℕ0 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((1 / 9)↑𝑘))) ⇝ (9 / (8 · (9↑𝑁))))
212 expcl 12825 . . . . . . . . 9 (((1 / 9) ∈ ℂ ∧ 𝑛 ∈ ℕ0) → ((1 / 9)↑𝑛) ∈ ℂ)
213153, 47, 212sylancr 694 . . . . . . . 8 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → ((1 / 9)↑𝑛) ∈ ℂ)
214170, 213eqeltrd 2698 . . . . . . 7 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → ((𝑘 ∈ ℕ0 ↦ ((1 / 9)↑𝑘))‘𝑛) ∈ ℂ)
21547, 70syl 17 . . . . . . . 8 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → ((𝑘 ∈ ℕ0 ↦ ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑘)))‘𝑛) = ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑛)))
216170oveq2d 6626 . . . . . . . 8 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → ((2 / (3 · ((2 · 𝑁) + 1))) · ((𝑘 ∈ ℕ0 ↦ ((1 / 9)↑𝑘))‘𝑛)) = ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑛)))
217215, 216eqtr4d 2658 . . . . . . 7 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → ((𝑘 ∈ ℕ0 ↦ ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑘)))‘𝑛) = ((2 / (3 · ((2 · 𝑁) + 1))) · ((𝑘 ∈ ℕ0 ↦ ((1 / 9)↑𝑘))‘𝑛)))
21833, 46, 88, 211, 214, 217isermulc2 14329 . . . . . 6 (𝑁 ∈ ℕ0 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑘)))) ⇝ ((2 / (3 · ((2 · 𝑁) + 1))) · (9 / (8 · (9↑𝑁)))))
219 seqex 12750 . . . . . . 7 seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑘)))) ∈ V
220 ovex 6638 . . . . . . 7 ((2 / (3 · ((2 · 𝑁) + 1))) · (9 / (8 · (9↑𝑁)))) ∈ V
221219, 220breldm 5294 . . . . . 6 (seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑘)))) ⇝ ((2 / (3 · ((2 · 𝑁) + 1))) · (9 / (8 · (9↑𝑁)))) → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑘)))) ∈ dom ⇝ )
222218, 221syl 17 . . . . 5 (𝑁 ∈ ℕ0 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑘)))) ∈ dom ⇝ )
22333, 46, 48, 49, 100, 104, 150, 52, 222isumle 14508 . . . 4 (𝑁 ∈ ℕ0 → Σ𝑛 ∈ (ℤ𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ≤ Σ𝑛 ∈ (ℤ𝑁)(2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛))))
224104recnd 10019 . . . . 5 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → (2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛))) ∈ ℂ)
225 3cn 11046 . . . . . . . . . . . 12 3 ∈ ℂ
226 4cn 11049 . . . . . . . . . . . 12 4 ∈ ℂ
227 2cn 11042 . . . . . . . . . . . 12 2 ∈ ℂ
228 4ne0 11068 . . . . . . . . . . . 12 4 ≠ 0
229 3ne0 11066 . . . . . . . . . . . 12 3 ≠ 0
230 2ne0 11064 . . . . . . . . . . . 12 2 ≠ 0
231225, 226, 227, 225, 228, 229, 230divdivdivi 10739 . . . . . . . . . . 11 ((3 / 4) / (2 / 3)) = ((3 · 3) / (4 · 2))
232 3t3e9 11131 . . . . . . . . . . . 12 (3 · 3) = 9
233 4t2e8 11132 . . . . . . . . . . . 12 (4 · 2) = 8
234232, 233oveq12i 6622 . . . . . . . . . . 11 ((3 · 3) / (4 · 2)) = (9 / 8)
235231, 234eqtri 2643 . . . . . . . . . 10 ((3 / 4) / (2 / 3)) = (9 / 8)
236235oveq2i 6621 . . . . . . . . 9 ((2 / 3) · ((3 / 4) / (2 / 3))) = ((2 / 3) · (9 / 8))
237225, 226, 228divcli 10718 . . . . . . . . . 10 (3 / 4) ∈ ℂ
238227, 225, 229divcli 10718 . . . . . . . . . 10 (2 / 3) ∈ ℂ
239227, 225, 230, 229divne0i 10724 . . . . . . . . . 10 (2 / 3) ≠ 0
240237, 238, 239divcan2i 10719 . . . . . . . . 9 ((2 / 3) · ((3 / 4) / (2 / 3))) = (3 / 4)
241236, 240eqtr3i 2645 . . . . . . . 8 ((2 / 3) · (9 / 8)) = (3 / 4)
242241oveq1i 6620 . . . . . . 7 (((2 / 3) · (9 / 8)) / (((2 · 𝑁) + 1) · (9↑𝑁))) = ((3 / 4) / (((2 · 𝑁) + 1) · (9↑𝑁)))
243 2cnd 11044 . . . . . . . . . 10 (𝑁 ∈ ℕ0 → 2 ∈ ℂ)
244225a1i 11 . . . . . . . . . 10 (𝑁 ∈ ℕ0 → 3 ∈ ℂ)
24583nncnd 10987 . . . . . . . . . 10 (𝑁 ∈ ℕ0 → ((2 · 𝑁) + 1) ∈ ℂ)
246229a1i 11 . . . . . . . . . 10 (𝑁 ∈ ℕ0 → 3 ≠ 0)
24783nnne0d 11016 . . . . . . . . . 10 (𝑁 ∈ ℕ0 → ((2 · 𝑁) + 1) ≠ 0)
248243, 244, 245, 246, 247divdiv1d 10783 . . . . . . . . 9 (𝑁 ∈ ℕ0 → ((2 / 3) / ((2 · 𝑁) + 1)) = (2 / (3 · ((2 · 𝑁) + 1))))
249248, 208oveq12d 6628 . . . . . . . 8 (𝑁 ∈ ℕ0 → (((2 / 3) / ((2 · 𝑁) + 1)) · ((9 / 8) / (9↑𝑁))) = ((2 / (3 · ((2 · 𝑁) + 1))) · (9 / (8 · (9↑𝑁)))))
250238a1i 11 . . . . . . . . 9 (𝑁 ∈ ℕ0 → (2 / 3) ∈ ℂ)
25172, 183, 199divcli 10718 . . . . . . . . . 10 (9 / 8) ∈ ℂ
252251a1i 11 . . . . . . . . 9 (𝑁 ∈ ℕ0 → (9 / 8) ∈ ℂ)
253250, 245, 252, 194, 247, 197divmuldivd 10793 . . . . . . . 8 (𝑁 ∈ ℕ0 → (((2 / 3) / ((2 · 𝑁) + 1)) · ((9 / 8) / (9↑𝑁))) = (((2 / 3) · (9 / 8)) / (((2 · 𝑁) + 1) · (9↑𝑁))))
254249, 253eqtr3d 2657 . . . . . . 7 (𝑁 ∈ ℕ0 → ((2 / (3 · ((2 · 𝑁) + 1))) · (9 / (8 · (9↑𝑁)))) = (((2 / 3) · (9 / 8)) / (((2 · 𝑁) + 1) · (9↑𝑁))))
255226a1i 11 . . . . . . . . . 10 (𝑁 ∈ ℕ0 → 4 ∈ ℂ)
256255, 245, 194mulassd 10014 . . . . . . . . 9 (𝑁 ∈ ℕ0 → ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁)) = (4 · (((2 · 𝑁) + 1) · (9↑𝑁))))
257256oveq2d 6626 . . . . . . . 8 (𝑁 ∈ ℕ0 → (3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁))) = (3 / (4 · (((2 · 𝑁) + 1) · (9↑𝑁)))))
25883, 193nnmulcld 11019 . . . . . . . . . 10 (𝑁 ∈ ℕ0 → (((2 · 𝑁) + 1) · (9↑𝑁)) ∈ ℕ)
259258nncnd 10987 . . . . . . . . 9 (𝑁 ∈ ℕ0 → (((2 · 𝑁) + 1) · (9↑𝑁)) ∈ ℂ)
260228a1i 11 . . . . . . . . 9 (𝑁 ∈ ℕ0 → 4 ≠ 0)
261258nnne0d 11016 . . . . . . . . 9 (𝑁 ∈ ℕ0 → (((2 · 𝑁) + 1) · (9↑𝑁)) ≠ 0)
262244, 255, 259, 260, 261divdiv1d 10783 . . . . . . . 8 (𝑁 ∈ ℕ0 → ((3 / 4) / (((2 · 𝑁) + 1) · (9↑𝑁))) = (3 / (4 · (((2 · 𝑁) + 1) · (9↑𝑁)))))
263257, 262eqtr4d 2658 . . . . . . 7 (𝑁 ∈ ℕ0 → (3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁))) = ((3 / 4) / (((2 · 𝑁) + 1) · (9↑𝑁))))
264242, 254, 2633eqtr4a 2681 . . . . . 6 (𝑁 ∈ ℕ0 → ((2 / (3 · ((2 · 𝑁) + 1))) · (9 / (8 · (9↑𝑁)))) = (3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁))))
265218, 264breqtrd 4644 . . . . 5 (𝑁 ∈ ℕ0 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑘)))) ⇝ (3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁))))
26633, 46, 100, 224, 265isumclim 14423 . . . 4 (𝑁 ∈ ℕ0 → Σ𝑛 ∈ (ℤ𝑁)(2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛))) = (3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁))))
267223, 266breqtrd 4644 . . 3 (𝑁 ∈ ℕ0 → Σ𝑛 ∈ (ℤ𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ≤ (3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁))))
268 4nn 11138 . . . . . . 7 4 ∈ ℕ
269 nnmulcl 10994 . . . . . . 7 ((4 ∈ ℕ ∧ ((2 · 𝑁) + 1) ∈ ℕ) → (4 · ((2 · 𝑁) + 1)) ∈ ℕ)
270268, 83, 269sylancr 694 . . . . . 6 (𝑁 ∈ ℕ0 → (4 · ((2 · 𝑁) + 1)) ∈ ℕ)
271270, 193nnmulcld 11019 . . . . 5 (𝑁 ∈ ℕ0 → ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁)) ∈ ℕ)
272 nndivre 11007 . . . . 5 ((3 ∈ ℝ ∧ ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁)) ∈ ℕ) → (3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁))) ∈ ℝ)
273126, 271, 272sylancr 694 . . . 4 (𝑁 ∈ ℕ0 → (3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁))) ∈ ℝ)
274 elicc2 12187 . . . 4 ((0 ∈ ℝ ∧ (3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁))) ∈ ℝ) → (Σ𝑛 ∈ (ℤ𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ (0[,](3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁)))) ↔ (Σ𝑛 ∈ (ℤ𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ ℝ ∧ 0 ≤ Σ𝑛 ∈ (ℤ𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∧ Σ𝑛 ∈ (ℤ𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ≤ (3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁))))))
275155, 273, 274sylancr 694 . . 3 (𝑁 ∈ ℕ0 → (Σ𝑛 ∈ (ℤ𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ (0[,](3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁)))) ↔ (Σ𝑛 ∈ (ℤ𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ ℝ ∧ 0 ≤ Σ𝑛 ∈ (ℤ𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∧ Σ𝑛 ∈ (ℤ𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ≤ (3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁))))))
27653, 65, 267, 275mpbir3and 1243 . 2 (𝑁 ∈ ℕ0 → Σ𝑛 ∈ (ℤ𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ (0[,](3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁)))))
27756, 276eqeltrd 2698 1 (𝑁 ∈ ℕ0 → ((log‘2) − Σ𝑛 ∈ (0...(𝑁 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ∈ (0[,](3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁)))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  w3a 1036   = wceq 1480  wcel 1987  wne 2790   class class class wbr 4618  cmpt 4678  dom cdm 5079  cfv 5852  (class class class)co 6610  cc 9885  cr 9886  0cc0 9887  1c1 9888   + caddc 9890   · cmul 9892   < clt 10025  cle 10026  cmin 10217   / cdiv 10635  cn 10971  2c2 11021  3c3 11022  4c4 11023  8c8 11027  9c9 11028  0cn0 11243  cz 11328  cuz 11638  [,]cicc 12127  ...cfz 12275  seqcseq 12748  cexp 12807  abscabs 13915  cli 14156  Σcsu 14357  logclog 24218
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909  ax-inf2 8489  ax-cnex 9943  ax-resscn 9944  ax-1cn 9945  ax-icn 9946  ax-addcl 9947  ax-addrcl 9948  ax-mulcl 9949  ax-mulrcl 9950  ax-mulcom 9951  ax-addass 9952  ax-mulass 9953  ax-distr 9954  ax-i2m1 9955  ax-1ne0 9956  ax-1rid 9957  ax-rnegex 9958  ax-rrecex 9959  ax-cnre 9960  ax-pre-lttri 9961  ax-pre-lttrn 9962  ax-pre-ltadd 9963  ax-pre-mulgt0 9964  ax-pre-sup 9965  ax-addf 9966  ax-mulf 9967
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-fal 1486  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-int 4446  df-iun 4492  df-iin 4493  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-se 5039  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5644  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-isom 5861  df-riota 6571  df-ov 6613  df-oprab 6614  df-mpt2 6615  df-of 6857  df-om 7020  df-1st 7120  df-2nd 7121  df-supp 7248  df-wrecs 7359  df-recs 7420  df-rdg 7458  df-1o 7512  df-2o 7513  df-oadd 7516  df-er 7694  df-map 7811  df-pm 7812  df-ixp 7860  df-en 7907  df-dom 7908  df-sdom 7909  df-fin 7910  df-fsupp 8227  df-fi 8268  df-sup 8299  df-inf 8300  df-oi 8366  df-card 8716  df-cda 8941  df-pnf 10027  df-mnf 10028  df-xr 10029  df-ltxr 10030  df-le 10031  df-sub 10219  df-neg 10220  df-div 10636  df-nn 10972  df-2 11030  df-3 11031  df-4 11032  df-5 11033  df-6 11034  df-7 11035  df-8 11036  df-9 11037  df-n0 11244  df-xnn0 11315  df-z 11329  df-dec 11445  df-uz 11639  df-q 11740  df-rp 11784  df-xneg 11897  df-xadd 11898  df-xmul 11899  df-ioo 12128  df-ioc 12129  df-ico 12130  df-icc 12131  df-fz 12276  df-fzo 12414  df-fl 12540  df-mod 12616  df-seq 12749  df-exp 12808  df-fac 13008  df-bc 13037  df-hash 13065  df-shft 13748  df-cj 13780  df-re 13781  df-im 13782  df-sqrt 13916  df-abs 13917  df-limsup 14143  df-clim 14160  df-rlim 14161  df-sum 14358  df-ef 14730  df-sin 14732  df-cos 14733  df-tan 14734  df-pi 14735  df-dvds 14915  df-struct 15790  df-ndx 15791  df-slot 15792  df-base 15793  df-sets 15794  df-ress 15795  df-plusg 15882  df-mulr 15883  df-starv 15884  df-sca 15885  df-vsca 15886  df-ip 15887  df-tset 15888  df-ple 15889  df-ds 15892  df-unif 15893  df-hom 15894  df-cco 15895  df-rest 16011  df-topn 16012  df-0g 16030  df-gsum 16031  df-topgen 16032  df-pt 16033  df-prds 16036  df-xrs 16090  df-qtop 16095  df-imas 16096  df-xps 16098  df-mre 16174  df-mrc 16175  df-acs 16177  df-mgm 17170  df-sgrp 17212  df-mnd 17223  df-submnd 17264  df-mulg 17469  df-cntz 17678  df-cmn 18123  df-psmet 19666  df-xmet 19667  df-met 19668  df-bl 19669  df-mopn 19670  df-fbas 19671  df-fg 19672  df-cnfld 19675  df-top 20627  df-topon 20644  df-topsp 20657  df-bases 20670  df-cld 20742  df-ntr 20743  df-cls 20744  df-nei 20821  df-lp 20859  df-perf 20860  df-cn 20950  df-cnp 20951  df-haus 21038  df-cmp 21109  df-tx 21284  df-hmeo 21477  df-fil 21569  df-fm 21661  df-flim 21662  df-flf 21663  df-xms 22044  df-ms 22045  df-tms 22046  df-cncf 22600  df-limc 23549  df-dv 23550  df-ulm 24048  df-log 24220  df-atan 24507
This theorem is referenced by:  log2ub  24589
  Copyright terms: Public domain W3C validator