---

Step * 1 of Lemma one_divs_any


1. a : ℤ@i
⊢ 1 | a
BY
{ Unfold `divides` 0 }

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

---

Latex:

---

Latex:

1.  a  :  \mBbbZ{}@i
\mvdash{}  1  |  a


By

---

Latex:
Unfold  `divides`  0

---

Home Index