---

Step * 2 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 + 1) - 1)) = (a (n + 1))
12. j : ℕn
⊢ (Σi≤n. b_i * z j^i) = r0
BY
{ ((D -3 With ⌜z j⌝  THENA Auto) THEN (RWO "7" (-1) THENA Auto)) }

1
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. (b ((n + 1) - 1)) = (a (n + 1))
11. j : ℕn
12. r0 = (((z j) - z n) * (Σi≤(n + 1) - 1. b_i * z j^i))
⊢ (Σi≤n. b_i * z j^i) = r0

---

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  +  1)  -  1))  =  (a  (n  +  1))
12.  j  :  \mBbbN{}n
\mvdash{}  (\mSigma{}i\mleq{}n.  b\_i  *  z  j\^{}i)  =  r0


By

---

Latex:
((D  -3  With  \mkleeneopen{}z  j\mkleeneclose{}    THENA  Auto)  THEN  (RWO  "7"  (-1)  THENA  Auto))

---

Home Index