# 自然數質數：證明 97 是質數、91 是合數，並排除 0 與 1

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

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

derivation-mko-prime-number-01 · production-20261019-adopted-96



## 目標與範圍

依 MKO 定義（p 為質數 ⇔ 2≤p 且 p 的每個自然數因數 d 都滿足 d=1 或 d=p）：(1) 說明 0 與 1 不是質數；(2) 證明 2 是質數；(3) 以見證 7 證明 91 是合數，並說明只測 2、3、5 會誤判；(4) 證明「若 n=dk 且 d、k≥2，則 min(d,k)²≤n」，據此只需檢查 2 到 9，證明 97 是質數；(5) 證明 2 是唯一的偶質數。

只在包含 0 的自然數中工作，使用自然數整除與精確的整數比較（MKO 假設 a1、a2），不用浮點平方根。平方根界由本稿證明的引理給出。不處理質因數分解的唯一性、質數無窮多或大整數的質數證書；不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- order_basics
- division_algorithm
- mul_zero
- numeric_evaluation


- G1 — p、d 是包含 0 的自然數；整除依 MKO 自然數整除，見證必須是自然數（MKO 假設 a1）。
- G2 — 因數判定用自然數整除與精確整數比較，不用近似平方根或浮點除法（MKO 假設 a2）。
- G3 — 候選：0、1、2、91、97，以及大於 2 的偶數。


- p — 候選的自然數
- d\mid p — d 整除 p
- m=\min(d,k) — 因數對中較小者
- n\bmod m — n 除以 m 的餘數





## 規則與來源


- 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。
- division_algorithm · prerequisite — 帶餘除法：對整數 a 與正整數 b，存在唯一的整數 q、r 使 a=bq+r 且 0≤r<b。
- mul_zero · prerequisite — 乘以零：u·0=0。理由：u·0=u·(0+0)=u·0+u·0，兩邊同減 u·0 得 0=u·0。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
- exists_elim · prerequisite — ∃消去：由 ∃x∈D, P(x)，可取一個新名字 a 表示某個滿足 P(a) 的元素；只要最後結論不含 a，就可用 a 推理。
- contradiction · prerequisite — 反證法：若假設 ¬P 推出矛盾（某命題與其否定同時成立），則 P 成立。
- mul_one · prerequisite — 乘法單位元：1·u=u。
- case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
- exists_intro · prerequisite — ∃引入：若找到 a∈D 使 P(a) 成立，則 ∃x∈D, P(x)。
- mul_comm · prerequisite — 乘法交換律：uv=vu（在交換的數系中，例如 ℤ、ℚ、ℝ、ℂ）。
- quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。
- forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
- mko_prime_def · cited — 自然數 p 為質數，當且僅當 2≤p，且每個自然數 d 若 d∣p，則 d=1 或 d=p。0 與 1 都不是質數。 · mko-prime-number
- mko_dvd_def · cited — 對自然數 a、b，a∣b 當且僅當存在自然數 k 使 b=a·k。 · mko-natural-divisibility
- rem_test · prerequisite — 對自然數 n 與正自然數 m：m∣n ⇔ n 除以 m 的餘數為 0（由帶餘除法的唯一性得到）。
- L_div_bound · lemma — 若 d∣n、n>0，且 n=dk，則 d≥1、k≥1 且 d≤n。
- L_small_factor · lemma — 若 n=d·k，且 d≥2、k≥2，則 m=min(d,k) 滿足 2≤m、m∣n 且 m²≤n。





## 逐步主鏈

S01 · definition操作前

p\ \text{prime}

操作後

2\le p\ \land\ \forall d\in\mathbb{N}\,(d\mid p\Rightarrow d=1\lor d=p)

條件：無

規則：mko_prime_def · 依賴：G1, mko_prime_def

葉節點依據：mko_prime_def + def_unfold

依 MKO 的定義，質數要同時滿足兩個條件：p≥2，以及 p 沒有 1 與 p 以外的自然數因數。要否定只需其中一個條件失敗；要肯定則必須排除所有可能的非平凡因數。



S02 · implies操作前

d\mid n,\ n>0

操作後

1\le d\le n

條件：n>0

規則：L_div_bound · 依賴：mko_dvd_def, L_div_bound

葉節點依據：mul_zero + order_basics + exists_elim

