---

Step * of Lemma qmul-positive2

∀a,b:ℚ.  ((0 < a ∧ 0 < b) ∨ (a < 0 ∧ b < 0) ⇐⇒ 0 < a * b)
BY
{ (InstLemma `qmul-positive` [] THEN RepeatFor 5 (ParallelLast') THEN (QMul ⌜-1⌝ 0⋅ THEN Auto)⋅) }

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbQ{}.    ((0  <  a  \mwedge{}  0  <  b)  \mvee{}  (a  <  0  \mwedge{}  b  <  0)  \mLeftarrow{}{}\mRightarrow{}  0  <  a  *  b)


By

---

Latex:
(InstLemma  `qmul-positive`  []  THEN  RepeatFor  5  (ParallelLast')  THEN  (QMul  \mkleeneopen{}-1\mkleeneclose{}  0\mcdot{}  THEN  Auto)\mcdot{})

---

Home Index