---

Step * of Lemma geometric-series-one-half

Σn.(r1/r(2)^n) = r(2)
BY
{ ((InstLemma `series-sum_functionality` [⌜λ2n.(r1/r(2))^n⌝;⌜λ2n.(r1/r(2)^n)⌝;⌜(r1/r1 - (r1/r(2)))⌝;⌜r(2)⌝]⋅
   THENM (BHyp -1 THEN BLemma `geometric-series-converges` THEN Auto)
   )
   THEN Auto
   ) }

1
1. n : ℕ
⊢ r(2)^n ≠ r0

2
r1 - (r1/r(2)) ≠ r0

3
1. n : ℕ
⊢ (r1/r(2))^n = (r1/r(2)^n)

4
r1 - (r1/r(2)) ≠ r0

---

Latex:

---

Latex:
\mSigma{}n.(r1/r(2)\^{}n)  =  r(2)


By

---

Latex:
((InstLemma  `series-sum\_functionality`  [\mkleeneopen{}\mlambda{}\msubtwo{}n.(r1/r(2))\^{}n\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}n.(r1/r(2)\^{}n)\mkleeneclose{};\mkleeneopen{}(r1/r1  -  (r1/r(2)))\mkleeneclose{};
    \mkleeneopen{}r(2)\mkleeneclose{}]\mcdot{}
  THENM  (BHyp  -1  THEN  BLemma  `geometric-series-converges`  THEN  Auto)
  )
  THEN  Auto
  )

---

Home Index