Greatest common divisor is the smallest positive number that can be written as $sa+tb$
Solution 1:
A conceptual proof of Bezout's gcd Identity: the set $\rm\,S\,$ of all integers of form $\rm\,a\,x + b\,y,\,\ x,y\in \mathbb Z,\,$ is closed under subtraction $\ ax+by-(a\bar x+b\bar y)\, =\, a(x\!-\bar x)+b(y\!-\!\bar y),\, $ so via Lemma below, every positive $\rm\,n\in S\,$ is divisible by $\rm\,d = $ least positive $\rm\in S.\,$ So $\rm\,a,b\in S\,$ $\Rightarrow$ $\rm\,d\mid a,b,\,$ i.e. $\rm\,d\,$ is a common divisor of $\rm\,a,b,\,$ necessarily greatest such by $\rm\ c\mid a,b\,$ $\Rightarrow$ $\rm\,c\mid d = a\,x_1\!+\! b\,y_1\Rightarrow$ $\rm\,c\le d.$
Lemma $\ \ $ Let $\,\rm S\ne\emptyset \,$ be a set of integers $>0$ closed under subtraction $> 0,\,$ i.e. for all $\rm\,n,m\in S, \,$ $\rm\ n > m\ \Rightarrow\ n-m\, \in\, S.\,$ Then every element of $\rm\,S\,$ is a multiple of the least element $\rm\:\ell = \min\, S.$
Proof ${\bf\ 1}\,\ $ If not there is a least nonmultiple $\rm\,n\in S,\,$ contra $\rm\,n-\ell \in S\,$ is a nonmultiple of $\rm\,\ell.$
Proof ${\bf\ 2}\,\rm\,\ \ S\,$ closed under subtraction $\rm\,\Rightarrow\,S\,$ closed under remainder (mod), when it is $\ne 0,$ since mod is computable by repeated subtraction, i.e. $\rm\, a\ mod\ b\, =\, a - k b\, =\, a-b-b-\cdots -b.\,$ Thus $\rm\,n\in S\,$ $\Rightarrow$ $\rm\, (n\ mod\ \ell) = 0,\,$ else it is $\rm\,\in S\,$ and smaller than $\rm\,\ell,\,$ contra mimimality of $\rm\:\ell.$
Remark $\ $ In a nutshell, two applications of induction yield the following inferences
$ \rm\begin{eqnarray}\rm S\ closed\ under\ {\bf subtraction} &\Rightarrow\:&\rm S\ closed\ under\ {\bf mod} = remainder = repeated\ subtraction \\ &\Rightarrow\:&\rm S\ closed\ under\,\ {\bf gcd}\, = repeated\ mod\ (Euclid's\ algorithm) \end{eqnarray}$
Interpreted constructively, this yields the extended Euclidean algorithm for the gcd. Namely, $ $ starting from the two elements of $\rm\,S\,$ that we know: $\rm\ a \,=\, 1\cdot a + 0\cdot b,\ \ b \,=\, 0\cdot a + 1\cdot b,\ $ we search for the least element of $\rm\,S\,$ by repeatedly subtracting elements of $\,\rm S\,$ to produce smaller elements of $\rm\,S\,$ (while keeping track of each elements linear representation in terms of $\rm\,a\,$ and $\rm\,b).\:$ This is essentially the subtractive form of the Euclidean algorithm (vs. mod/remainder form).
Note: in more general numbers systems enjoying Division with Remainder (i.e. Euclidean domains) it is not true that $\!\bmod\!$ is equivalent to repeated subtraction, so in such rings the above descent is achieved by $\!\bmod\!$ (vs. subtraction), as in Proof $2,\,$ e.g. this is true for polynomial rings over a field.
The conceptual structure will be clarified when one studies ideals of rings, where the above proof generalizes to show that Euclidean domains are PIDs.
Beware $ $ This linear representation of the the gcd need not hold true in all domains where gcds exist, e.g. in the domain $\rm\:D = \mathbb Q[x,y]\:$ of polynomials in $\rm\:x,y\:$ with rational coefficients we have $\rm\:gcd(x,y) = 1\:$ but there are no $\rm\:f(x,y),\: g(x,y)\in D\:$ such that $\rm\:x\:f(x,y) + y\:g(x,y) = 1;\:$ indeed, if so, then evaluating at $\rm\:x = 0 = y\:$ yields $\:0 = 1.$
Solution 2:
I think I've figured it out.
Suppose $\gcd(a, b) = m$ where $m \geq d$. By Bezout's identity $m$ can be written as $va + ub$.
Clearly $m | d$, implying $m \leq d$ since $m$, $d \geq 0$. Thus $m = d$.