---

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


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)
BY
{ ((Assert ∀i:ℕn. (rprod(0;n - 1;j.(z i) - y j) = r0) BY
          ((D 0 THENA Auto)
           THEN (D 5 With ⌜z i⌝  THENA Auto)
           THEN (RWO "-1" 0 THENA Auto)
           THEN (BLemma `rprod-is-zero` THEN Auto)
           THEN D 0 With ⌜i⌝ 
           THEN Auto))
   THEN (Assert ∀i:ℕn. (rprod(0;n - 1;j.(y i) - z j) = r0) BY
               ((D 0 THENA Auto)
                THEN (D 5 With ⌜y i⌝  THENA Auto)
                THEN (RWO "-1<" 0 THENA Auto)
                THEN (BLemma `rprod-is-zero` THEN Auto)
                THEN D 0 With ⌜i⌝ 
                THEN Auto))
   ) }

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)))
8. ∀i:ℕn. (rprod(0;n - 1;j.(z i) - y j) = r0)
9. ∀i:ℕn. (rprod(0;n - 1;j.(y i) - z j) = r0)
⊢ (z j) = (y j)

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}\msupplus{}
2.  z  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbR{}
3.  y  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbR{}
4.  j  :  \mBbbN{}n
5.  \mforall{}[x:\mBbbR{}].  (rprod(0;n  -  1;j.x  -  y  j)  =  rprod(0;n  -  1;j.x  -  z  j))
6.  \mforall{}i,j:\mBbbN{}n.    (i  <  j  {}\mRightarrow{}  ((z  i)  <  (z  j)))
7.  \mforall{}i,j:\mBbbN{}n.    (i  <  j  {}\mRightarrow{}  ((y  i)  <  (y  j)))
\mvdash{}  (z  j)  =  (y  j)


By

---

Latex:
((Assert  \mforall{}i:\mBbbN{}n.  (rprod(0;n  -  1;j.(z  i)  -  y  j)  =  r0)  BY
                ((D  0  THENA  Auto)
                  THEN  (D  5  With  \mkleeneopen{}z  i\mkleeneclose{}    THENA  Auto)
                  THEN  (RWO  "-1"  0  THENA  Auto)
                  THEN  (BLemma  `rprod-is-zero`  THEN  Auto)
                  THEN  D  0  With  \mkleeneopen{}i\mkleeneclose{} 
                  THEN  Auto))
  THEN  (Assert  \mforall{}i:\mBbbN{}n.  (rprod(0;n  -  1;j.(y  i)  -  z  j)  =  r0)  BY
                          ((D  0  THENA  Auto)
                            THEN  (D  5  With  \mkleeneopen{}y  i\mkleeneclose{}    THENA  Auto)
                            THEN  (RWO  "-1<"  0  THENA  Auto)
                            THEN  (BLemma  `rprod-is-zero`  THEN  Auto)
                            THEN  D  0  With  \mkleeneopen{}i\mkleeneclose{} 
                            THEN  Auto))
  )

---

Home Index