# 有理數：同一個有理數的不同分數表示、交叉相乘與約分

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

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

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



## 目標與範圍

依 MKO 的定義（存在整數 p、q，q≠0，使 x=p/q），證明 6/(−8)、−3/4、9/(−12) 表示同一個有理數，並把 6/(−8) 精確約成正規形式 −3/4；以交叉相乘證明 2/3≠3/5；說明「5/0」不表示任何數；說明有限小數 −1.25=−5/4 與整數 7=7/1 都是有理數；並在分母為正時用交叉相乘證明 −3/4<−2/3。

在 ℝ 中討論分數（p/q 定義為 p·(1/q)），只用域的運算與序。證明兩個引理：分母非零時以交叉相乘判定相等，分母為正時以交叉相乘判定大小。不證明正規形式（既約且分母為正）的唯一性，不處理與 Lean Rat.divInt 的對接；不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- mul_inverse_nonzero
- frac_rules
- zero_product
- order_basics
- numeric_evaluation


- G1 — 在實數 ℝ 中討論，整數 ℤ⊆ℝ；對 q≠0，p/q 表示 p·(1/q)；0 沒有倒數。
- G2 — MKO 的定義：數 x 是有理數，若存在整數 p、q，q≠0，使 x=p/q（假設 a1、a2）。
- G3 — 正規顯示慣例（MKO 說明）：分子與分母互質（最大公因數為 1），且分母為正。
- G4 — 資料：6/(−8)、−3/4、9/(−12)、2/3、3/5、字串「5/0」、有限小數 −1.25、整數 7、−2/3。


- \mathbb{Q} — 有理數集合
- \frac{p}{q} — p·(1/q)，q≠0
- (p,q) — 表示有理數的一對整數
- \gcd(a,b) — 最大公因數
- k — 約分時分子分母同乘的非零數





## 規則與來源


- 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）。
- zero_product · prerequisite — 零乘積性質：在 ℤ、ℚ、ℝ、ℂ（或任何整域）中，uv=0 ⇔ u=0 或 v=0。
- 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。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- mul_assoc · prerequisite — 乘法結合律：(uv)w=u(vw)。
- mul_comm · prerequisite — 乘法交換律：uv=vu（在交換的數系中，例如 ℤ、ℚ、ℝ、ℂ）。
- mul_one · prerequisite — 乘法單位元：1·u=u。
- eq_congruence · prerequisite — 等式同用：若 u=v，對兩邊做同一個有定義的運算 f，得 f(u)=f(v)。只對一邊做運算不屬於此規則。
- neg_mul · prerequisite — 負號與乘法：(−u)v=−(uv)，(−u)(−v)=uv。
- eq_refl_symm_trans · prerequisite — 等號的性質：u=u；若 u=v 則 v=u；若 u=v 且 v=w 則 u=w。
- divides_def · prerequisite — 整除：對整數 a、b，a∣b 表示存在整數 k 使 b=ak。
- mul_zero · prerequisite — 乘以零：u·0=0。理由：u·0=u·(0+0)=u·0+u·0，兩邊同減 u·0 得 0=u·0。
- contradiction · prerequisite — 反證法：若假設 ¬P 推出矛盾（某命題與其否定同時成立），則 P 成立。
- exists_intro · prerequisite — ∃引入：若找到 a∈D 使 P(a) 成立，則 ∃x∈D, P(x)。
- forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
- and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
- mko_rat_def · cited — 數 x 是有理數，若存在整數 p、q 且 q≠0，使 x=p/q。不同整數對可以表示同一個有理數。 · mko-rational-number
- canonical_def · prerequisite — 正規形式：p/q 中 gcd(|p|,q)=1 且 q>0。
- gcd_def · prerequisite — 整數 a、b 不全為 0 時，gcd(a,b) 是同時整除 a 與 b 的最大正整數。
- decimal_def · prerequisite — 有限小數：整數部分加上小數點後第 j 位數字乘以 10^{−j} 之和；例如 1.25=1+2/10+5/100。
- L_cross · lemma — 對實數 p、q、r、s，q≠0、s≠0：p/q=r/s ⇔ ps=rq。
- L_cross_order · lemma — 對實數 p、q、r、s，q>0、s>0：p/q<r/s ⇔ ps<rq。





## 逐步主鏈

S01 · definition操作前

x\in\mathbb{Q}

操作後

\exists p,q\in\mathbb{Z},\ q\neq 0:\ x=\frac{p}{q}

條件：無

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

葉節點依據：mko_rat_def + mul_inverse_nonzero

依 MKO，判定 x 是有理數，就是找出一對整數 (p,q)，q≠0，使 x=p/q。定義只要求「存在」這樣一對，並沒有說這一對唯一；不同的整數對可以表示同一個有理數，這正是以下要處理的。



