---

Step * 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. ∀j:ℕ1. ((Σi≤1. a_i * z j^i) = r0)
6. x : ℝ
⊢ (Σi≤1. a_i * x^i) = ((a 1) * rprod(0;1 - 1;j.x - z j))
BY
{ ((D -2 With ⌜0⌝  THENA Auto)
   THEN (InstLemma `rpolynomial-linear-factor` [⌜1⌝;⌜a⌝;⌜z 0⌝]⋅ THENA Auto)
   THEN ExRepD
   THEN (RWO  "-2" 0 THENA Auto)
   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) * (Σi≤0. b_i * x^i)) = ((a 1) * rprod(0;0;j.x - z j))

---

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.  \mforall{}j:\mBbbN{}1.  ((\mSigma{}i\mleq{}1.  a\_i  *  z  j\^{}i)  =  r0)
6.  x  :  \mBbbR{}
\mvdash{}  (\mSigma{}i\mleq{}1.  a\_i  *  x\^{}i)  =  ((a  1)  *  rprod(0;1  -  1;j.x  -  z  j))


By

---

Latex:
((D  -2  With  \mkleeneopen{}0\mkleeneclose{}    THENA  Auto)
  THEN  (InstLemma  `rpolynomial-linear-factor`  [\mkleeneopen{}1\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}z  0\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ExRepD
  THEN  (RWO    "-2"  0  THENA  Auto)
  THEN  Reduce  0)

---

Home Index