---

Step * of Lemma trivial-cancel

∀[g:ℤ-o]. ∀[v:ℤ].  uiff((g * v) = 0 ∈ ℤ;v = 0 ∈ ℤ)
BY
{ Auto }

1
1. g : ℤ-o
2. v : ℤ
3. (g * v) = 0 ∈ ℤ
⊢ v = 0 ∈ ℤ

2
1. g : ℤ-o
2. v : ℤ
3. v = 0 ∈ ℤ
⊢ (g * v) = 0 ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[g:\mBbbZ{}\msupminus{}\msupzero{}].  \mforall{}[v:\mBbbZ{}].    uiff((g  *  v)  =  0;v  =  0)


By

---

Latex:
Auto

---

Home Index