S02 · equivalent操作前

\frac{p}{q}=\frac{r}{s}\quad(q\neq0,\ s\neq0)

操作後

ps=rq

條件：q\neq 0; s\neq 0

規則：L_cross · 依賴：G1, L_cross

葉節點依據：L_cross

比較兩個分數是否相等的工具是引理 L_cross：分母都不為 0 時，p/q=r/s ⇔ ps=rq。引理在 S02.1、S02.2 證明，之後 S03、S04、S07、S09 都用它。



S03 · equivalent操作前

6\cdot 4=24=(-3)\cdot(-8)

操作後

\frac{6}{-8}=\frac{-3}{4}

條件：-8\neq 0; 4\neq 0

規則：L_cross · 依賴：S02, G4

葉節點依據：L_cross + numeric_evaluation + neg_mul

取 p=6、q=−8、r=−3、s=4：ps=6·4=24，rq=(−3)·(−8)=24。兩者相等，依 L_cross，6/(−8)=−3/4。



S04 · equivalent操作前

6\cdot(-12)=-72=9\cdot(-8)

操作後

\frac{6}{-8}=\frac{9}{-12}=\frac{-3}{4}

條件：-8\neq 0; -12\neq 0

規則：L_cross · 依賴：S02, S03, G4

葉節點依據：L_cross + numeric_evaluation + eq_refl_symm_trans

取 p=6、q=−8、r=9、s=−12：ps=6·(−12)=−72，rq=9·(−8)=−72，所以 6/(−8)=9/(−12)；配合 S03，三個不同的整數對 (6,−8)、(−3,4)、(9,−12) 表示同一個有理數。這正是 MKO 所說「不同整數對可以表示同一個有理數」。



S05 · equivalent操作前

\frac{6}{-8}

操作後

\frac{6\cdot(-\frac12)}{(-8)\cdot(-\frac12)}=\frac{-3}{4}

條件：-\tfrac{1}{2}\neq 0

規則：frac_rules · 依賴：G1, frac_rules

葉節點依據：frac_rules + numeric_evaluation

約分：gcd(6,8)=2（N20），把分子分母同乘 k=−1/2（等於同除以 −2，負號一併移到分子）。依分數規則 a/b=(ak)/(bk)（k≠0），6/(−8)=(6·(−1/2))/((−8)·(−1/2))=(−3)/4（N7、N8）。這是精確等式，不是近似。



S06 · implies操作前

\frac{-3}{4}

操作後

\gcd(3,4)=1,\ 4>0:\ \text{canonical form}

條件：無

規則：canonical_def · 依賴：S05, G3, gcd_def

葉節點依據：canonical_def + gcd_def + divides_def + numeric_evaluation

4 的正因數是 1、2、4；2 與 4 都不整除 3，所以 gcd(3,4)=1（N9）；分母 4>0。所以 −3/4 符合 G3 的正規顯示慣例。正規化改變的是表示，不是數值（S05 是等式）。



S07 · equivalent操作前

2\cdot5=10\neq 9=3\cdot3

操作後

\frac{2}{3}\neq\frac{3}{5}

條件：3\neq 0; 5\neq 0

規則：L_cross · 依賴：S02, G4

葉節點依據：L_cross + numeric_evaluation

取 p=2、q=3、r=3、s=5：ps=10，rq=9，10≠9。L_cross 是雙條件，兩邊同時否定仍等價：ps≠rq ⇔ p/q≠r/s，所以 2/3≠3/5。



S08 · implies操作前

x\cdot 0=5\ \text{for some}\ x

操作後

0=5,\ \text{a contradiction}

條件：無

規則：contradiction · 依賴：G1, mul_zero

葉節點依據：mul_zero + contradiction + mul_inverse_nonzero

若「5/0」表示某個數 x，則 x 應滿足 x·0=5。但對任何 x，x·0=0（乘以零），於是 0=5，矛盾。所以沒有任何數是 5/0；整數對 (5,0) 違反 q≠0（假設 a2），不表示任何有理數。對照：0/5=0·(1/5)=0 是合法的有理數，分子可以是 0（N11）。



S09 · implies操作前

-1.25

操作後

-\frac{125}{100}=-\frac{5}{4}\in\mathbb{Q}

條件：100\neq 0

規則：exists_intro · 依賴：S02, G4, decimal_def

葉節點依據：decimal_def + exists_intro + L_cross + numeric_evaluation

依有限小數的意義，−1.25=−(1+2/10+5/100)=−125/100（N12）。取 p=−125、q=100≠0，依定義 −1.25 是有理數。再約分：(−125)·4=−500=(−5)·100，依 L_cross，−125/100=−5/4（N13、N14）。有限小數是精確的分數，不是另一種數。



