---

Step * 1 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) * (b 0) * r1) = ((a 1) * r1 * (x - z 0))
BY
{ (Reduce -1 THEN RWO "-1" 0 THEN Auto) }

---

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)  *  (b  0)  *  r1)  =  ((a  1)  *  r1  *  (x  -  z  0))


By

---

Latex:
(Reduce  -1  THEN  RWO  "-1"  0  THEN  Auto)

---

Home Index