---

Step * of Lemma from-upto-singleton

∀[n,m,k:ℤ].  uiff([n, m) = [k] ∈ (ℤ List);(m = (n + 1) ∈ ℤ) ∧ (k = n ∈ ℤ))
BY
{ Auto }

1
1. n : ℤ
2. m : ℤ
3. k : ℤ
4. [n, m) = [k] ∈ (ℤ List)
⊢ m = (n + 1) ∈ ℤ

2
1. n : ℤ
2. m : ℤ
3. k : ℤ
4. [n, m) = [k] ∈ (ℤ List)
⊢ k = n ∈ ℤ

3
1. n : ℤ
2. m : ℤ
3. k : ℤ
4. m = (n + 1) ∈ ℤ
5. k = n ∈ ℤ
⊢ [n, m) = [k] ∈ (ℤ List)

---

Latex:

---

Latex:
\mforall{}[n,m,k:\mBbbZ{}].    uiff([n,  m)  =  [k];(m  =  (n  +  1))  \mwedge{}  (k  =  n))


By

---

Latex:
Auto

---

Home Index