# 方程式：在定義域內解 x²/(x−1)=1/(x−1)

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

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

derivation-mko-equation-01 · production-20261019-adopted-96



## 目標與範圍

在允許範圍 ℝ 中，求方程 x²/(x−1)=1/(x−1) 的解集；並說明為什麼兩邊乘以 x−1 後得到的方程 x²=1 有兩個解，而原方程只有一個。

依 MKO 的定義：解集由使兩側都有定義且相等的允許 x 組成。只處理一個含分式的實數方程，示範定義域、乘以非零式的等價變形、零乘積、排除候選值與代回核對。不處理一般有理方程的理論或複數解；不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- mul_inverse_nonzero
- eq_congruence
- distributive
- zero_product
- set_builder
- numeric_evaluation


- G1 — 允許範圍與運算：變數 x 取值於 ℝ；使用實數的加、減、乘、除，v/u 只在 u≠0 時有定義（mul_inverse_nonzero）。
- G2 — 方程：L(x)=R(x)，其中 L(x)=x²/(x−1)，R(x)=1/(x−1)。
- G3 — 解集的定義（MKO）：𝒮={x∈ℝ ∣ L(x) 與 R(x) 都有定義且 L(x)=R(x)}。


- L(x)=\frac{x^2}{x-1} — 左側表達式
- R(x)=\frac{1}{x-1} — 右側表達式
- D — 兩側都有定義的 x 所成的集合
- \mathcal{S} — 原方程的解集
- u\neq 0 — 非零條件；除以 u 或使用 1/u 都需要它





## 規則與來源


- mul_inverse_nonzero · prerequisite — 非零數的倒數：在 ℚ、ℝ、ℂ 中，若 u≠0，存在 1/u 使 u·(1/u)=1；對 u≠0 定義 v/u 為 v·(1/u)。u=0 時沒有倒數，v/0 不定義。
- eq_congruence · prerequisite — 等式同用：若 u=v，對兩邊做同一個有定義的運算 f，得 f(u)=f(v)。只對一邊做運算不屬於此規則。
- distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。
- zero_product · prerequisite — 零乘積性質：在 ℤ、ℚ、ℝ、ℂ（或任何整域）中，uv=0 ⇔ u=0 或 v=0。
- set_builder · prerequisite — 集合建構式：x∈{y∈A ∣ P(y)} 當且僅當 x∈A 且 P(x)。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
- add_assoc · prerequisite — 加法結合律：(u+v)+w=u+(v+w)。
- add_inverse · prerequisite — 加法反元素：每個 u 都有 −u，使 u+(−u)=0；u−v 定義為 u+(−v)。
- add_zero · prerequisite — 加法單位元：u+0=u。
- eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。
- add_comm · prerequisite — 加法交換律：u+v=v+u。
- mul_assoc · prerequisite — 乘法結合律：(uv)w=u(vw)。
- mul_one · prerequisite — 乘法單位元：1·u=u。
- mul_comm · prerequisite — 乘法交換律：uv=vu（在交換的數系中，例如 ℤ、ℚ、ℝ、ℂ）。
- neg_mul · prerequisite — 負號與乘法：(−u)v=−(uv)，(−u)(−v)=uv。
- logic_chain · prerequisite — 推論的傳遞：由 P⇒Q 與 Q⇒R 得 P⇒R；⇔ 同理。
- set_extensionality · prerequisite — 集合相等：A=B 當且僅當 A⊆B 且 B⊆A，即兩者有相同元素。
- case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
- 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）。
- and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
- mko_equation · cited — 給定兩個具有共同語境的表達式 L(x)、R(x)，方程式 L(x)=R(x) 的解集由所有使兩側皆有定義且值相等的允許 x 組成。 · mko-equation
- L_zero_diff · lemma — 對實數 u、c：u−c=0 ⇔ u=c。
- L_den · lemma — 對實數 a、b 與 u≠0：a/u=b/u ⇔ a=b。





## 逐步主鏈

S01 · definition操作前

L(x)=R(x)\ \text{over}\ \mathbb{R}

