# 自然數整除：以乘數見證判定、處理 0 的情形並證明遞移性

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

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

derivation-mko-natural-divisibility-01 · production-20261019-adopted-96



## 目標與範圍

依 MKO 定義（a∣b ⇔ 存在自然數 k 使 b=a·k）：(1) 證明 6∣84；(2) 證明 6∤87；(3) 證明 4∤10，雖然 10/4=5/2 是一個數；(4) 證明每個 a 都整除 0；(5) 證明 0∣b ⇔ b=0，並說明 0∣0 的見證不唯一、0∤5；(6) 證明 a>0 時見證至多一個（若 a∣b，則既有見證唯一）；(7) 證明整除的自反性與遞移性，並由 3∣6、6∣84 求出 3∣84 的見證。

只在包含 0 的自然數中工作（MKO 假設 a1），見證必須是自然數（a2）。為判定 a>0 的情形，本稿由帶餘除法（引用的前置規則）證明「a∣b ⇔ 餘數為 0」。不處理負整數的整除、最大公因數或質數；不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- division_algorithm
- order_basics
- mul_zero
- mul_assoc
- numeric_evaluation


- G1 — ℕ 包含 0；乘法是自然數乘法，自然數的和與積仍是自然數（MKO 假設 a1）。
- G2 — 整除的見證 k 必須是自然數；非整數的商不是見證（MKO 假設 a2）。
- G3 — 要判定的數對：(6,84)、(6,87)、(4,10)、(3,6)、(0,0)、(0,5)。


- a\mid b — a 整除 b
- a\nmid b — a 不整除 b
- k — 乘數見證，必須是自然數
- b\bmod a — b 除以 a（a>0）的餘數
- \mathbb{N} — 自然數，包含 0





## 規則與來源


- 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。
- 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)。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
- exists_intro · prerequisite — ∃引入：若找到 a∈D 使 P(a) 成立，則 ∃x∈D, P(x)。
- contradiction · prerequisite — 反證法：若假設 ¬P 推出矛盾（某命題與其否定同時成立），則 P 成立。
- add_zero · prerequisite — 加法單位元：u+0=u。
- mul_inverse_nonzero · prerequisite — 非零數的倒數：在 ℚ、ℝ、ℂ 中，若 u≠0，存在 1/u 使 u·(1/u)=1；對 u≠0 定義 v/u 為 v·(1/u)。u=0 時沒有倒數，v/0 不定義。
- frac_rules · prerequisite — 分數運算（分母皆非零）：a/c+b/c=(a+b)/c；(a/b)(c/d)=(ac)/(bd)；(a/b)/(c/d)=(ad)/(bc)（另需 c≠0）；a/b=(ak)/(bk)（k≠0）。
- forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
- mul_comm · prerequisite — 乘法交換律：uv=vu（在交換的數系中，例如 ℤ、ℚ、ℝ、ℂ）。
- case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
- mul_one · prerequisite — 乘法單位元：1·u=u。
- exists_elim · prerequisite — ∃消去：由 ∃x∈D, P(x)，可取一個新名字 a 表示某個滿足 P(a) 的元素；只要最後結論不含 a，就可用 a 推理。
- eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。
- forall_elim · prerequisite — ∀消去（代入特例）：若 ∀x∈D, P(x) 成立且 a∈D，則 P(a) 成立。
- mko_dvd_def · cited — 對自然數 a、b，a∣b 當且僅當存在自然數 k 使 b=a·k。 · mko-natural-divisibility
- nat_discrete · prerequisite — 自然數沒有中間值：對自然數 k 與 n，必有 k≤n 或 k≥n+1。
- L_rem_test · lemma — 對自然數 b 與正自然數 a：a∣b ⇔ b 除以 a 的餘數 r 為 0。





## 逐步主鏈

S01 · definition操作前

a\mid b

操作後

\exists k\in\mathbb{N}:\ b=a\cdot k

條件：a,b\in\mathbb{N}

規則：mko_dvd_def · 依賴：G1, G2, mko_dvd_def

葉節點依據：mko_dvd_def + def_unfold

依 MKO 的定義，a∣b 的意思是存在一個自然數 k（乘數見證）使 b=a·k。要證 a∣b，就要給出這樣的 k；要證 a∤b，就要說明沒有任何自然數 k 能做到。



S02 · implies操作前

