---

Step * 1 1 of Lemma int_lt_to_int_upper_uniform


1. i : ℤ@i
2. [A] : {i + 1...} ⟶ ℙ
3. ∀[j:ℤ]. A[j] supposing i < j@i
4. [j] : {i + 1...}
⊢ A[j]
BY
{ (BackThruHyp 3 THEN Auto) }

---

Latex:

---

Latex:

1.  i  :  \mBbbZ{}@i
2.  [A]  :  \{i  +  1...\}  {}\mrightarrow{}  \mBbbP{}
3.  \mforall{}[j:\mBbbZ{}].  A[j]  supposing  i  <  j@i
4.  [j]  :  \{i  +  1...\}
\mvdash{}  A[j]


By

---

Latex:
(BackThruHyp  3  THEN  Auto)

---

Home Index