---

Step * 1 1 of Lemma qexp-qdiv


∀a,b,v,v1:ℚ.  ((¬(b = 0 ∈ ℚ)) ⇒ (¬(v = 0 ∈ ℚ)) ⇒ (((v1/v) * (a/b)) = (v1 * a/v * b) ∈ ℚ))
BY
{ (Auto THEN QMul ⌜v * b⌝ 0⋅ THEN BLemma `qmul-not-zero` THEN Auto) }

---

Latex:

---

Latex:

\mforall{}a,b,v,v1:\mBbbQ{}.    ((\mneg{}(b  =  0))  {}\mRightarrow{}  (\mneg{}(v  =  0))  {}\mRightarrow{}  (((v1/v)  *  (a/b))  =  (v1  *  a/v  *  b)))


By

---

Latex:
(Auto  THEN  QMul  \mkleeneopen{}v  *  b\mkleeneclose{}  0\mcdot{}  THEN  BLemma  `qmul-not-zero`  THEN  Auto)

---

Home Index