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

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-gcd-coprime/)

This is an owner-adopted natural-language teaching guide. Finite/arithmetic checks are not universal proofs; no Lean was run, and review scope is recorded per revision. Original source status labels are retained as historical data. Formulas retain exact TeX; no new semantic AST is invented.

derivation-mko-gcd-coprime-01 · production-20261019-adopted-96



## 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

S01 · definitionBefore

d=\gcd(a,b)

After

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

Conditions: none

Rule: mko_gcd_def · Uses: G1, mko_gcd_def

Leaf basis: mko_gcd_def + def_unfold

By the MKO, the gcd is characterized in two parts: d is a common divisor, and every common divisor divides d. 'Greatest' is expressed by divisibility, not by numerical size. Coprime means gcd=1.



S02 · impliesBefore

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

After

d=d'

Conditions: none

Rule: L_dvd_antisymm · Uses: S01, L_dvd_antisymm

Leaf basis: mko_dvd_def + exists_elim + order_basics

d′ is a common divisor, and the characterization of d says every common divisor divides d, so d′∣d; symmetrically d∣d′. By Lemma L_dvd_antisymm (proved in S02.1 and S02.2), d=d′. So whenever it exists, the gcd is unique and may be called 'the' gcd.



S03 · impliesBefore

(x,0)

After

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

Conditions: none

Rule: dvd_basic · Uses: S01, dvd_basic

Leaf basis: dvd_basic + and_intro_elim

x∣x and x∣0 (dvd_basic), so x is a common divisor; if c∣x and c∣0, then certainly c∣x. So x satisfies the characterization, and by S02 it is gcd(x,0). This includes x=0: 0 satisfies the characterization for (0,0), so the MKO's convention gcd(0,0)=0 agrees with the characterization.



S04 · equivalentBefore

x=yq+r,\ y>0

After

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

Conditions: y>0

Rule: L_cd_step · Uses: mko_dvd_def, L_cd_step

Leaf basis: distributive + order_basics + exists_intro

By Lemma L_cd_step (proved in S04.1 and S04.2), one step of the algorithm does not change the set of common divisors: CD(x,y)=CD(y,r).



S05 · equivalentBefore

x=yq+r,\ y>0

After

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

Conditions: y>0

Rule: set_extensionality · Uses: S01, S04

Leaf basis: set_extensionality + eq_replace

The characterization S01 depends on the inputs only through the set of common divisors: 'd∈CD and every c in CD divides d'. S04 says CD(x,y)=CD(y,r), so the two characterizations are identical. Hence gcd(x,y)=gcd(y, x mod y).



S06 · impliesBefore

(84,36)

After

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

Conditions: 36>0

Rule: division_algorithm · Uses: G2, G3, division_algorithm

Leaf basis: division_algorithm + numeric_evaluation

First step: 36≠0, and 84 divided by 36 gives quotient 2 and remainder 12 (N1, N2), so (84,36) becomes (36,12).



S07 · impliesBefore

(36,12)

After

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

Conditions: 12>0

Rule: division_algorithm · Uses: S06, division_algorithm

Leaf basis: division_algorithm + numeric_evaluation

Second step: 12≠0 and 36=12·3+0 (N3), so (36,12) becomes (12,0). The second entry is 0, so the algorithm stops and outputs 12.



S08 · impliesBefore

\gcd(12,0)=12

After

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

Conditions: none

Rule: logic_chain · Uses: S03, S05, S06, S07

Leaf basis: logic_chain + eq_refl_symm_trans

By S03, 12 is gcd(12,0). S05 applied to the step of S07 (36=12·3+0) shows 12 also satisfies the characterization for (36,12); applied again to the step of S06 (84=36·2+12) it shows 12 satisfies the characterization for (84,36). So gcd(84,36)=12 (N4 is an independent recomputation).



S09 · impliesBefore

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

After

\text{the algorithm stops after finitely many steps}

Conditions: none

Rule: well_ordering · Uses: G2, division_algorithm, well_ordering

Leaf basis: well_ordering + division_algorithm + contradiction

Each step replaces the second entry y by the remainder r with 0≤r<y. If the algorithm never stopped, the second entries would form an infinite strictly decreasing sequence of naturals; its set of values is nonempty but has no least element (every value is followed by a smaller one), contradicting well-ordering. So the algorithm reaches second entry 0 after finitely many steps, at most the initial y of them. Here the second entries 36, 12, 0 decrease strictly.



S10 · impliesBefore

d=12

After

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

Conditions: none

Rule: mko_gcd_def · Uses: S04, S06, S08

Leaf basis: mko_gcd_def + exists_intro + numeric_evaluation

