---

Step * of Lemma rmul-zero-div

∀[x,y:ℝ].  ((r0/y) * x) = r0 supposing y ≠ r0
BY
{ (Auto THEN RWO "rdiv-zero" 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[x,y:\mBbbR{}].    ((r0/y)  *  x)  =  r0  supposing  y  \mneq{}  r0


By

---

Latex:
(Auto  THEN  RWO  "rdiv-zero"  0  THEN  Auto)

---

Home Index