---

Step * 1 2 of Lemma int_lt_to_int_upper_uniform


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

---

Latex:

---

Latex:

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


By

---

Latex:
(BackThruHyp  3  THEN  Auto)

---

Home Index