---

Step * 1 1 of Lemma qmul-negative


1. a : ℚ@i
2. b : ℚ@i
3. a * b < 0@i
⊢ 0 < -(a) * b
BY
{ (QMul ⌜-1⌝ 0⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  a  :  \mBbbQ{}@i
2.  b  :  \mBbbQ{}@i
3.  a  *  b  <  0@i
\mvdash{}  0  <  -(a)  *  b


By

---

Latex:
(QMul  \mkleeneopen{}-1\mkleeneclose{}  0\mcdot{}  THEN  Auto)

---

Home Index