---

Step * of Lemma rinv-of-rinv

∀[x:ℝ]. rinv(rinv(x)) = x supposing x ≠ r0
BY
{ ((EAuto 1 THEN (Assert rinv(x) ≠ r0 BY EAuto 1))
   THEN Symmetry
   THEN Auto
   THEN BLemma `rmul-inverse-is-rinv`
   THEN Auto
   THEN BLemma `rmul-rinv2`
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
((EAuto  1  THEN  (Assert  rinv(x)  \mneq{}  r0  BY  EAuto  1))
  THEN  Symmetry
  THEN  Auto
  THEN  BLemma  `rmul-inverse-is-rinv`
  THEN  Auto
  THEN  BLemma  `rmul-rinv2`
  THEN  Auto)

---

Home Index