[proofplan]
Write $A=a/d$ and $B=b/d$, so that $A$ and $B$ are coprime integers. First we verify by direct substitution that every pair in the displayed parametrized family solves the equation. For the converse, subtract the known solution from an arbitrary solution to get $AX+BY=0$, where $X=x-x_0$ and $Y=y-y_0$. If $B\ne 0$, Euclid's lemma forces $B\mid X$, and the equation then determines $Y$; if $B=0$, coprimality gives $A=\pm 1$, so the same parametrization follows directly.
[/proofplan]
custom_env
admin
[step:Introduce the reduced coprime coefficients]Define integers $A,B\in \mathbb{Z}$ by
\begin{align*}
A=\frac{a}{d}, \qquad B=\frac{b}{d}.
\end{align*}
These are integers because $d=\gcd(a,b)$ divides both $a$ and $b$. Since $d>0$ and $(a,b)\ne (0,0)$, we also have $(A,B)\ne (0,0)$ and $\gcd(A,B)=1$.[/step]
custom_env
admin
[guided]The point of dividing by $d=\gcd(a,b)$ is to remove the common factor from the two coefficients. Define
\begin{align*}
A=\frac{a}{d}, \qquad B=\frac{b}{d}.
\end{align*}
Because $d$ divides both $a$ and $b$, both $A$ and $B$ are integers. Since $d>0$ and at least one of $a,b$ is nonzero, at least one of $A,B$ is nonzero.
We now check that $A$ and $B$ are coprime. If an integer $e$ divides both $A$ and $B$, then $ed$ divides both $a=dA$ and $b=dB$. Since $d$ is the greatest positive common divisor of $a$ and $b$, this forces $|e|=1$. Hence $\gcd(A,B)=1$.[/guided]
custom_env
admin
[step:Verify that every parametrized pair is an integer solution]
Let $t\in \mathbb{Z}$, and define $(x_t,y_t)\in \mathbb{Z}^2$ by
\begin{align*}
(x_t,y_t)=\left(x_0+Bt,\ y_0-At\right).
\end{align*}
Since $A,B,x_0,y_0,t\in \mathbb{Z}$, the pair $(x_t,y_t)$ is integral. Using $a=dA$ and $b=dB$, we compute
\begin{align*}
ax_t+by_t=a(x_0+Bt)+b(y_0-At).
\end{align*}
Expanding and grouping the $t$-terms gives
\begin{align*}
ax_t+by_t=ax_0+by_0+(aB-bA)t.
\end{align*}
Since $aB=dAB$ and $bA=dBA$, the coefficient $aB-bA$ is zero. Therefore
\begin{align*}
ax_t+by_t=ax_0+by_0=c.
\end{align*}
Thus every displayed parametrized pair is a solution.
[/step]
custom_env
admin
[step:Subtract the fixed solution from an arbitrary solution]
Let $(x,y)\in \mathbb{Z}^2$ be any solution of $ax+by=c$. Define integers $X,Y\in \mathbb{Z}$ by
\begin{align*}
X=x-x_0, \qquad Y=y-y_0.
\end{align*}
Subtracting the equation $ax_0+by_0=c$ from $ax+by=c$ gives
\begin{align*}
aX+bY=0.
\end{align*}
Since $a=dA$ and $b=dB$, division by the positive integer $d$ gives
\begin{align*}
AX+BY=0.
\end{align*}
[/step]
custom_env
admin
[step:Use coprimality to find the parameter when $B\ne 0$]
Assume first that $B\ne 0$. From $AX+BY=0$ we have
\begin{align*}
AX=-BY.
\end{align*}
Hence $B\mid AX$. Since $\gcd(A,B)=1$, Euclid's lemma applies and gives $B\mid X$. Thus there exists $t\in \mathbb{Z}$ such that
\begin{align*}
X=Bt.
\end{align*}
Substituting this into $AX+BY=0$ gives
\begin{align*}
ABt+BY=0.
\end{align*}
Factoring out the nonzero integer $B$ gives
\begin{align*}
B(At+Y)=0.
\end{align*}
Because $\mathbb{Z}$ has no zero divisors and $B\ne 0$, we get $At+Y=0$, so
\begin{align*}
Y=-At.
\end{align*}
Therefore
\begin{align*}
x=x_0+Bt, \qquad y=y_0-At.
\end{align*}
In terms of $a,b,d$, this is
\begin{align*}
(x,y)=\left(x_0+\frac{b}{d}t,\ y_0-\frac{a}{d}t\right).
\end{align*}
[/step]
custom_env
admin
[step:Handle the case where $B=0$]
Assume now that $B=0$. Since $\gcd(A,B)=1$, we have $\gcd(A,0)=1$, hence $A=\pm 1$. The equation $AX+BY=0$ reduces to
\begin{align*}
AX=0.
\end{align*}
Since $A=\pm 1$, this gives $X=0$. Define $t\in \mathbb{Z}$ by
\begin{align*}
t=-AY.
\end{align*}
Then $B=0$ gives $X=Bt$, and since $A^2=1$,
\begin{align*}
-At=-A(-AY)=Y.
\end{align*}
Thus
\begin{align*}
x=x_0+Bt, \qquad y=y_0-At.
\end{align*}
Equivalently,
\begin{align*}
(x,y)=\left(x_0+\frac{b}{d}t,\ y_0-\frac{a}{d}t\right).
\end{align*}
[/step]
custom_env
admin
[step:Conclude that the parametrized family is exactly the solution set]
The second step proved that every pair in the displayed family is an integral solution. The remaining steps proved that every integral solution belongs to that family for some $t\in \mathbb{Z}$. Therefore the integer solutions to $ax+by=c$ are precisely
\begin{align*}
\left(x_0+\frac{b}{d}t,\ y_0-\frac{a}{d}t\right), \qquad t\in \mathbb{Z}.
\end{align*}
This proves the theorem.
[/step]