---

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


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)))
16. (y (n - 1)) < (z (n - 1))
⊢ False
BY
{ ((D -5 With ⌜n - 1⌝  THENA Auto)
   THEN ((Assert r0 < rprod(0;n - 1;j.(z (n - 1)) - y j) BY (BLemma `rprod-of-positive` THEN Auto)) THENM Auto)
   THEN ((Decide ⌜j1 = (n - 1) ∈ ℤ⌝⋅ THEN Auto)
         THENL [(HypSubst' (-1) 0 THEN Auto)
               ; ((Assert (y j1) < (y (n - 1)) BY (BackThruSomeHyp THEN Auto)) THEN nRAdd ⌜y j1⌝ 0⋅ THEN Auto)]
   )) }

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  n  :  \mBbbZ{}
3.  0  <  n
4.  \mforall{}z,y:\mBbbN{}n  -  1  {}\mrightarrow{}  \mBbbR{}.  \mforall{}j:\mBbbN{}n  -  1.
          ((\mforall{}i,j:\mBbbN{}n  -  1.    (i  <  j  {}\mRightarrow{}  ((z  i)  <  (z  j))))
          {}\mRightarrow{}  (\mforall{}i,j:\mBbbN{}n  -  1.    (i  <  j  {}\mRightarrow{}  ((y  i)  <  (y  j))))
          {}\mRightarrow{}  (\mforall{}i:\mBbbN{}n  -  1.  (rprod(0;n  -  1  -  1;j.(z  i)  -  y  j)  =  r0))
          {}\mRightarrow{}  (\mforall{}i:\mBbbN{}n  -  1.  (rprod(0;n  -  1  -  1;j.(y  i)  -  z  j)  =  r0))
          {}\mRightarrow{}  (\mforall{}i:\mBbbN{}n  -  1.  (((z  i)  <  x)  \mwedge{}  ((y  i)  <  x)))
          {}\mRightarrow{}  (rprod(0;n  -  1  -  1;j.x  -  y  j)  =  rprod(0;n  -  1  -  1;j.x  -  z  j))
          {}\mRightarrow{}  ((z  j)  =  (y  j)))
5.  z  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbR{}
6.  \mforall{}y:\mBbbN{}n  -  1  {}\mrightarrow{}  \mBbbR{}.  \mforall{}j:\mBbbN{}n  -  1.
          ((\mforall{}i,j:\mBbbN{}n  -  1.    (i  <  j  {}\mRightarrow{}  ((z  i)  <  (z  j))))
          {}\mRightarrow{}  (\mforall{}i,j:\mBbbN{}n  -  1.    (i  <  j  {}\mRightarrow{}  ((y  i)  <  (y  j))))
          {}\mRightarrow{}  (\mforall{}i:\mBbbN{}n  -  1.  (rprod(0;n  -  1  -  1;j.(z  i)  -  y  j)  =  r0))
          {}\mRightarrow{}  (\mforall{}i:\mBbbN{}n  -  1.  (rprod(0;n  -  1  -  1;j.(y  i)  -  z  j)  =  r0))
          {}\mRightarrow{}  (\mforall{}i:\mBbbN{}n  -  1.  (((z  i)  <  x)  \mwedge{}  ((y  i)  <  x)))
          {}\mRightarrow{}  (rprod(0;n  -  1  -  1;j.x  -  y  j)  =  rprod(0;n  -  1  -  1;j.x  -  z  j))
          {}\mRightarrow{}  ((z  j)  =  (y  j)))
7.  y  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbR{}
8.  \mforall{}j:\mBbbN{}n  -  1
          ((\mforall{}i,j:\mBbbN{}n  -  1.    (i  <  j  {}\mRightarrow{}  ((z  i)  <  (z  j))))
          {}\mRightarrow{}  (\mforall{}i,j:\mBbbN{}n  -  1.    (i  <  j  {}\mRightarrow{}  ((y  i)  <  (y  j))))
          {}\mRightarrow{}  (\mforall{}i:\mBbbN{}n  -  1.  (rprod(0;n  -  1  -  1;j.(z  i)  -  y  j)  =  r0))
          {}\mRightarrow{}  (\mforall{}i:\mBbbN{}n  -  1.  (rprod(0;n  -  1  -  1;j.(y  i)  -  z  j)  =  r0))
          {}\mRightarrow{}  (\mforall{}i:\mBbbN{}n  -  1.  (((z  i)  <  x)  \mwedge{}  ((y  i)  <  x)))
          {}\mRightarrow{}  (rprod(0;n  -  1  -  1;j.x  -  y  j)  =  rprod(0;n  -  1  -  1;j.x  -  z  j))
          {}\mRightarrow{}  ((z  j)  =  (y  j)))
9.  j  :  \mBbbN{}n
10.  \mforall{}i,j:\mBbbN{}n.    (i  <  j  {}\mRightarrow{}  ((z  i)  <  (z  j)))
11.  \mforall{}i,j:\mBbbN{}n.    (i  <  j  {}\mRightarrow{}  ((y  i)  <  (y  j)))
12.  \mforall{}i:\mBbbN{}n.  (rprod(0;n  -  1;j.(z  i)  -  y  j)  =  r0)
13.  \mforall{}i:\mBbbN{}n.  (rprod(0;n  -  1;j.(y  i)  -  z  j)  =  r0)
14.  \mforall{}i:\mBbbN{}n.  (((z  i)  <  x)  \mwedge{}  ((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)))
16.  (y  (n  -  1))  <  (z  (n  -  1))
\mvdash{}  False


By

---

Latex:
((D  -5  With  \mkleeneopen{}n  -  1\mkleeneclose{}    THENA  Auto)
  THEN  ((Assert  r0  <  rprod(0;n  -  1;j.(z  (n  -  1))  -  y  j)  BY
                            (BLemma  `rprod-of-positive`  THEN  Auto))
  THENM  Auto
  )
  THEN  ((Decide  \mkleeneopen{}j1  =  (n  -  1)\mkleeneclose{}\mcdot{}  THEN  Auto)
              THENL  [(HypSubst'  (-1)  0  THEN  Auto)
                          ;  ((Assert  (y  j1)  <  (y  (n  -  1))  BY
                                              (BackThruSomeHyp  THEN  Auto))
                                THEN  nRAdd  \mkleeneopen{}y  j1\mkleeneclose{}  0\mcdot{}
                                THEN  Auto)]
  ))

---

Home Index