---

Step * 1 1 1 of Lemma implies-strict-inc


1. f : ℕ ⟶ ℕ
2. ∀i:ℕ. f i < f (i + 1)
3. j : ℤ
4. 0 < j
5. ∀i:ℕj - 1. f i < f (j - 1)
6. i : ℕj@i
7. f (j - 1) < f j
⊢ f i < f j
BY
{ (Decide i < j - 1 THENA Auto) }

1
1. f : ℕ ⟶ ℕ
2. ∀i:ℕ. f i < f (i + 1)
3. j : ℤ
4. 0 < j
5. ∀i:ℕj - 1. f i < f (j - 1)
6. i : ℕj@i
7. f (j - 1) < f j
8. i < j - 1
⊢ f i < f j

2
1. f : ℕ ⟶ ℕ
2. ∀i:ℕ. f i < f (i + 1)
3. j : ℤ
4. 0 < j
5. ∀i:ℕj - 1. f i < f (j - 1)
6. i : ℕj@i
7. f (j - 1) < f j
8. ¬i < j - 1
⊢ f i < f j

---

Latex:

---

Latex:

1.  f  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}
2.  \mforall{}i:\mBbbN{}.  f  i  <  f  (i  +  1)
3.  j  :  \mBbbZ{}
4.  0  <  j
5.  \mforall{}i:\mBbbN{}j  -  1.  f  i  <  f  (j  -  1)
6.  i  :  \mBbbN{}j@i
7.  f  (j  -  1)  <  f  j
\mvdash{}  f  i  <  f  j


By

---

Latex:
(Decide  i  <  j  -  1  THENA  Auto)

---

Home Index