# 最大公因數與互質：以整除刻畫驗證歐幾里得算法

[← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-gcd-coprime/)

這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。

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



## 目標與範圍

依 MKO 的整除刻畫（d∣a、d∣b，且每個公因數 c 都整除 d）：(1) 證明滿足刻畫的 d 至多一個；(2) 證明歐幾里得算法每一步保持公因數集合且必會停止，並以它算出 gcd(84,36)=12，再直接驗證 12 滿足刻畫；(3) 說明公因數 6 不是 gcd；(4) 算出 gcd(8,15)=1，說明 8 與 15 互質但都不是質數；(5) 處理含 0 的情形 gcd(0,1)=1、gcd(0,6)=6、gcd(0,0)=0。

在包含 0 的自然數中，以整除刻畫定義 gcd（MKO 假設 a1、a2）。歐幾里得算法的正確性由「每步保持公因數集合」與「gcd(x,0)=x」兩個事實推出，停止性由良序原理推出。不處理 Bézout 等式、負整數或多個數的 gcd；不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- division_algorithm
- order_basics
- distributive
- well_ordering
- numeric_evaluation


- G1 — a、b 是自然數，可以為 0（MKO 假設 a1）；整除依 MKO 自然數整除的定義，見證須為自然數。
- G2 — 歐幾里得算法（MKO 段落 0）：當 y≠0 時，把 (x,y) 換成 (y, x mod y)；y=0 時輸出 x。(0,0) 依約定輸出 0。
- G3 — 輸入：(84,36)、(8,15)、(0,1)、(0,6)、(0,0)。


- \gcd(a,b) — 最大公因數（整除刻畫）
- \mathrm{CD}(a,b) — a、b 的公因數集合
- (x,y)\mapsto(y,\,x\bmod y) — 歐幾里得算法的一步（y>0）
- c\mid x — c 整除 x





## 規則與來源


- division_algorithm · prerequisite — 帶餘除法：對整數 a 與正整數 b，存在唯一的整數 q、r 使 a=bq+r 且 0≤r<b。
- order_basics · prerequisite — 實數的序：任兩數恰有 u<v、u=v、u>v 之一；u<v 且 v<w 推出 u<w；u<v 推出 u+w<v+w；u<v 且 w>0 推出 uw<vw；u<v 且 w<0 推出 uw>vw。
- distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。
- well_ordering · prerequisite — 良序原理：ℕ 的每個非空子集都有最小元素。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
- exists_elim · prerequisite — ∃消去：由 ∃x∈D, P(x)，可取一個新名字 a 表示某個滿足 P(a) 的元素；只要最後結論不含 a，就可用 a 推理。
- mul_zero · prerequisite — 乘以零：u·0=0。理由：u·0=u·(0+0)=u·0+u·0，兩邊同減 u·0 得 0=u·0。
- mul_assoc · prerequisite — 乘法結合律：(uv)w=u(vw)。
- case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
- contradiction · prerequisite — 反證法：若假設 ¬P 推出矛盾（某命題與其否定同時成立），則 P 成立。
- and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
- exists_intro · prerequisite — ∃引入：若找到 a∈D 使 P(a) 成立，則 ∃x∈D, P(x)。
- set_extensionality · prerequisite — 集合相等：A=B 當且僅當 A⊆B 且 B⊆A，即兩者有相同元素。
- eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。
- logic_chain · prerequisite — 推論的傳遞：由 P⇒Q 與 Q⇒R 得 P⇒R；⇔ 同理。
- eq_refl_symm_trans · prerequisite — 等號的性質：u=u；若 u=v 則 v=u；若 u=v 且 v=w 則 u=w。
- mko_gcd_def · cited — 自然數 d=gcd(a,b) 由 d∣a、d∣b，且每個同時整除 a、b 的自然數 c 都滿足 c∣d 刻畫。採 gcd(0,0)=0；a、b 互質表示 gcd(a,b)=1。 · mko-gcd-coprime
- mko_dvd_def · cited — 對自然數 a、b，a∣b 當且僅當存在自然數 k 使 b=a·k。 · mko-natural-divisibility
- dvd_basic · prerequisite — 自然數整除的基本事實：a∣a（a=a·1）；a∣0（0=a·0）；a>0 時 a∣b ⇔ b 除以 a 的餘數為 0。
- L_dvd_antisymm · lemma — 對自然數 d、e：若 d∣e 且 e∣d，則 d=e。
- L_cd_step · lemma — 對自然數 x、y、q、r，若 y>0 且 x=yq+r，則每個自然數 c 都有 (c∣x 且 c∣y) ⇔ (c∣y 且 c∣r)。





