---

Step * 1 of Lemma rpolynomial-complete-roots-unique


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)
BY
{ (((InstLemma `sorted-seq-iff` [⌜ℝ⌝;⌜λ2x y.x < y⌝;⌜<n, z>⌝]⋅ THENA (Auto THEN D 0 THEN Reduce 0 THEN Auto))
    THEN (RepeatFor 2 (D -1) THENA (RepUR ``seq-len seq-item`` 0 THEN Trivial))
    THEN RepUR ``sorted-seq seq-len seq-item`` -1
    THEN Thin 6
    THEN Thin (-2))
   THEN (InstLemma `sorted-seq-iff` [⌜ℝ⌝;⌜λ2x y.x < y⌝;⌜<n, y>⌝]⋅ THENA (Auto THEN D 0 THEN Reduce 0 THEN Auto))
   THEN (RepeatFor 2 (D -1) THENA (RepUR ``seq-len seq-item`` 0 THEN Trivial))
   THEN RepUR ``sorted-seq seq-len seq-item`` -1
   THEN Thin 6
   THEN Thin (-2)
   THEN ThinVar `a') }

1
1. n : ℕ+
2. z : ℕn ⟶ ℝ
3. y : ℕn ⟶ ℝ
4. j : ℕn
5. ∀[x:ℝ]. (rprod(0;n - 1;j.x - y j) = rprod(0;n - 1;j.x - z j))
6. ∀i,j:ℕn.  (i < j ⇒ ((z i) < (z j)))
7. ∀i,j:ℕn.  (i < j ⇒ ((y i) < (y j)))
⊢ (z j) = (y j)

---

Latex:

---

Latex:

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


By

---

Latex:
(((InstLemma  `sorted-seq-iff`  [\mkleeneopen{}\mBbbR{}\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x  y.x  <  y\mkleeneclose{};\mkleeneopen{}<n,  z>\mkleeneclose{}]\mcdot{}
      THENA  (Auto  THEN  D  0  THEN  Reduce  0  THEN  Auto)
      )
    THEN  (RepeatFor  2  (D  -1)  THENA  (RepUR  ``seq-len  seq-item``  0  THEN  Trivial))
    THEN  RepUR  ``sorted-seq  seq-len  seq-item``  -1
    THEN  Thin  6
    THEN  Thin  (-2))
  THEN  (InstLemma  `sorted-seq-iff`  [\mkleeneopen{}\mBbbR{}\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x  y.x  <  y\mkleeneclose{};\mkleeneopen{}<n,  y>\mkleeneclose{}]\mcdot{}
              THENA  (Auto  THEN  D  0  THEN  Reduce  0  THEN  Auto)
              )
  THEN  (RepeatFor  2  (D  -1)  THENA  (RepUR  ``seq-len  seq-item``  0  THEN  Trivial))
  THEN  RepUR  ``sorted-seq  seq-len  seq-item``  -1
  THEN  Thin  6
  THEN  Thin  (-2)
  THEN  ThinVar  `a')

---

Home Index