Verify both parts of the characterization directly: 84=12·7 and 36=12·3 (N5, N6), so 12 is a common divisor; for any common divisor c, the ⇒ direction of S04 (x=84, y=36, q=2, r=12) gives c∣12. For example the common divisors 1, 2, 3, 4, 6, 12 of 84 and 36 all divide 12.



S11 · impliesBefore

6\mid 84,\ 6\mid 36

After

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

Conditions: none

Rule: mko_gcd_def · Uses: S01, S10

Leaf basis: mko_gcd_def + order_basics + numeric_evaluation

84=6·14 and 36=6·6, so 6 is a common divisor. But 12 is also a common divisor and 12∤6: in 6=12·k, k=0 gives 0 and k≥1 gives at least 12, neither equal to 6. The second part of the characterization fails, so 6 is not the gcd. This is the misconception the MKO warns about: calling any common divisor the greatest one.



S12 · impliesBefore

(8,15)

After

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

Conditions: none

Rule: division_algorithm · Uses: G2, G3, S03, S05

Leaf basis: division_algorithm + logic_chain + numeric_evaluation

Step by step: 8=15·0+8 →(15,8); 15=8·1+7 →(8,7); 8=7·1+1 →(7,1); 7=1·7+0 →(1,0) (N10 to N13). Every divisor used is positive. By S03, gcd(1,0)=1, and applying S05 backwards step by step, gcd(8,15)=1 (N14 is an independent recomputation). The first step only swaps the order, since 8<15.



S13 · impliesBefore

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

After

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

Conditions: none

Rule: mko_gcd_def · Uses: S12, mko_gcd_def

Leaf basis: mko_gcd_def + exists_intro + numeric_evaluation

By the definition, gcd=1 means coprime. 8 has the divisor 2 (2≠1, 2≠8) and 15 has the divisor 3 (3≠1, 3≠15), so neither is prime. Coprimality is a relation between two numbers and does not require either to be prime (MKO paragraph 2).



S14 · impliesBefore

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

After

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

Conditions: none

Rule: logic_chain · Uses: G2, G3, S03, S05

Leaf basis: logic_chain + dvd_basic + numeric_evaluation

(0,1): 0=1·0+0 →(1,0), gcd=1, so 0 and 1 are coprime. (0,6): 0=6·0+0 →(6,0), gcd=6≠1, not coprime (2 divides both 0 and 6). (0,0): by S03, 0 satisfies the characterization, agreeing with the convention; note that every natural divides 0, so (0,0) has no numerically largest common divisor, and the divisibility characterization is what makes 0 the natural answer.







## Substeps and lemmas

S02.1 · case_splitBefore

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

After

e=0=d

Conditions: d=0

Rule: mul_zero · Uses: mko_dvd_def, mul_zero

Leaf basis: mul_zero + exists_elim

From d∣e and e∣d take witnesses: e=dk and d=el. Case d=0: e=0·k=0=d.



S02.2 · case_splitBefore

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

After

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

Conditions: d>0

Rule: order_basics · Uses: mko_dvd_def, order_basics

Leaf basis: order_basics + mul_assoc + case_analysis + contradiction

Case d>0: substituting gives d=(dk)l=d(kl)=d·1. If kl≠1, then kl<1 or kl>1, and d>0 gives d(kl)<d or d(kl)>d, both contradictions; so kl=1. For naturals k, l with product 1, k≠0; if k≥2 then kl≥2l with l≥1 (since kl≠0), so kl≥2, a contradiction; hence k=1 and e=d·1=d. S02.1 and S02.2 together prove Lemma L_dvd_antisymm.



S04.1 · impliesBefore

y=cu,\ r=cv

After

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

Conditions: none

Rule: distributive · Uses: mko_dvd_def, distributive

Leaf basis: distributive + mul_assoc + exists_intro

(The ⇐ direction) From c∣y and c∣r take witnesses y=cu and r=cv. Then x=yq+r=cuq+cv=c(uq+v), and uq+v is natural, so c∣x; c∣y is given.



S04.2 · impliesBefore

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

After

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

Conditions: y>0

Rule: order_basics · Uses: mko_dvd_def, order_basics

Leaf basis: order_basics + distributive + contradiction + exists_intro

(The ⇒ direction) From c∣x and c∣y take witnesses x=cs and y=cu. Since y>0, c≠0, so c>0. Also cs=x=yq+r≥yq=c(uq); if s<uq then cs<c(uq), a contradiction; so s≥uq and t=s−uq is natural. Then x=c(uq)+ct=yq+ct, and comparing with x=yq+r gives r=ct, so c∣r. S04.1 and S04.2 together prove Lemma L_cd_step.







## 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 divisorThe 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 primesThe 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 firstIn 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)](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-gcd-coprime-01.json)