## 逐步主鏈

S01 · definition操作前

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)

條件：無

規則：mko_gcd_def · 依賴：G1, mko_gcd_def

葉節點依據：mko_gcd_def + def_unfold

依 MKO，gcd 由兩部分刻畫：d 是公因數；每個公因數都整除 d。「最大」是以整除關係表達，不是以數值大小。互質表示 gcd=1。



S02 · implies操作前

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

操作後

d=d'

條件：無

規則：L_dvd_antisymm · 依賴：S01, L_dvd_antisymm

葉節點依據：mko_dvd_def + exists_elim + order_basics

d′ 是公因數，而 d 的刻畫說每個公因數都整除 d，所以 d′∣d；對稱地 d∣d′。依引理 L_dvd_antisymm（S02.1、S02.2 證明），d=d′。所以只要存在，gcd 就唯一，可以稱為「the」gcd。



S03 · implies操作前

(x,0)

操作後

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

條件：無

規則：dvd_basic · 依賴：S01, dvd_basic

葉節點依據：dvd_basic + and_intro_elim

x∣x 且 x∣0（dvd_basic），所以 x 是公因數；若 c∣x 且 c∣0，當然 c∣x。所以 x 滿足刻畫，依 S02 它就是 gcd(x,0)。這包括 x=0：0 滿足 (0,0) 的刻畫，所以 MKO 的約定 gcd(0,0)=0 與刻畫一致。



S04 · equivalent操作前

x=yq+r,\ y>0

操作後

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

條件：y>0

規則：L_cd_step · 依賴：mko_dvd_def, L_cd_step

葉節點依據：distributive + order_basics + exists_intro

依引理 L_cd_step（S04.1、S04.2 證明），算法的一步不改變公因數集合：CD(x,y)=CD(y,r)。



S05 · equivalent操作前

x=yq+r,\ y>0

操作後

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

條件：y>0

規則：set_extensionality · 依賴：S01, S04

葉節點依據：set_extensionality + eq_replace

S01 的刻畫只透過公因數集合依賴輸入：「d∈CD 且 CD 中每個 c 都整除 d」。S04 說 CD(x,y)=CD(y,r)，所以兩個刻畫完全相同。因此 gcd(x,y)=gcd(y, x mod y)。



S06 · implies操作前

(84,36)

操作後

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

條件：36>0

規則：division_algorithm · 依賴：G2, G3, division_algorithm

葉節點依據：division_algorithm + numeric_evaluation

第一步：36≠0，84 除以 36 得商 2、餘數 12（N1、N2），所以 (84,36) 換成 (36,12)。



S07 · implies操作前

(36,12)

操作後

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

條件：12>0

規則：division_algorithm · 依賴：S06, division_algorithm

葉節點依據：division_algorithm + numeric_evaluation

第二步：12≠0，36=12·3+0（N3），所以 (36,12) 換成 (12,0)。第二個數為 0，算法停止，輸出 12。



S08 · implies操作前

\gcd(12,0)=12

操作後

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

條件：無

規則：logic_chain · 依賴：S03, S05, S06, S07

葉節點依據：logic_chain + eq_refl_symm_trans

由 S03，12 是 gcd(12,0)。S05 用於 S07 的一步（36=12·3+0）得 12 也滿足 (36,12) 的刻畫；再用於 S06 的一步（84=36·2+12）得 12 滿足 (84,36) 的刻畫。所以 gcd(84,36)=12（N4 為獨立重算）。



S09 · implies操作前

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

操作後

\text{the algorithm stops after finitely many steps}

條件：無

規則：well_ordering · 依賴：G2, division_algorithm, well_ordering

葉節點依據：well_ordering + division_algorithm + contradiction

每一步把第二個數 y 換成餘數 r，且 0≤r<y。若算法永不停止，第二個數會形成一個無窮嚴格遞減的自然數列；它的值集合非空，卻沒有最小元素（每個值之後都有更小的值），與良序原理矛盾。所以算法必在有限步後到達第二個數為 0，步數不超過起始的 y。本例的第二個數 36、12、0 嚴格遞減。



S10 · implies操作前

d=12

操作後

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

條件：無

規則：mko_gcd_def · 依賴：S04, S06, S08

葉節點依據：mko_gcd_def + exists_intro + numeric_evaluation

直接驗證刻畫的兩部分：84=12·7、36=12·3（N5、N6），所以 12 是公因數；任一公因數 c，依 S04 的 ⇒ 方向（x=84、y=36、q=2、r=12）得 c∣12。例如 84 與 36 的公因數 1、2、3、4、6、12 都整除 12。



