[proofplan] We translate subgroup containment in the additive group $\mathbb{Z}$ into ordinary inclusion of subsets. If $m\mathbb{Z} \subseteq n\mathbb{Z}$, then the particular element $m = m \cdot 1$ lies in $n\mathbb{Z}$, which is exactly the existential definition of $n \mid m$. Conversely, if $m = nk$, then every integer multiple of $m$ is also an integer multiple of $n$. The case $n=0$ is automatically handled because divisibility is being used in its existential form. [/proofplan]

[step:Extract divisibility from containment by testing the generator $m$]Assume $m\mathbb{Z} \le n\mathbb{Z}$. Since subgroup containment means set inclusion for subgroups of $(\mathbb{Z},+)$, we have $m\mathbb{Z} \subseteq n\mathbb{Z}$. The integer $1 \in \mathbb{Z}$, so \begin{align*} m = m \cdot 1 \in m\mathbb{Z}. \end{align*} By the inclusion $m\mathbb{Z} \subseteq n\mathbb{Z}$, it follows that $m \in n\mathbb{Z}$. By the definition of $n\mathbb{Z}$, there exists $k \in \mathbb{Z}$ such that \begin{align*} m = nk. \end{align*} This is precisely $n \mid m$ under the stated definition of divisibility.[/step]

[guided]Assume $m\mathbb{Z} \le n\mathbb{Z}$. In the additive group $(\mathbb{Z},+)$, the symbol $\le$ between subgroups means containment as sets, so this hypothesis says \begin{align*} m\mathbb{Z} \subseteq n\mathbb{Z}. \end{align*} To prove $n \mid m$, we must produce an integer $k \in \mathbb{Z}$ such that $m = nk$. The containment gives information about every element of $m\mathbb{Z}$, so we choose the most useful one: the generator $m$ itself. Since $1 \in \mathbb{Z}$, the definition of $m\mathbb{Z}$ gives \begin{align*} m = m \cdot 1 \in m\mathbb{Z}. \end{align*} Using $m\mathbb{Z} \subseteq n\mathbb{Z}$, we obtain $m \in n\mathbb{Z}$. By the definition \begin{align*} n\mathbb{Z} = \{nb : b \in \mathbb{Z}\}, \end{align*} membership of $m$ in $n\mathbb{Z}$ means that there exists some $k \in \mathbb{Z}$ with \begin{align*} m = nk. \end{align*} This is exactly the existential definition of $n \mid m$.[/guided]

[step:Use divisibility to show every multiple of $m$ is a multiple of $n$] Assume $n \mid m$. By definition, there exists $k \in \mathbb{Z}$ such that \begin{align*} m = nk. \end{align*} Let $x \in m\mathbb{Z}$. By the definition of $m\mathbb{Z}$, there exists $a \in \mathbb{Z}$ such that \begin{align*} x = ma. \end{align*} Substituting $m = nk$ gives \begin{align*} x = nka. \end{align*} Since $k,a \in \mathbb{Z}$ and $\mathbb{Z}$ is closed under multiplication, $ka \in \mathbb{Z}$. Therefore \begin{align*} x = n(ka) \in n\mathbb{Z}. \end{align*} Thus every $x \in m\mathbb{Z}$ lies in $n\mathbb{Z}$, so $m\mathbb{Z} \subseteq n\mathbb{Z}$. Hence $m\mathbb{Z} \le n\mathbb{Z}$ as subgroups of $(\mathbb{Z},+)$. [/step]

[step:Confirm that the zero divisor case is covered by the same argument] The proof used only the definition $n \mid m$ iff there exists $k \in \mathbb{Z}$ with $m = nk$. Therefore, if $n=0$, the condition $0 \mid m$ means that there exists $k \in \mathbb{Z}$ with \begin{align*} m = 0 \cdot k = 0. \end{align*} Thus $0 \mid m$ holds exactly when $m=0$. In the subgroup statement, $m\mathbb{Z} \le 0\mathbb{Z}$ means $m\mathbb{Z} \subseteq \{0\}$, which also holds exactly when $m=0$. Hence the equivalence remains valid for $n=0$, and the two implications above prove the theorem for all $m,n \in \mathbb{Z}_{\ge 0}$. [/step]