---

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


1. n : ℕ+
2. a : ℕn + 1 ⟶ ℝ
3. z : ℕn ⟶ ℝ
4. ∀j:ℕn - 1. ((z j) < (z (j + 1)))
5. d : ℤ
6. [%2] : 0 < d
7. ∀j:ℕ. (j + (d - 1) + 1 < n ⇒ ((z j) < (z (j + (d - 1) + 1))))
8. j : ℕ
9. j + d + 1 < n
⊢ (z j) < (z (j + d + 1))
BY
{ ((D 4 With ⌜j⌝  THENA Auto) THEN (D 6 With ⌜j + 1⌝  THENA Auto)) }

1
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. (j + 1) + (d - 1) + 1 < n ⇒ ((z (j + 1)) < (z ((j + 1) + (d - 1) + 1)))
⊢ (z j) < (z (j + d + 1))

---

Latex:

---

Latex:

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


By

---

Latex:
((D  4  With  \mkleeneopen{}j\mkleeneclose{}    THENA  Auto)  THEN  (D  6  With  \mkleeneopen{}j  +  1\mkleeneclose{}    THENA  Auto))

---

Home Index