---

Step * of Lemma qdiv_wf

∀[r,s:ℚ].  (r/s) ∈ ℚ supposing ¬(s = 0 ∈ ℚ)
BY
{ (Unfold `qdiv` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[r,s:\mBbbQ{}].    (r/s)  \mmember{}  \mBbbQ{}  supposing  \mneg{}(s  =  0)


By

---

Latex:
(Unfold  `qdiv`  0  THEN  Auto)

---

Home Index