---

Step * 2 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 : ℝ
⊢ (Σi≤n + 1. a_i * x^i) = ((a (n + 1)) * rprod(0;(n + 1) - 1;j.x - z j))
BY
{ ((InstLemma `rpolynomial-linear-factor` [⌜n + 1⌝;⌜a⌝;⌜z n⌝]⋅ THENA Auto)
   THEN ExRepD
   THEN (InstHyp [⌜b⌝;⌜z⌝;⌜x⌝] 3⋅ 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. ∀[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

2
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. (Σi≤n. b_i * x^i) = ((b n) * rprod(0;n - 1;j.x - z j))
⊢ (Σi≤n + 1. a_i * x^i) = ((a (n + 1)) * rprod(0;(n + 1) - 1;j.x - z j))

---

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{}
\mvdash{}  (\mSigma{}i\mleq{}n  +  1.  a\_i  *  x\^{}i)  =  ((a  (n  +  1))  *  rprod(0;(n  +  1)  -  1;j.x  -  z  j))


By

---

Latex:
((InstLemma  `rpolynomial-linear-factor`  [\mkleeneopen{}n  +  1\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}z  n\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ExRepD
  THEN  (InstHyp  [\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]  3\mcdot{}  THENA  Auto))

---

Home Index