---

Step * 2 2 1 1 of Lemma rpolynomial-complete-factors


1. n : ℤ
2. 0 < n
3. ∀a:ℕn + 1 ⟶ ℝ. ∀z:ℕn ⟶ ℝ.
     ((∀i,j:ℕn.  ((¬(i = j ∈ ℤ)) ⇒ z i ≠ z j))
     ⇒ ∀[x:ℝ]. ((Σi≤n. a_i * x^i) = ((a n) * rprod(0;n - 1;j.x - z j))) supposing ∀j:ℕn. ((Σi≤n. a_i * z j^i) = r0))
4. a : ℕ(n + 1) + 1 ⟶ ℝ
5. z : ℕn + 1 ⟶ ℝ
6. ∀i,j:ℕn + 1.  ((¬(i = j ∈ ℤ)) ⇒ z i ≠ z j)
7. ∀j:ℕn + 1. ((Σi≤n + 1. a_i * z j^i) = r0)
8. x : ℝ
9. b : ℕn + 1 ⟶ ℝ
10. ∀[x:ℝ]. ((Σi≤n + 1. a_i * x^i) = ((x - z n) * (Σi≤(n + 1) - 1. b_i * x^i)))
11. (b n) = (a (n + 1))
12. (Σi≤n. b_i * x^i) = ((b n) * rprod(0;n - 1;j.x - z j))
13. v : ℝ
14. (a (n + 1)) = v ∈ ℝ
⊢ ((x - z n) * v * rprod(0;n - 1;j.x - z j)) = (v * rprod(0;n;j.x - z j))
BY
{ (RW (AddrC [2;2] UnfoldTopAbC) 0 THEN AutoSplit) }

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  0  <  n
3.  \mforall{}a:\mBbbN{}n  +  1  {}\mrightarrow{}  \mBbbR{}.  \mforall{}z:\mBbbN{}n  {}\mrightarrow{}  \mBbbR{}.
          ((\mforall{}i,j:\mBbbN{}n.    ((\mneg{}(i  =  j))  {}\mRightarrow{}  z  i  \mneq{}  z  j))
          {}\mRightarrow{}  \mforall{}[x:\mBbbR{}].  ((\mSigma{}i\mleq{}n.  a\_i  *  x\^{}i)  =  ((a  n)  *  rprod(0;n  -  1;j.x  -  z  j))) 
                supposing  \mforall{}j:\mBbbN{}n.  ((\mSigma{}i\mleq{}n.  a\_i  *  z  j\^{}i)  =  r0))
4.  a  :  \mBbbN{}(n  +  1)  +  1  {}\mrightarrow{}  \mBbbR{}
5.  z  :  \mBbbN{}n  +  1  {}\mrightarrow{}  \mBbbR{}
6.  \mforall{}i,j:\mBbbN{}n  +  1.    ((\mneg{}(i  =  j))  {}\mRightarrow{}  z  i  \mneq{}  z  j)
7.  \mforall{}j:\mBbbN{}n  +  1.  ((\mSigma{}i\mleq{}n  +  1.  a\_i  *  z  j\^{}i)  =  r0)
8.  x  :  \mBbbR{}
9.  b  :  \mBbbN{}n  +  1  {}\mrightarrow{}  \mBbbR{}
10.  \mforall{}[x:\mBbbR{}].  ((\mSigma{}i\mleq{}n  +  1.  a\_i  *  x\^{}i)  =  ((x  -  z  n)  *  (\mSigma{}i\mleq{}(n  +  1)  -  1.  b\_i  *  x\^{}i)))
11.  (b  n)  =  (a  (n  +  1))
12.  (\mSigma{}i\mleq{}n.  b\_i  *  x\^{}i)  =  ((b  n)  *  rprod(0;n  -  1;j.x  -  z  j))
13.  v  :  \mBbbR{}
14.  (a  (n  +  1))  =  v
\mvdash{}  ((x  -  z  n)  *  v  *  rprod(0;n  -  1;j.x  -  z  j))  =  (v  *  rprod(0;n;j.x  -  z  j))


By

---

Latex:
(RW  (AddrC  [2;2]  UnfoldTopAbC)  0  THEN  AutoSplit)

---

Home Index