S10 · implies操作前

n\in\mathbb{Z}

操作後

n=\frac{n}{1}\in\mathbb{Q}

條件：1\neq 0

規則：exists_intro · 依賴：S01, mul_one

葉節點依據：exists_intro + mul_one + forall_intro

對任意整數 n：1·1=1，所以 1/1=1，n/1=n·1=n。取 p=n、q=1≠0，依定義 n∈ℚ。特別地 7=7/1 是有理數（N15）。n 是任意的，所以每個整數都是有理數。



S11 · equivalent操作前

(-3)\cdot3=-9<-8=(-2)\cdot4

操作後

\frac{-3}{4}<\frac{-2}{3}

條件：4>0; 3>0

規則：L_cross_order · 依賴：G4, L_cross_order

葉節點依據：L_cross_order + numeric_evaluation

兩個分母 4、3 都為正。依引理 L_cross_order（p=−3、q=4、r=−2、s=3）：ps=(−3)·3=−9，rq=(−2)·4=−8，−9<−8，所以 −3/4<−2/3（N16、N17）。引理在 S11.1 證明；分母皆為正是本引理採用的充分前提，不宣稱它是保持此比較方向的最弱條件，這也是正規形式要求分母為正的好處。



S12 · implies操作前

\text{S04, S06 to S11}

操作後

\tfrac{6}{-8}=\tfrac{9}{-12}=\tfrac{-3}{4};\ \tfrac{2}{3}\neq\tfrac{3}{5};\ -1.25,\ 7\in\mathbb{Q};\ \tfrac{-3}{4}<\tfrac{-2}{3}

條件：無

規則：and_intro_elim · 依賴：S04, S06, S07, S08, S09, S10, S11

葉節點依據：and_intro_elim

三個整數對表示同一個有理數，正規形式是 −3/4；2/3 與 3/5 不同；「5/0」不表示任何數；−1.25=−5/4 與 7=7/1 是有理數；−3/4<−2/3。







## 局部子步與引理

S02.1 · implies操作前

q\neq 0,\ s\neq 0

操作後

qs\neq 0,\ \frac{p}{q}\cdot qs=ps,\ \frac{r}{s}\cdot qs=rq

條件：q\neq 0; s\neq 0

規則：zero_product · 依賴：G1, zero_product

葉節點依據：zero_product + mul_inverse_nonzero + mul_assoc + mul_comm + mul_one

依零乘積性質，qs=0 ⇔ q=0 或 s=0；兩者都不成立，所以 qs≠0。又 (p/q)·qs=p·(1/q)·q·s=p·1·s=ps（結合律、交換律與 q·(1/q)=1）；同理 (r/s)·qs=r·(1/s)·s·q=rq。



S02.2 · equivalent操作前

\frac{p}{q}=\frac{r}{s}

操作後

ps=rq

條件：qs\neq 0

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

葉節點依據：eq_congruence + mul_inverse_nonzero + frac_rules

⇒：兩邊同乘 qs，依 S02.1 得 ps=rq。⇐：兩邊同乘 1/(qs)（qs≠0，所以存在），ps·(1/(qs))=p/q、rq·(1/(qs))=r/s，得 p/q=r/s。S02.1 與 S02.2 合起來證得引理 L_cross。



S11.1 · equivalent操作前

q>0,\ s>0,\ \frac{p}{q}<\frac{r}{s}

操作後

ps<rq

條件：q>0; s>0

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

葉節點依據：order_basics + mul_inverse_nonzero + frac_rules

q>0、s>0 推出 qs>0，也推出 1/(qs)>0。⇒：不等式兩邊同乘正數 qs，方向不變，依 S02.1 的化簡得 ps<rq。⇐：兩邊同乘正數 1/(qs) 得 p/q<r/s。這證得引理 L_cross_order。若某個分母為負，乘以 qs 可能使不等號反向，引理就不適用。







## 逐步反向審查


