---

Step * of Lemma member-from-upto

∀n,m:ℤ. ∀k:{x:ℤ| (n ≤ x) ∧ x < m} .  (k ∈ [n, m))
BY
{ (Auto THEN With ⌜k - n⌝ (D 0)⋅ THEN DVar `k' THEN Auto' THEN RWW "select-from-upto length-from-upto" 0 THEN Auto') }

---

Latex:

---

Latex:
\mforall{}n,m:\mBbbZ{}.  \mforall{}k:\{x:\mBbbZ{}|  (n  \mleq{}  x)  \mwedge{}  x  <  m\}  .    (k  \mmember{}  [n,  m))


By

---

Latex:
(Auto
  THEN  With  \mkleeneopen{}k  -  n\mkleeneclose{}  (D  0)\mcdot{}
  THEN  DVar  `k'
  THEN  Auto'
  THEN  RWW  "select-from-upto  length-from-upto"  0
  THEN  Auto')

---

Home Index