Greatest common divisor and coprimality: checking Euclid's algorithm against the divisibility characterization

Goal and scope

From the MKO's divisibility characterization (d∣a, d∣b, and every common divisor c divides d): (1) prove that at most one d satisfies it; (2) prove that each step of Euclid's algorithm preserves the set of common divisors and that the algorithm stops, use it to compute gcd(84,36)=12, and verify directly that 12 satisfies the characterization; (3) explain why the common divisor 6 is not the gcd; (4) compute gcd(8,15)=1 and explain that 8 and 15 are coprime although neither is prime; (5) treat the zero cases gcd(0,1)=1, gcd(0,6)=6 and gcd(0,0)=0.

Defines the gcd by the divisibility characterization in the naturals including 0 (MKO assumptions a1 and a2). Correctness of Euclid's algorithm is derived from two facts, 'each step preserves the set of common divisors' and 'gcd(x,0)=x', and termination from well-ordering. Bézout's identity, negative integers and gcds of more than two numbers are not treated; the canonical MKO and its English edition are not changed.

Givens and symbols

• division_algorithm
• order_basics
• distributive
• well_ordering
• numeric_evaluation

• G1 — a and b are natural numbers and may be 0 (MKO assumption a1); divisibility follows the natural-divisibility MKO, with natural witnesses.
• G2 — Euclid's algorithm (MKO paragraph 0): while y≠0, replace (x,y) by (y, x mod y); when y=0, output x. For (0,0) the convention outputs 0.
• G3 — Inputs: (84,36), (8,15), (0,1), (0,6), (0,0).

• \gcd(a,b) — greatest common divisor (divisibility characterization)
• \mathrm{CD}(a,b) — the set of common divisors of a and b
• (x,y)\mapsto(y,\,x\bmod y) — one step of Euclid's algorithm (y>0)
• c\mid x — c divides x

Rules and sources

• division_algorithm · prerequisite — Division algorithm: for an integer a and a positive integer b there are unique integers q, r with a=bq+r and 0≤r<b.
• order_basics · prerequisite — Order of the reals: exactly one of u<v, u=v, u>v holds; u<v and v<w give u<w; u<v gives u+w<v+w; u<v and w>0 give uw<vw; u<v and w<0 give uw>vw.
• distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu.
• well_ordering · prerequisite — Well-ordering principle: every nonempty subset of ℕ has a least element.
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• def_unfold · prerequisite — Unfolding a definition: replacing a defined term by its definition (or folding it back) does not change whether a statement is true.
• exists_elim · prerequisite — ∃-elimination: from ∃x∈D, P(x) we may name some element a with P(a) by a fresh name; reasoning with a is allowed as long as the final conclusion does not mention a.
• mul_zero · prerequisite — Multiplying by zero: u·0=0. Reason: u·0=u·(0+0)=u·0+u·0; subtracting u·0 from both sides gives 0=u·0.
• mul_assoc · prerequisite — Associativity of multiplication: (uv)w=u(vw).
• case_analysis · prerequisite — Proof by cases: if P∨Q holds and both P⇒R and Q⇒R are proved, then R holds. The cases must cover every possibility.
• contradiction · prerequisite — Proof by contradiction: if assuming ¬P leads to a contradiction (a statement and its negation both hold), then P holds.
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• exists_intro · prerequisite — ∃-introduction: if some a∈D satisfies P(a), then ∃x∈D, P(x).
• set_extensionality · prerequisite — Set equality: A=B if and only if A⊆B and B⊆A, i.e. they have the same elements.
• eq_replace · prerequisite — Replacement of equals: an expression inside a statement may be replaced by an equal expression without changing whether the statement is true.
• logic_chain · prerequisite — Chaining: from P⇒Q and Q⇒R infer P⇒R; likewise for ⇔.
• eq_refl_symm_trans · prerequisite — Properties of equality: u=u; if u=v then v=u; if u=v and v=w then u=w.
• mko_gcd_def · cited — The natural number d=gcd(a,b) is characterized by d∣a and d∣b, with c∣d for every natural c that divides both a and b. Adopt gcd(0,0)=0. The inputs a and b are coprime exactly when gcd(a,b)=1. · mko-gcd-coprime
• mko_dvd_def · cited — For natural numbers a and b, a∣b exactly when there is a natural number k such that b=a·k. · mko-natural-divisibility
• dvd_basic · prerequisite — Basic facts of natural divisibility: a∣a (a=a·1); a∣0 (0=a·0); for a>0, a∣b ⇔ b leaves remainder 0 on division by a.
• L_dvd_antisymm · lemma — For naturals d and e: if d∣e and e∣d, then d=e.
• L_cd_step · lemma — For naturals x, y, q, r with y>0 and x=yq+r, every natural c satisfies (c∣x and c∣y) ⇔ (c∣y and c∣r).