操作後

\mathcal{S}=\{x\in\mathbb{R}\mid L(x),R(x)\ \text{defined}\ \land\ L(x)=R(x)\}

條件：無

規則：mko_equation · 依賴：G1, G2, G3

葉節點依據：mko_equation + set_builder

依 MKO，方程的解集不是「讓式子看起來相等的數」，而是同時滿足兩個條件的允許 x：兩側都有定義，而且值相等。這裡允許範圍是 ℝ，運算是實數運算（G1）。之後每一步都要同時追蹤「有定義」與「相等」這兩個條件。



S02 · equivalent操作前

L(x)\ \text{and}\ R(x)\ \text{defined}

操作後

x-1\neq 0

條件：無

規則：mul_inverse_nonzero · 依賴：G1, G2

葉節點依據：mul_inverse_nonzero + def_unfold

L(x)=x²/(x−1) 與 R(x)=1/(x−1) 各只含一個除法，除數都是 x−1；分子 x² 與 1 對每個實數都有定義。依 mul_inverse_nonzero，v/u 有定義當且僅當 u≠0，所以兩側都有定義 ⇔ x−1≠0。



S03 · equivalent操作前

x-1\neq 0

操作後

x\neq 1;\quad D=\{x\in\mathbb{R}\mid x\neq 1\}

條件：無

規則：L_zero_diff · 依賴：S02

葉節點依據：eq_congruence + add_assoc + add_inverse + add_zero

依引理 L_zero_diff（u=x、c=1），x−1=0 ⇔ x=1；兩邊同取否定得 x−1≠0 ⇔ x≠1。所以兩側都有定義的 x 恰是 D={x∈ℝ ∣ x≠1}，而且 𝒮⊆D。



S04 · equivalent操作前

\frac{x^2}{x-1}=\frac{1}{x-1},\ x\in D

操作後

x^2=1,\ x\in D

條件：x-1\neq 0

規則：L_den · 依賴：S03, G2

葉節點依據：eq_congruence + mul_inverse_nonzero + mul_assoc + mul_one

對 x∈D，x−1≠0。依引理 L_den（a=x²、b=1、u=x−1）：x²/(x−1)=1/(x−1) ⇔ x²=1。這個等價只在 D 中成立：它的條件 u≠0 正是 x∈D。



S05 · equivalent操作前

x^2=1

操作後

x^2-1=0

條件：無

規則：L_zero_diff · 依賴：S04

葉節點依據：eq_congruence + add_inverse + add_assoc + add_zero

依引理 L_zero_diff（u=x²、c=1）：x²−1=0 ⇔ x²=1。把方程整理成「某式=0」，才能使用零乘積性質。



S06 · equivalent操作前

x^2-1=0

操作後

(x-1)(x+1)=0

條件：無

規則：distributive · 依賴：S05

葉節點依據：distributive + neg_mul + add_inverse + eq_replace

依分配律：(x−1)(x+1)=x·x+x·1−1·x−1·1=x²+x−x−1=x²−1。兩式對每個實數相等，代換後等式真假不變。



S07 · equivalent操作前

(x-1)(x+1)=0

操作後

x-1=0\ \lor\ x+1=0

條件：無

規則：zero_product · 依賴：S06

葉節點依據：zero_product

依零乘積性質（ℝ 沒有零因子）：兩個實數的積為 0，當且僅當至少一個因子為 0。



S08 · equivalent操作前

x-1=0\ \lor\ x+1=0

操作後

x=1\ \lor\ x=-1

條件：無

規則：L_zero_diff · 依賴：S07

葉節點依據：eq_congruence + add_inverse + add_zero + numeric_evaluation

依引理 L_zero_diff：x−1=0 ⇔ x=1；又 x+1=x−(−1)，所以 x+1=0 ⇔ x=−1。兩個析取支各自等價變形，析取前後同真同假。



S09 · equivalent操作前

x\in D:\ L(x)=R(x)

操作後

\mathcal{S}=\{x\in\mathbb{R}\mid x\in D\ \land\ (x=1\lor x=-1)\}

