---

Step * 2 1 2 1 1 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(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)))
BY
{ (Unfold `rsub` 0 THEN BLemma `radd_functionality` 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(n + 2))) = (Σ{(r(2)/r(i + 1)) | 0 + 1≤i≤n} + Σ{(r(-2)/r(i + 2)) | 0≤i≤n - 1} + (r(-2)/r(n + 2)))

2
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(0 + 1))

---

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)))
=  ((r(2)/r(0  +  1))
    +  \mSigma{}\{(r(2)/r(i  +  1))  |  0  +  1\mleq{}i\mleq{}n\}
    +  \mSigma{}\{(r(-2)/r(i  +  2))  |  0\mleq{}i\mleq{}n  -  1\}
    +  (r(-2)/r(n  +  2)))


By

---

Latex:
(Unfold  `rsub`  0  THEN  BLemma  `radd\_functionality`  THEN  Auto)

---

Home Index