---

Step * of Lemma rmul-nonzero

∀x,y:ℝ.  (x * y ≠ r0 ⇐⇒ x ≠ r0 ∧ y ≠ r0)
BY
{ (EAuto 1
   THEN D (-1)
   THEN Try ((FLemma `rmul-is-negative` [-1] THEN Auto THEN D -1 THEN Auto))
   THEN Try ((FLemma `rmul-is-positive` [-1] THEN Auto THEN D -1 THEN Auto)⋅)) }

1
1. x : ℝ@i
2. y : ℝ@i
3. (x * y) < r0@i
4. y < r0
⊢ x ≠ r0

2
1. x : ℝ@i
2. y : ℝ@i
3. (x * y) < r0@i
4. x < r0
⊢ y ≠ r0

---

Latex:

---

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


By

---

Latex:
(EAuto  1
  THEN  D  (-1)
  THEN  Try  ((FLemma  `rmul-is-negative`  [-1]  THEN  Auto  THEN  D  -1  THEN  Auto))
  THEN  Try  ((FLemma  `rmul-is-positive`  [-1]  THEN  Auto  THEN  D  -1  THEN  Auto)\mcdot{}))

---

Home Index