---

Step * 1 1 2 of Lemma rmul-is-positive


1. x : ℝ
2. y : ℝ
3. r0 < (x * y)
4. y < r0
⊢ x < r0
BY
{ (nRMul ⌜r(-1)⌝ (-1)⋅ THEN nRMul ⌜r(-1)⌝ 0⋅ THEN (Assert (x * y) = (-(x) * -(y)) BY (nRNorm 0 THEN Auto))) }

1
1. x : ℝ
2. y : ℝ
3. r0 < (x * y)
4. r0 < -(y)
5. (x * y) = (-(x) * -(y))
⊢ r0 < -(x)

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  y  :  \mBbbR{}
3.  r0  <  (x  *  y)
4.  y  <  r0
\mvdash{}  x  <  r0


By

---

Latex:
(nRMul  \mkleeneopen{}r(-1)\mkleeneclose{}  (-1)\mcdot{}
  THEN  nRMul  \mkleeneopen{}r(-1)\mkleeneclose{}  0\mcdot{}
  THEN  (Assert  (x  *  y)  =  (-(x)  *  -(y))  BY
                          (nRNorm  0  THEN  Auto)))

---

Home Index