---

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

.....assertion..... 
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(i + 1)) | 0 + 1≤i≤n} + Σ{(r(-2)/r(i + 2)) | 0≤i≤n - 1}) = r0
BY
{ (All Thin⋅ THEN (InstLemma `rsum-shift` [⌜1⌝]⋅ THENA Auto)) }

1
1. n : ℕ
2. ∀[n,m:ℤ]. ∀[x:Top].  (Σ{x[i] | n≤i≤m} ~ Σ{x[i + 1] | n - 1≤i≤m - 1})
⊢ (Σ{(r(2)/r(i + 1)) | 0 + 1≤i≤n} + Σ{(r(-2)/r(i + 2)) | 0≤i≤n - 1}) = r0

---

Latex:

---

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


By

---

Latex:
(All  Thin\mcdot{}  THEN  (InstLemma  `rsum-shift`  [\mkleeneopen{}1\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index