[proofplan] We prove the two implications separately. If an integer solution exists, then every common divisor of $a$ and $b$, in particular $\gcd(a,b)$, divides the integer linear combination $ax+by=c$. Conversely, if $\gcd(a,b)$ divides $c$, we use the Bezout representation of $\gcd(a,b)$ as an integer linear combination of $a$ and $b$, then scale that representation by the integer quotient $c/\gcd(a,b)$. [/proofplan] [step:Show that any solution forces $\gcd(a,b)$ to divide $c$] Suppose there exist integers $x,y \in \mathbb{Z}$ satisfying \begin{align*} ax + by = c. \end{align*} Let $h := \gcd(a,b)$. Since $h \mid a$ and $h \mid b$, there exist integers $r,s \in \mathbb{Z}$ such that $a = hr$ and $b = hs$. Substituting into the equation gives \begin{align*} c = ax + by = hrx + hsy = h(rx + sy). \end{align*} Because $rx+sy \in \mathbb{Z}$, this proves $h \mid c$, that is, $\gcd(a,b) \mid c$. [/step] [step:Scale a Bezout representation when $\gcd(a,b)$ divides $c$] Suppose $\gcd(a,b) \mid c$. Let $h := \gcd(a,b)$. Since $a,b \in \mathbb{N}$, we have $h \in \mathbb{N}$, so division by $h$ is defined in $\mathbb{Q}$. The divisibility hypothesis gives an integer $q \in \mathbb{Z}$ such that \begin{align*} c = hq. \end{align*} By the [GCD as Linear Combination](/theorems/727), applied to the natural numbers $a$ and $b$, there exist integers $x_0,y_0 \in \mathbb{Z}$ such that \begin{align*} ax_0 + by_0 = h. \end{align*} Define integers $x,y \in \mathbb{Z}$ by \begin{align*} x := qx_0, \qquad y := qy_0. \end{align*} Then \begin{align*} ax + by &= a(qx_0) + b(qy_0) \\ &= q(ax_0 + by_0) \\ &= qh \\ &= c. \end{align*} Thus the equation $ax+by=c$ has an integer solution. [guided] Assume $\gcd(a,b) \mid c$, and let $h := \gcd(a,b)$. Since $a,b \in \mathbb{N}$, the greatest common divisor $h$ is a positive integer. The divisibility assumption means exactly that there is an integer $q \in \mathbb{Z}$ with \begin{align*} c = hq. \end{align*} We now use the ingredient that converts the greatest common divisor into a linear expression in $a$ and $b$. By GCD as Linear Combination, whose hypotheses apply because $a,b \in \mathbb{N}$, there exist integers $x_0,y_0 \in \mathbb{Z}$ such that \begin{align*} ax_0 + by_0 = h. \end{align*} The goal is to obtain $c$ on the right-hand side rather than $h$. Since $c = hq$, we multiply the Bezout identity by the integer $q$. Define \begin{align*} x := qx_0, \qquad y := qy_0. \end{align*} Because $q,x_0,y_0 \in \mathbb{Z}$ and $\mathbb{Z}$ is closed under multiplication, both $x$ and $y$ are integers. Substituting these definitions gives \begin{align*} ax + by &= a(qx_0) + b(qy_0) \\ &= q(ax_0 + by_0) \\ &= qh \\ &= c. \end{align*} Therefore $x,y \in \mathbb{Z}$ solve $ax+by=c$. [/guided] [/step] [step:Combine the two implications] The first step proves that the existence of integers $x,y \in \mathbb{Z}$ satisfying $ax+by=c$ implies $\gcd(a,b) \mid c$. The second step proves that $\gcd(a,b) \mid c$ implies the existence of such integers $x,y$. Hence the equation $ax+by=c$ has an integer solution if and only if $\gcd(a,b) \mid c$. [/step]