---

Step * of Lemma int_seg_finite

∀n,m:ℤ.  finite({n..m-})
BY
{ ((Unfold `finite` 0 THEN Auto) THEN (Decide ⌜n ≤ m⌝⋅ THENA Auto)) }

1
1. n : ℤ
2. m : ℤ
3. n ≤ m
⊢ ∃n@0:ℕ. {n..m-} ~ ℕn@0

2
1. n : ℤ
2. m : ℤ
3. ¬(n ≤ m)
⊢ ∃n@0:ℕ. {n..m-} ~ ℕn@0

---

Latex:

---

Latex:
\mforall{}n,m:\mBbbZ{}.    finite(\{n..m\msupminus{}\})


By

---

Latex:
((Unfold  `finite`  0  THEN  Auto)  THEN  (Decide  \mkleeneopen{}n  \mleq{}  m\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index