---

Step * of Lemma q-elim

∀r:ℚ. ∃p:ℤ. ∃q:ℕ+. ((¬(q = 0 ∈ ℚ)) c∧ (r = (p/q) ∈ ℚ))
BY
{ xxx(Auto THEN (InstLemma `equals-qrep` [⌜r⌝]⋅ THENA Auto) THEN (RevHypSubst (-1) 0) THEN Auto)xxx }

1
1. r : ℚ
2. qrep(r) = r ∈ ℚ
⊢ ∃p:ℤ. ∃q:ℕ+. ((¬(q = 0 ∈ ℚ)) c∧ (qrep(r) = (p/q) ∈ ℚ))

---

Latex:

---

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


By

---

Latex:
xxx(Auto  THEN  (InstLemma  `equals-qrep`  [\mkleeneopen{}r\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  (RevHypSubst  (-1)  0)  THEN  Auto)xxx

---

Home Index