---

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


1. a : ℕ ⟶ ℝ
2. g : ℝ ⟶ ℝ
3. ∀x:ℝ. Σi.a[i] * x^i = g[x]
4. x : ℝ
⊢ Σi.a[i] * x - r0^i = g[x]
BY
{ (InstHyp [⌜x⌝] (-2)⋅ THENA Auto) }

1
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]

---

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{}
\mvdash{}  \mSigma{}i.a[i]  *  x  -  r0\^{}i  =  g[x]


By

---

Latex:
(InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto)

---

Home Index