---

Step * of Lemma rpolynomial-complete-roots-unique

No Annotations
∀[n:ℕ+]. ∀[a:ℕn + 1 ⟶ ℝ].
  ∀[z,y:ℕn ⟶ ℝ].
    (∀[j:ℕn]. ((z j) = (y j))) supposing 
       ((∀j:ℕn. ((Σi≤n. a_i * z j^i) = r0)) and 
       (∀j:ℕn. ((Σi≤n. a_i * y j^i) = r0)) and 
       (∀j:ℕn - 1. ((y j) < (y (j + 1)))) and 
       (∀j:ℕn - 1. ((z j) < (z (j + 1))))) 
  supposing a n ≠ r0
BY
{ (Auto
   THEN (Assert ∀[x:ℝ]. (rprod(0;n - 1;j.x - y j) = rprod(0;n - 1;j.x - z j)) BY
               ((D 0 THENA Auto)
                THEN (InstLemma `rpolynomial-complete-factors-ordered` [⌜n⌝;⌜a⌝;⌜z⌝;⌜x⌝]⋅ THENA Auto)
                THEN (InstLemma `rpolynomial-complete-factors-ordered` [⌜n⌝;⌜a⌝;⌜y⌝;⌜x⌝]⋅ THENA Auto)
                THEN nRMul ⌜a n⌝ 0⋅
                THEN Auto))
   ) }

1
1. n : ℕ+
2. a : ℕn + 1 ⟶ ℝ
3. a n ≠ r0
4. z : ℕn ⟶ ℝ
5. y : ℕn ⟶ ℝ
6. ∀j:ℕn - 1. ((z j) < (z (j + 1)))
7. ∀j:ℕn - 1. ((y j) < (y (j + 1)))
8. ∀j:ℕn. ((Σi≤n. a_i * y j^i) = r0)
9. ∀j:ℕn. ((Σi≤n. a_i * z j^i) = r0)
10. j : ℕn
11. ∀[x:ℝ]. (rprod(0;n - 1;j.x - y j) = rprod(0;n - 1;j.x - z j))
⊢ (z j) = (y j)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[n:\mBbbN{}\msupplus{}].  \mforall{}[a:\mBbbN{}n  +  1  {}\mrightarrow{}  \mBbbR{}].
    \mforall{}[z,y:\mBbbN{}n  {}\mrightarrow{}  \mBbbR{}].
        (\mforall{}[j:\mBbbN{}n].  ((z  j)  =  (y  j)))  supposing 
              ((\mforall{}j:\mBbbN{}n.  ((\mSigma{}i\mleq{}n.  a\_i  *  z  j\^{}i)  =  r0))  and 
              (\mforall{}j:\mBbbN{}n.  ((\mSigma{}i\mleq{}n.  a\_i  *  y  j\^{}i)  =  r0))  and 
              (\mforall{}j:\mBbbN{}n  -  1.  ((y  j)  <  (y  (j  +  1))))  and 
              (\mforall{}j:\mBbbN{}n  -  1.  ((z  j)  <  (z  (j  +  1))))) 
    supposing  a  n  \mneq{}  r0


By

---

Latex:
(Auto
  THEN  (Assert  \mforall{}[x:\mBbbR{}].  (rprod(0;n  -  1;j.x  -  y  j)  =  rprod(0;n  -  1;j.x  -  z  j))  BY
                          ((D  0  THENA  Auto)
                            THEN  (InstLemma  `rpolynomial-complete-factors-ordered`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)
                            THEN  (InstLemma  `rpolynomial-complete-factors-ordered`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)
                            THEN  nRMul  \mkleeneopen{}a  n\mkleeneclose{}  0\mcdot{}
                            THEN  Auto))
  )

---

Home Index