正數的因數夾在 1 與它自己之間：依引理 L_div_bound（S02.1、S02.2 證明）。這讓「列出所有因數」成為有限的工作。



S03 · implies操作前

p=0,\ p=1

操作後

0,\ 1\ \text{not prime}

條件：無

規則：mko_prime_def · 依賴：S01, S02, G3

葉節點依據：mko_prime_def + order_basics + mul_zero

2≤0 與 2≤1 都不成立，所以 0、1 都不是質數。值得注意：1 的因數依 S02 只有 1（1≤d≤1），所以 1 其實通過「因數只有 1 與自身」的條件，它被排除完全是因為 2≤p。0 則兩個條件都失敗：0=2·0，所以 2∣0 而 2∉{1,0}。



S04 · implies操作前

p=2

操作後

2\ \text{prime}

條件：無

規則：mko_prime_def · 依賴：S01, S02

葉節點依據：mko_prime_def + case_analysis + order_basics

2≥2。若 d∣2，依 S02 有 1≤d≤2，而 1 與 2 之間的自然數只有 1 與 2，所以 d=1 或 d=2。兩個條件都成立，2 是質數（N22 為獨立核對）。



S05 · implies操作前

91=7\cdot 13

操作後

7\mid 91,\ 7\notin\{1,91\};\ 91\ \text{not prime}

條件：無

規則：mko_prime_def · 依賴：S01, mko_dvd_def, G3

葉節點依據：mko_prime_def + exists_intro + numeric_evaluation

7·13=91（N1），所以 7∣91，見證是 13。7≠1、7≠91，因數條件失敗，91 不是質數；7 是合數見證（MKO 段落 2）。



S06 · implies操作前

91\bmod 2=91\bmod 3=91\bmod 5=1

操作後

2,3,5\nmid 91,\ \text{yet}\ 91\ \text{is composite}

條件：無

規則：rem_test · 依賴：S05, rem_test

葉節點依據：rem_test + numeric_evaluation

91 除以 2、3、5 的餘數都是 1（N2 到 N4），依 rem_test 它們都不整除 91。若只測這三個就宣稱 91 是質數，結論錯誤，因為 S05 已找到因數 7。在不完整的候選表中找不到因數，不能當作質數證明（MKO 段落 2）。



S07 · implies操作前

d\mid 97,\ d\neq 1,\ d\neq 97

操作後

97=dk,\ 2\le d\le 96,\ k\ge 2

條件：無

規則：L_div_bound · 依賴：S01, S02, G3

葉節點依據：exists_elim + order_basics + case_analysis

97≥2 成立。為證因數條件，用反證：假設有 d∣97 且 d≠1、d≠97，取見證 97=dk。由 S02，1≤d≤97，再排除 1 與 97 得 2≤d≤96。又 k≥1（S02.1）；若 k=1 則 d=97，已排除；所以 k≥2。



S08 · implies操作前

97=dk,\ d\ge 2,\ k\ge 2

操作後

m=\min(d,k):\ 2\le m,\ m\mid 97,\ m^2\le 97

條件：d\ge 2; k\ge 2

規則：L_small_factor · 依賴：S07, L_small_factor

葉節點依據：order_basics + mul_comm + exists_intro

依引理 L_small_factor（S08.1、S08.2 證明），因數對中較小的 m 也整除 97，而且 m²≤97。這就是「只需檢查到平方根」的理由，而且用的是精確整數比較。



S09 · implies操作前

m^2\le 97

操作後

2\le m\le 9

條件：無

規則：order_basics · 依賴：S08, G2

葉節點依據：order_basics + numeric_evaluation + contradiction

若 m≥10，則 m²≥100>97（N5），與 m²≤97 矛盾；所以 m≤9。而 9²=81≤97（N6），所以 9 是滿足 m²≤97 的最大整數。這裡用的是精確的整數平方比較，不是浮點 √97。



S10 · case_split操作前

m\in\{2,3,4,5,6,7,8,9\}

操作後

97\bmod m\in\{1,1,1,2,1,6,1,7\}\neq 0,\ \text{so}\ m\nmid 97

條件：無

規則：rem_test · 依賴：S09, rem_test

葉節點依據：rem_test + case_analysis + numeric_evaluation