條件：x\in D

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

葉節點依據：logic_chain + set_builder

S04 到 S08 每一步都是 x∈D 條件下的等價，依推論的傳遞串起來：對 x∈D，L(x)=R(x) ⇔ x=1 ∨ x=−1。再配合 S01 與 S03（有定義 ⇔ x∈D），得 𝒮={x∈ℝ ∣ x∈D 且 (x=1 或 x=−1)}。



S10 · implies操作前

x=1

操作後

1\notin D,\ \text{so}\ 1\notin\mathcal{S}

條件：無

規則：set_builder · 依賴：S03, S09

葉節點依據：set_builder + numeric_evaluation

候選值 x=1：1−1=0，所以 1∉D，L(1) 與 R(1) 都含除以 0，都沒有定義。依 S09 的集合條件，1∉𝒮。這個候選值滿足 x²=1，但不屬於原方程的解集。



S11 · implies操作前

x=-1

操作後

-1\in D,\ \text{so}\ -1\in\mathcal{S}

條件：-1-1\neq 0

規則：set_builder · 依賴：S03, S09

葉節點依據：set_builder + numeric_evaluation

候選值 x=−1：−1−1=−2≠0，所以 −1∈D；而且 x=−1 滿足析取的第二支。依 S09 的集合條件，兩個合取項都成立，所以 −1∈𝒮。



S12 · implies操作前

x\in\mathcal{S}\iff x\in D\land(x=1\lor x=-1)

操作後

\mathcal{S}=\{-1\}

條件：無

規則：set_extensionality · 依賴：S09, S10, S11

葉節點依據：set_extensionality + case_analysis

對任意 x：若 x∈𝒮，則 x∈D 且 x=1 或 x=−1；x=1 與 x∈D 不相容（S10），所以 x=−1。反之 x=−1 時 x∈𝒮（S11）。兩個包含合起來，依集合相等，𝒮={−1}。



S13 · implies操作前

x=-1\ \text{in}\ L,\ R

操作後

L(-1)=\frac{1}{-2}=-\tfrac{1}{2}=R(-1)

條件：無

規則：numeric_evaluation · 依賴：S12, G2

葉節點依據：numeric_evaluation + frac_rules

依 MKO，驗證候選解要把值代入原方程，兩側分別計算：L(−1)=(−1)²/(−1−1)=1/(−2)=−1/2；R(−1)=1/(−1−1)=−1/2。兩側都有定義且相等，與 S12 一致。



S14 · implies操作前

\{x\in\mathbb{R}\mid x^2=1\}

操作後

\{-1,1\}\supsetneq\mathcal{S}=\{-1\}

條件：無

規則：set_extensionality · 依賴：S05, S06, S07, S08, S12

葉節點依據：set_extensionality + logic_chain

若忽略定義域，把兩邊乘以 x−1 後在整個 ℝ 上解 x²=1，S05 到 S08 的等價（它們不依賴 x∈D）給出 {−1,1}。多出來的 1 正是乘數 x−1 為 0 的地方：乘以 x−1 能把原方程的解帶到新方程，但在 x−1=0 處不能乘 1/(x−1) 回去，所以新方程多了一個不屬於原方程的解。



S15 · implies操作前

\mathcal{S}=\{-1\},\ \{x\mid x^2=1\}=\{-1,1\}

操作後

\text{answer: }\mathcal{S}=\{-1\};\ 1\ \text{excluded since}\ 1\notin D

條件：無

規則：and_intro_elim · 依賴：S12, S13, S14

葉節點依據：and_intro_elim

原方程 x²/(x−1)=1/(x−1) 在 ℝ 中的解集是 {−1}；x²=1 的另一個解 1 因兩側在 x=1 沒有定義而被排除。







## 局部子步與引理

S03.1 · equivalent操作前

u-c=0

操作後

(u-c)+c=0+c

條件：無

規則：eq_congruence · 依賴：eq_congruence

葉節點依據：eq_congruence + add_inverse

兩邊同加 c。反向是兩邊同加 −c，再依 S03.2 的同類化簡。



