---

Step * of Lemma rmul-neq-zero

∀x,y:ℝ.  (x ≠ r0 ⇒ y ≠ r0 ⇒ x * y ≠ r0)
BY
{ (Unfold `rneq` 0
   THEN Auto
   THEN SplitOrHyps
   THEN ((All (RWO "rless-iff-rpositive")⋅ THENA Auto)
         THEN All nRNorm
         THEN Auto
         THEN (FLemma `rpositive-rmul` [-2;-1] THENM nRNorm (-1))
         THEN Auto)⋅) }

---

Latex:

---

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


By

---

Latex:
(Unfold  `rneq`  0
  THEN  Auto
  THEN  SplitOrHyps
  THEN  ((All  (RWO  "rless-iff-rpositive")\mcdot{}  THENA  Auto)
              THEN  All  nRNorm
              THEN  Auto
              THEN  (FLemma  `rpositive-rmul`  [-2;-1]  THENM  nRNorm  (-1))
              THEN  Auto)\mcdot{})

---

Home Index