[proofplan] We prove the two implications separately. If an integral solution exists, then $d$ divides both terms $ax$ and $by$, so it divides their sum $c$. Conversely, if $d \mid c$, Bezout's identity provides an integral linear combination of $a$ and $b$ equal to $d$; multiplying that identity by $c/d$ produces an integral solution. [/proofplan] [step:Show that any integral solution forces $d$ to divide $c$] Assume that $(x,y) \in \mathbb{Z}^2$ satisfies \begin{align*} ax + by = c. \end{align*} Since $d = \gcd(a,b)$, the integer $d$ divides both $a$ and $b$. Hence there exist $\alpha,\beta \in \mathbb{Z}$ such that \begin{align*} a = d\alpha \end{align*} and \begin{align*} b = d\beta. \end{align*} Substituting these expressions into the equation gives \begin{align*} c = ax + by = d\alpha x + d\beta y = d(\alpha x + \beta y). \end{align*} Since $\alpha x + \beta y \in \mathbb{Z}$, this proves $d \mid c$. [/step] [step:Use Bezout's identity to build a solution when $d$ divides $c$] Assume conversely that $d \mid c$. By the definition of divisibility, there exists $k \in \mathbb{Z}$ such that \begin{align*} c = dk. \end{align*} By Bezout's identity (citing a result not yet in the wiki: Bezout's Identity), since $d = \gcd(a,b)$ and $(a,b) \ne (0,0)$, there exist $u,v \in \mathbb{Z}$ such that \begin{align*} au + bv = d. \end{align*} Define $x_0,y_0 \in \mathbb{Z}$ by \begin{align*} x_0 = uk \end{align*} and \begin{align*} y_0 = vk. \end{align*} Then \begin{align*} ax_0 + by_0 = a(uk) + b(vk) = k(au + bv) = kd = c. \end{align*} Thus $(x_0,y_0) \in \mathbb{Z}^2$ is a solution. [guided] Now assume $d \mid c$. The goal is to manufacture integers $x$ and $y$ whose linear combination with coefficients $a$ and $b$ gives $c$. The divisibility hypothesis means precisely that there is an integer multiplier $k \in \mathbb{Z}$ such that \begin{align*} c = dk. \end{align*} The missing ingredient is a way to write $d$ itself as an integral linear combination of $a$ and $b$. This is exactly Bezout's identity (citing a result not yet in the wiki: Bezout's Identity): because $d = \gcd(a,b)$ and $(a,b) \ne (0,0)$, there exist integers $u,v \in \mathbb{Z}$ satisfying \begin{align*} au + bv = d. \end{align*} Multiplying this identity by the integer $k$ gives \begin{align*} a(uk) + b(vk) = k(au + bv) = kd. \end{align*} Since $c = dk$ and integer multiplication is commutative, $kd = c$. Therefore \begin{align*} a(uk) + b(vk) = c. \end{align*} Define the candidate solution by \begin{align*} x_0 = uk \end{align*} and \begin{align*} y_0 = vk. \end{align*} Because $u,v,k \in \mathbb{Z}$ and $\mathbb{Z}$ is closed under multiplication, we have $x_0,y_0 \in \mathbb{Z}$. The displayed calculation proves \begin{align*} ax_0 + by_0 = c, \end{align*} so $(x_0,y_0) \in \mathbb{Z}^2$ is an integral solution. [/guided] [/step] [step:Combine the two implications] The first step proves that existence of an integral solution implies $d \mid c$. The second step proves that $d \mid c$ implies existence of an integral solution. Hence \begin{align*} \exists (x,y) \in \mathbb{Z}^2 \text{ such that } ax + by = c \iff d \mid c. \end{align*} This is the desired criterion. [/step]