---

Step * of Lemma qdiv-qminus

∀[x,y:ℚ].  (x/-(y)) = (-(x)/y) ∈ ℚ supposing ¬(y = 0 ∈ ℚ)
BY
{ xxx(Auto
      THEN (Assert ¬(-(y) = 0 ∈ ℚ) BY
                  (ParallelLast THEN (QMul ⌜-1⌝ (-1))⋅ THEN Auto))
      THEN (Assert ¬(-(-(y)) = 0 ∈ ℚ) BY
                  (ParallelLast THEN (QMul ⌜-1⌝ (-1))⋅ THEN Auto))
      THEN QMul ⌜(1/-1)⌝ 0⋅
      THEN ((RW (AddrC [2] (LemmaC `qmul-qdiv`)) 0) THENA Auto)
      THEN Subst ⌜(1/-1) = (-1) ∈ ℚ⌝ 0⋅
      THEN Auto
      THEN QMul ⌜y⌝ 0⋅)xxx }

---

Latex:

---

Latex:
\mforall{}[x,y:\mBbbQ{}].    (x/-(y))  =  (-(x)/y)  supposing  \mneg{}(y  =  0)


By

---

Latex:
xxx(Auto
        THEN  (Assert  \mneg{}(-(y)  =  0)  BY
                                (ParallelLast  THEN  (QMul  \mkleeneopen{}-1\mkleeneclose{}  (-1))\mcdot{}  THEN  Auto))
        THEN  (Assert  \mneg{}(-(-(y))  =  0)  BY
                                (ParallelLast  THEN  (QMul  \mkleeneopen{}-1\mkleeneclose{}  (-1))\mcdot{}  THEN  Auto))
        THEN  QMul  \mkleeneopen{}(1/-1)\mkleeneclose{}  0\mcdot{}
        THEN  ((RW  (AddrC  [2]  (LemmaC  `qmul-qdiv`))  0)  THENA  Auto)
        THEN  Subst  \mkleeneopen{}(1/-1)  =  (-1)\mkleeneclose{}  0\mcdot{}
        THEN  Auto
        THEN  QMul  \mkleeneopen{}y\mkleeneclose{}  0\mcdot{})xxx

---

Home Index