---

Step * 1 1 of Lemma power-series-converges-everywhere


1. a : ℕ ⟶ ℝ
2. g : ℝ ⟶ ℝ
3. ∀x:ℝ. Σi.a[i] * x^i = g[x]
4. x : ℝ
5. Σi.a[i] * x^i = g[x]
⊢ Σi.a[i] * x - r0^i = g[x]
BY
{ (MoveToConcl (-1) THEN BLemma `series-sum_functionality` THEN Auto) }

---

Latex:

---

Latex:

1.  a  :  \mBbbN{}  {}\mrightarrow{}  \mBbbR{}
2.  g  :  \mBbbR{}  {}\mrightarrow{}  \mBbbR{}
3.  \mforall{}x:\mBbbR{}.  \mSigma{}i.a[i]  *  x\^{}i  =  g[x]
4.  x  :  \mBbbR{}
5.  \mSigma{}i.a[i]  *  x\^{}i  =  g[x]
\mvdash{}  \mSigma{}i.a[i]  *  x  -  r0\^{}i  =  g[x]


By

---

Latex:
(MoveToConcl  (-1)  THEN  BLemma  `series-sum\_functionality`  THEN  Auto)

---

Home Index