---

Step * of Lemma better-q-elim

∀r:ℚ. ∃p:ℤ. ∃q:ℕ+. ((¬(q = 0 ∈ ℚ)) c∧ (r = (p/q) ∈ ℚ))
BY
{ (InstLemma `q-elim` [] THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}r:\mBbbQ{}.  \mexists{}p:\mBbbZ{}.  \mexists{}q:\mBbbN{}\msupplus{}.  ((\mneg{}(q  =  0))  c\mwedge{}  (r  =  (p/q)))


By

---

Latex:
(InstLemma  `q-elim`  []  THEN  Trivial)

---

Home Index