S11 · implies操作前

6\mid 84,\ 6\mid 36

操作後

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

條件：無

規則：mko_gcd_def · 依賴：S01, S10

葉節點依據：mko_gcd_def + order_basics + numeric_evaluation

84=6·14、36=6·6，所以 6 是公因數。但 12 也是公因數，而 12∤6：6=12·k 時，k=0 給 0、k≥1 給至少 12，都不是 6。刻畫的第二部分失敗，所以 6 不是 gcd。這正是 MKO 提醒的誤解：把任一共同因數稱為最大公因數。



S12 · implies操作前

(8,15)

操作後

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

條件：無

規則：division_algorithm · 依賴：G2, G3, S03, S05

葉節點依據：division_algorithm + logic_chain + numeric_evaluation

逐步：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 到 N13）。每步除數都大於 0。由 S03，gcd(1,0)=1，再依 S05 逐步回推，gcd(8,15)=1（N14 為獨立重算）。第一步只是交換次序，因為 8<15。



S13 · implies操作前

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

操作後

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

條件：無

規則：mko_gcd_def · 依賴：S12, mko_gcd_def

葉節點依據：mko_gcd_def + exists_intro + numeric_evaluation

依定義，gcd=1 即互質。8 有因數 2（2≠1、2≠8），15 有因數 3（3≠1、3≠15），所以兩者都不是質數。互質是兩數之間的關係，不要求兩數本身是質數（MKO 段落 2）。



S14 · implies操作前

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

操作後

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

條件：無

規則：logic_chain · 依賴：G2, G3, S03, S05

葉節點依據：logic_chain + dvd_basic + numeric_evaluation

(0,1)：0=1·0+0 →(1,0)，gcd=1，所以 0 與 1 互質。(0,6)：0=6·0+0 →(6,0)，gcd=6≠1，不互質（2 同時整除 0 與 6）。(0,0)：由 S03，0 滿足刻畫，與約定一致；注意每個自然數都整除 0，所以 (0,0) 沒有「數值上最大」的公因數，整除刻畫正是讓 0 成為自然答案的方式。







## 局部子步與引理

S02.1 · case_split操作前

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

操作後

e=0=d

條件：d=0

規則：mul_zero · 依賴：mko_dvd_def, mul_zero

葉節點依據：mul_zero + exists_elim

由 d∣e 與 e∣d 取見證：e=dk、d=el。情況 d=0：e=0·k=0=d。



S02.2 · case_split操作前

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

操作後

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

條件：d>0

規則：order_basics · 依賴：mko_dvd_def, order_basics

葉節點依據：order_basics + mul_assoc + case_analysis + contradiction

情況 d>0：代入得 d=(dk)l=d(kl)=d·1。若 kl≠1，則 kl<1 或 kl>1，因 d>0 分別得 d(kl)<d 或 d(kl)>d，都矛盾；所以 kl=1。自然數 k、l 的積為 1，則 k≠0；若 k≥2，則 kl≥2l，而 l≥1（因 kl≠0），得 kl≥2，矛盾；故 k=1，e=d·1=d。S02.1 與 S02.2 合起來證得引理 L_dvd_antisymm。



S04.1 · implies操作前

y=cu,\ r=cv

操作後

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

條件：無

規則：distributive · 依賴：mko_dvd_def, distributive

葉節點依據：distributive + mul_assoc + exists_intro

（⇐ 方向）由 c∣y、c∣r 取見證 y=cu、r=cv。則 x=yq+r=cuq+cv=c(uq+v)，uq+v 是自然數，所以 c∣x；而 c∣y 已知。



S04.2 · implies操作前

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

操作後

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

條件：y>0

規則：order_basics · 依賴：mko_dvd_def, order_basics

葉節點依據：order_basics + distributive + contradiction + exists_intro

（⇒ 方向）由 c∣x、c∣y 取見證 x=cs、y=cu。因 y>0，c≠0，即 c>0。又 cs=x=yq+r≥yq=c(uq)；若 s<uq，則 cs<c(uq)，矛盾；所以 s≥uq，t=s−uq 是自然數。於是 x=c(uq)+ct=yq+ct，與 x=yq+r 比較得 r=ct，所以 c∣r。S04.1 與 S04.2 合起來證得引理 L_cd_step。







## 逐步反向審查