- S12 · sufficient_goal_reduction · S03, S04, S05, S06, S07, S08, S09, S10, S11 — 目標是 goal 所列各項。足夠條件 H：S03 到 S11 各自成立；H 推出目標只用合取。每一項都由定義、兩個引理與精確計算正向證成，沒有把目標當作前提。
- S11.1 · inverse_equivalence · order_basics, S02.1, mul_inverse_nonzero — 乘以正數 qs 與乘以正數 1/(qs) 都保持不等號方向，互為反運算。
- S11 · inverse_equivalence · L_cross_order, numeric_evaluation — 本稿在兩個分母都為正的前提下證明此雙條件；這是已證明的適用範圍，不表示其他符號情形一律不成立。
- S10 · premise_audit · exists_intro, mul_one, forall_intro — 反向（每個有理數都是整數）不成立，例如 −5/4 不是整數。
- S09 · premise_audit · decimal_def, exists_intro, L_cross, numeric_evaluation — 存在性只需一對 (p,q)；約分是另外的等式。
- S08 · premise_audit · mul_zero, contradiction, mul_inverse_nonzero — 矛盾來自 x·0=0 對所有 x 成立；這正是 0 沒有倒數的原因。
- S07 · inverse_equivalence · L_cross, numeric_evaluation — P⇔Q 與 ¬P⇔¬Q 等價（N10）。
- S06 · premise_audit · gcd_def, canonical_def, divides_def — 只檢查 −3/4 是正規形式；正規形式的唯一性不在本稿證明（開放項目）。
- S05 · inverse_equivalence · frac_rules, numeric_evaluation — 反向：分子分母同乘 −2 回到 6/(−8)；k≠0 是規則的條件。
- S04 · inverse_equivalence · L_cross, numeric_evaluation, eq_refl_symm_trans — 每個相等都由雙條件得到，並以等號傳遞連起來（N4 到 N6）。
- S03 · inverse_equivalence · L_cross, numeric_evaluation — L_cross 是雙條件；計算可重算（N1、N2、N3）。
- S02.2 · inverse_equivalence · eq_congruence, mul_inverse_nonzero, S02.1 — 乘 qs 與乘 1/(qs) 互為反運算，前提 qs≠0。
- S02.1 · premise_audit · zero_product, mul_inverse_nonzero, mul_assoc, mul_comm — 需要 q≠0 與 s≠0，才有 1/q 與 1/s。
- S02 · inverse_equivalence · L_cross — 引理是雙條件，兩個方向都在子步證明；分母非零不可省。
- S01 · premise_audit · mko_rat_def, G1 — q≠0 是定義的一部分（假設 a2），不能省略；q=0 時 p/q 沒有定義。





## 錯誤控制與反例

分母不可為零MKO 指出的誤解之一是允許零分母。「5/0」看起來像分數，但若它是某個數 x，就要有 x·0=5，而 x·0 永遠是 0（S08）。所以 (5,0) 不表示任何有理數；相對地，0/5=0 是合法的有理數。

外觀不同的分數可以相等MKO 的另一誤解是把不同分數外觀當成不同數值。6/(−8)、−3/4、9/(−12) 看起來不同，卻是同一個有理數（S03、S04）；判定要用交叉相乘 L_cross，而不是比較分子或分母。比較大小時還要先讓分母為正：1/(−2) 與 1/3 若直接交叉相乘，1·3=3>−2=1·(−2) 會誤判 1/(−2)>1/3，事實上 −1/2<1/3（N18、N19）。

約分是精確等式，不是近似MKO 提醒不要把約分視為近似。6/(−8)=−3/4 由 a/b=(ak)/(bk)（k≠0）得到，是精確等式（S05）。真正改變數值的是四捨五入：把 −0.75 寫成 −0.8，而 −0.8≠−3/4（N21）。


- 5/0 是有理數，因為 5 與 0 都是整數 → reject — 定義要求 q≠0；而且沒有任何數 x 滿足 x·0=5（S08）。
- 6/(−8) 與 −3/4 外觀不同，所以是不同的有理數 → reject — 交叉乘積 6·4=24=(−3)·(−8)，依 L_cross 兩者相等（S03）。
- 把 6/(−8) 約成 −3/4 只是近似 → reject — a/b=(ak)/(bk)（k=−1/2≠0）是精確等式（S05）。
- 因為 1·3>1·(−2)，所以 1/(−2)>1/3 → reject — L_cross_order 需要分母為正；事實上 −1/2<1/3（N19）。





## 結論與限制

6/(−8)、−3/4、9/(−12) 是同一個有理數（交叉乘積 24=24、−72=−72），正規形式為 −3/4（gcd(3,4)=1，分母為正），約分是精確等式；2/3≠3/5（10≠9）；「5/0」不表示任何數；−1.25=−125/100=−5/4 與 7=7/1 都是有理數；分母為正時 −3/4<−2/3（−9<−8）。


- 本稿只檢查 −3/4 是正規形式，不證明每個有理數恰有一個正規形式（唯一性需要例如歐幾里得引理）。
- 與 Lean Rat.divInt、非零分母與正規化分子分母聲明的對接（MKO formal next）未在此處理。





## 驗證及來源綁定

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


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: 7082af66df1018fc25b71890f73e46bebc2e117da1918db747a20e274bd8bc19
- original source SHA-256: b6cd86f150bfd74850fefee9d1f793b0b5d8bf486f024406abf8d1a96e33ec1f
- Lean: NOT_RUN · independent AI: NOT_MEASURED

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