---

Step * 1 of Lemma decidable-exists-int_seg-subtype


1. i : ℤ
2. j : {i + 1...}
3. P : {i..j-} ⟶ ℙ
4. ¬P[i]
5. k : ℤ@i
6. i ≤ k@i
7. k < j@i
8. P[k]@i
⊢ (i + 1) ≤ k
BY
{ (Decide k = i ∈ ℤ THEN Auto) }

1
1. i : ℤ
2. j : {i + 1...}
3. P : {i..j-} ⟶ ℙ
4. ¬P[i]
5. k : ℤ@i
6. i ≤ k@i
7. k < j@i
8. P[k]@i
9. k = i ∈ ℤ
⊢ (i + 1) ≤ k

---

Latex:

---

Latex:

1.  i  :  \mBbbZ{}
2.  j  :  \{i  +  1...\}
3.  P  :  \{i..j\msupminus{}\}  {}\mrightarrow{}  \mBbbP{}
4.  \mneg{}P[i]
5.  k  :  \mBbbZ{}@i
6.  i  \mleq{}  k@i
7.  k  <  j@i
8.  P[k]@i
\mvdash{}  (i  +  1)  \mleq{}  k


By

---

Latex:
(Decide  k  =  i  THEN  Auto)

---

Home Index