Main derivation

d=\gcd(a,b)

d\mid a\ \land\ d\mid b\ \land\ \forall c\in\mathbb{N}\,(c\mid a\land c\mid b\Rightarrow c\mid d)

d,\ d'\ \text{both satisfy S01 for}\ (a,b)

d=d'

(x,0)

x\ \text{satisfies S01 for}\ (x,0),\ \text{so}\ \gcd(x,0)=x

x=yq+r,\ y>0

c\mid x\land c\mid y\iff c\mid y\land c\mid r

x=yq+r,\ y>0

d\ \text{satisfies S01 for}\ (x,y)\iff d\ \text{satisfies S01 for}\ (y,r)

(84,36)

84=36\cdot 2+12,\ 0\le 12<36;\ (84,36)\mapsto(36,12)

(36,12)

36=12\cdot 3+0;\ (36,12)\mapsto(12,0)

\gcd(12,0)=12

\gcd(84,36)=\gcd(36,12)=\gcd(12,0)=12

(x,y)\mapsto(y,\,x\bmod y),\ y>0

\text{the algorithm stops after finitely many steps}

d=12

12\mid 84,\ 12\mid 36,\ (c\mid 84\land c\mid 36\Rightarrow c\mid 12)

6\mid 84,\ 6\mid 36

12\nmid 6,\ \text{so}\ 6\neq\gcd(84,36)

(8,15)

(8,15)\mapsto(15,8)\mapsto(8,7)\mapsto(7,1)\mapsto(1,0);\ \gcd(8,15)=1

\gcd(8,15)=1,\ 8=2\cdot 4,\ 15=3\cdot 5

8,15\ \text{coprime, neither prime}

(0,1),\ (0,6),\ (0,0)

\gcd(0,1)=1,\ \gcd(0,6)=6,\ \gcd(0,0)=0

Substeps and lemmas

e=dk,\ d=el,\ d=0

e=0=d

d=el=d(kl),\ d>0

kl=1,\ k=1,\ e=d

y=cu,\ r=cv

x=c(uq+v),\ \text{so}\ c\mid x

x=cs,\ y=cu,\ y>0

r=c(s-uq),\ s-uq\in\mathbb{N},\ \text{so}\ c\mid r

Reverse audits

