---

Step * of Lemma rpolynomial-linear-factor

∀n:ℕ+. ∀a:ℕn + 1 ⟶ ℝ. ∀z:ℝ.
  ∃b:ℕn ⟶ ℝ. ((∀[x:ℝ]. ((Σi≤n. a_i * x^i) = ((x - z) * (Σi≤n - 1. b_i * x^i)))) ∧ ((b (n - 1)) = (a n))) 
  supposing (Σi≤n. a_i * z^i) = r0
BY
{ (Auto THEN D 0 With ⌜rpolydiv(n;a;z)⌝  THEN Auto) }

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

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

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}\msupplus{}.  \mforall{}a:\mBbbN{}n  +  1  {}\mrightarrow{}  \mBbbR{}.  \mforall{}z:\mBbbR{}.
    \mexists{}b:\mBbbN{}n  {}\mrightarrow{}  \mBbbR{}
      ((\mforall{}[x:\mBbbR{}].  ((\mSigma{}i\mleq{}n.  a\_i  *  x\^{}i)  =  ((x  -  z)  *  (\mSigma{}i\mleq{}n  -  1.  b\_i  *  x\^{}i))))  \mwedge{}  ((b  (n  -  1))  =  (a  n))) 
    supposing  (\mSigma{}i\mleq{}n.  a\_i  *  z\^{}i)  =  r0


By

---

Latex:
(Auto  THEN  D  0  With  \mkleeneopen{}rpolydiv(n;a;z)\mkleeneclose{}    THEN  Auto)

---

Home Index