84=6\cdot 14,\ 14\in\mathbb{N}

操作後

6\mid 84

條件：無

規則：exists_intro · 依賴：S01, G3

葉節點依據：exists_intro + numeric_evaluation

6·14=84（N1），且 14 是自然數，所以 k=14 是見證，6∣84。



S03 · equivalent操作前

a\mid b\quad(a>0)

操作後

b\bmod a=0

條件：a>0

規則：L_rem_test · 依賴：S01, L_rem_test

葉節點依據：division_algorithm + exists_intro + order_basics

a>0 時，整除可以用餘數判定：依引理 L_rem_test（S03.1 到 S03.3 證明），a∣b 恰好當 b 除以 a 的餘數為 0。這把「找見證」換成一次可重算的帶餘除法。



S04 · implies操作前

87=6\cdot 14+3,\ 0\le 3<6

操作後

6\nmid 87

條件：6>0

規則：L_rem_test · 依賴：S03, G3

葉節點依據：division_algorithm + nat_discrete + order_basics + numeric_evaluation

87 除以 6 的餘數是 3≠0（N2、N3），依 S03 的等價，6∤87。直接核對也一致：6·14=84<87<90=6·15，而每個自然數 k 都有 k≤14（則 6k≤84）或 k≥15（則 6k≥90），所以沒有 k 使 6k=87。在有理數中 87/6=29/2=14.5，不是自然數。



S05 · implies操作前

10=4k,\ k\in\mathbb{N}\ ?

操作後

4\nmid 10

條件：4\neq 0

規則：mul_inverse_nonzero · 依賴：S01, S03, G2

葉節點依據：mul_inverse_nonzero + frac_rules + numeric_evaluation

在有理數中 4k=10 唯一的解是 k=10/4=5/2（4≠0，可除）。5/2 不是自然數，依 G2 不能當見證，所以沒有自然數見證，4∤10。用 S03 核對：10=4·2+2，餘數 2≠0，結論相同。



S06 · implies操作前

a\in\mathbb{N}

操作後

0=a\cdot 0,\ \text{so}\ a\mid 0

條件：無

規則：exists_intro · 依賴：S01, mul_zero

葉節點依據：mul_zero + exists_intro + forall_intro

對任意自然數 a，a·0=0，而 0 是自然數，所以 k=0 是見證，a∣0。a 是任意的，包括 a=0。



S07 · equivalent操作前

0\mid b

操作後

b=0

條件：無

規則：mul_zero · 依賴：S01, mul_zero

葉節點依據：mul_zero + mul_comm + exists_intro

0∣b 表示存在自然數 k 使 b=0·k。但對每個 k 都有 0·k=0，所以這句話等於說 b=0。



S08 · implies操作前

0=0\cdot 0=0\cdot 5,\quad 5\neq 0

操作後

0\mid 0\ \text{with non-unique witness};\ 0\nmid 5

條件：無

規則：mul_zero · 依賴：S07, G3

葉節點依據：mul_zero + numeric_evaluation

0∣0 成立，而且 k=0 與 k=5 都是見證（0·5=0，N9），見證不唯一。5≠0，所以依 S07，0∤5。可見「除數是 0 就一律不整除」是錯的：0∣0 為真。



S09 · implies操作前

b=a k=a k',\ a>0,\ k,k'\in\mathbb{N}

操作後

k=k'

條件：a>0

規則：order_basics · 依賴：S01, order_basics

葉節點依據：order_basics + case_analysis + contradiction

依三分律，k<k′、k=k′、k>k′ 恰有一個成立。若 k<k′，因 a>0 得 ak<ak′，與 ak=ak′ 矛盾；k>k′ 同理。所以 k=k′：在見證存在時它唯一，亦即 a>0 時見證至多一個。這與 S08 中 a=0 的情形形成對比。



S10 · implies操作前

a\in\mathbb{N}

操作後

a=a\cdot 1,\ \text{so}\ a\mid a

條件：無

規則：exists_intro · 依賴：S01, mul_one

葉節點依據：mul_one + mul_comm + exists_intro

自反性：a·1=a，1 是自然數，所以 a∣a；包括 0∣0（0=0·1）。



S11 · implies操作前

a\mid b,\ b\mid c

操作後

a\mid c

條件：無

規則：exists_elim · 依賴：S01

葉節點依據：exists_elim + mul_assoc + exists_intro

