---

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

.....assertion..... 
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)
⊢ ∃x:ℝ. ∀i:ℕn. (((z i) < x) ∧ ((y i) < x))
BY
{ (D 0 With ⌜rmax((z (n - 1)) + r1;(y (n - 1)) + r1)⌝  THEN Auto THEN BLemma `rmax_strict_ub` 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)
10. i : ℕn
⊢ ((z i) < ((z (n - 1)) + r1)) ∨ ((z i) < ((y (n - 1)) + r1))

2
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)
10. i : ℕn
11. (z i) < rmax((z (n - 1)) + r1;(y (n - 1)) + r1)
⊢ ((y i) < ((z (n - 1)) + r1)) ∨ ((y i) < ((y (n - 1)) + r1))

---

Latex:

---

Latex:
.....assertion..... 
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)))
8.  \mforall{}i:\mBbbN{}n.  (rprod(0;n  -  1;j.(z  i)  -  y  j)  =  r0)
9.  \mforall{}i:\mBbbN{}n.  (rprod(0;n  -  1;j.(y  i)  -  z  j)  =  r0)
\mvdash{}  \mexists{}x:\mBbbR{}.  \mforall{}i:\mBbbN{}n.  (((z  i)  <  x)  \mwedge{}  ((y  i)  <  x))


By

---

Latex:
(D  0  With  \mkleeneopen{}rmax((z  (n  -  1))  +  r1;(y  (n  -  1))  +  r1)\mkleeneclose{} 
  THEN  Auto
  THEN  BLemma  `rmax\_strict\_ub`
  THEN  Auto)

---

Home Index