---

Step * 1 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
8. i < j - 1
⊢ f i < f j
BY
{ (InstHyp [⌜i⌝] (-4)⋅ THEN Auto) }

---

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
8.  i  <  j  -  1
\mvdash{}  f  i  <  f  j


By

---

Latex:
(InstHyp  [\mkleeneopen{}i\mkleeneclose{}]  (-4)\mcdot{}  THEN  Auto)

---

Home Index