---

Step * of Lemma qmul-qdiv

∀[a,b,c,d:ℚ].  (((a/c) * (b/d)) = (a * b/c * d) ∈ ℚ) supposing ((¬(d = 0 ∈ ℚ)) and (¬(c = 0 ∈ ℚ)))
BY
{ (Auto THEN (QMul ⌜c⌝ 0⋅ THENM Try (QMul ⌜d⌝ 0⋅))) }

---

Latex:

---

Latex:
\mforall{}[a,b,c,d:\mBbbQ{}].    (((a/c)  *  (b/d))  =  (a  *  b/c  *  d))  supposing  ((\mneg{}(d  =  0))  and  (\mneg{}(c  =  0)))


By

---

Latex:
(Auto  THEN  (QMul  \mkleeneopen{}c\mkleeneclose{}  0\mcdot{}  THENM  Try  (QMul  \mkleeneopen{}d\mkleeneclose{}  0\mcdot{})))

---

Home Index