---

Step * 1 1 1 1 1 1 of Lemma rpolynomial-complete-factors-ordered


1. n : ℕ+
2. a : ℕn + 1 ⟶ ℝ
3. z : ℕn ⟶ ℝ
4. d : ℤ
5. [%2] : 0 < d
6. j : ℕ
7. j + d + 1 < n
8. (z j) < (z (j + 1))
9. (z (j + 1)) < (z ((j + 1) + (d - 1) + 1))
⊢ (z j) < (z (j + d + 1))
BY
{ (Subst' (j + 1) + (d - 1) + 1 ~ j + d + 1 -1 THEN Auto) }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}\msupplus{}
2.  a  :  \mBbbN{}n  +  1  {}\mrightarrow{}  \mBbbR{}
3.  z  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbR{}
4.  d  :  \mBbbZ{}
5.  [\%2]  :  0  <  d
6.  j  :  \mBbbN{}
7.  j  +  d  +  1  <  n
8.  (z  j)  <  (z  (j  +  1))
9.  (z  (j  +  1))  <  (z  ((j  +  1)  +  (d  -  1)  +  1))
\mvdash{}  (z  j)  <  (z  (j  +  d  +  1))


By

---

Latex:
(Subst'  (j  +  1)  +  (d  -  1)  +  1  \msim{}  j  +  d  +  1  -1  THEN  Auto)

---

Home Index