---

Step * of Lemma int-to-real_wf

∀[n:ℤ]. (r(n) ∈ ℝ)
BY
{ (ProveWfLemma
   THEN MemTypeCD
   THEN Auto
   THEN D 0
   THEN Reduce 0
   THEN Auto
   THEN RW IntNormC 0
   THEN Auto
   THEN Unfold `absval` 0
   THEN Reduce 0
   THEN Auto') }

---

Latex:

---

Latex:
\mforall{}[n:\mBbbZ{}].  (r(n)  \mmember{}  \mBbbR{})


By

---

Latex:
(ProveWfLemma
  THEN  MemTypeCD
  THEN  Auto
  THEN  D  0
  THEN  Reduce  0
  THEN  Auto
  THEN  RW  IntNormC  0
  THEN  Auto
  THEN  Unfold  `absval`  0
  THEN  Reduce  0
  THEN  Auto')

---

Home Index