---

Step * of Lemma qmul-qdiv-cancel

∀[a,b:ℚ].  (a * (b/a)) = b ∈ ℚ supposing ¬(a = 0 ∈ ℚ)
BY
{ xxx(xxxAutoxxx
      THEN (Assert ¬↑qeq(a;0) BY
                  (RW assert_pushdownC 0 THEN Auto))
      THEN Unfold `qdiv` 0
      THEN QNorm 0
      THEN (RWO "qmul_assoc<" 0 THENA Auto)
      THEN (Subst' (1/a * a) = 1 ∈ ℚ 0 THENA Auto)
      THEN QNorm 0
      THEN (RWO "qmul_com" 0 THENM RWO "qmul_inv" 0)
      THEN Auto)xxx }

---

Latex:

---

Latex:
\mforall{}[a,b:\mBbbQ{}].    (a  *  (b/a))  =  b  supposing  \mneg{}(a  =  0)


By

---

Latex:
xxx(xxxAutoxxx
        THEN  (Assert  \mneg{}\muparrow{}qeq(a;0)  BY
                                (RW  assert\_pushdownC  0  THEN  Auto))
        THEN  Unfold  `qdiv`  0
        THEN  QNorm  0
        THEN  (RWO  "qmul\_assoc<"  0  THENA  Auto)
        THEN  (Subst'  (1/a  *  a)  =  1  0  THENA  Auto)
        THEN  QNorm  0
        THEN  (RWO  "qmul\_com"  0  THENM  RWO  "qmul\_inv"  0)
        THEN  Auto)xxx

---

Home Index