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