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

Theorem log2tlbnd 24893
Description: Bound the error term in the series of log2cnv 24892. (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 11924 . . . . . 6 0 = (ℤ‘0)
2 0zd 11591 . . . . . 6 (𝑁 ∈ ℕ0 → 0 ∈ ℤ)
3 oveq2 6801 . . . . . . . . . . . 12 (𝑘 = 𝑛 → (2 · 𝑘) = (2 · 𝑛))
43oveq1d 6808 . . . . . . . . . . 11 (𝑘 = 𝑛 → ((2 · 𝑘) + 1) = ((2 · 𝑛) + 1))
54oveq2d 6809 . . . . . . . . . 10 (𝑘 = 𝑛 → (3 · ((2 · 𝑘) + 1)) = (3 · ((2 · 𝑛) + 1)))
6 oveq2 6801 . . . . . . . . . 10 (𝑘 = 𝑛 → (9↑𝑘) = (9↑𝑛))
75, 6oveq12d 6811 . . . . . . . . 9 (𝑘 = 𝑛 → ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘)) = ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))
87oveq2d 6809 . . . . . . . 8 (𝑘 = 𝑛 → (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))) = (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))))
9 eqid 2771 . . . . . . . 8 (𝑘 ∈ ℕ0 ↦ (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘)))) = (𝑘 ∈ ℕ0 ↦ (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))))
10 ovex 6823 . . . . . . . 8 (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ V
118, 9, 10fvmpt 6424 . . . . . . 7 (𝑛 ∈ ℕ0 → ((𝑘 ∈ ℕ0 ↦ (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))))‘𝑛) = (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))))
1211adantl 467 . . . . . 6 ((𝑁 ∈ ℕ0𝑛 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))))‘𝑛) = (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))))
13 2re 11292 . . . . . . . 8 2 ∈ ℝ
14 3nn 11388 . . . . . . . . . 10 3 ∈ ℕ
15 2nn0 11511 . . . . . . . . . . . 12 2 ∈ ℕ0
16 simpr 471 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ0𝑛 ∈ ℕ0) → 𝑛 ∈ ℕ0)
17 nn0mulcl 11531 . . . . . . . . . . . 12 ((2 ∈ ℕ0𝑛 ∈ ℕ0) → (2 · 𝑛) ∈ ℕ0)
1815, 16, 17sylancr 575 . . . . . . . . . . 11 ((𝑁 ∈ ℕ0𝑛 ∈ ℕ0) → (2 · 𝑛) ∈ ℕ0)
19 nn0p1nn 11534 . . . . . . . . . . 11 ((2 · 𝑛) ∈ ℕ0 → ((2 · 𝑛) + 1) ∈ ℕ)
2018, 19syl 17 . . . . . . . . . 10 ((𝑁 ∈ ℕ0𝑛 ∈ ℕ0) → ((2 · 𝑛) + 1) ∈ ℕ)
21 nnmulcl 11245 . . . . . . . . . 10 ((3 ∈ ℕ ∧ ((2 · 𝑛) + 1) ∈ ℕ) → (3 · ((2 · 𝑛) + 1)) ∈ ℕ)
2214, 20, 21sylancr 575 . . . . . . . . 9 ((𝑁 ∈ ℕ0𝑛 ∈ ℕ0) → (3 · ((2 · 𝑛) + 1)) ∈ ℕ)
23 9nn 11394 . . . . . . . . . 10 9 ∈ ℕ
24 nnexpcl 13080 . . . . . . . . . 10 ((9 ∈ ℕ ∧ 𝑛 ∈ ℕ0) → (9↑𝑛) ∈ ℕ)
2523, 16, 24sylancr 575 . . . . . . . . 9 ((𝑁 ∈ ℕ0𝑛 ∈ ℕ0) → (9↑𝑛) ∈ ℕ)
2622, 25nnmulcld 11270 . . . . . . . 8 ((𝑁 ∈ ℕ0𝑛 ∈ ℕ0) → ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)) ∈ ℕ)
27 nndivre 11258 . . . . . . . 8 ((2 ∈ ℝ ∧ ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)) ∈ ℕ) → (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ ℝ)
2813, 26, 27sylancr 575 . . . . . . 7 ((𝑁 ∈ ℕ0𝑛 ∈ ℕ0) → (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ ℝ)
2928recnd 10270 . . . . . 6 ((𝑁 ∈ ℕ0𝑛 ∈ ℕ0) → (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ ℂ)
309log2cnv 24892 . . . . . . 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 14696 . . . . 5 (𝑁 ∈ ℕ0 → Σ𝑛 ∈ ℕ0 (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) = (log‘2))
33 eqid 2771 . . . . . 6 (ℤ𝑁) = (ℤ𝑁)
34 id 22 . . . . . 6 (𝑁 ∈ ℕ0𝑁 ∈ ℕ0)
35 seqex 13010 . . . . . . . 8 seq0( + , (𝑘 ∈ ℕ0 ↦ (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))))) ∈ V
36 fvex 6342 . . . . . . . 8 (log‘2) ∈ V
3735, 36breldm 5467 . . . . . . 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 14779 . . . . 5 (𝑁 ∈ ℕ0 → Σ𝑛 ∈ ℕ0 (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) = (Σ𝑛 ∈ (0...(𝑁 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) + Σ𝑛 ∈ (ℤ𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))))
4032, 39eqtr3d 2807 . . . 4 (𝑁 ∈ ℕ0 → (log‘2) = (Σ𝑛 ∈ (0...(𝑁 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) + Σ𝑛 ∈ (ℤ𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))))
4140oveq1d 6808 . . 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 12980 . . . . 5 (𝑁 ∈ ℕ0 → (0...(𝑁 − 1)) ∈ Fin)
43 elfznn0 12640 . . . . . 6 (𝑛 ∈ (0...(𝑁 − 1)) → 𝑛 ∈ ℕ0)
4443, 29sylan2 580 . . . . 5 ((𝑁 ∈ ℕ0𝑛 ∈ (0...(𝑁 − 1))) → (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ ℂ)
4542, 44fsumcl 14672 . . . 4 (𝑁 ∈ ℕ0 → Σ𝑛 ∈ (0...(𝑁 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ ℂ)
46 nn0z 11602 . . . . . 6 (𝑁 ∈ ℕ0𝑁 ∈ ℤ)
47 eluznn0 11960 . . . . . . 7 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → 𝑛 ∈ ℕ0)
4847, 11syl 17 . . . . . 6 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → ((𝑘 ∈ ℕ0 ↦ (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))))‘𝑛) = (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))))
4947, 28syldan 579 . . . . . 6 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ ℝ)
5012, 29eqeltrd 2850 . . . . . . . 8 ((𝑁 ∈ ℕ0𝑛 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))))‘𝑛) ∈ ℂ)
511, 34, 50iserex 14595 . . . . . . 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 14704 . . . . 5 (𝑁 ∈ ℕ0 → Σ𝑛 ∈ (ℤ𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ ℝ)
5453recnd 10270 . . . 4 (𝑁 ∈ ℕ0 → Σ𝑛 ∈ (ℤ𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ ℂ)
5545, 54pncan2d 10596 . . 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 2805 . 2 (𝑁 ∈ ℕ0 → ((log‘2) − Σ𝑛 ∈ (0...(𝑁 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) = Σ𝑛 ∈ (ℤ𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))))
5713a1i 11 . . . . . 6 ((𝑁 ∈ ℕ0𝑛 ∈ ℕ0) → 2 ∈ ℝ)
58 0le2 11313 . . . . . . 7 0 ≤ 2
5958a1i 11 . . . . . 6 ((𝑁 ∈ ℕ0𝑛 ∈ ℕ0) → 0 ≤ 2)
6026nnred 11237 . . . . . 6 ((𝑁 ∈ ℕ0𝑛 ∈ ℕ0) → ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)) ∈ ℝ)
6126nngt0d 11266 . . . . . 6 ((𝑁 ∈ ℕ0𝑛 ∈ ℕ0) → 0 < ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))
62 divge0 11094 . . . . . 6 (((2 ∈ ℝ ∧ 0 ≤ 2) ∧ (((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)) ∈ ℝ ∧ 0 < ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) → 0 ≤ (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))))
6357, 59, 60, 61, 62syl22anc 1477 . . . . 5 ((𝑁 ∈ ℕ0𝑛 ∈ ℕ0) → 0 ≤ (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))))
6447, 63syldan 579 . . . 4 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → 0 ≤ (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))))
6533, 46, 48, 49, 52, 64isumge0 14705 . . 3 (𝑁 ∈ ℕ0 → 0 ≤ Σ𝑛 ∈ (ℤ𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))))
66 oveq2 6801 . . . . . . . . . 10 (𝑘 = 𝑛 → ((1 / 9)↑𝑘) = ((1 / 9)↑𝑛))
6766oveq2d 6809 . . . . . . . . 9 (𝑘 = 𝑛 → ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑘)) = ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑛)))
68 eqid 2771 . . . . . . . . 9 (𝑘 ∈ ℕ0 ↦ ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑘))) = (𝑘 ∈ ℕ0 ↦ ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑘)))
69 ovex 6823 . . . . . . . . 9 ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑛)) ∈ V
7067, 68, 69fvmpt 6424 . . . . . . . 8 (𝑛 ∈ ℕ0 → ((𝑘 ∈ ℕ0 ↦ ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑘)))‘𝑛) = ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑛)))
7170adantl 467 . . . . . . 7 ((𝑁 ∈ ℕ0𝑛 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑘)))‘𝑛) = ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑛)))
72 9cn 11310 . . . . . . . . . . 11 9 ∈ ℂ
7372a1i 11 . . . . . . . . . 10 ((𝑁 ∈ ℕ0𝑛 ∈ ℕ0) → 9 ∈ ℂ)
7423nnne0i 11257 . . . . . . . . . . 11 9 ≠ 0
7574a1i 11 . . . . . . . . . 10 ((𝑁 ∈ ℕ0𝑛 ∈ ℕ0) → 9 ≠ 0)
76 nn0z 11602 . . . . . . . . . . 11 (𝑛 ∈ ℕ0𝑛 ∈ ℤ)
7776adantl 467 . . . . . . . . . 10 ((𝑁 ∈ ℕ0𝑛 ∈ ℕ0) → 𝑛 ∈ ℤ)
7873, 75, 77exprecd 13223 . . . . . . . . 9 ((𝑁 ∈ ℕ0𝑛 ∈ ℕ0) → ((1 / 9)↑𝑛) = (1 / (9↑𝑛)))
7978oveq2d 6809 . . . . . . . 8 ((𝑁 ∈ ℕ0𝑛 ∈ ℕ0) → ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑛)) = ((2 / (3 · ((2 · 𝑁) + 1))) · (1 / (9↑𝑛))))
80 nn0mulcl 11531 . . . . . . . . . . . . . . 15 ((2 ∈ ℕ0𝑁 ∈ ℕ0) → (2 · 𝑁) ∈ ℕ0)
8115, 80mpan 670 . . . . . . . . . . . . . 14 (𝑁 ∈ ℕ0 → (2 · 𝑁) ∈ ℕ0)
82 nn0p1nn 11534 . . . . . . . . . . . . . 14 ((2 · 𝑁) ∈ ℕ0 → ((2 · 𝑁) + 1) ∈ ℕ)
8381, 82syl 17 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ0 → ((2 · 𝑁) + 1) ∈ ℕ)
84 nnmulcl 11245 . . . . . . . . . . . . 13 ((3 ∈ ℕ ∧ ((2 · 𝑁) + 1) ∈ ℕ) → (3 · ((2 · 𝑁) + 1)) ∈ ℕ)
8514, 83, 84sylancr 575 . . . . . . . . . . . 12 (𝑁 ∈ ℕ0 → (3 · ((2 · 𝑁) + 1)) ∈ ℕ)
86 nndivre 11258 . . . . . . . . . . . 12 ((2 ∈ ℝ ∧ (3 · ((2 · 𝑁) + 1)) ∈ ℕ) → (2 / (3 · ((2 · 𝑁) + 1))) ∈ ℝ)
8713, 85, 86sylancr 575 . . . . . . . . . . 11 (𝑁 ∈ ℕ0 → (2 / (3 · ((2 · 𝑁) + 1))) ∈ ℝ)
8887recnd 10270 . . . . . . . . . 10 (𝑁 ∈ ℕ0 → (2 / (3 · ((2 · 𝑁) + 1))) ∈ ℂ)
8988adantr 466 . . . . . . . . 9 ((𝑁 ∈ ℕ0𝑛 ∈ ℕ0) → (2 / (3 · ((2 · 𝑁) + 1))) ∈ ℂ)
9025nncnd 11238 . . . . . . . . 9 ((𝑁 ∈ ℕ0𝑛 ∈ ℕ0) → (9↑𝑛) ∈ ℂ)
9125nnne0d 11267 . . . . . . . . 9 ((𝑁 ∈ ℕ0𝑛 ∈ ℕ0) → (9↑𝑛) ≠ 0)
9289, 90, 91divrecd 11006 . . . . . . . 8 ((𝑁 ∈ ℕ0𝑛 ∈ ℕ0) → ((2 / (3 · ((2 · 𝑁) + 1))) / (9↑𝑛)) = ((2 / (3 · ((2 · 𝑁) + 1))) · (1 / (9↑𝑛))))
93 2cnd 11295 . . . . . . . . 9 ((𝑁 ∈ ℕ0𝑛 ∈ ℕ0) → 2 ∈ ℂ)
9485adantr 466 . . . . . . . . . 10 ((𝑁 ∈ ℕ0𝑛 ∈ ℕ0) → (3 · ((2 · 𝑁) + 1)) ∈ ℕ)
9594nncnd 11238 . . . . . . . . 9 ((𝑁 ∈ ℕ0𝑛 ∈ ℕ0) → (3 · ((2 · 𝑁) + 1)) ∈ ℂ)
9694nnne0d 11267 . . . . . . . . 9 ((𝑁 ∈ ℕ0𝑛 ∈ ℕ0) → (3 · ((2 · 𝑁) + 1)) ≠ 0)
9793, 95, 90, 96, 91divdiv1d 11034 . . . . . . . 8 ((𝑁 ∈ ℕ0𝑛 ∈ ℕ0) → ((2 / (3 · ((2 · 𝑁) + 1))) / (9↑𝑛)) = (2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛))))
9879, 92, 973eqtr2d 2811 . . . . . . 7 ((𝑁 ∈ ℕ0𝑛 ∈ ℕ0) → ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑛)) = (2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛))))
9971, 98eqtrd 2805 . . . . . 6 ((𝑁 ∈ ℕ0𝑛 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑘)))‘𝑛) = (2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛))))
10047, 99syldan 579 . . . . 5 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → ((𝑘 ∈ ℕ0 ↦ ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑘)))‘𝑛) = (2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛))))
10194, 25nnmulcld 11270 . . . . . . 7 ((𝑁 ∈ ℕ0𝑛 ∈ ℕ0) → ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛)) ∈ ℕ)
102 nndivre 11258 . . . . . . 7 ((2 ∈ ℝ ∧ ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛)) ∈ ℕ) → (2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛))) ∈ ℝ)
10313, 101, 102sylancr 575 . . . . . 6 ((𝑁 ∈ ℕ0𝑛 ∈ ℕ0) → (2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛))) ∈ ℝ)
10447, 103syldan 579 . . . . 5 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → (2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛))) ∈ ℝ)
10581adantr 466 . . . . . . . . . 10 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → (2 · 𝑁) ∈ ℕ0)
106105nn0red 11554 . . . . . . . . 9 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → (2 · 𝑁) ∈ ℝ)
10715, 47, 17sylancr 575 . . . . . . . . . 10 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → (2 · 𝑛) ∈ ℕ0)
108107nn0red 11554 . . . . . . . . 9 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → (2 · 𝑛) ∈ ℝ)
109 1red 10257 . . . . . . . . 9 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → 1 ∈ ℝ)
110 eluzle 11901 . . . . . . . . . . 11 (𝑛 ∈ (ℤ𝑁) → 𝑁𝑛)
111110adantl 467 . . . . . . . . . 10 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → 𝑁𝑛)
112 nn0re 11503 . . . . . . . . . . . 12 (𝑁 ∈ ℕ0𝑁 ∈ ℝ)
113112adantr 466 . . . . . . . . . . 11 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → 𝑁 ∈ ℝ)
11447nn0red 11554 . . . . . . . . . . 11 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → 𝑛 ∈ ℝ)
11513a1i 11 . . . . . . . . . . 11 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → 2 ∈ ℝ)
116 2pos 11314 . . . . . . . . . . . 12 0 < 2
117116a1i 11 . . . . . . . . . . 11 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → 0 < 2)
118 lemul2 11078 . . . . . . . . . . 11 ((𝑁 ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (𝑁𝑛 ↔ (2 · 𝑁) ≤ (2 · 𝑛)))
119113, 114, 115, 117, 118syl112anc 1480 . . . . . . . . . 10 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → (𝑁𝑛 ↔ (2 · 𝑁) ≤ (2 · 𝑛)))
120111, 119mpbid 222 . . . . . . . . 9 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → (2 · 𝑁) ≤ (2 · 𝑛))
121106, 108, 109, 120leadd1dd 10843 . . . . . . . 8 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → ((2 · 𝑁) + 1) ≤ ((2 · 𝑛) + 1))
12283adantr 466 . . . . . . . . . 10 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → ((2 · 𝑁) + 1) ∈ ℕ)
123122nnred 11237 . . . . . . . . 9 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → ((2 · 𝑁) + 1) ∈ ℝ)
12447, 20syldan 579 . . . . . . . . . 10 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → ((2 · 𝑛) + 1) ∈ ℕ)
125124nnred 11237 . . . . . . . . 9 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → ((2 · 𝑛) + 1) ∈ ℝ)
126 3re 11296 . . . . . . . . . 10 3 ∈ ℝ
127126a1i 11 . . . . . . . . 9 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → 3 ∈ ℝ)
128 3pos 11316 . . . . . . . . . 10 0 < 3
129128a1i 11 . . . . . . . . 9 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → 0 < 3)
130 lemul2 11078 . . . . . . . . 9 ((((2 · 𝑁) + 1) ∈ ℝ ∧ ((2 · 𝑛) + 1) ∈ ℝ ∧ (3 ∈ ℝ ∧ 0 < 3)) → (((2 · 𝑁) + 1) ≤ ((2 · 𝑛) + 1) ↔ (3 · ((2 · 𝑁) + 1)) ≤ (3 · ((2 · 𝑛) + 1))))
131123, 125, 127, 129, 130syl112anc 1480 . . . . . . . 8 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → (((2 · 𝑁) + 1) ≤ ((2 · 𝑛) + 1) ↔ (3 · ((2 · 𝑁) + 1)) ≤ (3 · ((2 · 𝑛) + 1))))
132121, 131mpbid 222 . . . . . . 7 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → (3 · ((2 · 𝑁) + 1)) ≤ (3 · ((2 · 𝑛) + 1)))
13385adantr 466 . . . . . . . . 9 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → (3 · ((2 · 𝑁) + 1)) ∈ ℕ)
134133nnred 11237 . . . . . . . 8 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → (3 · ((2 · 𝑁) + 1)) ∈ ℝ)
13547, 22syldan 579 . . . . . . . . 9 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → (3 · ((2 · 𝑛) + 1)) ∈ ℕ)
136135nnred 11237 . . . . . . . 8 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → (3 · ((2 · 𝑛) + 1)) ∈ ℝ)
13723, 47, 24sylancr 575 . . . . . . . . 9 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → (9↑𝑛) ∈ ℕ)
138137nnred 11237 . . . . . . . 8 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → (9↑𝑛) ∈ ℝ)
139137nngt0d 11266 . . . . . . . 8 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → 0 < (9↑𝑛))
140 lemul1 11077 . . . . . . . 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 1480 . . . . . . 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 579 . . . . . . . 8 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛)) ∈ ℕ)
144143nnred 11237 . . . . . . 7 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛)) ∈ ℝ)
145143nngt0d 11266 . . . . . . 7 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → 0 < ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛)))
14647, 60syldan 579 . . . . . . 7 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)) ∈ ℝ)
14747, 61syldan 579 . . . . . . 7 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → 0 < ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))
148 lediv2 11115 . . . . . . 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 1492 . . . . . 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 11309 . . . . . . . . . . . 12 9 ∈ ℝ
152151, 74rereccli 10992 . . . . . . . . . . 11 (1 / 9) ∈ ℝ
153152recni 10254 . . . . . . . . . 10 (1 / 9) ∈ ℂ
154153a1i 11 . . . . . . . . 9 (𝑁 ∈ ℕ0 → (1 / 9) ∈ ℂ)
155 0re 10242 . . . . . . . . . . . . 13 0 ∈ ℝ
156 9pos 11324 . . . . . . . . . . . . . 14 0 < 9
157151, 156recgt0ii 11131 . . . . . . . . . . . . 13 0 < (1 / 9)
158155, 152, 157ltleii 10362 . . . . . . . . . . . 12 0 ≤ (1 / 9)
159 absid 14244 . . . . . . . . . . . 12 (((1 / 9) ∈ ℝ ∧ 0 ≤ (1 / 9)) → (abs‘(1 / 9)) = (1 / 9))
160152, 158, 159mp2an 672 . . . . . . . . . . 11 (abs‘(1 / 9)) = (1 / 9)
161 1lt9 11431 . . . . . . . . . . . . 13 1 < 9
162 recgt1i 11122 . . . . . . . . . . . . 13 ((9 ∈ ℝ ∧ 1 < 9) → (0 < (1 / 9) ∧ (1 / 9) < 1))
163151, 161, 162mp2an 672 . . . . . . . . . . . 12 (0 < (1 / 9) ∧ (1 / 9) < 1)
164163simpri 473 . . . . . . . . . . 11 (1 / 9) < 1
165160, 164eqbrtri 4807 . . . . . . . . . 10 (abs‘(1 / 9)) < 1
166165a1i 11 . . . . . . . . 9 (𝑁 ∈ ℕ0 → (abs‘(1 / 9)) < 1)
167 eqid 2771 . . . . . . . . . . 11 (𝑘 ∈ ℕ0 ↦ ((1 / 9)↑𝑘)) = (𝑘 ∈ ℕ0 ↦ ((1 / 9)↑𝑘))
168 ovex 6823 . . . . . . . . . . 11 ((1 / 9)↑𝑛) ∈ V
16966, 167, 168fvmpt 6424 . . . . . . . . . 10 (𝑛 ∈ ℕ0 → ((𝑘 ∈ ℕ0 ↦ ((1 / 9)↑𝑘))‘𝑛) = ((1 / 9)↑𝑛))
17047, 169syl 17 . . . . . . . . 9 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → ((𝑘 ∈ ℕ0 ↦ ((1 / 9)↑𝑘))‘𝑛) = ((1 / 9)↑𝑛))
171154, 166, 34, 170geolim2 14809 . . . . . . . 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 13223 . . . . . . . . . 10 (𝑁 ∈ ℕ0 → ((1 / 9)↑𝑁) = (1 / (9↑𝑁)))
17572, 74dividi 10960 . . . . . . . . . . . . 13 (9 / 9) = 1
176175oveq1i 6803 . . . . . . . . . . . 12 ((9 / 9) − (1 / 9)) = (1 − (1 / 9))
177 ax-1cn 10196 . . . . . . . . . . . . . 14 1 ∈ ℂ
17872, 74pm3.2i 447 . . . . . . . . . . . . . 14 (9 ∈ ℂ ∧ 9 ≠ 0)
179 divsubdir 10923 . . . . . . . . . . . . . 14 ((9 ∈ ℂ ∧ 1 ∈ ℂ ∧ (9 ∈ ℂ ∧ 9 ≠ 0)) → ((9 − 1) / 9) = ((9 / 9) − (1 / 9)))
18072, 177, 178, 179mp3an 1572 . . . . . . . . . . . . 13 ((9 − 1) / 9) = ((9 / 9) − (1 / 9))
181 df-9 11288 . . . . . . . . . . . . . . . 16 9 = (8 + 1)
182181oveq1i 6803 . . . . . . . . . . . . . . 15 (9 − 1) = ((8 + 1) − 1)
183 8cn 11308 . . . . . . . . . . . . . . . 16 8 ∈ ℂ
184183, 177pncan3oi 10499 . . . . . . . . . . . . . . 15 ((8 + 1) − 1) = 8
185182, 184eqtri 2793 . . . . . . . . . . . . . 14 (9 − 1) = 8
186185oveq1i 6803 . . . . . . . . . . . . 13 ((9 − 1) / 9) = (8 / 9)
187180, 186eqtr3i 2795 . . . . . . . . . . . 12 ((9 / 9) − (1 / 9)) = (8 / 9)
188176, 187eqtr3i 2795 . . . . . . . . . . 11 (1 − (1 / 9)) = (8 / 9)
189188a1i 11 . . . . . . . . . 10 (𝑁 ∈ ℕ0 → (1 − (1 / 9)) = (8 / 9))
190174, 189oveq12d 6811 . . . . . . . . 9 (𝑁 ∈ ℕ0 → (((1 / 9)↑𝑁) / (1 − (1 / 9))) = ((1 / (9↑𝑁)) / (8 / 9)))
191177a1i 11 . . . . . . . . . 10 (𝑁 ∈ ℕ0 → 1 ∈ ℂ)
192 nnexpcl 13080 . . . . . . . . . . . 12 ((9 ∈ ℕ ∧ 𝑁 ∈ ℕ0) → (9↑𝑁) ∈ ℕ)
19323, 192mpan 670 . . . . . . . . . . 11 (𝑁 ∈ ℕ0 → (9↑𝑁) ∈ ℕ)
194193nncnd 11238 . . . . . . . . . 10 (𝑁 ∈ ℕ0 → (9↑𝑁) ∈ ℂ)
195183, 72, 74divcli 10969 . . . . . . . . . . 11 (8 / 9) ∈ ℂ
196195a1i 11 . . . . . . . . . 10 (𝑁 ∈ ℕ0 → (8 / 9) ∈ ℂ)
197193nnne0d 11267 . . . . . . . . . 10 (𝑁 ∈ ℕ0 → (9↑𝑁) ≠ 0)
198 8nn 11393 . . . . . . . . . . . . 13 8 ∈ ℕ
199198nnne0i 11257 . . . . . . . . . . . 12 8 ≠ 0
200183, 72, 199, 74divne0i 10975 . . . . . . . . . . 11 (8 / 9) ≠ 0
201200a1i 11 . . . . . . . . . 10 (𝑁 ∈ ℕ0 → (8 / 9) ≠ 0)
202191, 194, 196, 197, 201divdiv32d 11028 . . . . . . . . 9 (𝑁 ∈ ℕ0 → ((1 / (9↑𝑁)) / (8 / 9)) = ((1 / (8 / 9)) / (9↑𝑁)))
203 recdiv 10933 . . . . . . . . . . . 12 (((8 ∈ ℂ ∧ 8 ≠ 0) ∧ (9 ∈ ℂ ∧ 9 ≠ 0)) → (1 / (8 / 9)) = (9 / 8))
204183, 199, 72, 74, 203mp4an 673 . . . . . . . . . . 11 (1 / (8 / 9)) = (9 / 8)
205204oveq1i 6803 . . . . . . . . . 10 ((1 / (8 / 9)) / (9↑𝑁)) = ((9 / 8) / (9↑𝑁))
206183a1i 11 . . . . . . . . . . 11 (𝑁 ∈ ℕ0 → 8 ∈ ℂ)
207199a1i 11 . . . . . . . . . . 11 (𝑁 ∈ ℕ0 → 8 ≠ 0)
208172, 206, 194, 207, 197divdiv1d 11034 . . . . . . . . . 10 (𝑁 ∈ ℕ0 → ((9 / 8) / (9↑𝑁)) = (9 / (8 · (9↑𝑁))))
209205, 208syl5eq 2817 . . . . . . . . 9 (𝑁 ∈ ℕ0 → ((1 / (8 / 9)) / (9↑𝑁)) = (9 / (8 · (9↑𝑁))))
210190, 202, 2093eqtrd 2809 . . . . . . . 8 (𝑁 ∈ ℕ0 → (((1 / 9)↑𝑁) / (1 − (1 / 9))) = (9 / (8 · (9↑𝑁))))
211171, 210breqtrd 4812 . . . . . . 7 (𝑁 ∈ ℕ0 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((1 / 9)↑𝑘))) ⇝ (9 / (8 · (9↑𝑁))))
212 expcl 13085 . . . . . . . . 9 (((1 / 9) ∈ ℂ ∧ 𝑛 ∈ ℕ0) → ((1 / 9)↑𝑛) ∈ ℂ)
213153, 47, 212sylancr 575 . . . . . . . 8 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → ((1 / 9)↑𝑛) ∈ ℂ)
214170, 213eqeltrd 2850 . . . . . . 7 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → ((𝑘 ∈ ℕ0 ↦ ((1 / 9)↑𝑘))‘𝑛) ∈ ℂ)
21547, 70syl 17 . . . . . . . 8 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → ((𝑘 ∈ ℕ0 ↦ ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑘)))‘𝑛) = ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑛)))
216170oveq2d 6809 . . . . . . . 8 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → ((2 / (3 · ((2 · 𝑁) + 1))) · ((𝑘 ∈ ℕ0 ↦ ((1 / 9)↑𝑘))‘𝑛)) = ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑛)))
217215, 216eqtr4d 2808 . . . . . . 7 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → ((𝑘 ∈ ℕ0 ↦ ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑘)))‘𝑛) = ((2 / (3 · ((2 · 𝑁) + 1))) · ((𝑘 ∈ ℕ0 ↦ ((1 / 9)↑𝑘))‘𝑛)))
21833, 46, 88, 211, 214, 217isermulc2 14596 . . . . . 6 (𝑁 ∈ ℕ0 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑘)))) ⇝ ((2 / (3 · ((2 · 𝑁) + 1))) · (9 / (8 · (9↑𝑁)))))
219 seqex 13010 . . . . . . 7 seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑘)))) ∈ V
220 ovex 6823 . . . . . . 7 ((2 / (3 · ((2 · 𝑁) + 1))) · (9 / (8 · (9↑𝑁)))) ∈ V
221219, 220breldm 5467 . . . . . 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 14783 . . . 4 (𝑁 ∈ ℕ0 → Σ𝑛 ∈ (ℤ𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ≤ Σ𝑛 ∈ (ℤ𝑁)(2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛))))
224104recnd 10270 . . . . 5 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → (2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛))) ∈ ℂ)
225 3cn 11297 . . . . . . . . . . . 12 3 ∈ ℂ
226 4cn 11300 . . . . . . . . . . . 12 4 ∈ ℂ
227 2cn 11293 . . . . . . . . . . . 12 2 ∈ ℂ
228 4ne0 11319 . . . . . . . . . . . 12 4 ≠ 0
229 3ne0 11317 . . . . . . . . . . . 12 3 ≠ 0
230 2ne0 11315 . . . . . . . . . . . 12 2 ≠ 0
231225, 226, 227, 225, 228, 229, 230divdivdivi 10990 . . . . . . . . . . 11 ((3 / 4) / (2 / 3)) = ((3 · 3) / (4 · 2))
232 3t3e9 11382 . . . . . . . . . . . 12 (3 · 3) = 9
233 4t2e8 11383 . . . . . . . . . . . 12 (4 · 2) = 8
234232, 233oveq12i 6805 . . . . . . . . . . 11 ((3 · 3) / (4 · 2)) = (9 / 8)
235231, 234eqtri 2793 . . . . . . . . . 10 ((3 / 4) / (2 / 3)) = (9 / 8)
236235oveq2i 6804 . . . . . . . . 9 ((2 / 3) · ((3 / 4) / (2 / 3))) = ((2 / 3) · (9 / 8))
237225, 226, 228divcli 10969 . . . . . . . . . 10 (3 / 4) ∈ ℂ
238227, 225, 229divcli 10969 . . . . . . . . . 10 (2 / 3) ∈ ℂ
239227, 225, 230, 229divne0i 10975 . . . . . . . . . 10 (2 / 3) ≠ 0
240237, 238, 239divcan2i 10970 . . . . . . . . 9 ((2 / 3) · ((3 / 4) / (2 / 3))) = (3 / 4)
241236, 240eqtr3i 2795 . . . . . . . 8 ((2 / 3) · (9 / 8)) = (3 / 4)
242241oveq1i 6803 . . . . . . 7 (((2 / 3) · (9 / 8)) / (((2 · 𝑁) + 1) · (9↑𝑁))) = ((3 / 4) / (((2 · 𝑁) + 1) · (9↑𝑁)))
243 2cnd 11295 . . . . . . . . . 10 (𝑁 ∈ ℕ0 → 2 ∈ ℂ)
244225a1i 11 . . . . . . . . . 10 (𝑁 ∈ ℕ0 → 3 ∈ ℂ)
24583nncnd 11238 . . . . . . . . . 10 (𝑁 ∈ ℕ0 → ((2 · 𝑁) + 1) ∈ ℂ)
246229a1i 11 . . . . . . . . . 10 (𝑁 ∈ ℕ0 → 3 ≠ 0)
24783nnne0d 11267 . . . . . . . . . 10 (𝑁 ∈ ℕ0 → ((2 · 𝑁) + 1) ≠ 0)
248243, 244, 245, 246, 247divdiv1d 11034 . . . . . . . . 9 (𝑁 ∈ ℕ0 → ((2 / 3) / ((2 · 𝑁) + 1)) = (2 / (3 · ((2 · 𝑁) + 1))))
249248, 208oveq12d 6811 . . . . . . . 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 10969 . . . . . . . . . 10 (9 / 8) ∈ ℂ
252251a1i 11 . . . . . . . . 9 (𝑁 ∈ ℕ0 → (9 / 8) ∈ ℂ)
253250, 245, 252, 194, 247, 197divmuldivd 11044 . . . . . . . 8 (𝑁 ∈ ℕ0 → (((2 / 3) / ((2 · 𝑁) + 1)) · ((9 / 8) / (9↑𝑁))) = (((2 / 3) · (9 / 8)) / (((2 · 𝑁) + 1) · (9↑𝑁))))
254249, 253eqtr3d 2807 . . . . . . 7 (𝑁 ∈ ℕ0 → ((2 / (3 · ((2 · 𝑁) + 1))) · (9 / (8 · (9↑𝑁)))) = (((2 / 3) · (9 / 8)) / (((2 · 𝑁) + 1) · (9↑𝑁))))
255226a1i 11 . . . . . . . . . 10 (𝑁 ∈ ℕ0 → 4 ∈ ℂ)
256255, 245, 194mulassd 10265 . . . . . . . . 9 (𝑁 ∈ ℕ0 → ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁)) = (4 · (((2 · 𝑁) + 1) · (9↑𝑁))))
257256oveq2d 6809 . . . . . . . 8 (𝑁 ∈ ℕ0 → (3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁))) = (3 / (4 · (((2 · 𝑁) + 1) · (9↑𝑁)))))
25883, 193nnmulcld 11270 . . . . . . . . . 10 (𝑁 ∈ ℕ0 → (((2 · 𝑁) + 1) · (9↑𝑁)) ∈ ℕ)
259258nncnd 11238 . . . . . . . . 9 (𝑁 ∈ ℕ0 → (((2 · 𝑁) + 1) · (9↑𝑁)) ∈ ℂ)
260228a1i 11 . . . . . . . . 9 (𝑁 ∈ ℕ0 → 4 ≠ 0)
261258nnne0d 11267 . . . . . . . . 9 (𝑁 ∈ ℕ0 → (((2 · 𝑁) + 1) · (9↑𝑁)) ≠ 0)
262244, 255, 259, 260, 261divdiv1d 11034 . . . . . . . 8 (𝑁 ∈ ℕ0 → ((3 / 4) / (((2 · 𝑁) + 1) · (9↑𝑁))) = (3 / (4 · (((2 · 𝑁) + 1) · (9↑𝑁)))))
263257, 262eqtr4d 2808 . . . . . . 7 (𝑁 ∈ ℕ0 → (3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁))) = ((3 / 4) / (((2 · 𝑁) + 1) · (9↑𝑁))))
264242, 254, 2633eqtr4a 2831 . . . . . 6 (𝑁 ∈ ℕ0 → ((2 / (3 · ((2 · 𝑁) + 1))) · (9 / (8 · (9↑𝑁)))) = (3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁))))
265218, 264breqtrd 4812 . . . . 5 (𝑁 ∈ ℕ0 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑘)))) ⇝ (3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁))))
26633, 46, 100, 224, 265isumclim 14696 . . . 4 (𝑁 ∈ ℕ0 → Σ𝑛 ∈ (ℤ𝑁)(2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛))) = (3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁))))
267223, 266breqtrd 4812 . . 3 (𝑁 ∈ ℕ0 → Σ𝑛 ∈ (ℤ𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ≤ (3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁))))
268 4nn 11389 . . . . . . 7 4 ∈ ℕ
269 nnmulcl 11245 . . . . . . 7 ((4 ∈ ℕ ∧ ((2 · 𝑁) + 1) ∈ ℕ) → (4 · ((2 · 𝑁) + 1)) ∈ ℕ)
270268, 83, 269sylancr 575 . . . . . 6 (𝑁 ∈ ℕ0 → (4 · ((2 · 𝑁) + 1)) ∈ ℕ)
271270, 193nnmulcld 11270 . . . . 5 (𝑁 ∈ ℕ0 → ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁)) ∈ ℕ)
272 nndivre 11258 . . . . 5 ((3 ∈ ℝ ∧ ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁)) ∈ ℕ) → (3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁))) ∈ ℝ)
273126, 271, 272sylancr 575 . . . 4 (𝑁 ∈ ℕ0 → (3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁))) ∈ ℝ)
274 elicc2 12443 . . . 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 575 . . 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 1427 . 2 (𝑁 ∈ ℕ0 → Σ𝑛 ∈ (ℤ𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ (0[,](3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁)))))
27756, 276eqeltrd 2850 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 382  w3a 1071   = wceq 1631  wcel 2145  wne 2943   class class class wbr 4786  cmpt 4863  dom cdm 5249  cfv 6031  (class class class)co 6793  cc 10136  cr 10137  0cc0 10138  1c1 10139   + caddc 10141   · cmul 10143   < clt 10276  cle 10277  cmin 10468   / cdiv 10886  cn 11222  2c2 11272  3c3 11273  4c4 11274  8c8 11278  9c9 11279  0cn0 11494  cz 11579  cuz 11888  [,]cicc 12383  ...cfz 12533  seqcseq 13008  cexp 13067  abscabs 14182  cli 14423  Σcsu 14624  logclog 24522
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4904  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096  ax-inf2 8702  ax-cnex 10194  ax-resscn 10195  ax-1cn 10196  ax-icn 10197  ax-addcl 10198  ax-addrcl 10199  ax-mulcl 10200  ax-mulrcl 10201  ax-mulcom 10202  ax-addass 10203  ax-mulass 10204  ax-distr 10205  ax-i2m1 10206  ax-1ne0 10207  ax-1rid 10208  ax-rnegex 10209  ax-rrecex 10210  ax-cnre 10211  ax-pre-lttri 10212  ax-pre-lttrn 10213  ax-pre-ltadd 10214  ax-pre-mulgt0 10215  ax-pre-sup 10216  ax-addf 10217  ax-mulf 10218
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3or 1072  df-3an 1073  df-tru 1634  df-fal 1637  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-int 4612  df-iun 4656  df-iin 4657  df-br 4787  df-opab 4847  df-mpt 4864  df-tr 4887  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-se 5209  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-isom 6040  df-riota 6754  df-ov 6796  df-oprab 6797  df-mpt2 6798  df-of 7044  df-om 7213  df-1st 7315  df-2nd 7316  df-supp 7447  df-wrecs 7559  df-recs 7621  df-rdg 7659  df-1o 7713  df-2o 7714  df-oadd 7717  df-er 7896  df-map 8011  df-pm 8012  df-ixp 8063  df-en 8110  df-dom 8111  df-sdom 8112  df-fin 8113  df-fsupp 8432  df-fi 8473  df-sup 8504  df-inf 8505  df-oi 8571  df-card 8965  df-cda 9192  df-pnf 10278  df-mnf 10279  df-xr 10280  df-ltxr 10281  df-le 10282  df-sub 10470  df-neg 10471  df-div 10887  df-nn 11223  df-2 11281  df-3 11282  df-4 11283  df-5 11284  df-6 11285  df-7 11286  df-8 11287  df-9 11288  df-n0 11495  df-xnn0 11566  df-z 11580  df-dec 11696  df-uz 11889  df-q 11992  df-rp 12036  df-xneg 12151  df-xadd 12152  df-xmul 12153  df-ioo 12384  df-ioc 12385  df-ico 12386  df-icc 12387  df-fz 12534  df-fzo 12674  df-fl 12801  df-mod 12877  df-seq 13009  df-exp 13068  df-fac 13265  df-bc 13294  df-hash 13322  df-shft 14015  df-cj 14047  df-re 14048  df-im 14049  df-sqrt 14183  df-abs 14184  df-limsup 14410  df-clim 14427  df-rlim 14428  df-sum 14625  df-ef 15004  df-sin 15006  df-cos 15007  df-tan 15008  df-pi 15009  df-dvds 15190  df-struct 16066  df-ndx 16067  df-slot 16068  df-base 16070  df-sets 16071  df-ress 16072  df-plusg 16162  df-mulr 16163  df-starv 16164  df-sca 16165  df-vsca 16166  df-ip 16167  df-tset 16168  df-ple 16169  df-ds 16172  df-unif 16173  df-hom 16174  df-cco 16175  df-rest 16291  df-topn 16292  df-0g 16310  df-gsum 16311  df-topgen 16312  df-pt 16313  df-prds 16316  df-xrs 16370  df-qtop 16375  df-imas 16376  df-xps 16378  df-mre 16454  df-mrc 16455  df-acs 16457  df-mgm 17450  df-sgrp 17492  df-mnd 17503  df-submnd 17544  df-mulg 17749  df-cntz 17957  df-cmn 18402  df-psmet 19953  df-xmet 19954  df-met 19955  df-bl 19956  df-mopn 19957  df-fbas 19958  df-fg 19959  df-cnfld 19962  df-top 20919  df-topon 20936  df-topsp 20958  df-bases 20971  df-cld 21044  df-ntr 21045  df-cls 21046  df-nei 21123  df-lp 21161  df-perf 21162  df-cn 21252  df-cnp 21253  df-haus 21340  df-cmp 21411  df-tx 21586  df-hmeo 21779  df-fil 21870  df-fm 21962  df-flim 21963  df-flf 21964  df-xms 22345  df-ms 22346  df-tms 22347  df-cncf 22901  df-limc 23850  df-dv 23851  df-ulm 24351  df-log 24524  df-atan 24815
This theorem is referenced by:  log2ub  24897
  Copyright terms: Public domain W3C validator