---

Step * of Lemma qmul-preserves-eq

∀[a,b,c:ℚ].  uiff(a = b ∈ ℚ;(c * a) = (c * b) ∈ ℚ) supposing ¬(c = 0 ∈ ℚ)
BY
{ (Auto THEN Try ((HypSubst' -1 0 THEN Auto))) }

1
1. a : ℚ
2. b : ℚ
3. c : ℚ
4. ¬(c = 0 ∈ ℚ)
5. (c * a) = (c * b) ∈ ℚ
⊢ a = b ∈ ℚ

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  Try  ((HypSubst'  -1  0  THEN  Auto)))

---

Home Index