遞移性：由 a∣b 取見證 k 使 b=ak；由 b∣c 取見證 l 使 c=bl（S11.1）。代入並用結合律得 c=a(kl)，且 kl 是自然數（S11.2），所以 a∣c，見證是 kl。



S12 · implies操作前

6=3\cdot 2,\ 84=6\cdot 14

操作後

84=3\cdot 28,\ 3\mid 84

條件：無

規則：forall_elim · 依賴：S11, G3

葉節點依據：forall_elim + numeric_evaluation

3∣6 的見證 k=2，6∣84 的見證 l=14；依 S11，3∣84 的見證是 kl=28。核對：3·28=84，84 除以 3 的餘數為 0（N10 到 N12）。



S13 · case_split操作前

(a,b)\in\mathbb{N}^2

操作後

a=0:\ a\mid b\iff b=0;\quad a>0:\ a\mid b\iff b\bmod a=0

條件：無

規則：case_analysis · 依賴：S03, S07, S02, S04, S05, S08

葉節點依據：case_analysis + order_basics

判定程序：先看 a=0，此時 a∣b ⇔ b=0（S07）；否則 a>0，a∣b ⇔ 餘數為 0（S03）。兩種情況涵蓋所有自然數 a。套用：(6,84) 餘數 0，整除；(6,87) 餘數 3，不整除；(4,10) 餘數 2，不整除；(0,0) 整除；(0,5) 不整除。







## 局部子步與引理

S03.1 · implies操作前

b=aq+r,\ 0\le r<a,\ q\in\mathbb{Z},\ b\ge 0

操作後

q\ge 0,\ \text{so}\ q\in\mathbb{N}

條件：a>0

規則：order_basics · 依賴：division_algorithm, order_basics

葉節點依據：division_algorithm + order_basics + contradiction

帶餘除法給出整數 q 與 r。若 q≤−1，則 aq≤−a，於是 b=aq+r≤−a+r<−a+a=0，與 b≥0 矛盾。所以 q≥0，q 是自然數。



S03.2 · implies操作前

b=aq+0,\ q\in\mathbb{N}

操作後

a\mid b

條件：r=0

規則：exists_intro · 依賴：S03.1, S01

葉節點依據：exists_intro + add_zero

（⇐ 方向）若餘數 r=0，則 b=aq，而 q 是自然數（S03.1），所以 q 是見證，a∣b。



S03.3 · implies操作前

b=a\cdot k,\ k\in\mathbb{N}

操作後

b\bmod a=0

條件：a>0

規則：division_algorithm · 依賴：S01, division_algorithm

葉節點依據：division_algorithm + add_zero

（⇒ 方向）若 b=ak，則 b=a·k+0，且 0≤0<a。帶餘除法的商與餘數唯一，所以 b 除以 a 的餘數就是 0（商就是 k）。S03.1 到 S03.3 合起來證得引理 L_rem_test。



S11.1 · implies操作前

b=ak,\ c=bl

操作後

c=(ak)l

條件：無

規則：eq_replace · 依賴：S01, exists_elim

葉節點依據：eq_replace

把 c=bl 中的 b 換成相等的 ak。



S11.2 · implies操作前

c=(ak)l

操作後

c=a(kl),\ kl\in\mathbb{N}

條件：無

規則：mul_assoc · 依賴：S11.1, G1

葉節點依據：mul_assoc

乘法結合律給 (ak)l=a(kl)；自然數的積仍是自然數（G1），所以 kl 是合法見證。







## 逐步反向審查