S03.2 · equivalent操作前

(u-c)+c=0+c

操作後

u=c

條件：無

規則：eq_replace · 依賴：S03.1

葉節點依據：add_assoc + add_comm + add_inverse + add_zero + eq_replace

左邊 (u+(−c))+c=u+((−c)+c)=u+0=u（u−c 的意義、結合律、交換律、反元素、單位元）；右邊 0+c=c。S03.1 與 S03.2 合起來證得引理 L_zero_diff。



S04.1 · equivalent操作前

\frac{a}{u}=\frac{b}{u}

操作後

\frac{a}{u}\cdot u=\frac{b}{u}\cdot u

條件：u\neq 0

規則：eq_congruence · 依賴：eq_congruence, mul_inverse_nonzero

葉節點依據：eq_congruence + mul_inverse_nonzero + mul_assoc

向前：兩邊同乘 u。向後：兩邊同乘 1/u，需要 u≠0，因為 ((a/u)u)(1/u)=(a/u)(u·(1/u))=a/u。所以在 u≠0 時兩式等價。



S04.2 · equivalent操作前

\frac{a}{u}\cdot u=\frac{b}{u}\cdot u

操作後

a=b

條件：u\neq 0

規則：eq_replace · 依賴：S04.1

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

依 a/u=a·(1/u)：(a·(1/u))u=a((1/u)u)=a·1=a；右邊同理得 b。S04.1 與 S04.2 合起來證得引理 L_den。







## 逐步反向審查


- S15 · sufficient_goal_reduction · S12, S13, S14, and_intro_elim — 目標 G：求 𝒮 並說明 x²=1 多出的解。足夠條件 H：S12（𝒮={−1}）與 S14（多出的解來自 x−1=0）；H⇒G 直接成立。H 由 G1 到 G3 正向證成，沒有把 G 當作前提；S13 是獨立核對。
- S14 · premise_audit · S05, S08, S12, set_extensionality — 兩集合只差 1，而 1∉D；這解釋了差異，但不宣稱乘以任何式子都只會多出乘數的零點以外沒有別的影響。
- S13 · premise_audit · S12, G2, numeric_evaluation — 這是對 x=−1 的獨立核對；它確認 −1 是解，但不能單獨證明沒有其他解，那由 S04 到 S12 的等價鏈負責。
- S12 · premise_audit · S10, S11, set_extensionality, case_analysis — 需要兩個包含：𝒮⊆{−1} 用 S10 排除 x=1，{−1}⊆𝒮 用 S11。
- S11 · premise_audit · S03, S09, set_builder — 兩個合取項都檢查了：x∈D 與 x=1∨x=−1。
- S10 · premise_audit · S03, S09, set_builder — 只需 1 不滿足合取項 x∈D；不必（也無法）計算兩側的值。
- S09 · inverse_equivalence · logic_chain, S04, S08 — 每一環都是雙向的，而且 S04 只在 x∈D 中使用；所以串起來的等價也只在 D 中成立，並把 x∈D 保留在集合條件裡。
- S08 · inverse_equivalence · L_zero_diff, numeric_evaluation — 代回：1−1=0、(−1)+1=0；兩支都是雙向等價。
- S07 · inverse_equivalence · zero_product — 向前需要 ℝ 沒有零因子；向後用 u·0=0。兩個方向都包含在 zero_product 中。
- S06 · inverse_equivalence · distributive, eq_replace — 這是對所有實數成立的恆等式（N4 是獨立的多項式核對），等值代換雙向成立。
- S05 · inverse_equivalence · L_zero_diff — 引理兩向都已證；這一步對每個實數成立，不依賴 x∈D。
- S04.2 · inverse_equivalence · mul_assoc, mul_comm, mul_inverse_nonzero, mul_one — 等值代換雙向成立；(1/u)u=1 需要 u≠0。
- S04.1 · inverse_equivalence · eq_congruence, mul_inverse_nonzero, mul_assoc — 向後乘以 1/u 需要 u≠0。若 u=0，a/u 與 b/u 原本就未定義，不能先乘 0 再把它們算成 0。另對已定義的實數式，乘以 0 雖會把兩邊變成 0，卻會失去原式資訊；這是另一個警告，不是本步在 u=0 的求值。
- S04 · inverse_equivalence · L_den, S03 — 反向是兩邊同乘 1/(x−1)，需要 x−1≠0；在 D 之外（x=1）反向不能做，所以這裡一直帶著「x∈D」。
- S03.2 · inverse_equivalence · add_assoc, add_comm, add_inverse, add_zero — 只把式子換成相等的式子，等式真假不變，雙向成立。
- S03.1 · inverse_equivalence · eq_congruence, add_inverse — 加 c 與加 −c 互為反運算，對任何實數都可做，沒有附加條件。
- S03 · inverse_equivalence · L_zero_diff — 等價的兩邊同取否定仍是等價；引理的兩個方向都在子步證明。
- S02 · inverse_equivalence · mul_inverse_nonzero — 若 x−1≠0，1/(x−1) 存在，兩側都有定義；若 x−1=0，兩側都含除以 0，都沒有定義。兩個方向都有理由。
- S01 · premise_audit · G1, G2, G3, mko_equation — 此步只寫出解集的定義，不推出新事實。





