---

Step * of Lemma rmul-rinv2

∀[x:ℝ]. (rinv(x) * x) = r1 supposing x ≠ r0
BY
{ (Auto THEN RWO "rmul_comm" 0 THEN EAuto 1) }

---

Latex:

---

Latex:
\mforall{}[x:\mBbbR{}].  (rinv(x)  *  x)  =  r1  supposing  x  \mneq{}  r0


By

---

Latex:
(Auto  THEN  RWO  "rmul\_comm"  0  THEN  EAuto  1)

---

Home Index