逐一計算 97 除以 m 的餘數：m=2 餘 1、3 餘 1、4 餘 1、5 餘 2、6 餘 1、7 餘 6、8 餘 1、9 餘 7（N7 到 N14）。沒有一個是 0，依 rem_test，2 到 9 都不整除 97。這與 S08、S09 的「存在 2≤m≤9 且 m∣97」矛盾。



S11 · implies操作前

\text{assumption of S07 leads to a contradiction}

操作後

\forall d\,(d\mid 97\Rightarrow d=1\lor d=97);\ 97\ \text{prime}

條件：無

規則：contradiction · 依賴：S07, S10

葉節點依據：contradiction + quantifier_negation + mko_prime_def

S07 的假設「有 d∣97 且 d∉{1,97}」推出 S10 的矛盾，所以假設不成立：97 的每個因數都是 1 或 97。加上 97≥2，依定義 97 是質數。N15 以內建質數判定獨立核對。



S12 · implies操作前

91,\ 9^2\le 91<10^2

操作後

\text{the complete search}\ 2\le m\le 9\ \text{finds}\ 7

條件：無

規則：L_small_factor · 依賴：S05, S08, G2

葉節點依據：order_basics + rem_test + numeric_evaluation

同一個界套用到 91：9²=81≤91<100=10²（N18、N19），所以合數 91 必有 2 到 9 之間的因數；完整搜尋在 m=7 找到（91 除以 7 餘 0，N17），與 S05 一致。對照 S06：只測 2、3、5 是不完整的搜尋，才會漏掉 7。



S13 · implies操作前

p=2j,\ p\ge 2,\ p\neq 2

操作後

2\mid p,\ 2\notin\{1,p\};\ p\ \text{not prime}

條件：p\neq 2

規則：mko_prime_def · 依賴：S01, S04, mko_dvd_def

葉節點依據：mko_prime_def + exists_intro + forall_intro

偶數 p=2j 有因數 2（見證 j）。若 p≠2，則 2≠1 且 2≠p，因數條件失敗，p 不是質數。配合 S04，2 是唯一的偶質數（N21 對 4 到 120 的偶數做有限核對，只支持這些點）。







## 局部子步與引理

S02.1 · implies操作前

n=dk,\ n>0

操作後

d\ge 1,\ k\ge 1

條件：n>0

規則：mul_zero · 依賴：mko_dvd_def, mul_zero

葉節點依據：mul_zero + contradiction

若 d=0 或 k=0，則 n=dk=0，與 n>0 矛盾。所以 d≠0、k≠0；自然數非零即至少為 1。



S02.2 · implies操作前

k\ge 1,\ d\ge 0

操作後

n=dk\ge d\cdot 1=d

條件：無

規則：order_basics · 依賴：S02.1, order_basics

葉節點依據：order_basics + mul_one

k≥1 且 d≥0，所以 dk≥d·1=d，即 d≤n。S02.1 與 S02.2 合起來證得引理 L_div_bound。



S08.1 · implies操作前

n=dk

操作後

d\mid n,\ k\mid n,\ \text{so}\ m\mid n

條件：無

規則：exists_intro · 依賴：mko_dvd_def, mul_comm

葉節點依據：exists_intro + mul_comm + case_analysis

n=d·k 給 d∣n（見證 k）；由交換律 n=k·d 給 k∣n（見證 d）。m 是 d 或 k 其中之一，所以 m∣n；又 d、k≥2，故 m≥2。



S08.2 · implies操作前

m\le d,\ m\le k,\ m\ge 0

操作後

m^2=m\cdot m\le d\cdot m\le d\cdot k=n

條件：無

規則：order_basics · 依賴：order_basics

葉節點依據：order_basics + mul_comm

m≤d 兩邊乘非負的 m 得 m·m≤d·m；m≤k 兩邊乘非負的 d 得 d·m≤d·k。串接得 m²≤n。S08.1 與 S08.2 合起來證得引理 L_small_factor。







## 逐步反向審查


