---

Step * 2 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)))
⊢ (rpolydiv(n;a;z) (n - 1)) = (a n)
BY
{ ((InstLemma `rpolydiv-rec` [⌜n⌝;⌜a⌝;⌜z⌝]⋅ THENA Auto) THEN D -1 THEN RWO "-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.  \mforall{}[x:\mBbbR{}].  ((\mSigma{}i\mleq{}n.  a\_i  *  x\^{}i)  =  ((x  -  z)  *  (\mSigma{}i\mleq{}n  -  1.  rpolydiv(n;a;z)\_i  *  x\^{}i)))
\mvdash{}  (rpolydiv(n;a;z)  (n  -  1))  =  (a  n)


By

---

Latex:
((InstLemma  `rpolydiv-rec`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  D  -1  THEN  RWO  "-2"  0  THEN  Auto)

---

Home Index