---

Step * 3 of Lemma qmul-positive


1. a : ℚ
2. b : ℚ
3. 0 < a * b
⊢ (0 < a ∧ 0 < b) ∨ (0 < -(a) ∧ 0 < -(b))
BY
{ ((RWO "assert-qpositive<" (-1)⋅ THEN Auto)
   THEN (InstLemma `q_trichotomy` [⌜a⌝]⋅ THENA Auto)
   THEN (InstLemma `q_trichotomy` [⌜b⌝]⋅ THENA Auto)
   THEN SplitOrHyps
   THEN Auto
   THEN Try (xxx(xxxSubst ⌜a = 0 ∈ ℚ⌝ 3⋅xxx THEN Auto THEN QNorm  3 THEN RepUR ``qpositive`` 3 THEN Trivial)xxx)
   THEN Try (xxx(xxxSubst ⌜b = 0 ∈ ℚ⌝ 3⋅xxx THEN Auto THEN QNorm  3 THEN RepUR ``qpositive`` 3 THEN Trivial)xxx)
   THEN Try (xxx(OrLeft⋅ THEN Auto THEN RWO "assert-qpositive<" 0⋅ THEN Complete (Auto))xxx)
   THEN Try (xxx(OrRight⋅ THEN Auto THEN RWO "assert-qpositive<" 0⋅ THEN Complete (Auto))⋅xxx)
   THEN (xxxFLemma `qmul_positive` [-1;-2]xxx THENA Auto)
   THEN (FLemma `qminus_positive` [3] THENA Auto)
   THEN D -1
   THEN xxxAll QNormxxx
   THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
((RWO  "assert-qpositive<"  (-1)\mcdot{}  THEN  Auto)
  THEN  (InstLemma  `q\_trichotomy`  [\mkleeneopen{}a\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `q\_trichotomy`  [\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  SplitOrHyps
  THEN  Auto
  THEN  Try  (xxx(xxxSubst  \mkleeneopen{}a  =  0\mkleeneclose{}  3\mcdot{}xxx
                              THEN  Auto
                              THEN  QNorm    3
                              THEN  RepUR  ``qpositive``  3
                              THEN  Trivial)xxx)
  THEN  Try  (xxx(xxxSubst  \mkleeneopen{}b  =  0\mkleeneclose{}  3\mcdot{}xxx
                              THEN  Auto
                              THEN  QNorm    3
                              THEN  RepUR  ``qpositive``  3
                              THEN  Trivial)xxx)
  THEN  Try  (xxx(OrLeft\mcdot{}  THEN  Auto  THEN  RWO  "assert-qpositive<"  0\mcdot{}  THEN  Complete  (Auto))xxx)
  THEN  Try  (xxx(OrRight\mcdot{}  THEN  Auto  THEN  RWO  "assert-qpositive<"  0\mcdot{}  THEN  Complete  (Auto))\mcdot{}xxx)
  THEN  (xxxFLemma  `qmul\_positive`  [-1;-2]xxx  THENA  Auto)
  THEN  (FLemma  `qminus\_positive`  [3]  THENA  Auto)
  THEN  D  -1
  THEN  xxxAll  QNormxxx
  THEN  Auto)

---

Home Index