---

Step * 1 of Lemma implies-strictly-increasing-seq

.....assertion..... 
1. n : ℕ
2. s : ℕn ⟶ ℤ
3. ∀i:ℕn - 1. s i < s (i + 1)
⊢ ∀d:ℕ. ∀j:ℕn. ∀i:ℕj.  (((j - i) ≤ d) ⇒ s i < s j)
BY
{ (InductionOnNat THEN Auto') }

1
1. n : ℕ
2. s : ℕn ⟶ ℤ
3. ∀i:ℕn - 1. s i < s (i + 1)
4. d : ℤ
5. 0 < d
6. ∀j:ℕn. ∀i:ℕj.  (((j - i) ≤ (d - 1)) ⇒ s i < s j)
7. j : ℕn
8. i : ℕj
9. (j - i) ≤ d
⊢ s i < s j

---

Latex:

---

Latex:
.....assertion..... 
1.  n  :  \mBbbN{}
2.  s  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbZ{}
3.  \mforall{}i:\mBbbN{}n  -  1.  s  i  <  s  (i  +  1)
\mvdash{}  \mforall{}d:\mBbbN{}.  \mforall{}j:\mBbbN{}n.  \mforall{}i:\mBbbN{}j.    (((j  -  i)  \mleq{}  d)  {}\mRightarrow{}  s  i  <  s  j)


By

---

Latex:
(InductionOnNat  THEN  Auto')

---

Home Index