## 錯誤控制與反例

乘以可能為零的式子MKO 列出的誤解包括「乘零後仍宣稱解集不變」與「除以可能為零的式子」。兩邊乘以 x−1 只在 x−1≠0 時是等價變形（S04）；在 x=1 處乘數為 0，變形不可逆，x²=1 因而多出解 1（S14）。正確做法是先寫出定義域 D={x ∣ x≠1}，並在整條等價鏈中保留 x∈D。

求得候選值後要代回原式MKO 提醒求得候選值後要代回原式檢查。候選值 1 代入原式時兩側都是除以 0，沒有定義，所以不是解（S10）；候選值 −1 代入後兩側都是 −1/2（S13）。只把候選值代入 x²=1 檢查會錯把 1 當成解，因為 x²=1 已經不是原方程。

約分也不能丟掉定義域類似的方程 (x²−1)/(x−1)=2，若先約分寫成 x+1=2，會得 x=1；但 x=1 時左側除以 0，沒有定義。約分 (x²−1)/(x−1)=x+1 只在 x≠1 時成立，所以這個方程的解集是空集。只化簡一側時，必須連同它成立的條件一起帶著。


- 原方程的解集是 {−1,1} → reject — x=1 時 1−1=0，兩側都沒有定義，1∉𝒮（S10）。
- x=1 是解，因為 1²=1 → reject — 那是在檢查 x²=1，不是原方程；原方程在 x=1 兩側都沒有定義。
- 兩邊同乘一個式子永遠不改變解集 → reject — x=2 兩邊乘 0 得 0=0，解集從 {2} 變成 ℝ；本題乘以 x−1 也多出解 1（S14）。
- x²/(x−1) 本身就是一個方程 → reject — 它沒有等號，只是一個表達式（方程的一側）；沒有另一側就沒有解集。





## 結論與限制

在 ℝ 中，x²/(x−1)=1/(x−1) 的解集是 {−1}。兩側只在 x≠1 時有定義；在這個範圍內方程等價於 x²=1，即 x=1 或 x=−1，而 x=1 不在定義域內。兩邊乘以 x−1 後的方程 x²=1 有解 {−1,1}，多出的 1 正是乘數 x−1 為零之處。


- 本稿只處理一個具體方程；一般有理方程（多個分母、高次分子）需要同樣的定義域追蹤，但不在此證明。
- 零乘積性質與分式規則以規則表中的前提使用，不在此由域公理推出。





## 驗證及來源綁定

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


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: 70e4d5766cd19e87cc7a8b9f5a847402b534f1a14a56165b9364b027e1664496
- original source SHA-256: 105cc4d24c32a42632c2fa35bdefc5573f9ebff81adc1112f41ccac5a8a97832
- Lean: NOT_RUN · independent AI: NOT_MEASURED

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