---

Step * 1 of Lemma rpolynomial-linear-factor


1. n : ℕ+
2. a : ℕn + 1 ⟶ ℝ
3. z : ℝ
4. (Σi≤n. a_i * z^i) = r0
5. x : ℝ
⊢ (Σi≤n. a_i * x^i) = ((x - z) * (Σi≤n - 1. rpolydiv(n;a;z)_i * x^i))
BY
{ (InstLemma  `rpolydiv-property` [⌜n⌝;⌜a⌝;⌜z⌝;⌜x⌝]⋅ THENA Auto) }

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

---

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{}
\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:
(InstLemma    `rpolydiv-property`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index