Proof:Gcd(a,b) is greater than all other common divisors of a and b

From CS2800 wiki
For all [math]a, b, c \href{/cs2800/wiki/index.php/%E2%88%88}{∈} ℕ [/math], if [math]c \href{/cs2800/wiki/index.php/%E2%9D%98}{❘} a [/math] and [math]c \href{/cs2800/wiki/index.php/%E2%9D%98}{❘} b [/math], then [math]c ≤ \href{/cs2800/wiki/index.php/Gcd}{gcd}(a,b) [/math].

In fact, we will prove the following claim, which is stronger:

For all [math]a, b, c \href{/cs2800/wiki/index.php/%E2%88%88}{∈} ℕ [/math], if [math]c \href{/cs2800/wiki/index.php/%E2%9D%98}{❘} a [/math] and [math]c \href{/cs2800/wiki/index.php/%E2%9D%98}{❘} b [/math], then [math]c \href{/cs2800/wiki/index.php/%E2%9D%98}{❘} \href{/cs2800/wiki/index.php/Gcd}{gcd}(a,b) [/math].

This claim is stronger because if c ❘ g then c ≤ g.

Proof: of stronger claim
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, c \href{/cs2800/wiki/index.php/%E2%88%88}{∈} \href{/cs2800/wiki/index.php/%E2%84%95}{ℕ} [/math], if [math]c \href{/cs2800/wiki/index.php/%E2%9D%98}{❘} a [/math] and [math]c \href{/cs2800/wiki/index.php/%E2%9D%98}{❘} b [/math] then [math]c \href{/cs2800/wiki/index.php/%E2%9D%98}{❘} \href{/cs2800/wiki/index.php/Gcd}{gcd}(a,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]P(0) [/math], assume [math]c \href{/cs2800/wiki/index.php/%E2%9D%98}{❘} a [/math] and [math]c \href{/cs2800/wiki/index.php/%E2%9D%98}{❘} 0 [/math]. We want to show that [math]c [/math] divides [math]\href{/cs2800/wiki/index.php/Gcd}{gcd}(a,0) = a [/math]. Well, we have assumed this, so there's nothing to show!

Now, choose an arbitrary [math]b [/math]; we will show [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]. Assume that [math]c \href{/cs2800/wiki/index.php/%E2%9D%98}{❘} a [/math] and [math]c \href{/cs2800/wiki/index.php/%E2%9D%98}{❘} b [/math]. Let [math]g := \href{/cs2800/wiki/index.php/Gcd}{gcd}(a,b) = \href{/cs2800/wiki/index.php/Gcd}{gcd}(b,r) [/math]; we want to show that [math]c \href{/cs2800/wiki/index.php/%E2%9D%98}{❘} g [/math].

Note that 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], so we have assumed [math]P(r) [/math]. We could apply [math]P(r) [/math] to show that [math]c \href{/cs2800/wiki/index.php/%E2%9D%98}{❘} g [/math] if we could show that [math]c \href{/cs2800/wiki/index.php/%E2%9D%98}{❘} b [/math] and [math]c \href{/cs2800/wiki/index.php/%E2%9D%98}{❘} r [/math]. And we're already halfway there: we've already assumed [math]c \href{/cs2800/wiki/index.php/%E2%9D%98}{❘} b [/math]. Thus we just need to show that [math]c \href{/cs2800/wiki/index.php/%E2%9D%98}{❘} r [/math].

Let's take stock of where we are:

  • [math]c \href{/cs2800/wiki/index.php/%E2%9D%98}{❘} a [/math] so there exists [math]s \href{/cs2800/wiki/index.php/%E2%88%88}{∈} ℕ [/math] with [math]sc = a [/math]
  • [math]c \href{/cs2800/wiki/index.php/%E2%9D%98}{❘} b [/math] so there exists [math]t \href{/cs2800/wiki/index.php/%E2%88%88}{∈} ℕ [/math] with [math]tc = b [/math]
  • Since [math]r = \href{/cs2800/wiki/index.php/Rem}{rem}(a,b) [/math] we know that [math]a = qb + r [/math] for some [math]q [/math].
  • We want to show [math]c \href{/cs2800/wiki/index.php/%E2%9D%98}{❘} r [/math], i.e. that there exists [math]k \href{/cs2800/wiki/index.php/%E2%88%88}{∈} \href{/cs2800/wiki/index.php/%E2%84%95}{ℕ} [/math] with [math]r = kc [/math].

Putting the things we know together, we have

[math]r = a - qb = sc - qtc = (s-qt)c [/math]

So choosing [math]k := s-qt [/math] gives [math]r = kc [/math] as required.