• S14 · premise_audit · S03, S05, dvd_basic — (0,1) and (0,6) use one algorithm step with S03 and S05; (0,0) uses S03 directly.
• S13 · premise_audit · S12, mko_gcd_def — Only the definition of coprime and two nontrivial divisor witnesses are used.
• S12 · premise_audit · S03, S05, division_algorithm — The same structure as S06 to S08; each remainder satisfies 0≤r<y.
• S11 · premise_audit · S01, S10, order_basics — Refutation needs only one common divisor that does not divide 6 (namely 12).
• S10 · premise_audit · S04, S06, mko_gcd_def — The second part is a general argument for every common divisor, not just the six listed; the list is only an illustration.
• S09 · premise_audit · division_algorithm, well_ordering, contradiction — Termination needs only r<y and well-ordering; it ensures that the backward argument of S08 starts from a finite end point.
• S08 · premise_audit · S03, S05, S06, S07, logic_chain — S05 is applied backwards from the end of the run; each step's premise y>0 was confirmed (36>0, 12>0).
• S07 · premise_audit · division_algorithm, numeric_evaluation — The remainder 0 satisfies 0≤0<12.
• S06 · premise_audit · division_algorithm, numeric_evaluation — It needs 0≤12<36, which makes 12 the unique remainder.
• S05 · inverse_equivalence · S04, set_extensionality — Equality of sets is two-way, so the equivalence of the characterizations is two-way.
• S04.2 · premise_audit · order_basics, distributive, contradiction — The natural subtraction s−uq is natural only when s≥uq, so s≥uq is proved first; this needs c>0, which y>0 guarantees. The lemma itself is not used.
• S04.1 · premise_audit · distributive, mul_assoc, exists_intro — Only distributivity and closure of ℕ under addition and multiplication are used; the lemma itself is not used.
• S04 · inverse_equivalence · L_cd_step — The two directions of the lemma are proved in S04.1 and S04.2.
• S03 · premise_audit · S01, S02, dvd_basic — Both parts of the characterization are checked; uniqueness comes from S02.
• S02.2 · premise_audit · order_basics, mul_assoc, case_analysis — The cases d=0 and d>0 cover every natural d; the lemma itself is not used.
• S02.1 · premise_audit · mko_dvd_def, mul_zero — Only multiplication by zero is used; the lemma itself is not used.
• S02 · premise_audit · S01, L_dvd_antisymm — Only the characterizations of the two candidates are used; existence comes separately from the algorithm (S08).
• S01 · premise_audit · G1, mko_gcd_def — This step only unfolds the definition; checking a candidate d requires both parts (MKO paragraph 1).

Error controls and negative controls

A common divisor need not be the greatest common divisor

The misconception the MKO names: calling any common divisor the greatest one. 6 divides both 84 and 36, but the common divisor 12 does not divide 6, so the second part of the characterization fails (S11). Checking a candidate requires that every common divisor divide it; finding one large common divisor is not enough.

Coprime does not require primes

The other misconception the MKO names: thinking that coprime numbers must both be prime. 8 and 15 are not prime yet coprime; 0 and 1 are coprime too (S13, S14).

Justify natural subtraction first

In S04.2, r=c(s−uq) requires first proving s≥uq so that s−uq is natural and the witness is legitimate; this uses c>0, which comes from y>0.

• 6 is the greatest common divisor of 84 and 36 because it divides both → reject — The common divisor 12 does not divide 6; gcd(84,36)=12.
• 8 and 15 are not coprime because neither is prime → reject — gcd(8,15)=1, so they are coprime.
• 0 and 6 are coprime → reject — gcd(0,6)=6≠1; 2 divides both 0 and 6.
• gcd(0,0) does not exist because every number divides 0 → reject — Under the divisibility characterization, 0 is a common divisor and every common divisor divides 0, so gcd(0,0)=0, in agreement with the MKO's convention.

Result and limitations

At most one d satisfies the divisibility characterization; each step of Euclid's algorithm preserves the set of common divisors and the algorithm stops. gcd(84,36)=12 (84→36→12→0), and 12 satisfies the characterization directly; the common divisor 6 is not the gcd because 12∤6. gcd(8,15)=1, so 8 and 15 are coprime although neither is prime. gcd(0,1)=1 (coprime), gcd(0,6)=6 (not coprime), gcd(0,0)=0 (consistent with the characterization).

• Bézout's identity (the gcd as an integer linear combination of the inputs) is not treated here.
• dvd_basic and the division algorithm are used as prerequisites; the former is proved in the natural-divisibility guide and not re-proved here.

Verification and source binding

19 declared checks for this guide; only the listed expressions are covered.

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: f39e3c663a8c3440ba12db2b5c23ca110fbd1985af55bf32133cce444b5f2c07
• original source SHA-256: f39e3c663a8c3440ba12db2b5c23ca110fbd1985af55bf32133cce444b5f2c07
• Lean: NOT_RUN · independent AI: NOT_MEASURED

Same-source full JSON (formulas, ASTs, controls and revision log)