# 二元聯立一次方程組：唯一解公式、兩列核對與 D=0 的一致性判定 [← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-system-linear-equations/) 這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。 derivation-mko-system-linear-equations-01 · production-20261019-adopted-96 ## 目標與範圍 (I) 解 2x+3y=7、x−y=1：證明 D=ae−bd≠0 時的唯一解公式，求解並代入兩列核對；(II) 判定 x+2y=3、2x+4y=7；(III) 判定 x+2y=3、2x+4y=6；並以 (IV) 0x+0y=1、0x+0y=2 說明 D 與兩個 Cramer 分子都為零時不能斷定有無限多解。 在 MKO 的範圍內工作：實數未知數 x、y 的兩個方程；四組具體例子的係數為整數，一般唯一解公式則對 G1 的實數係數證明。完整證明 D≠0 時恰有一解及其公式；D=0 時以列運算（保持解集的等價變形）逐例判定無解或無限多解，並檢查零列。不給出 D=0 時一般的秩判準證明；不從示意直線交點猜解；不改動 canonical MKO 或英文 edition。 ## 已知條件與符號 - eq_congruence - distributive - mul_inverse_nonzero - mul_zero - numeric_evaluation - solution_def - G1 — 未知數 x、y 為實數；一般系統為 ax+by=c、dx+ey=f，係數與右側常數為實數；L(x,y)=(ax+by−c, dx+ey−f)，z=(0,0)，D=ae−bd。 - G2 — 系統 I：2x+3y=7、x−y=1，即 a=2、b=3、c=7、d=1、e=−1、f=1。 - G3 — 系統 II：x+2y=3、2x+4y=7；系統 III：x+2y=3、2x+4y=6；系統 IV：0x+0y=1、0x+0y=2（零係數列容許作為限制，MKO 假設 a2）。 - ax+by=c,\ dx+ey=f — 兩列方程（係數 a 到 f 為實數） - L(x,y) — (ax+by−c, dx+ey−f) - z — 零向量 (0,0) - D — ae−bd，二階行列式 - r_1,\ r_2 — 第一列、第二列方程 - r_2-\lambda r_1 — 第二列減去第一列的 λ 倍 ## 規則與來源 - eq_congruence · prerequisite — 等式同用：若 u=v，對兩邊做同一個有定義的運算 f，得 f(u)=f(v)。只對一邊做運算不屬於此規則。 - distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。 - mul_inverse_nonzero · prerequisite — 非零數的倒數：在 ℚ、ℝ、ℂ 中，若 u≠0，存在 1/u 使 u·(1/u)=1；對 u≠0 定義 v/u 為 v·(1/u)。u=0 時沒有倒數，v/0 不定義。 - mul_zero · prerequisite — 乘以零：u·0=0。理由：u·0=u·(0+0)=u·0+u·0，兩邊同減 u·0 得 0=u·0。 - numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。 - cartesian_product_def · prerequisite — 笛卡兒積：A×B 是所有有序對 (a,b)（a∈A、b∈B）的集合；(a,b)=(c,d) ⇔ a=c 且 b=d。 - 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）。 - mul_comm · prerequisite — 乘法交換律：uv=vu（在交換的數系中，例如 ℤ、ℚ、ℝ、ℂ）。 - add_inverse · prerequisite — 加法反元素：每個 u 都有 −u，使 u+(−u)=0；u−v 定義為 u+(−v)。 - mul_assoc · prerequisite — 乘法結合律：(uv)w=u(vw)。 - mul_one · prerequisite — 乘法單位元：1·u=u。 - add_assoc · prerequisite — 加法結合律：(u+v)+w=u+(v+w)。 - add_zero · prerequisite — 加法單位元：u+0=u。 - and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。 - set_extensionality · prerequisite — 集合相等：A=B 當且僅當 A⊆B 且 B⊆A，即兩者有相同元素。 - injective_surjective_def · prerequisite — 單射：f(a)=f(a′) ⇒ a=a′。滿射：每個 b∈B 都有 a∈A 使 f(a)=b。雙射：既單又滿，此時有唯一反函數 f⁻¹ 使 f⁻¹∘f=id_A、f∘f⁻¹=id_B。 - mko_linear_system · cited — 令 x、y 為實數未知數，要求 a x+b y=c 與 d x+e y=f 同時成立。令 L(x,y)=(a x+b y−c,d x+e y−f)，z=(0,0)，則解集滿足 L(x,y)=z。D=ae−bd≠0 時唯一解為 x=(ce−bf)/D、y=(af−cd)/D；D=0 時須檢查一致性，可能無解或無限多解。 · mko-system-linear-equations - solution_def · prerequisite — (x,y)∈ℝ² 是系統的解，當且僅當 L(x,y)=z，即兩個方程同時成立（有序對相等）。 - L_cramer · lemma — 若 D=ae−bd≠0，則系統 ax+by=c、dx+ey=f 恰有一解，即 x=(ce−bf)/D、y=(af−cd)/D。 - L_row_replace · lemma — 對任意實數 λ，系統 {ax+by=c, dx+ey=f} 與 {ax+by=c, (d−λa)x+(e−λb)y=f−λc} 有相同的解集。 ## 逐步主鏈 S01 · equivalent操作前 L(x,y)=z 操作後 ax+by=c\ \land\ dx+ey=f 條件：無 規則：solution_def · 依賴：G1, solution_def, mko_linear_system 葉節點依據：solution_def + cartesian_product_def + eq_congruence 依 MKO，解集由 L(x,y)=z 刻畫。L(x,y)=(ax+by−c, dx+ey−f) 與 z=(0,0) 相等，當且僅當兩個分量都是 0，即 ax+by−c=0 且 dx+ey−f=0，兩邊同加常數就是兩個方程同時成立。所以「解」永遠指同時滿足兩列的 (x,y)。 S02 · equivalent操作前 D=ae-bd 操作後 D=2\cdot(-1)-3\cdot 1=-5\neq 0 條件：無 規則：numeric_evaluation · 依賴：G2 葉節點依據：numeric_evaluation 代入 a=2、b=3、d=1、e=−1：D=2·(−1)−3·1=−2−3=−5，不為零。 S03 · theorem_application操作前 D=-5\neq 0 操作後 x=\frac{7\cdot(-1)-3\cdot 1}{-5}=2,\quad y=\frac{2\cdot 1-7\cdot 1}{-5}=1 條件：D\neq 0 規則：L_cramer · 依賴：S02, G2, L_cramer 葉節點依據：eq_congruence + distributive + mul_inverse_nonzero + frac_rules 因 D≠0，引理 L_cramer 適用：系統 I 恰有一解，x=(ce−bf)/D=(−7−3)/(−5)=2，y=(af−cd)/D=(2−7)/(−5)=1。所以唯一解是 (2,1)。引理在子步 S03.1 到 S03.4 證明。 S04 · implies操作前 (x,y)=(2,1) 操作後 2\cdot 2+3\cdot 1=7\ \land\ 2-1=1 條件：無 規則：numeric_evaluation · 依賴：S03, G2, solution_def 葉節點依據：numeric_evaluation + solution_def 獨立核對：把 (2,1) 代入兩列，第一列 4+3=7，第二列 2−1=1，兩列都成立。這一步不依賴公式，可以抓出代入公式時的計算錯誤。 S05 · implies操作前 (x,y)=(5,-1) 操作後 2\cdot 5+3\cdot(-1)=7,\ \ 5-(-1)=6\neq 1 條件：無 規則：solution_def · 依賴：G2, solution_def 葉節點依據：solution_def + numeric_evaluation 只代入一列的陷阱：(5,−1) 使第一列成立（10−3=7），但第二列給 5−(−1)=6≠1。依解的定義必須兩列同時成立，所以 (5,−1) 不是系統 I 的解。這也與 S03 的唯一解 (2,1) 一致。 S06 · implies操作前 x+2y=3,\ 2x+4y=7 操作後 D=1\cdot 4-2\cdot 2=0 條件：無 規則：mko_linear_system · 依賴：G3, mko_linear_system 葉節點依據：mko_linear_system + numeric_evaluation 系統 II 的 D=1·4−2·2=0，所以 L_cramer 不適用，公式中的除法沒有定義。依 MKO，D=0 時必須另外檢查一致性。（它的 Cramer 分子 ce−bf=3·4−2·7=−2≠0，但本稿不以分子作判準，而用 S07 的列運算直接判定。） S07 · equivalent操作前 x+2y=3\ \land\ 2x+4y=7 操作後 x+2y=3\ \land\ 0x+0y=1 條件：\lambda=2 規則：L_row_replace · 依賴：S06, L_row_replace 葉節點依據：eq_congruence + distributive + numeric_evaluation 依引理 L_row_replace，取 λ=2，把第二列換成第二列減第一列的 2 倍：(2−2·1)x+(4−2·2)y=7−2·3，即 0x+0y=1。新系統與原系統解集相同。 S08 · implies操作前 0x+0y=1 操作後 0=1\ \text{for every}\ (x,y),\ \text{solution set of II}=\varnothing 條件：無 規則：mul_zero · 依賴：S07, mul_zero, add_zero 葉節點依據：mul_zero + add_zero + numeric_evaluation 對每個 (x,y)，0x+0y=0+0=0（乘以零、加法單位元），所以 0x+0y=1 等於要求 0=1，沒有任何 (x,y) 滿足。依 S07 的等價，系統 II 無解。MKO 假設 a2：0=c≠0 的零列不一致。 S09 · equivalent操作前 x+2y=3\ \land\ 2x+4y=6 操作後 x+2y=3\ \land\ 0x+0y=0\ \Leftrightarrow\ x+2y=3 條件：\lambda=2 規則：L_row_replace · 依賴：G3, L_row_replace, mul_zero, add_zero 葉節點依據：eq_congruence + distributive + mul_zero + add_zero + and_intro_elim 系統 III 的 D 也是 1·4−2·2=0。取 λ=2 做同樣的列運算：第二列變成 0x+0y=6−2·3=0。對每個 (x,y)，0x+0y=0 恆成立，不加任何限制（MKO 假設 a2），所以系統 III 等價於單一方程 x+2y=3。 S10 · equivalent操作前 \{(x,y)\in\mathbb{R}^2\mid x+2y=3\} 操作後 \{(3-2t,\,t)\mid t\in\mathbb{R}\} 條件：無 規則：set_extensionality · 依賴：S09, set_extensionality 葉節點依據：set_extensionality + eq_congruence + add_inverse + numeric_evaluation ⊆：若 x+2y=3，取 t=y，則 x=3−2t（兩邊同減 2y），所以 (x,y)=(3−2t,t)。⊇：對任意實數 t，(3−2t)+2t=3（N17），所以 (3−2t,t) 是解。兩個方向都成立，依集合相等兩集合相同。 S11 · implies操作前 \{(3-2t,\,t)\mid t\in\mathbb{R}\} 操作後 \text{infinitely many solutions, e.g.}\ (3,0),\ (1,1) 條件：無 規則：cartesian_product_def · 依賴：S10, cartesian_product_def 葉節點依據：cartesian_product_def + injective_surjective_def + numeric_evaluation 不同的 t 給出不同的解，因為第二分量就是 t（有序對相等需要第二分量相等）。ℝ 有無限多個元素，所以系統 III 有無限多解。例：t=0 得 (3,0)，t=1 得 (1,1)；兩者都滿足原系統的兩列：3+0=3、6+0=6；1+2=3、2+4=6（N18 對一般 t 核對第二列）。 S12 · implies操作前 0x+0y=1,\ 0x+0y=2 操作後 D=0,\ ce-bf=0,\ af-cd=0,\ \text{yet no solution} 條件：無 規則：mul_zero · 依賴：G3, mul_zero, add_zero 葉節點依據：mul_zero + add_zero + numeric_evaluation 系統 IV：a=b=d=e=0、c=1、f=2。D=0·0−0·0=0，ce−bf=1·0−0·2=0，af−cd=0·2−1·0=0，三者都是零。但第一列對每個 (x,y) 都讀作 0=1，為假，所以系統無解。可見「D 與兩個 Cramer 分子都為零」不能推出無限多解，必須先檢查不一致的零列（MKO 第三段）。 S13 · implies操作前 \text{S03, S04, S08, S10, S11, S12} 操作後 \text{I}:\ \{(2,1)\};\ \text{II}:\ \varnothing;\ \text{III}:\ \{(3-2t,t)\mid t\in\mathbb{R}\};\ \text{IV}:\ \varnothing 條件：無 規則：and_intro_elim · 依賴：S03, S04, S08, S10, S11, S12 葉節點依據：and_intro_elim 彙整：系統 I 的 D=−5≠0，唯一解 (2,1)，已代入兩列核對；系統 II 的 D=0，列運算出現 0=1，無解；系統 III 的 D=0，列運算得 0=0，解集為 {(3−2t,t) ∣ t∈ℝ}，無限多解；系統 IV 三個行列式值都是零，但無解。 ## 局部子步與引理 S03.1 · implies操作前 ax+by=c\ \land\ dx+ey=f 操作後 (ae-bd)x=ce-bf 條件：無 規則：eq_congruence · 依賴：eq_congruence, distributive 葉節點依據：eq_congruence + distributive + mul_comm + add_inverse 設 (x,y) 是解。第一列兩邊乘 e、第二列兩邊乘 b，再相減：e(ax+by)−b(dx+ey)=ec−bf。左邊展開為 aex+bey−bdx−bey=(ae−bd)x（N4 核對這個恆等式）。所以任何解都滿足 (ae−bd)x=ce−bf。 S03.2 · implies操作前 ax+by=c\ \land\ dx+ey=f 操作後 (ae-bd)y=af-cd 條件：無 規則：eq_congruence · 依賴：eq_congruence, distributive 葉節點依據：eq_congruence + distributive + mul_comm + add_inverse 同理消去 x：第二列乘 a、第一列乘 d，再相減：a(dx+ey)−d(ax+by)=af−dc。左邊展開為 adx+aey−adx−bdy=(ae−bd)y（N5）。所以任何解都滿足 (ae−bd)y=af−cd。 S03.3 · implies操作前 Dx=ce-bf,\quad Dy=af-cd,\quad D\neq 0 操作後 x=\frac{ce-bf}{D},\quad y=\frac{af-cd}{D} 條件：D\neq 0 規則：mul_inverse_nonzero · 依賴：S03.1, S03.2, mul_inverse_nonzero 葉節點依據：mul_inverse_nonzero + eq_congruence + mul_assoc + mul_one 因 D≠0，1/D 存在，兩式同乘 1/D 得 x 與 y 的值。所以任何解都等於這一對數：解至多一個（唯一性）。若 D=0，1/D 不存在，這一步不能做，這正是 MKO 說「不得在 D=0 時套唯一解除法」的原因。 S03.4 · implies操作前 x_0=\frac{ce-bf}{D},\ y_0=\frac{af-cd}{D} 操作後 ax_0+by_0=c\ \land\ dx_0+ey_0=f 條件：D\neq 0 規則：frac_rules · 依賴：frac_rules, distributive 葉節點依據：frac_rules + distributive + mul_comm + add_inverse + mul_inverse_nonzero 存在性：代回第一列，ax₀+by₀=(a(ce−bf)+b(af−cd))/D=(ace−abf+abf−bcd)/D=c(ae−bd)/D=c；代回第二列，dx₀+ey₀=(d(ce−bf)+e(af−cd))/D=(cde−bdf+aef−cde)/D=f(ae−bd)/D=f（N6、N7 核對兩個恆等式）。S03.1 到 S03.4 合起來證得引理 L_cramer：D≠0 時恰有一解。 S07.1 · equivalent操作前 ax+by=c\ \land\ dx+ey=f 操作後 ax+by=c\ \land\ (d-\lambda a)x+(e-\lambda b)y=f-\lambda c 條件：無 規則：eq_congruence · 依賴：eq_congruence, distributive 葉節點依據：eq_congruence + distributive + add_inverse + add_assoc ⇒：設兩列成立。第一列兩邊乘 λ 得 λ(ax+by)=λc；從第二列兩邊減去它：(dx+ey)−λ(ax+by)=f−λc，依分配律整理為 (d−λa)x+(e−λb)y=f−λc；第一列保留不變。⇐：設新系統成立，把第一列的 λ 倍加回新第二列，得 dx+ey=f。兩向都只用「對等式兩邊做同一運算」。這證得引理 L_row_replace。 ## 逐步反向審查 - S13 · sufficient_goal_reduction · S03, S04, S08, S10, S11, S12, and_intro_elim — 目標 G：四個系統的判定。足夠條件 H：所列各步的結論；H⇒G 只是合取，H 由 G1 到 G3 正向證成，沒有把 G 當作前提。 - S12 · premise_audit · mul_zero, add_zero, numeric_evaluation — 一個具體反例就足以否定這個一般說法（N19 到 N21）；此步不給出 D=0 時的一般判準。 - S11 · premise_audit · S10, cartesian_product_def — 需要參數化是單射（不同 t 不同解）；例子只是示範，結論來自參數化。 - S10 · inverse_equivalence · set_extensionality, eq_congruence — 兩個包含都已證明，所以是集合相等。 - S09 · inverse_equivalence · L_row_replace, mul_zero, add_zero, and_intro_elim — 列運算雙向保持解集；與恆真條件做合取不改變真假，雙向成立。 - S08 · premise_audit · mul_zero, add_zero, S07 — 需要 S07 的解集等價；只因 D=0 不能推出無解，必須看到不一致的零列。 - S07.1 · inverse_equivalence · eq_congruence, distributive — 兩向都有理由；關鍵是第一列被保留，所以可以把它的 λ 倍加回去。 - S07 · inverse_equivalence · L_row_replace — 引理兩向在 S07.1 證明：減去 2 倍第一列，與加回 2 倍第一列，互為反運算。 - S06 · premise_audit · mko_linear_system, numeric_evaluation — D 的計算可重算（N12、N22）；此步只排除公式，不判定解集。 - S05 · premise_audit · solution_def, numeric_evaluation — 一列失敗就足以排除（N10、N11）。 - S04 · premise_audit · solution_def, numeric_evaluation — 必須代入兩列（N8、N9）；唯一性另由 S03.3 保證，不由這次代入推出。 - S03.4 · premise_audit · frac_rules, distributive, mul_inverse_nonzero — 同分母相加與約去 D 都需要 D≠0。唯一性（S03.3）加存在性（此步）才是「恰有一解」。 - S03.3 · premise_audit · S03.1, S03.2, mul_inverse_nonzero — 此步只給唯一性；這一對數確實是解（存在性）另在 S03.4 證明。 - S03.2 · premise_audit · eq_congruence, distributive — 同 S03.1，只是必要條件，不宣稱反向。 - S03.1 · premise_audit · eq_congruence, distributive — 這是必要條件：只推出 x 必須滿足的方程，反向不宣稱（D=0 時這一行可能是 0=0，什麼也不限制）。 - S03 · premise_audit · S02, L_cramer — 唯一的前提是 D≠0（S02）；數值見 N2、N3。D=0 時這一步不可用。 - S02 · inverse_equivalence · numeric_evaluation — 精確整數計算，可重算（N1）。 - S01 · inverse_equivalence · cartesian_product_def, eq_congruence — 有序對相等是雙向的；兩邊同加或同減常數也是雙向的。 ## 錯誤控制與反例 只代入一列不夠MKO 指出的誤解之一是只代入一列。(5,−1) 滿足 2x+3y=7，卻使 x−y=6≠1（S05）。驗證候選解必須代入兩列，且若候選值含分母，要先確認分母非零。 D=0 時不能除MKO 的第二個誤解是在 D=0 時套用除法。系統 II 與 III 的 D 都是 0，結果卻一個無解、一個有無限多解（S08、S11）；公式除以 0 沒有定義，也分辨不出這兩種情況。必須用保持解集的列運算或一致性檢查來判定。 不要忽略 0=非零 的零列MKO 的第三個誤解是忽略不一致零列。0x+0y=c 在 c≠0 時對任何 (x,y) 都不成立，整個系統因此無解（S08、S12）。系統 IV 的 D 與兩個 Cramer 分子都為零，若只看這三個數會誤判為無限多解。 - (5,−1) 滿足 2x+3y=7，所以是系統 I 的解 → reject — 第二列 5−(−1)=6≠1；解必須同時滿足兩列。 - 系統 II 的解是 x=(3·4−2·7)/0 → reject — 除以 0 沒有定義；系統 II 經列運算出現 0=1，無解。 - 系統 IV 的 D 與兩個 Cramer 分子都為零，所以有無限多解 → reject — 第一列對每個 (x,y) 都是 0=1，為假，所以無解。 - 系統 III 的解只有 (3,0) → reject — (1,1) 也滿足兩列；解集是 {(3−2t,t) ∣ t∈ℝ}，有無限多個。 ## 結論與限制 D≠0 時系統恰有一解 x=(ce−bf)/D、y=(af−cd)/D（已完整證明）。系統 I（D=−5）的唯一解是 (2,1)，兩列都已核對；(5,−1) 只滿足一列，不是解。系統 II（D=0）化為 0=1，無解；系統 III（D=0）化為 x+2y=3，解集 {(3−2t,t) ∣ t∈ℝ}，無限多解；系統 IV 的 D 與兩個 Cramer 分子都為零，卻無解。 - D=0 時一般的秩與增廣矩陣一致性判準未在本稿證明；系統 II、III、IV 是逐例以列運算或零列判定。 - N4 到 N7 是多項式恆等式的格點核對（每個變數次數至多 2），對應 S03.1 到 S03.4 的代數展開；論證不依賴它們。 ## 驗證及來源綁定 22 個本稿宣告算術檢查；只支持所列算式。 - source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f - adopted source SHA-256: 0f098bbbe0d8574f864b3569777f182c32f28dd1c5a192d61ca7d28c7748ec19 - original source SHA-256: 2f1efd35aa77f21aa1e0568cb94972c9eea89944a758fa7c0c901c5d58cc423a - Lean: NOT_RUN · independent AI: NOT_MEASURED [同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-system-linear-equations-01.json)