---

Step * 1 1 of Lemma rpolynomial-linear-factor


1. n : ℕ+
2. a : ℕn + 1 ⟶ ℝ
3. z : ℝ
4. (Σi≤n. a_i * z^i) = r0
5. x : ℝ
6. (Σi≤n. a_i * x^i) = (((x - z) * (Σi≤n - 1. rpolydiv(n;a;z)_i * x^i)) + (Σi≤n. a_i * z^i))
⊢ (Σi≤n. a_i * x^i) = ((x - z) * (Σi≤n - 1. rpolydiv(n;a;z)_i * x^i))
BY
{ (MoveToConcl (-1)
   THEN MoveToConcl (-2)
   THEN GenConclTerms Auto [⌜(x - z) * (Σi≤n - 1. rpolydiv(n;a;z)_i * x^i)⌝;⌜(Σi≤n. a_i * x^i)⌝;⌜(Σi≤n. a_i * z^i)⌝]⋅
   THEN All Thin
   THEN Auto
   THEN RWW "-1 -2" 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}\msupplus{}
2.  a  :  \mBbbN{}n  +  1  {}\mrightarrow{}  \mBbbR{}
3.  z  :  \mBbbR{}
4.  (\mSigma{}i\mleq{}n.  a\_i  *  z\^{}i)  =  r0
5.  x  :  \mBbbR{}
6.  (\mSigma{}i\mleq{}n.  a\_i  *  x\^{}i)  =  (((x  -  z)  *  (\mSigma{}i\mleq{}n  -  1.  rpolydiv(n;a;z)\_i  *  x\^{}i))  +  (\mSigma{}i\mleq{}n.  a\_i  *  z\^{}i))
\mvdash{}  (\mSigma{}i\mleq{}n.  a\_i  *  x\^{}i)  =  ((x  -  z)  *  (\mSigma{}i\mleq{}n  -  1.  rpolydiv(n;a;z)\_i  *  x\^{}i))


By

---

Latex:
(MoveToConcl  (-1)
  THEN  MoveToConcl  (-2)
  THEN  GenConclTerms  Auto  [\mkleeneopen{}(x  -  z)  *  (\mSigma{}i\mleq{}n  -  1.  rpolydiv(n;a;z)\_i  *  x\^{}i)\mkleeneclose{};\mkleeneopen{}(\mSigma{}i\mleq{}n.  a\_i  *  x\^{}i)\mkleeneclose{};
  \mkleeneopen{}(\mSigma{}i\mleq{}n.  a\_i  *  z\^{}i)\mkleeneclose{}]\mcdot{}
  THEN  All  Thin
  THEN  Auto
  THEN  RWW  "-1  -2"  0
  THEN  Auto)

---

Home Index