---

Step * of Lemma from-upto-member-nat

∀n,m,k:ℕ.  uiff((k ∈ [n, m));(n ≤ k) ∧ k < m)
BY
{ ((UnivCD THENA Auto) THEN RepeatFor 2 ((D 0 THENA Auto))) }

1
1. n : ℕ
2. m : ℕ
3. k : ℕ
4. (k ∈ [n, m))
⊢ (n ≤ k) ∧ k < m

2
1. n : ℕ
2. m : ℕ
3. k : ℕ
4. (n ≤ k) ∧ k < m
⊢ (k ∈ [n, m))

---

Latex:

---

Latex:
\mforall{}n,m,k:\mBbbN{}.    uiff((k  \mmember{}  [n,  m));(n  \mleq{}  k)  \mwedge{}  k  <  m)


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  RepeatFor  2  ((D  0  THENA  Auto)))

---

Home Index