Proof:Gcd(a,b) is a common divisor of a and b

From CS2800 wiki
Definition: gcd
Euclid's GCD algorithm is the function [math]\href{/cs2800/wiki/index.php/Gcd}{gcd} : \href{/cs2800/wiki/index.php/%E2%84%95}{ℕ} \href{/cs2800/wiki/index.php/%C3%97}{×} \href{/cs2800/wiki/index.php/%E2%84%95}{ℕ} \href{/cs2800/wiki/index.php/%E2%86%92}{→} \href{/cs2800/wiki/index.php/%E2%84%95}{ℕ} [/math] which is given as follows: [math]\href{/cs2800/wiki/index.php/Gcd}{gcd}(a,0) := a [/math], and for [math]b \gt 0 [/math], [math]\href{/cs2800/wiki/index.php/Gcd}{gcd}(a,b) = \href{/cs2800/wiki/index.php?title=G&action=edit&redlink=1}{g}(b,r) [/math] where [math]r = \href{/cs2800/wiki/index.php/Rem}{rem}(a,b) [/math].

This function is a good inductively defined function because by definition, [math]\href{/cs2800/wiki/index.php/Rem}{rem}(a,b) \lt b [/math], so the second argument is decreasing in the inductive definition.

The algorithm can be extended to operate on negative integers by simply taking the gcd of the absolute values of its arguments.

For all [math]a, b ∈ ℕ [/math], [math]\href{/cs2800/wiki/index.php/Gcd}{gcd}(a,b) \href{/cs2800/wiki/index.php/%E2%9D%98}{❘} a [/math] and [math]\href{/cs2800/wiki/index.php/Gcd}{gcd}(a,b) \href{/cs2800/wiki/index.php/%E2%9D%98}{❘} b [/math]
We will do this proof by induction. Since the inductive principle used to define [math]\href{/cs2800/wiki/index.php/Gcd}{gcd} [/math] uses strong induction on the second argument, we will use the same inductive principle for the proof. Let [math]\href{/cs2800/wiki/index.php?title=P&action=edit&redlink=1}{P}(b) [/math] be the statement "for all [math]a \href{/cs2800/wiki/index.php/%E2%88%88}{∈} \href{/cs2800/wiki/index.php/%E2%84%95}{ℕ} [/math], [math]\href{/cs2800/wiki/index.php/Gcd}{gcd}(a,b) \href{/cs2800/wiki/index.php/%5Cmid}{\mid} a [/math] and [math]\href{/cs2800/wiki/index.php/Gcd}{gcd}(a,b) \href{/cs2800/wiki/index.php/%E2%9D%98}{❘} b [/math]". We will prove [math]P(0) [/math] and [math]P(b) [/math] assuming [math]\href{/cs2800/wiki/index.php?title=P&action=edit&redlink=1}{P}(k) [/math] for all [math]k \lt b [/math].

To see [math]\href{/cs2800/wiki/index.php?title=P&action=edit&redlink=1}{P}(0) [/math], we want to show that [math]\href{/cs2800/wiki/index.php/Gcd}{gcd}(a,0) \href{/cs2800/wiki/index.php/%E2%9D%98}{❘} a [/math] and [math]\href{/cs2800/wiki/index.php/Gcd}{gcd}(a,0) \href{/cs2800/wiki/index.php/%E2%9D%98}{❘} 0 [/math]. Note that by definition, [math]\href{/cs2800/wiki/index.php/Gcd}{gcd}(a,0) = a [/math]. [math]a \href{/cs2800/wiki/index.php/%E2%9D%98}{❘} a [/math] because [math]1 \cdot a = a [/math], and [math]a \href{/cs2800/wiki/index.php/%E2%9D%98}{❘} 0 [/math] because [math]0 \cdot a = 0 [/math].

Now, to see [math]\href{/cs2800/wiki/index.php?title=P&action=edit&redlink=1}{P}(b) [/math], assume [math]\href{/cs2800/wiki/index.php?title=P&action=edit&redlink=1}{P}(k) [/math] for all [math]k \lt b [/math]. To save some writing, let's define [math]g \href{/cs2800/wiki/index.php/Definition}{:=} \href{/cs2800/wiki/index.php/Gcd}{gcd}(a,b) [/math], by definition, we have [math]g = \href{/cs2800/wiki/index.php/Gcd}{gcd}(b,r) [/math] (for simplicity, let's call this number [math]g [/math]); thus we want to show that [math]g \href{/cs2800/wiki/index.php/%E2%9D%98}{❘} a [/math] and [math]g \href{/cs2800/wiki/index.php/%E2%9D%98}{❘} b [/math].

Now, since [math]r = \href{/cs2800/wiki/index.php?title=Rem(a,b)&action=edit&redlink=1}{rem(a,b)} [/math], we know [math]r \lt b [/math]. Thus we can apply [math]P(r) [/math] (with [math]b [/math] plugged in for [math]a [/math]), to conclude that [math]g \href{/cs2800/wiki/index.php/%E2%9D%98}{❘} b [/math] and [math]g \href{/cs2800/wiki/index.php/%E2%9D%98}{❘} r [/math]. This gives us one of the two things we need to prove, so all that's left is to show that [math]g \href{/cs2800/wiki/index.php/%E2%9D%98}{❘} a [/math].

Let's take stock of where we are:

  • Since [math]g \href{/cs2800/wiki/index.php/%E2%9D%98}{❘} b [/math] we have [math]sg = b [/math] for some [math]s [/math].
  • We also have [math]tg = r [/math] for some [math]t [/math] since [math]g \href{/cs2800/wiki/index.php/%E2%9D%98}{❘} r [/math].
  • We also know [math]a = qb + r [/math] for some [math]q [/math] since [math]r = \href{/cs2800/wiki/index.php/Rem}{rem}(a,b) [/math].
  • We want to show that there exists [math]c \href{/cs2800/wiki/index.php/%E2%88%88}{∈} \href{/cs2800/wiki/index.php/%E2%84%95}{ℕ} [/math] with [math]a = cg [/math].

Combining these equations, we have

[math]a = qb + r = qsg + tg = (qs + t)g [/math]

Thus, choosing [math]c = (qs + t) [/math] shows [math]a = cg [/math] as required.