---

Step * 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 - 1) + 1)
⊢ f i < f j
BY
{ (Subst' (j - 1) + 1 ~ 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
⊢ 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  -  1)  +  1)
\mvdash{}  f  i  <  f  j


By

---

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

---

Home Index