- S13 · sufficient_goal_reduction · S03, S07, case_analysis — 目標 G：對每個數對正確判定。足夠條件 H：a=0 與 a>0 兩種情況各有已證的判準；H⇒G 由分情況論證。H 由 S03、S07 正向證成。
- S12 · premise_audit · S11, forall_elim, numeric_evaluation — 這是 S11 的一個實例並附數值核對；它不能取代一般證明。
- S11.2 · premise_audit · mul_assoc, G1 — 需要 ℕ 對乘法封閉；在有理數中這一步會允許非自然數見證。
- S11.1 · premise_audit · eq_replace — 等值代換。
- S11 · premise_audit · S01, exists_elim, mul_assoc — 結論不含暫取的名字 k、l，所以 ∃消去合法。不宣稱反向：a∣c 不推出 a∣b。
- S10 · premise_audit · mul_one, exists_intro — 只用乘法單位元。
- S09 · premise_audit · order_basics, case_analysis — 需要 a>0 才能保持嚴格不等；a=0 時結論不成立（S08）。
- S08 · premise_audit · S07, mul_zero — 只是 S07 的兩個實例與一個見證不唯一的例子。
- S07 · inverse_equivalence · mul_zero, exists_intro — 反向：若 b=0，取 k=0 得 b=0·0，所以 0∣b。兩向都成立。
- S06 · premise_audit · S01, mul_zero, exists_intro, forall_intro — 只用乘以零的性質；對每個 a 都成立，所以可全稱推廣。
- S05 · premise_audit · S01, S03, G2, mul_inverse_nonzero — 論證依賴「有理解唯一」：若唯一的解不是自然數，就沒有自然數解。有一個數值商不代表整除。
- S04 · premise_audit · S03, nat_discrete, order_basics — 否定需要排除所有 k，S03 的等價或 nat_discrete 的兩段夾擠都做到了這一點；只檢查幾個 k 不夠。
- S03.3 · premise_audit · division_algorithm — 關鍵是帶餘除法的唯一性；若只有存在性，不能由一種寫法推出餘數為 0。沒有使用引理本身。
- S03.2 · premise_audit · S03.1, exists_intro — 只用到 q 是自然數；沒有使用引理本身。
- S03.1 · premise_audit · division_algorithm, order_basics — 需要 a>0 與 b≥0；這保證商可以當自然數見證。
- S03 · inverse_equivalence · L_rem_test — 引理的兩個方向（S03.2、S03.3）都已證；前提 a>0 是帶餘除法所需。
- S02 · premise_audit · S01, exists_intro, numeric_evaluation — 存在性只需一個見證；這一步不宣稱見證唯一（唯一性見 S09）。
- S01 · premise_audit · G1, G2, mko_dvd_def — 此步只展開定義；見證限定為自然數（G2），不是有理數。





## 錯誤控制與反例

有數值商不等於整除MKO 指出的誤解：看到 b/a 是一個數就宣稱 a∣b。10/4=5/2 是有理數，但見證必須是自然數，所以 4∤10（S05）。判定要看自然數見證或餘數是否為 0。

除數為 0 不是一律不整除MKO 指出的另一個誤解：把除數為零一律判成沒有整除關係。依定義 0∣b ⇔ b=0（S07），所以 0∣0 成立，0∤5。注意這裡沒有做「除以 0」，只是找乘數見證。

否定要排除所有見證證明 6∤87 時，試 k=14、15 兩個值不夠；必須用餘數引理或 nat_discrete 的夾擠排除所有 k（S04）。同理，6∣3 不成立：3=6·(1/2) 的 1/2 不是自然數，3 除以 6 的餘數是 3。


- 4∣10，因為 10/4=2.5 是一個數 → reject — 見證必須是自然數；10=4·2+2，餘數 2≠0。
- 0 不整除任何數 → reject — 0=0·0，所以 0∣0。
- 0∣5 → reject — 對每個 k，0·k=0≠5。
- 6∣3，因為 3=6·(1/2) → reject — 1/2 不是自然數；3=6·0+3，餘數 3≠0。
- 0∣0 的見證唯一 → reject — 0=0·0=0·5，k=0 與 k=5 都是見證。





## 結論與限制

6∣84（見證 14）；6∤87（餘數 3）；4∤10（唯一的有理解 5/2 不是自然數，餘數 2）；每個 a 都整除 0（見證 0）；0∣b ⇔ b=0，所以 0∣0 而 0∤5，且 0∣0 的見證不唯一；a>0 時見證至多一個，存在時唯一；整除具自反性與遞移性，3∣84 的見證為 2·14=28。


- 帶餘除法（存在與唯一）作為前置規則引用，本稿只由它推出餘數判準 L_rem_test。
- 本稿只處理 ℕ；含負數的整數整除不在範圍內。





## 驗證及來源綁定

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


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: c7700b425af628e5a943830098f9039a8ba739a667d2577ec46189e0e2124324
- original source SHA-256: 1b68c27c071f5fe0cfe48fffd7605f00b4dfae82833e7c47a8a473157438e68f
- Lean: NOT_RUN · independent AI: NOT_MEASURED

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