- S13 · premise_audit · S01, S04, mko_dvd_def — 一般論證對每個偶數 p≠2 成立；有限核對 N21 不是證明的一部分。
- S12 · premise_audit · S05, L_small_factor — 引理保證合數在界內有因數；這裡只是說明完整搜尋與部分搜尋的差別。
- S11 · sufficient_goal_reduction · S07, S10, contradiction, mko_prime_def — 目標 G：97 是質數。足夠條件 H：97≥2 且沒有非平凡因數；H⇒G 由定義。H 由反證法證成，沒有把 G 當作前提；N15 只是交叉核對，不是證明的一部分。
- S10 · premise_audit · S09, rem_test, case_analysis — 八種情況窮盡 2≤m≤9 的所有 m；這是完整檢查，不是抽樣。
- S09 · premise_audit · S08, order_basics, G2 — 上界必須涵蓋所有 m²≤97 的 m；取 9 不多也不少。
- S08.2 · premise_audit · order_basics — 乘以非負數保持 ≤；沒有使用引理本身。
- S08.1 · premise_audit · mko_dvd_def, mul_comm, exists_intro — 只用交換律與見證；沒有使用引理本身。
- S08 · premise_audit · S07, L_small_factor — 引理需要 d、k 都至少為 2，由 S07 提供。
- S07 · premise_audit · S02, exists_elim — 這是反證法的假設與它的直接推論；結論要到 S11 才釋放假設。
- S06 · premise_audit · S05, rem_test — 這一步只顯示部分檢查的不足，不改變 S05 的結論。
- S05 · premise_audit · S01, mko_dvd_def, numeric_evaluation — 否定只需一個非平凡因數。
- S04 · premise_audit · S01, S02, case_analysis — 因數範圍 1 到 2 已窮盡；沒有遺漏的候選。
- S03 · premise_audit · S01, S02, mul_zero — 否定只需一個條件失敗；這裡同時說明哪個條件對 1 是決定性的。
- S02.2 · premise_audit · order_basics, mul_one — 乘以非負數保持 ≤；沒有使用引理本身。
- S02.1 · premise_audit · mul_zero, contradiction — 只用乘以零；沒有使用引理本身。
- S02 · premise_audit · L_div_bound — 需要 n>0；n=0 時每個 d 都整除 0，沒有上界（S03）。
- S01 · premise_audit · G1, mko_prime_def — 此步只展開定義，不推出新事實。





## 錯誤控制與反例

1 不是質數MKO 指出的誤解：把 1 列為質數。1 的因數確實只有 1，但定義另要求 2≤p，所以 1 不是質數（S03）。0 則連因數條件也失敗，因為 2∣0。

只測少數小因數不夠MKO 指出的另一個誤解：只測少數小因數就宣稱是質數。91 不被 2、3、5 整除，卻等於 7·13（S06）。肯定質數必須排除所有可能的非平凡因數；引理 L_small_factor 把範圍縮到 m²≤n，但範圍內的每個 m 都要檢查（S10、S12）。

平方根界要用精確整數比較MKO 假設 a2 不允許用近似平方根。本稿以 m²≤97 與 10²=100>97 精確決定上界 9；若用四捨五入的浮點 √n 決定上界，在 n 是完全平方數附近可能少檢查一個候選。


- 1 是質數，因為它的因數只有 1 與它自己 → reject — 定義要求 2≤p，1 不滿足。
- 91 不被 2、3、5 整除，所以 91 是質數 → reject — 91=7·13；部分檢查不是證明。
- 要證 97 是質數，必須試除 2 到 96 的每一個數 → reject — 引理 L_small_factor 證明若有非平凡因數，必有一個 m 滿足 2≤m≤9，所以檢查 2 到 9 已足夠。
- 0 是質數，因為 0 沒有因數 → reject — 每個自然數都整除 0（例如 0=2·0），而且 2≤0 不成立。
- 所有質數都是奇數 → reject — 2 是質數（S04）且是偶數。





## 結論與限制

0 與 1 不是質數（2≤p 失敗；1 雖只有因數 1，仍被排除）；2 是質數，也是唯一的偶質數；91=7·13 是合數，只測 2、3、5 會漏掉 7；由 min(d,k)²≤n 只需檢查 2 到 9，而 97 除以 2 到 9 的餘數都不為 0，所以 97 是質數。


- rem_test 作為前置規則使用，其證明見自然數整除的教學稿。
- 只試除 2 到 9 中的質數（2、3、5、7）其實也足夠，但需要「最小的非平凡因數必為質數」這個額外事實，本稿沒有使用也沒有證明。
- N15、N16、N22 使用核對器內建的質數判定，只作獨立交叉核對；N21 是有限範圍核對。





## 驗證及來源綁定

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


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

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