---

Step * of Lemma from-upto-nil

∀[n,m:ℤ].  [n, m) ~ [] supposing m ≤ n
BY
{ (InstLemma `from-upto-is-nil` [] THEN RepeatFor 2 (ParallelLast)) }

1
1. ∀[n,m:ℤ].  uiff([n, m) ~ [];m ≤ n)
2. [n] : ℤ
3. ∀[m:ℤ]. uiff([n, m) ~ [];m ≤ n)
4. [m] : ℤ
5. uiff([n, m) ~ [];m ≤ n)
⊢ [n, m) ~ [] supposing m ≤ n

---

Latex:

---

Latex:
\mforall{}[n,m:\mBbbZ{}].    [n,  m)  \msim{}  []  supposing  m  \mleq{}  n


By

---

Latex:
(InstLemma  `from-upto-is-nil`  []  THEN  RepeatFor  2  (ParallelLast))

---

Home Index