---

Step * 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))
⊢ Σn.(r1/r(t(n + 1))) = r(2)
BY
{ ((Assert ∀i:ℕ. (¬(t(i + 1) = 0 ∈ ℤ)) BY
          (Auto THEN OnMaybeHyp 2 (\h. (InstHyp [⌜i⌝] h⋅ THEN Complete (Auto)))))
   THEN Unfold `series-sum` 0⋅
   THEN InstLemma `converges-to_functionality` [⌜λ2n.r(2) - (r(2)/r(n + 2))⌝;⌜λ2n.Σ{(r1/r(t(i + 1))) | 0≤i≤n}⌝;⌜r(2)⌝;
   ⌜r(2)⌝]⋅
   THEN Auto
   THEN (InstLemma `rsum_functionality` [⌜0⌝;⌜n⌝;⌜λ2i.(r1/r(t(i + 1)))⌝;⌜λ2i.(r(2)/r(i + 1)) + (r(-2)/r(i + 2))⌝]⋅
         THENA Auto
         )⋅) }

1
.....antecedent..... 
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 : ℕ
⊢ (r1/r(t(k + 1))) = (r(2)/r(k + 1)) + (r(-2)/r(k + 2)) for k ∈ [0,n]

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(n + 2))) = Σ{(r1/r(t(i + 1))) | 0≤i≤n}

---

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))
\mvdash{}  \mSigma{}n.(r1/r(t(n  +  1)))  =  r(2)


By

---

Latex:
((Assert  \mforall{}i:\mBbbN{}.  (\mneg{}(t(i  +  1)  =  0))  BY
                (Auto  THEN  OnMaybeHyp  2  (\mbackslash{}h.  (InstHyp  [\mkleeneopen{}i\mkleeneclose{}]  h\mcdot{}  THEN  Complete  (Auto)))))
  THEN  Unfold  `series-sum`  0\mcdot{}
  THEN  InstLemma  `converges-to\_functionality`  [\mkleeneopen{}\mlambda{}\msubtwo{}n.r(2)  -  (r(2)/r(n  +  2))\mkleeneclose{};
  \mkleeneopen{}\mlambda{}\msubtwo{}n.\mSigma{}\{(r1/r(t(i  +  1)))  |  0\mleq{}i\mleq{}n\}\mkleeneclose{};\mkleeneopen{}r(2)\mkleeneclose{};\mkleeneopen{}r(2)\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  (InstLemma  `rsum\_functionality`  [\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}i.(r1/r(t(i  +  1)))\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}i.(r(2)/r(i  +  1))
                                                                                                                                              +  (r(-2)/r(i  +  2))\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )\mcdot{})

---

Home Index