---

Step * 2 1 2 1 of Lemma triangular-reciprocal-series-sum


1. lim n→∞.r(2) - (r(2)/r(n + 2)) = r(2)
2. ∀i:ℕ. (1 ≤ t(i + 1))
3. ∀i:ℕ. (¬(t(i + 1) = 0 ∈ ℤ))
4. n : ℕ
5. Σ{(r1/r(t(k + 1))) | 0≤k≤n} = Σ{(r(2)/r(k + 1)) + (r(-2)/r(k + 2)) | 0≤k≤n}
⊢ (r(2) - (r(2)/r(n + 2))) = (Σ{(r(2)/r(i + 1)) | 0≤i≤n} + Σ{(r(-2)/r(i + 2)) | 0≤i≤n})
BY
{ ((RW (AddrC [2;1] (LemmaC `rsum-split-first`)) 0 THEN Auto)
   THEN RW (AddrC [2;2] (LemmaC `rsum-split-last`)) 0
   THEN Auto) }

1
1. lim n→∞.r(2) - (r(2)/r(n + 2)) = r(2)
2. ∀i:ℕ. (1 ≤ t(i + 1))
3. ∀i:ℕ. (¬(t(i + 1) = 0 ∈ ℤ))
4. n : ℕ
5. Σ{(r1/r(t(k + 1))) | 0≤k≤n} = Σ{(r(2)/r(k + 1)) + (r(-2)/r(k + 2)) | 0≤k≤n}
⊢ (r(2) - (r(2)/r(n + 2)))
= (((r(2)/r(0 + 1)) + Σ{(r(2)/r(i + 1)) | 0 + 1≤i≤n}) + Σ{(r(-2)/r(i + 2)) | 0≤i≤n - 1} + (r(-2)/r(n + 2)))

---

Latex:

---

Latex:

1.  lim  n\mrightarrow{}\minfty{}.r(2)  -  (r(2)/r(n  +  2))  =  r(2)
2.  \mforall{}i:\mBbbN{}.  (1  \mleq{}  t(i  +  1))
3.  \mforall{}i:\mBbbN{}.  (\mneg{}(t(i  +  1)  =  0))
4.  n  :  \mBbbN{}
5.  \mSigma{}\{(r1/r(t(k  +  1)))  |  0\mleq{}k\mleq{}n\}  =  \mSigma{}\{(r(2)/r(k  +  1))  +  (r(-2)/r(k  +  2))  |  0\mleq{}k\mleq{}n\}
\mvdash{}  (r(2)  -  (r(2)/r(n  +  2)))  =  (\mSigma{}\{(r(2)/r(i  +  1))  |  0\mleq{}i\mleq{}n\}  +  \mSigma{}\{(r(-2)/r(i  +  2))  |  0\mleq{}i\mleq{}n\})


By

---

Latex:
((RW  (AddrC  [2;1]  (LemmaC  `rsum-split-first`))  0  THEN  Auto)
  THEN  RW  (AddrC  [2;2]  (LemmaC  `rsum-split-last`))  0
  THEN  Auto)

---

Home Index