---

Step * of Lemma another-test-ring-req

∀a,b,c,d,e,x:ℝ.  (b ≠ r0 ⇒ d ≠ r0 ⇒ x ≠ r0 ⇒ (((a/b) * (c/d) * (b * e/x)) = ((a * c/d) * e/x)))
BY
{ (Auto THEN nRNorm 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}a,b,c,d,e,x:\mBbbR{}.    (b  \mneq{}  r0  {}\mRightarrow{}  d  \mneq{}  r0  {}\mRightarrow{}  x  \mneq{}  r0  {}\mRightarrow{}  (((a/b)  *  (c/d)  *  (b  *  e/x))  =  ((a  *  c/d)  *  e/x)))


By

---

Latex:
(Auto  THEN  nRNorm  0  THEN  Auto)

---

Home Index