---

Step * of Lemma rinverse-nonzero

∀x:ℝ. (x ≠ r0 ⇒ (r1/x) ≠ r0)
BY
{ (Auto THEN RepeatFor 2 (ParallelOp 2) THEN Auto THEN nRMul ⌜x⌝ 0⋅ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}x:\mBbbR{}.  (x  \mneq{}  r0  {}\mRightarrow{}  (r1/x)  \mneq{}  r0)


By

---

Latex:
(Auto  THEN  RepeatFor  2  (ParallelOp  2)  THEN  Auto  THEN  nRMul  \mkleeneopen{}x\mkleeneclose{}  0\mcdot{}  THEN  Auto)

---

Home Index