This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem log2tlbnd

Description: Bound the error term in the series of log2cnv . (Contributed by Mario Carneiro, 7-Apr-2015)

Ref Expression
Assertion log2tlbnd ( 𝑁 ∈ ℕ0 → ( ( log ‘ 2 ) − Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ) ∈ ( 0 [,] ( 3 / ( ( 4 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑁 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 fzfid ⊢ ( 𝑁 ∈ ℕ0 → ( 0 ... ( 𝑁 − 1 ) ) ∈ Fin )
2 elfznn0 ⊢ ( 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) → 𝑛 ∈ ℕ0 )
3 2re ⊢ 2 ∈ ℝ
4 3nn ⊢ 3 ∈ ℕ
5 2nn0 ⊢ 2 ∈ ℕ0
6 simpr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → 𝑛 ∈ ℕ0 )
7 nn0mulcl ⊢ ( ( 2 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( 2 · 𝑛 ) ∈ ℕ0 )
8 5 6 7 sylancr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( 2 · 𝑛 ) ∈ ℕ0 )
9 nn0p1nn ⊢ ( ( 2 · 𝑛 ) ∈ ℕ0 → ( ( 2 · 𝑛 ) + 1 ) ∈ ℕ )
10 8 9 syl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( ( 2 · 𝑛 ) + 1 ) ∈ ℕ )
11 nnmulcl ⊢ ( ( 3 ∈ ℕ ∧ ( ( 2 · 𝑛 ) + 1 ) ∈ ℕ ) → ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) ∈ ℕ )
12 4 10 11 sylancr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) ∈ ℕ )
13 9nn ⊢ 9 ∈ ℕ
14 nnexpcl ⊢ ( ( 9 ∈ ℕ ∧ 𝑛 ∈ ℕ0 ) → ( 9 ↑ 𝑛 ) ∈ ℕ )
15 13 6 14 sylancr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( 9 ↑ 𝑛 ) ∈ ℕ )
16 12 15 nnmulcld ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ∈ ℕ )
17 nndivre ⊢ ( ( 2 ∈ ℝ ∧ ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ∈ ℕ ) → ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ∈ ℝ )
18 3 16 17 sylancr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ∈ ℝ )
19 18 recnd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ∈ ℂ )
20 2 19 sylan2 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ∈ ℂ )
21 1 20 fsumcl ⊢ ( 𝑁 ∈ ℕ0 → Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ∈ ℂ )
22 eqid ⊢ ( ℤ≥ ‘ 𝑁 ) = ( ℤ≥ ‘ 𝑁 )
23 nn0z ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ )
24 eluznn0 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑛 ∈ ℕ0 )
25 oveq2 ⊢ ( 𝑘 = 𝑛 → ( 2 · 𝑘 ) = ( 2 · 𝑛 ) )
26 25 oveq1d ⊢ ( 𝑘 = 𝑛 → ( ( 2 · 𝑘 ) + 1 ) = ( ( 2 · 𝑛 ) + 1 ) )
27 26 oveq2d ⊢ ( 𝑘 = 𝑛 → ( 3 · ( ( 2 · 𝑘 ) + 1 ) ) = ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) )
28 oveq2 ⊢ ( 𝑘 = 𝑛 → ( 9 ↑ 𝑘 ) = ( 9 ↑ 𝑛 ) )
29 27 28 oveq12d ⊢ ( 𝑘 = 𝑛 → ( ( 3 · ( ( 2 · 𝑘 ) + 1 ) ) · ( 9 ↑ 𝑘 ) ) = ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) )
30 29 oveq2d ⊢ ( 𝑘 = 𝑛 → ( 2 / ( ( 3 · ( ( 2 · 𝑘 ) + 1 ) ) · ( 9 ↑ 𝑘 ) ) ) = ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) )
31 eqid ⊢ ( 𝑘 ∈ ℕ0 ↦ ( 2 / ( ( 3 · ( ( 2 · 𝑘 ) + 1 ) ) · ( 9 ↑ 𝑘 ) ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( 2 / ( ( 3 · ( ( 2 · 𝑘 ) + 1 ) ) · ( 9 ↑ 𝑘 ) ) ) )
32 ovex ⊢ ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ∈ V
33 30 31 32 fvmpt ⊢ ( 𝑛 ∈ ℕ0 → ( ( 𝑘 ∈ ℕ0 ↦ ( 2 / ( ( 3 · ( ( 2 · 𝑘 ) + 1 ) ) · ( 9 ↑ 𝑘 ) ) ) ) ‘ 𝑛 ) = ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) )
34 24 33 syl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 𝑘 ∈ ℕ0 ↦ ( 2 / ( ( 3 · ( ( 2 · 𝑘 ) + 1 ) ) · ( 9 ↑ 𝑘 ) ) ) ) ‘ 𝑛 ) = ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) )
35 24 18 syldan ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ∈ ℝ )
36 31 log2cnv ⊢ seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( 2 / ( ( 3 · ( ( 2 · 𝑘 ) + 1 ) ) · ( 9 ↑ 𝑘 ) ) ) ) ) ⇝ ( log ‘ 2 )
37 seqex ⊢ seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( 2 / ( ( 3 · ( ( 2 · 𝑘 ) + 1 ) ) · ( 9 ↑ 𝑘 ) ) ) ) ) ∈ V
38 fvex ⊢ ( log ‘ 2 ) ∈ V
39 37 38 breldm ⊢ ( seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( 2 / ( ( 3 · ( ( 2 · 𝑘 ) + 1 ) ) · ( 9 ↑ 𝑘 ) ) ) ) ) ⇝ ( log ‘ 2 ) → seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( 2 / ( ( 3 · ( ( 2 · 𝑘 ) + 1 ) ) · ( 9 ↑ 𝑘 ) ) ) ) ) ∈ dom ⇝ )
40 36 39 mp1i ⊢ ( 𝑁 ∈ ℕ0 → seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( 2 / ( ( 3 · ( ( 2 · 𝑘 ) + 1 ) ) · ( 9 ↑ 𝑘 ) ) ) ) ) ∈ dom ⇝ )
41 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
42 id ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℕ0 )
43 33 adantl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑘 ∈ ℕ0 ↦ ( 2 / ( ( 3 · ( ( 2 · 𝑘 ) + 1 ) ) · ( 9 ↑ 𝑘 ) ) ) ) ‘ 𝑛 ) = ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) )
44 43 19 eqeltrd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑘 ∈ ℕ0 ↦ ( 2 / ( ( 3 · ( ( 2 · 𝑘 ) + 1 ) ) · ( 9 ↑ 𝑘 ) ) ) ) ‘ 𝑛 ) ∈ ℂ )
45 41 42 44 iserex ⊢ ( 𝑁 ∈ ℕ0 → ( seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( 2 / ( ( 3 · ( ( 2 · 𝑘 ) + 1 ) ) · ( 9 ↑ 𝑘 ) ) ) ) ) ∈ dom ⇝ ↔ seq 𝑁 ( + , ( 𝑘 ∈ ℕ0 ↦ ( 2 / ( ( 3 · ( ( 2 · 𝑘 ) + 1 ) ) · ( 9 ↑ 𝑘 ) ) ) ) ) ∈ dom ⇝ ) )
46 40 45 mpbid ⊢ ( 𝑁 ∈ ℕ0 → seq 𝑁 ( + , ( 𝑘 ∈ ℕ0 ↦ ( 2 / ( ( 3 · ( ( 2 · 𝑘 ) + 1 ) ) · ( 9 ↑ 𝑘 ) ) ) ) ) ∈ dom ⇝ )
47 22 23 34 35 46 isumrecl ⊢ ( 𝑁 ∈ ℕ0 → Σ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ∈ ℝ )
48 47 recnd ⊢ ( 𝑁 ∈ ℕ0 → Σ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ∈ ℂ )
49 0zd ⊢ ( 𝑁 ∈ ℕ0 → 0 ∈ ℤ )
50 36 a1i ⊢ ( 𝑁 ∈ ℕ0 → seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( 2 / ( ( 3 · ( ( 2 · 𝑘 ) + 1 ) ) · ( 9 ↑ 𝑘 ) ) ) ) ) ⇝ ( log ‘ 2 ) )
51 41 49 43 19 50 isumclim ⊢ ( 𝑁 ∈ ℕ0 → Σ 𝑛 ∈ ℕ0 ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) = ( log ‘ 2 ) )
52 41 22 42 43 19 40 isumsplit ⊢ ( 𝑁 ∈ ℕ0 → Σ 𝑛 ∈ ℕ0 ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) = ( Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) + Σ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ) )
53 51 52 eqtr3d ⊢ ( 𝑁 ∈ ℕ0 → ( log ‘ 2 ) = ( Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) + Σ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ) )
54 21 48 53 mvrladdd ⊢ ( 𝑁 ∈ ℕ0 → ( ( log ‘ 2 ) − Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ) = Σ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) )
55 3 a1i ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → 2 ∈ ℝ )
56 0le2 ⊢ 0 ≤ 2
57 56 a1i ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → 0 ≤ 2 )
58 16 nnred ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ∈ ℝ )
59 16 nngt0d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → 0 < ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) )
60 divge0 ⊢ ( ( ( 2 ∈ ℝ ∧ 0 ≤ 2 ) ∧ ( ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ∈ ℝ ∧ 0 < ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ) → 0 ≤ ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) )
61 55 57 58 59 60 syl22anc ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → 0 ≤ ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) )
62 24 61 syldan ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 0 ≤ ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) )
63 22 23 34 35 46 62 isumge0 ⊢ ( 𝑁 ∈ ℕ0 → 0 ≤ Σ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) )
64 oveq2 ⊢ ( 𝑘 = 𝑛 → ( ( 1 / 9 ) ↑ 𝑘 ) = ( ( 1 / 9 ) ↑ 𝑛 ) )
65 64 oveq2d ⊢ ( 𝑘 = 𝑛 → ( ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) · ( ( 1 / 9 ) ↑ 𝑘 ) ) = ( ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) · ( ( 1 / 9 ) ↑ 𝑛 ) ) )
66 eqid ⊢ ( 𝑘 ∈ ℕ0 ↦ ( ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) · ( ( 1 / 9 ) ↑ 𝑘 ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) · ( ( 1 / 9 ) ↑ 𝑘 ) ) )
67 ovex ⊢ ( ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) · ( ( 1 / 9 ) ↑ 𝑛 ) ) ∈ V
68 65 66 67 fvmpt ⊢ ( 𝑛 ∈ ℕ0 → ( ( 𝑘 ∈ ℕ0 ↦ ( ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) · ( ( 1 / 9 ) ↑ 𝑘 ) ) ) ‘ 𝑛 ) = ( ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) · ( ( 1 / 9 ) ↑ 𝑛 ) ) )
69 68 adantl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) · ( ( 1 / 9 ) ↑ 𝑘 ) ) ) ‘ 𝑛 ) = ( ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) · ( ( 1 / 9 ) ↑ 𝑛 ) ) )
70 9cn ⊢ 9 ∈ ℂ
71 70 a1i ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → 9 ∈ ℂ )
72 13 nnne0i ⊢ 9 ≠ 0
73 72 a1i ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → 9 ≠ 0 )
74 nn0z ⊢ ( 𝑛 ∈ ℕ0 → 𝑛 ∈ ℤ )
75 74 adantl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → 𝑛 ∈ ℤ )
76 71 73 75 exprecd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( ( 1 / 9 ) ↑ 𝑛 ) = ( 1 / ( 9 ↑ 𝑛 ) ) )
77 76 oveq2d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) · ( ( 1 / 9 ) ↑ 𝑛 ) ) = ( ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) · ( 1 / ( 9 ↑ 𝑛 ) ) ) )
78 nn0mulcl ⊢ ( ( 2 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 2 · 𝑁 ) ∈ ℕ0 )
79 5 78 mpan ⊢ ( 𝑁 ∈ ℕ0 → ( 2 · 𝑁 ) ∈ ℕ0 )
80 nn0p1nn ⊢ ( ( 2 · 𝑁 ) ∈ ℕ0 → ( ( 2 · 𝑁 ) + 1 ) ∈ ℕ )
81 79 80 syl ⊢ ( 𝑁 ∈ ℕ0 → ( ( 2 · 𝑁 ) + 1 ) ∈ ℕ )
82 nnmulcl ⊢ ( ( 3 ∈ ℕ ∧ ( ( 2 · 𝑁 ) + 1 ) ∈ ℕ ) → ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ∈ ℕ )
83 4 81 82 sylancr ⊢ ( 𝑁 ∈ ℕ0 → ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ∈ ℕ )
84 nndivre ⊢ ( ( 2 ∈ ℝ ∧ ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ∈ ℕ ) → ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) ∈ ℝ )
85 3 83 84 sylancr ⊢ ( 𝑁 ∈ ℕ0 → ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) ∈ ℝ )
86 85 recnd ⊢ ( 𝑁 ∈ ℕ0 → ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) ∈ ℂ )
87 86 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) ∈ ℂ )
88 15 nncnd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( 9 ↑ 𝑛 ) ∈ ℂ )
89 15 nnne0d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( 9 ↑ 𝑛 ) ≠ 0 )
90 87 88 89 divrecd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) / ( 9 ↑ 𝑛 ) ) = ( ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) · ( 1 / ( 9 ↑ 𝑛 ) ) ) )
91 2cnd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → 2 ∈ ℂ )
92 83 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ∈ ℕ )
93 92 nncnd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ∈ ℂ )
94 92 nnne0d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ≠ 0 )
95 91 93 88 94 89 divdiv1d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) / ( 9 ↑ 𝑛 ) ) = ( 2 / ( ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) )
96 77 90 95 3eqtr2d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) · ( ( 1 / 9 ) ↑ 𝑛 ) ) = ( 2 / ( ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) )
97 69 96 eqtrd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) · ( ( 1 / 9 ) ↑ 𝑘 ) ) ) ‘ 𝑛 ) = ( 2 / ( ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) )
98 24 97 syldan ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) · ( ( 1 / 9 ) ↑ 𝑘 ) ) ) ‘ 𝑛 ) = ( 2 / ( ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) )
99 92 15 nnmulcld ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ∈ ℕ )
100 nndivre ⊢ ( ( 2 ∈ ℝ ∧ ( ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ∈ ℕ ) → ( 2 / ( ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ∈ ℝ )
101 3 99 100 sylancr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( 2 / ( ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ∈ ℝ )
102 24 101 syldan ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 2 / ( ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ∈ ℝ )
103 79 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 2 · 𝑁 ) ∈ ℕ0 )
104 103 nn0red ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 2 · 𝑁 ) ∈ ℝ )
105 5 24 7 sylancr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 2 · 𝑛 ) ∈ ℕ0 )
106 105 nn0red ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 2 · 𝑛 ) ∈ ℝ )
107 1red ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 1 ∈ ℝ )
108 eluzle ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) → 𝑁 ≤ 𝑛 )
109 108 adantl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑁 ≤ 𝑛 )
110 nn0re ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ )
111 110 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑁 ∈ ℝ )
112 24 nn0red ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑛 ∈ ℝ )
113 3 a1i ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 2 ∈ ℝ )
114 2pos ⊢ 0 < 2
115 114 a1i ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 0 < 2 )
116 lemul2 ⊢ ( ( 𝑁 ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( 𝑁 ≤ 𝑛 ↔ ( 2 · 𝑁 ) ≤ ( 2 · 𝑛 ) ) )
117 111 112 113 115 116 syl112anc ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑁 ≤ 𝑛 ↔ ( 2 · 𝑁 ) ≤ ( 2 · 𝑛 ) ) )
118 109 117 mpbid ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 2 · 𝑁 ) ≤ ( 2 · 𝑛 ) )
119 104 106 107 118 leadd1dd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 2 · 𝑁 ) + 1 ) ≤ ( ( 2 · 𝑛 ) + 1 ) )
120 81 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 2 · 𝑁 ) + 1 ) ∈ ℕ )
121 120 nnred ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 2 · 𝑁 ) + 1 ) ∈ ℝ )
122 24 10 syldan ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 2 · 𝑛 ) + 1 ) ∈ ℕ )
123 122 nnred ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 2 · 𝑛 ) + 1 ) ∈ ℝ )
124 3re ⊢ 3 ∈ ℝ
125 124 a1i ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 3 ∈ ℝ )
126 3pos ⊢ 0 < 3
127 126 a1i ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 0 < 3 )
128 lemul2 ⊢ ( ( ( ( 2 · 𝑁 ) + 1 ) ∈ ℝ ∧ ( ( 2 · 𝑛 ) + 1 ) ∈ ℝ ∧ ( 3 ∈ ℝ ∧ 0 < 3 ) ) → ( ( ( 2 · 𝑁 ) + 1 ) ≤ ( ( 2 · 𝑛 ) + 1 ) ↔ ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ≤ ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) ) )
129 121 123 125 127 128 syl112anc ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( ( 2 · 𝑁 ) + 1 ) ≤ ( ( 2 · 𝑛 ) + 1 ) ↔ ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ≤ ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) ) )
130 119 129 mpbid ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ≤ ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) )
131 83 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ∈ ℕ )
132 131 nnred ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ∈ ℝ )
133 24 12 syldan ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) ∈ ℕ )
134 133 nnred ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) ∈ ℝ )
135 13 24 14 sylancr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 9 ↑ 𝑛 ) ∈ ℕ )
136 135 nnred ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 9 ↑ 𝑛 ) ∈ ℝ )
137 135 nngt0d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 0 < ( 9 ↑ 𝑛 ) )
138 lemul1 ⊢ ( ( ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ∈ ℝ ∧ ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) ∈ ℝ ∧ ( ( 9 ↑ 𝑛 ) ∈ ℝ ∧ 0 < ( 9 ↑ 𝑛 ) ) ) → ( ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ≤ ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) ↔ ( ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ≤ ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) )
139 132 134 136 137 138 syl112anc ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ≤ ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) ↔ ( ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ≤ ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) )
140 130 139 mpbid ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ≤ ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) )
141 24 99 syldan ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ∈ ℕ )
142 141 nnred ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ∈ ℝ )
143 141 nngt0d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 0 < ( ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) )
144 24 58 syldan ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ∈ ℝ )
145 24 59 syldan ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 0 < ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) )
146 lediv2 ⊢ ( ( ( ( ( 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 ↑ 𝑛 ) ) ) ) )
147 142 143 144 145 113 115 146 syl222anc ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ≤ ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ↔ ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ≤ ( 2 / ( ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ) )
148 140 147 mpbid ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ≤ ( 2 / ( ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) )
149 9re ⊢ 9 ∈ ℝ
150 149 72 rereccli ⊢ ( 1 / 9 ) ∈ ℝ
151 150 recni ⊢ ( 1 / 9 ) ∈ ℂ
152 151 a1i ⊢ ( 𝑁 ∈ ℕ0 → ( 1 / 9 ) ∈ ℂ )
153 0re ⊢ 0 ∈ ℝ
154 9pos ⊢ 0 < 9
155 149 154 recgt0ii ⊢ 0 < ( 1 / 9 )
156 153 150 155 ltleii ⊢ 0 ≤ ( 1 / 9 )
157 absid ⊢ ( ( ( 1 / 9 ) ∈ ℝ ∧ 0 ≤ ( 1 / 9 ) ) → ( abs ‘ ( 1 / 9 ) ) = ( 1 / 9 ) )
158 150 156 157 mp2an ⊢ ( abs ‘ ( 1 / 9 ) ) = ( 1 / 9 )
159 1lt9 ⊢ 1 < 9
160 recgt1i ⊢ ( ( 9 ∈ ℝ ∧ 1 < 9 ) → ( 0 < ( 1 / 9 ) ∧ ( 1 / 9 ) < 1 ) )
161 149 159 160 mp2an ⊢ ( 0 < ( 1 / 9 ) ∧ ( 1 / 9 ) < 1 )
162 161 simpri ⊢ ( 1 / 9 ) < 1
163 158 162 eqbrtri ⊢ ( abs ‘ ( 1 / 9 ) ) < 1
164 163 a1i ⊢ ( 𝑁 ∈ ℕ0 → ( abs ‘ ( 1 / 9 ) ) < 1 )
165 eqid ⊢ ( 𝑘 ∈ ℕ0 ↦ ( ( 1 / 9 ) ↑ 𝑘 ) ) = ( 𝑘 ∈ ℕ0 ↦ ( ( 1 / 9 ) ↑ 𝑘 ) )
166 ovex ⊢ ( ( 1 / 9 ) ↑ 𝑛 ) ∈ V
167 64 165 166 fvmpt ⊢ ( 𝑛 ∈ ℕ0 → ( ( 𝑘 ∈ ℕ0 ↦ ( ( 1 / 9 ) ↑ 𝑘 ) ) ‘ 𝑛 ) = ( ( 1 / 9 ) ↑ 𝑛 ) )
168 24 167 syl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( 1 / 9 ) ↑ 𝑘 ) ) ‘ 𝑛 ) = ( ( 1 / 9 ) ↑ 𝑛 ) )
169 152 164 42 168 geolim2 ⊢ ( 𝑁 ∈ ℕ0 → seq 𝑁 ( + , ( 𝑘 ∈ ℕ0 ↦ ( ( 1 / 9 ) ↑ 𝑘 ) ) ) ⇝ ( ( ( 1 / 9 ) ↑ 𝑁 ) / ( 1 − ( 1 / 9 ) ) ) )
170 70 a1i ⊢ ( 𝑁 ∈ ℕ0 → 9 ∈ ℂ )
171 72 a1i ⊢ ( 𝑁 ∈ ℕ0 → 9 ≠ 0 )
172 170 171 23 exprecd ⊢ ( 𝑁 ∈ ℕ0 → ( ( 1 / 9 ) ↑ 𝑁 ) = ( 1 / ( 9 ↑ 𝑁 ) ) )
173 70 72 dividi ⊢ ( 9 / 9 ) = 1
174 173 oveq1i ⊢ ( ( 9 / 9 ) − ( 1 / 9 ) ) = ( 1 − ( 1 / 9 ) )
175 ax-1cn ⊢ 1 ∈ ℂ
176 70 72 pm3.2i ⊢ ( 9 ∈ ℂ ∧ 9 ≠ 0 )
177 divsubdir ⊢ ( ( 9 ∈ ℂ ∧ 1 ∈ ℂ ∧ ( 9 ∈ ℂ ∧ 9 ≠ 0 ) ) → ( ( 9 − 1 ) / 9 ) = ( ( 9 / 9 ) − ( 1 / 9 ) ) )
178 70 175 176 177 mp3an ⊢ ( ( 9 − 1 ) / 9 ) = ( ( 9 / 9 ) − ( 1 / 9 ) )
179 9m1e8 ⊢ ( 9 − 1 ) = 8
180 179 oveq1i ⊢ ( ( 9 − 1 ) / 9 ) = ( 8 / 9 )
181 178 180 eqtr3i ⊢ ( ( 9 / 9 ) − ( 1 / 9 ) ) = ( 8 / 9 )
182 174 181 eqtr3i ⊢ ( 1 − ( 1 / 9 ) ) = ( 8 / 9 )
183 182 a1i ⊢ ( 𝑁 ∈ ℕ0 → ( 1 − ( 1 / 9 ) ) = ( 8 / 9 ) )
184 172 183 oveq12d ⊢ ( 𝑁 ∈ ℕ0 → ( ( ( 1 / 9 ) ↑ 𝑁 ) / ( 1 − ( 1 / 9 ) ) ) = ( ( 1 / ( 9 ↑ 𝑁 ) ) / ( 8 / 9 ) ) )
185 175 a1i ⊢ ( 𝑁 ∈ ℕ0 → 1 ∈ ℂ )
186 nnexpcl ⊢ ( ( 9 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 9 ↑ 𝑁 ) ∈ ℕ )
187 13 186 mpan ⊢ ( 𝑁 ∈ ℕ0 → ( 9 ↑ 𝑁 ) ∈ ℕ )
188 187 nncnd ⊢ ( 𝑁 ∈ ℕ0 → ( 9 ↑ 𝑁 ) ∈ ℂ )
189 8cn ⊢ 8 ∈ ℂ
190 189 70 72 divcli ⊢ ( 8 / 9 ) ∈ ℂ
191 190 a1i ⊢ ( 𝑁 ∈ ℕ0 → ( 8 / 9 ) ∈ ℂ )
192 187 nnne0d ⊢ ( 𝑁 ∈ ℕ0 → ( 9 ↑ 𝑁 ) ≠ 0 )
193 8nn ⊢ 8 ∈ ℕ
194 193 nnne0i ⊢ 8 ≠ 0
195 189 70 194 72 divne0i ⊢ ( 8 / 9 ) ≠ 0
196 195 a1i ⊢ ( 𝑁 ∈ ℕ0 → ( 8 / 9 ) ≠ 0 )
197 185 188 191 192 196 divdiv32d ⊢ ( 𝑁 ∈ ℕ0 → ( ( 1 / ( 9 ↑ 𝑁 ) ) / ( 8 / 9 ) ) = ( ( 1 / ( 8 / 9 ) ) / ( 9 ↑ 𝑁 ) ) )
198 recdiv ⊢ ( ( ( 8 ∈ ℂ ∧ 8 ≠ 0 ) ∧ ( 9 ∈ ℂ ∧ 9 ≠ 0 ) ) → ( 1 / ( 8 / 9 ) ) = ( 9 / 8 ) )
199 189 194 70 72 198 mp4an ⊢ ( 1 / ( 8 / 9 ) ) = ( 9 / 8 )
200 199 oveq1i ⊢ ( ( 1 / ( 8 / 9 ) ) / ( 9 ↑ 𝑁 ) ) = ( ( 9 / 8 ) / ( 9 ↑ 𝑁 ) )
201 189 a1i ⊢ ( 𝑁 ∈ ℕ0 → 8 ∈ ℂ )
202 194 a1i ⊢ ( 𝑁 ∈ ℕ0 → 8 ≠ 0 )
203 170 201 188 202 192 divdiv1d ⊢ ( 𝑁 ∈ ℕ0 → ( ( 9 / 8 ) / ( 9 ↑ 𝑁 ) ) = ( 9 / ( 8 · ( 9 ↑ 𝑁 ) ) ) )
204 200 203 eqtrid ⊢ ( 𝑁 ∈ ℕ0 → ( ( 1 / ( 8 / 9 ) ) / ( 9 ↑ 𝑁 ) ) = ( 9 / ( 8 · ( 9 ↑ 𝑁 ) ) ) )
205 184 197 204 3eqtrd ⊢ ( 𝑁 ∈ ℕ0 → ( ( ( 1 / 9 ) ↑ 𝑁 ) / ( 1 − ( 1 / 9 ) ) ) = ( 9 / ( 8 · ( 9 ↑ 𝑁 ) ) ) )
206 169 205 breqtrd ⊢ ( 𝑁 ∈ ℕ0 → seq 𝑁 ( + , ( 𝑘 ∈ ℕ0 ↦ ( ( 1 / 9 ) ↑ 𝑘 ) ) ) ⇝ ( 9 / ( 8 · ( 9 ↑ 𝑁 ) ) ) )
207 expcl ⊢ ( ( ( 1 / 9 ) ∈ ℂ ∧ 𝑛 ∈ ℕ0 ) → ( ( 1 / 9 ) ↑ 𝑛 ) ∈ ℂ )
208 151 24 207 sylancr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 1 / 9 ) ↑ 𝑛 ) ∈ ℂ )
209 168 208 eqeltrd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( 1 / 9 ) ↑ 𝑘 ) ) ‘ 𝑛 ) ∈ ℂ )
210 24 68 syl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) · ( ( 1 / 9 ) ↑ 𝑘 ) ) ) ‘ 𝑛 ) = ( ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) · ( ( 1 / 9 ) ↑ 𝑛 ) ) )
211 168 oveq2d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) · ( ( 𝑘 ∈ ℕ0 ↦ ( ( 1 / 9 ) ↑ 𝑘 ) ) ‘ 𝑛 ) ) = ( ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) · ( ( 1 / 9 ) ↑ 𝑛 ) ) )
212 210 211 eqtr4d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) · ( ( 1 / 9 ) ↑ 𝑘 ) ) ) ‘ 𝑛 ) = ( ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) · ( ( 𝑘 ∈ ℕ0 ↦ ( ( 1 / 9 ) ↑ 𝑘 ) ) ‘ 𝑛 ) ) )
213 22 23 86 206 209 212 isermulc2 ⊢ ( 𝑁 ∈ ℕ0 → seq 𝑁 ( + , ( 𝑘 ∈ ℕ0 ↦ ( ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) · ( ( 1 / 9 ) ↑ 𝑘 ) ) ) ) ⇝ ( ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) · ( 9 / ( 8 · ( 9 ↑ 𝑁 ) ) ) ) )
214 seqex ⊢ seq 𝑁 ( + , ( 𝑘 ∈ ℕ0 ↦ ( ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) · ( ( 1 / 9 ) ↑ 𝑘 ) ) ) ) ∈ V
215 ovex ⊢ ( ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) · ( 9 / ( 8 · ( 9 ↑ 𝑁 ) ) ) ) ∈ V
216 214 215 breldm ⊢ ( seq 𝑁 ( + , ( 𝑘 ∈ ℕ0 ↦ ( ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) · ( ( 1 / 9 ) ↑ 𝑘 ) ) ) ) ⇝ ( ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) · ( 9 / ( 8 · ( 9 ↑ 𝑁 ) ) ) ) → seq 𝑁 ( + , ( 𝑘 ∈ ℕ0 ↦ ( ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) · ( ( 1 / 9 ) ↑ 𝑘 ) ) ) ) ∈ dom ⇝ )
217 213 216 syl ⊢ ( 𝑁 ∈ ℕ0 → seq 𝑁 ( + , ( 𝑘 ∈ ℕ0 ↦ ( ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) · ( ( 1 / 9 ) ↑ 𝑘 ) ) ) ) ∈ dom ⇝ )
218 22 23 34 35 98 102 148 46 217 isumle ⊢ ( 𝑁 ∈ ℕ0 → Σ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ≤ Σ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ( 2 / ( ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) )
219 102 recnd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 2 / ( ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ∈ ℂ )
220 3cn ⊢ 3 ∈ ℂ
221 4cn ⊢ 4 ∈ ℂ
222 2cn ⊢ 2 ∈ ℂ
223 4ne0 ⊢ 4 ≠ 0
224 3ne0 ⊢ 3 ≠ 0
225 2ne0 ⊢ 2 ≠ 0
226 220 221 222 220 223 224 225 divdivdivi ⊢ ( ( 3 / 4 ) / ( 2 / 3 ) ) = ( ( 3 · 3 ) / ( 4 · 2 ) )
227 3t3e9 ⊢ ( 3 · 3 ) = 9
228 4t2e8 ⊢ ( 4 · 2 ) = 8
229 227 228 oveq12i ⊢ ( ( 3 · 3 ) / ( 4 · 2 ) ) = ( 9 / 8 )
230 226 229 eqtri ⊢ ( ( 3 / 4 ) / ( 2 / 3 ) ) = ( 9 / 8 )
231 230 oveq2i ⊢ ( ( 2 / 3 ) · ( ( 3 / 4 ) / ( 2 / 3 ) ) ) = ( ( 2 / 3 ) · ( 9 / 8 ) )
232 220 221 223 divcli ⊢ ( 3 / 4 ) ∈ ℂ
233 222 220 224 divcli ⊢ ( 2 / 3 ) ∈ ℂ
234 222 220 225 224 divne0i ⊢ ( 2 / 3 ) ≠ 0
235 232 233 234 divcan2i ⊢ ( ( 2 / 3 ) · ( ( 3 / 4 ) / ( 2 / 3 ) ) ) = ( 3 / 4 )
236 231 235 eqtr3i ⊢ ( ( 2 / 3 ) · ( 9 / 8 ) ) = ( 3 / 4 )
237 236 oveq1i ⊢ ( ( ( 2 / 3 ) · ( 9 / 8 ) ) / ( ( ( 2 · 𝑁 ) + 1 ) · ( 9 ↑ 𝑁 ) ) ) = ( ( 3 / 4 ) / ( ( ( 2 · 𝑁 ) + 1 ) · ( 9 ↑ 𝑁 ) ) )
238 2cnd ⊢ ( 𝑁 ∈ ℕ0 → 2 ∈ ℂ )
239 220 a1i ⊢ ( 𝑁 ∈ ℕ0 → 3 ∈ ℂ )
240 81 nncnd ⊢ ( 𝑁 ∈ ℕ0 → ( ( 2 · 𝑁 ) + 1 ) ∈ ℂ )
241 224 a1i ⊢ ( 𝑁 ∈ ℕ0 → 3 ≠ 0 )
242 81 nnne0d ⊢ ( 𝑁 ∈ ℕ0 → ( ( 2 · 𝑁 ) + 1 ) ≠ 0 )
243 238 239 240 241 242 divdiv1d ⊢ ( 𝑁 ∈ ℕ0 → ( ( 2 / 3 ) / ( ( 2 · 𝑁 ) + 1 ) ) = ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) )
244 243 203 oveq12d ⊢ ( 𝑁 ∈ ℕ0 → ( ( ( 2 / 3 ) / ( ( 2 · 𝑁 ) + 1 ) ) · ( ( 9 / 8 ) / ( 9 ↑ 𝑁 ) ) ) = ( ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) · ( 9 / ( 8 · ( 9 ↑ 𝑁 ) ) ) ) )
245 233 a1i ⊢ ( 𝑁 ∈ ℕ0 → ( 2 / 3 ) ∈ ℂ )
246 70 189 194 divcli ⊢ ( 9 / 8 ) ∈ ℂ
247 246 a1i ⊢ ( 𝑁 ∈ ℕ0 → ( 9 / 8 ) ∈ ℂ )
248 245 240 247 188 242 192 divmuldivd ⊢ ( 𝑁 ∈ ℕ0 → ( ( ( 2 / 3 ) / ( ( 2 · 𝑁 ) + 1 ) ) · ( ( 9 / 8 ) / ( 9 ↑ 𝑁 ) ) ) = ( ( ( 2 / 3 ) · ( 9 / 8 ) ) / ( ( ( 2 · 𝑁 ) + 1 ) · ( 9 ↑ 𝑁 ) ) ) )
249 244 248 eqtr3d ⊢ ( 𝑁 ∈ ℕ0 → ( ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) · ( 9 / ( 8 · ( 9 ↑ 𝑁 ) ) ) ) = ( ( ( 2 / 3 ) · ( 9 / 8 ) ) / ( ( ( 2 · 𝑁 ) + 1 ) · ( 9 ↑ 𝑁 ) ) ) )
250 221 a1i ⊢ ( 𝑁 ∈ ℕ0 → 4 ∈ ℂ )
251 250 240 188 mulassd ⊢ ( 𝑁 ∈ ℕ0 → ( ( 4 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑁 ) ) = ( 4 · ( ( ( 2 · 𝑁 ) + 1 ) · ( 9 ↑ 𝑁 ) ) ) )
252 251 oveq2d ⊢ ( 𝑁 ∈ ℕ0 → ( 3 / ( ( 4 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑁 ) ) ) = ( 3 / ( 4 · ( ( ( 2 · 𝑁 ) + 1 ) · ( 9 ↑ 𝑁 ) ) ) ) )
253 81 187 nnmulcld ⊢ ( 𝑁 ∈ ℕ0 → ( ( ( 2 · 𝑁 ) + 1 ) · ( 9 ↑ 𝑁 ) ) ∈ ℕ )
254 253 nncnd ⊢ ( 𝑁 ∈ ℕ0 → ( ( ( 2 · 𝑁 ) + 1 ) · ( 9 ↑ 𝑁 ) ) ∈ ℂ )
255 223 a1i ⊢ ( 𝑁 ∈ ℕ0 → 4 ≠ 0 )
256 253 nnne0d ⊢ ( 𝑁 ∈ ℕ0 → ( ( ( 2 · 𝑁 ) + 1 ) · ( 9 ↑ 𝑁 ) ) ≠ 0 )
257 239 250 254 255 256 divdiv1d ⊢ ( 𝑁 ∈ ℕ0 → ( ( 3 / 4 ) / ( ( ( 2 · 𝑁 ) + 1 ) · ( 9 ↑ 𝑁 ) ) ) = ( 3 / ( 4 · ( ( ( 2 · 𝑁 ) + 1 ) · ( 9 ↑ 𝑁 ) ) ) ) )
258 252 257 eqtr4d ⊢ ( 𝑁 ∈ ℕ0 → ( 3 / ( ( 4 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑁 ) ) ) = ( ( 3 / 4 ) / ( ( ( 2 · 𝑁 ) + 1 ) · ( 9 ↑ 𝑁 ) ) ) )
259 237 249 258 3eqtr4a ⊢ ( 𝑁 ∈ ℕ0 → ( ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) · ( 9 / ( 8 · ( 9 ↑ 𝑁 ) ) ) ) = ( 3 / ( ( 4 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑁 ) ) ) )
260 213 259 breqtrd ⊢ ( 𝑁 ∈ ℕ0 → seq 𝑁 ( + , ( 𝑘 ∈ ℕ0 ↦ ( ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) · ( ( 1 / 9 ) ↑ 𝑘 ) ) ) ) ⇝ ( 3 / ( ( 4 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑁 ) ) ) )
261 22 23 98 219 260 isumclim ⊢ ( 𝑁 ∈ ℕ0 → Σ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ( 2 / ( ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) = ( 3 / ( ( 4 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑁 ) ) ) )
262 218 261 breqtrd ⊢ ( 𝑁 ∈ ℕ0 → Σ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ≤ ( 3 / ( ( 4 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑁 ) ) ) )
263 4nn ⊢ 4 ∈ ℕ
264 nnmulcl ⊢ ( ( 4 ∈ ℕ ∧ ( ( 2 · 𝑁 ) + 1 ) ∈ ℕ ) → ( 4 · ( ( 2 · 𝑁 ) + 1 ) ) ∈ ℕ )
265 263 81 264 sylancr ⊢ ( 𝑁 ∈ ℕ0 → ( 4 · ( ( 2 · 𝑁 ) + 1 ) ) ∈ ℕ )
266 265 187 nnmulcld ⊢ ( 𝑁 ∈ ℕ0 → ( ( 4 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑁 ) ) ∈ ℕ )
267 nndivre ⊢ ( ( 3 ∈ ℝ ∧ ( ( 4 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑁 ) ) ∈ ℕ ) → ( 3 / ( ( 4 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑁 ) ) ) ∈ ℝ )
268 124 266 267 sylancr ⊢ ( 𝑁 ∈ ℕ0 → ( 3 / ( ( 4 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑁 ) ) ) ∈ ℝ )
269 elicc2 ⊢ ( ( 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 ↑ 𝑁 ) ) ) ) ) )
270 153 268 269 sylancr ⊢ ( 𝑁 ∈ ℕ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 ↑ 𝑁 ) ) ) ) ) )
271 47 63 262 270 mpbir3and ⊢ ( 𝑁 ∈ ℕ0 → Σ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ∈ ( 0 [,] ( 3 / ( ( 4 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑁 ) ) ) ) )
272 54 271 eqeltrd ⊢ ( 𝑁 ∈ ℕ0 → ( ( log ‘ 2 ) − Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ) ∈ ( 0 [,] ( 3 / ( ( 4 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑁 ) ) ) ) )