---

Step * of Lemma qmul-not-zero

∀[a,b:ℚ].  uiff(¬((a * b) = 0 ∈ ℚ);(¬(a = 0 ∈ ℚ)) ∧ (¬(b = 0 ∈ ℚ)))
BY
{ (Auto THEN (ParallelLast THEN HypSubst' (-1) 0 THEN Auto THEN QNorm 0)⋅) }

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

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  (ParallelLast  THEN  HypSubst'  (-1)  0  THEN  Auto  THEN  QNorm  0)\mcdot{})

---

Home Index