---

Step * 1 of Lemma zero_divs_only_zero


1. a : ℤ
2. 0 | a
⊢ a = 0 ∈ ℤ
BY
{ (Unfold `divides` 2 THEN D 2) }

1
1. a : ℤ
2. c : ℤ
3. a = (0 * c) ∈ ℤ
⊢ a = 0 ∈ ℤ

---

Latex:

---

Latex:

1.  a  :  \mBbbZ{}
2.  0  |  a
\mvdash{}  a  =  0


By

---

Latex:
(Unfold  `divides`  2  THEN  D  2)

---

Home Index