---

Step * 1 1 of Lemma rpolynomial-complete-factors


1. n : ℕ+
2. a : ℕ1 + 1 ⟶ ℝ
3. z : ℕ1 ⟶ ℝ
4. ∀i,j:ℕ1.  ((¬(i = j ∈ ℤ)) ⇒ z i ≠ z j)
5. x : ℝ
6. (Σi≤1. a_i * z 0^i) = r0
7. b : ℕ1 ⟶ ℝ
8. ∀[x:ℝ]. ((Σi≤1. a_i * x^i) = ((x - z 0) * (Σi≤1 - 1. b_i * x^i)))
9. (b (1 - 1)) = (a 1)
⊢ ((x - z 0) * (Σi≤0. b_i * x^i)) = ((a 1) * rprod(0;0;j.x - z j))
BY
{ ((Unfolds ``rpolynomial rprod`` 0 THEN Reduce 0)
   THEN (RWO "rsum-single" 0 THENA Auto)
   THEN Unfold `rprod` 0
   THEN Reduce 0) }

1
1. n : ℕ+
2. a : ℕ1 + 1 ⟶ ℝ
3. z : ℕ1 ⟶ ℝ
4. ∀i,j:ℕ1.  ((¬(i = j ∈ ℤ)) ⇒ z i ≠ z j)
5. x : ℝ
6. (Σi≤1. a_i * z 0^i) = r0
7. b : ℕ1 ⟶ ℝ
8. ∀[x:ℝ]. ((Σi≤1. a_i * x^i) = ((x - z 0) * (Σi≤1 - 1. b_i * x^i)))
9. (b (1 - 1)) = (a 1)
⊢ ((x - z 0) * (b 0) * r1) = ((a 1) * r1 * (x - z 0))

---

Latex:

---

Latex:

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


By

---

Latex:
((Unfolds  ``rpolynomial  rprod``  0  THEN  Reduce  0)
  THEN  (RWO  "rsum-single"  0  THENA  Auto)
  THEN  Unfold  `rprod`  0
  THEN  Reduce  0)

---

Home Index