---

Step * of Lemma qmul-zero-div

∀[a:ℚ]. ∀[b:ℤ-o].  (((0/b) * a) = 0 ∈ ℚ)
BY
{ xxx(Auto THEN xxx(Subst ⌜(0/b) = 0 ∈ ℚ⌝ 0⋅ THENA Auto)xxx)xxx }

1
.....equality..... 
1. a : ℚ
2. b : ℤ-o
⊢ (0/b) = 0 ∈ ℚ

2
1. a : ℚ
2. b : ℤ-o
⊢ (0 * a) = 0 ∈ ℚ

---

Latex:

---

Latex:
\mforall{}[a:\mBbbQ{}].  \mforall{}[b:\mBbbZ{}\msupminus{}\msupzero{}].    (((0/b)  *  a)  =  0)


By

---

Latex:
xxx(Auto  THEN  xxx(Subst  \mkleeneopen{}(0/b)  =  0\mkleeneclose{}  0\mcdot{}  THENA  Auto)xxx)xxx

---

Home Index