- S14 · premise_audit · S03, S05, dvd_basic — (0,1) 與 (0,6) 用算法一步加 S03、S05；(0,0) 直接用 S03。
- S13 · premise_audit · S12, mko_gcd_def — 只用互質的定義與兩個非平凡因數見證。
- S12 · premise_audit · S03, S05, division_algorithm — 與 S06 到 S08 相同的結構；每一步的餘數都滿足 0≤r<y。
- S11 · premise_audit · S01, S10, order_basics — 否定只需一個不整除 6 的公因數（12）。
- S10 · premise_audit · S04, S06, mko_gcd_def — 第二部分是對所有公因數的一般論證，不是只看列出的六個；列出的只是例子。
- S09 · premise_audit · division_algorithm, well_ordering, contradiction — 停止性只需 r<y 與良序原理；它保證 S08 的回推從有限的終點開始。
- S08 · premise_audit · S03, S05, S06, S07, logic_chain — 從算法終點往回套用 S05；每一步的前提 y>0 都已確認（36>0、12>0）。
- S07 · premise_audit · division_algorithm, numeric_evaluation — 餘數 0 滿足 0≤0<12。
- S06 · premise_audit · division_algorithm, numeric_evaluation — 需要 0≤12<36，這使 12 是唯一的餘數。
- S05 · inverse_equivalence · S04, set_extensionality — 集合相等是雙向的，所以刻畫的等價也是雙向的。
- S04.2 · premise_audit · order_basics, distributive, contradiction — 自然數減法 s−uq 只有在 s≥uq 時才是自然數，所以先證 s≥uq；這需要 c>0，由 y>0 保證。沒有使用引理本身。
- S04.1 · premise_audit · distributive, mul_assoc, exists_intro — 只用分配律與 ℕ 對加法、乘法封閉；沒有使用引理本身。
- S04 · inverse_equivalence · L_cd_step — 引理的兩個方向分別在 S04.1、S04.2 證明。
- S03 · premise_audit · S01, S02, dvd_basic — 兩部分刻畫都已檢查；唯一性來自 S02。
- S02.2 · premise_audit · order_basics, mul_assoc, case_analysis — 兩種情況 d=0、d>0 涵蓋所有自然數 d；沒有使用引理本身。
- S02.1 · premise_audit · mko_dvd_def, mul_zero — 只用乘以零；沒有使用引理本身。
- S02 · premise_audit · S01, L_dvd_antisymm — 只用兩個候選各自的刻畫；存在性另由算法給出（S08）。
- S01 · premise_audit · G1, mko_gcd_def — 此步只展開定義；驗證候選 d 時兩部分都要檢查（MKO 段落 1）。





## 錯誤控制與反例

公因數不一定是最大公因數MKO 指出的誤解：把任何共同因數稱為最大公因數。6 同時整除 84 與 36，但公因數 12 不整除 6，刻畫第二部分失敗（S11）。驗證候選時必須檢查所有公因數都整除它，只找到一個大的公因數不夠。

互質不要求兩數是質數MKO 指出的另一個誤解：以為互質的兩數都必須是質數。8 與 15 都不是質數，卻互質；0 與 1 也互質（S13、S14）。

自然數減法要先確認不為負S04.2 中 r=c(s−uq) 必須先證 s≥uq，s−uq 才是自然數，見證才合法；這一步用到 c>0，而 c>0 來自 y>0。


- 6 是 84 與 36 的最大公因數，因為 6 同時整除兩者 → reject — 公因數 12 不整除 6；gcd(84,36)=12。
- 8 與 15 不互質，因為兩者都不是質數 → reject — gcd(8,15)=1，所以互質。
- 0 與 6 互質 → reject — gcd(0,6)=6≠1；2 同時整除 0 與 6。
- gcd(0,0) 不存在，因為每個數都整除 0 → reject — 依整除刻畫，0 是公因數且每個公因數都整除 0，所以 gcd(0,0)=0，與 MKO 約定一致。





## 結論與限制

滿足整除刻畫的 gcd 至多一個；歐幾里得算法每步保持公因數集合且必停止。gcd(84,36)=12（84→36→12→0），12 直接滿足刻畫；公因數 6 不是 gcd，因為 12∤6。gcd(8,15)=1，所以 8 與 15 互質，雖然兩者都不是質數。gcd(0,1)=1（互質）、gcd(0,6)=6（不互質）、gcd(0,0)=0（與刻畫一致）。


- Bézout 等式（gcd 可寫成兩數的整數線性組合）不在本稿處理。
- dvd_basic 與帶餘除法作為前置規則使用；前者的證明見自然數整除的教學稿，本稿不重證。





## 驗證及來源綁定

19 個本稿宣告算術檢查；只支持所列算式。


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

[同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-gcd-coprime-01.json)