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