---

Step * of Lemma any_divs_zero

∀b:ℤ. (b | 0)
BY
{ ((Unfold `divides` 0 THEN UnivCD) THENA Auto) }

1
1. b : ℤ@i
⊢ ∃c:ℤ. (0 = (b * c) ∈ ℤ)

---

Latex:

---

Latex:
\mforall{}b:\mBbbZ{}.  (b  |  0)


By

---

Latex:
((Unfold  `divides`  0  THEN  UnivCD)  THENA  Auto)

---

Home Index