---

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


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
10. s i < s (i + 1)
⊢ s i < s j
BY
{ (Decide ⌜i + 1 < j⌝⋅ THENA 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
10. s i < s (i + 1)
11. i + 1 < j
⊢ s i < s j

2
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
10. s i < s (i + 1)
11. ¬i + 1 < j
⊢ s i < s j

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  s  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbZ{}
3.  \mforall{}i:\mBbbN{}n  -  1.  s  i  <  s  (i  +  1)
4.  d  :  \mBbbZ{}
5.  0  <  d
6.  \mforall{}j:\mBbbN{}n.  \mforall{}i:\mBbbN{}j.    (((j  -  i)  \mleq{}  (d  -  1))  {}\mRightarrow{}  s  i  <  s  j)
7.  j  :  \mBbbN{}n
8.  i  :  \mBbbN{}j
9.  (j  -  i)  \mleq{}  d
10.  s  i  <  s  (i  +  1)
\mvdash{}  s  i  <  s  j


By

---

Latex:
(Decide  \mkleeneopen{}i  +  1  <  j\mkleeneclose{}\mcdot{}  THENA  Auto)

---

Home Index