---

Step * of Lemma rdiv-nonzero

∀x,y:ℝ.  (y ≠ r0 ⇒ ((x/y) ≠ r0 ⇐⇒ x ≠ r0))
BY
{ (RepeatFor 3 ((D 0 THENA Auto))
   THEN (InstLemma `rmul-nonzero` [⌜x⌝;⌜rinv(y)⌝]⋅ THENA Auto)
   THEN Fold `rdiv` (-1)
   THEN RWO "-1" 0
   THEN Auto
   THEN ThinVar `x') }

1
1. y : ℝ
2. y ≠ r0
⊢ rinv(y) ≠ r0

---

Latex:

---

Latex:
\mforall{}x,y:\mBbbR{}.    (y  \mneq{}  r0  {}\mRightarrow{}  ((x/y)  \mneq{}  r0  \mLeftarrow{}{}\mRightarrow{}  x  \mneq{}  r0))


By

---

Latex:
(RepeatFor  3  ((D  0  THENA  Auto))
  THEN  (InstLemma  `rmul-nonzero`  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}rinv(y)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Fold  `rdiv`  (-1)
  THEN  RWO  "-1"  0
  THEN  Auto
  THEN  ThinVar  `x')

---

Home Index