---

Step * of Lemma qabs-qdiv

∀[r:ℚ]. ∀[s:{s:ℚ| ¬(s = 0 ∈ ℚ)} ].  (|(r/s)| = (|r|/|s|) ∈ ℚ)
BY
{ xxx((Auto THEN Unfold `qdiv` 0)
      THEN D -1
      THEN (Assert ¬↑qeq(s;0) BY
                  (RW assert_pushdownC 0 THEN Auto))
      THEN (RWO "qabs-qinv<" 0 THENA Auto)
      THEN RWO "qabs-qmul" 0
      THEN Auto)xxx }

---

Latex:

---

Latex:
\mforall{}[r:\mBbbQ{}].  \mforall{}[s:\{s:\mBbbQ{}|  \mneg{}(s  =  0)\}  ].    (|(r/s)|  =  (|r|/|s|))


By

---

Latex:
xxx((Auto  THEN  Unfold  `qdiv`  0)
        THEN  D  -1
        THEN  (Assert  \mneg{}\muparrow{}qeq(s;0)  BY
                                (RW  assert\_pushdownC  0  THEN  Auto))
        THEN  (RWO  "qabs-qinv<"  0  THENA  Auto)
        THEN  RWO  "qabs-qmul"  0
        THEN  Auto)xxx

---

Home Index