---

Step * of Lemma qabs-qmul

∀[r,s:ℚ].  (|r * s| = (|r| * |s|) ∈ ℚ)
BY
{ xxx(Auto
      THEN (InstLemma `q_trichotomy` [⌜r⌝]⋅ THENA Auto)
      THEN (InstLemma `q_trichotomy` [⌜s⌝]⋅ THENA Auto)
      THEN (Unfold `qabs` 0 THEN (CallByValueReduce 0 THENA Auto))
      THEN OldAutoBoolCase ⌜qpositive(r)⌝⋅
      THEN OldAutoBoolCase ⌜qpositive(s)⌝⋅
      THEN OldAutoBoolCase ⌜qpositive(r * s)⌝⋅
      THEN QNorm 0
      THEN ((All (RWO "assert-qpositive")) THENA Auto)
      THEN ((RWO "qmul-positive<" (-1)) THENA Auto)
      THEN ((All (RWO "qminus-positive")) THENA Auto)
      THEN Try (Complete (((D (-1)) THEN Auto))))xxx }

1
1. r : ℚ
2. s : ℚ
3. 0 < r ∨ (r = 0 ∈ ℚ) ∨ r < 0
4. 0 < s ∨ (s = 0 ∈ ℚ) ∨ s < 0
5. ¬0 < r
6. ¬0 < s
7. ¬((0 < r ∧ 0 < s) ∨ (r < 0 ∧ s < 0))
⊢ -(r * s) = (r * s) ∈ ℚ

---

Latex:

---

Latex:
\mforall{}[r,s:\mBbbQ{}].    (|r  *  s|  =  (|r|  *  |s|))


By

---

Latex:
xxx(Auto
        THEN  (InstLemma  `q\_trichotomy`  [\mkleeneopen{}r\mkleeneclose{}]\mcdot{}  THENA  Auto)
        THEN  (InstLemma  `q\_trichotomy`  [\mkleeneopen{}s\mkleeneclose{}]\mcdot{}  THENA  Auto)
        THEN  (Unfold  `qabs`  0  THEN  (CallByValueReduce  0  THENA  Auto))
        THEN  OldAutoBoolCase  \mkleeneopen{}qpositive(r)\mkleeneclose{}\mcdot{}
        THEN  OldAutoBoolCase  \mkleeneopen{}qpositive(s)\mkleeneclose{}\mcdot{}
        THEN  OldAutoBoolCase  \mkleeneopen{}qpositive(r  *  s)\mkleeneclose{}\mcdot{}
        THEN  QNorm  0
        THEN  ((All  (RWO  "assert-qpositive"))  THENA  Auto)
        THEN  ((RWO  "qmul-positive<"  (-1))  THENA  Auto)
        THEN  ((All  (RWO  "qminus-positive"))  THENA  Auto)
        THEN  Try  (Complete  (((D  (-1))  THEN  Auto))))xxx

---

Home Index