---

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


1. n : ℕ+
2. z : ℕn ⟶ ℝ
3. y : ℕn ⟶ ℝ
4. j : ℕn
5. ∀i,j:ℕn.  (i < j ⇒ ((z i) < (z j)))
6. ∀i,j:ℕn.  (i < j ⇒ ((y i) < (y j)))
7. ∀i:ℕn. (rprod(0;n - 1;j.(z i) - y j) = r0)
8. ∀i:ℕn. (rprod(0;n - 1;j.(y i) - z j) = r0)
9. x : ℝ
10. ∀i:ℕn. (((z i) < x) ∧ ((y i) < x))
11. rprod(0;n - 1;j.x - y j) = rprod(0;n - 1;j.x - z j)
⊢ (z j) = (y j)
BY
{ (NatInd 1 THENL [Auto; (RepeatFor 2 (ParallelLast) THEN Auto THEN (RWO "rprod-split-last" (-1) THENA Auto))]) }

1
1. x : ℝ
2. n : ℤ
3. 0 < n
4. ∀z,y:ℕn - 1 ⟶ ℝ. ∀j:ℕn - 1.
     ((∀i,j:ℕn - 1.  (i < j ⇒ ((z i) < (z j))))
     ⇒ (∀i,j:ℕn - 1.  (i < j ⇒ ((y i) < (y j))))
     ⇒ (∀i:ℕn - 1. (rprod(0;n - 1 - 1;j.(z i) - y j) = r0))
     ⇒ (∀i:ℕn - 1. (rprod(0;n - 1 - 1;j.(y i) - z j) = r0))
     ⇒ (∀i:ℕn - 1. (((z i) < x) ∧ ((y i) < x)))
     ⇒ (rprod(0;n - 1 - 1;j.x - y j) = rprod(0;n - 1 - 1;j.x - z j))
     ⇒ ((z j) = (y j)))
5. z : ℕn ⟶ ℝ
6. ∀y:ℕn - 1 ⟶ ℝ. ∀j:ℕn - 1.
     ((∀i,j:ℕn - 1.  (i < j ⇒ ((z i) < (z j))))
     ⇒ (∀i,j:ℕn - 1.  (i < j ⇒ ((y i) < (y j))))
     ⇒ (∀i:ℕn - 1. (rprod(0;n - 1 - 1;j.(z i) - y j) = r0))
     ⇒ (∀i:ℕn - 1. (rprod(0;n - 1 - 1;j.(y i) - z j) = r0))
     ⇒ (∀i:ℕn - 1. (((z i) < x) ∧ ((y i) < x)))
     ⇒ (rprod(0;n - 1 - 1;j.x - y j) = rprod(0;n - 1 - 1;j.x - z j))
     ⇒ ((z j) = (y j)))
7. y : ℕn ⟶ ℝ
8. ∀j:ℕn - 1
     ((∀i,j:ℕn - 1.  (i < j ⇒ ((z i) < (z j))))
     ⇒ (∀i,j:ℕn - 1.  (i < j ⇒ ((y i) < (y j))))
     ⇒ (∀i:ℕn - 1. (rprod(0;n - 1 - 1;j.(z i) - y j) = r0))
     ⇒ (∀i:ℕn - 1. (rprod(0;n - 1 - 1;j.(y i) - z j) = r0))
     ⇒ (∀i:ℕn - 1. (((z i) < x) ∧ ((y i) < x)))
     ⇒ (rprod(0;n - 1 - 1;j.x - y j) = rprod(0;n - 1 - 1;j.x - z j))
     ⇒ ((z j) = (y j)))
9. j : ℕn
10. ∀i,j:ℕn.  (i < j ⇒ ((z i) < (z j)))
11. ∀i,j:ℕn.  (i < j ⇒ ((y i) < (y j)))
12. ∀i:ℕn. (rprod(0;n - 1;j.(z i) - y j) = r0)
13. ∀i:ℕn. (rprod(0;n - 1;j.(y i) - z j) = r0)
14. ∀i:ℕn. (((z i) < x) ∧ ((y i) < x))
15. (rprod(0;n - 1 - 1;j.x - y j) * (x - y (n - 1))) = (rprod(0;n - 1 - 1;j.x - z j) * (x - z (n - 1)))
⊢ (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{}i,j:\mBbbN{}n.    (i  <  j  {}\mRightarrow{}  ((z  i)  <  (z  j)))
6.  \mforall{}i,j:\mBbbN{}n.    (i  <  j  {}\mRightarrow{}  ((y  i)  <  (y  j)))
7.  \mforall{}i:\mBbbN{}n.  (rprod(0;n  -  1;j.(z  i)  -  y  j)  =  r0)
8.  \mforall{}i:\mBbbN{}n.  (rprod(0;n  -  1;j.(y  i)  -  z  j)  =  r0)
9.  x  :  \mBbbR{}
10.  \mforall{}i:\mBbbN{}n.  (((z  i)  <  x)  \mwedge{}  ((y  i)  <  x))
11.  rprod(0;n  -  1;j.x  -  y  j)  =  rprod(0;n  -  1;j.x  -  z  j)
\mvdash{}  (z  j)  =  (y  j)


By

---

Latex:
(NatInd  1
  THENL  [Auto;  (RepeatFor  2  (ParallelLast)  THEN  Auto  THEN  (RWO  "rprod-split-last"  (-1)  THENA  Auto))]
)

---

Home Index