---

Step * of Lemma ratreal-req

∀[a:ℤ]. ∀[b:ℕ+].  (ratreal(<a, b>) = (r(a)/r(b)))
BY
{ (Unfold `ratreal` 0 THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[a:\mBbbZ{}].  \mforall{}[b:\mBbbN{}\msupplus{}].    (ratreal(<a,  b>)  =  (r(a)/r(b)))


By

---

Latex:
(Unfold  `ratreal`  0  THEN  Reduce  0  THEN  Auto)

---

Home Index