---

Step * of Lemma divides_iff_div_exact

∀a:ℤ. ∀n:ℤ-o.  (n | a ⇐⇒ ((a ÷ n) * n) = a ∈ ℤ)
BY
{ Auto }

1
1. a : ℤ
2. n : ℤ-o
3. n | a
⊢ ((a ÷ n) * n) = a ∈ ℤ

2
1. a : ℤ
2. n : ℤ-o
3. ((a ÷ n) * n) = a ∈ ℤ
⊢ n | a

---

Latex:

---

Latex:
\mforall{}a:\mBbbZ{}.  \mforall{}n:\mBbbZ{}\msupminus{}\msupzero{}.    (n  |  a  \mLeftarrow{}{}\mRightarrow{}  ((a  \mdiv{}  n)  *  n)  =  a)


By

---

Latex:
Auto

---

Home Index