# 複數：以有序對計算 (2+3i)(4−5i) 並判定相等

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

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

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



## 目標與範圍

設 z=2+3i、w=4−5i。以有序對（實部, 虛部係數）求 z+w、z−w 與 z·w。乘法先由分配律與 i²=−1 推出一般公式 (a+bi)(c+di)=(ac−bd)+(ad+bc)i，再代入數值，並以直接展開交叉核對；最後判定 z·w 是否等於實數 23。

在 MKO 範圍內工作：整數實部與虛部係數（視為實數特例），加、減、乘三種運算，答案以有序對表示；不做複數除法、共軛、模或極式。ℂ 中加法與乘法的交換、結合與分配律作為前提使用，不在本稿由有序對構造推出。不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- distributive
- mul_assoc
- mul_comm
- add_comm
- add_assoc
- numeric_evaluation


- G1 — z=2+3i，w=4−5i；實部與虛部係數都是整數。
- G2 — 答案以有序對（實部, 虛部係數）表示；分量次序是語義資料，不由圖形位置或未標刻度補值；本稿不做複數除法（MKO 假設 a1、a2）。


- z=a+bi — 實部 a、虛部係數 b 的複數
- (a,b) — z 對應的有序對，次序為（實部, 虛部係數）
- i — 虛數單位，滿足 i^2=-1
- z,\ w — 本稿的兩個給定複數





## 規則與來源


- distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。
- mul_assoc · prerequisite — 乘法結合律：(uv)w=u(vw)。
- mul_comm · prerequisite — 乘法交換律：uv=vu（在交換的數系中，例如 ℤ、ℚ、ℝ、ℂ）。
- add_comm · prerequisite — 加法交換律：u+v=v+u。
- add_assoc · prerequisite — 加法結合律：(u+v)+w=u+(v+w)。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- add_inverse · prerequisite — 加法反元素：每個 u 都有 −u，使 u+(−u)=0；u−v 定義為 u+(−v)。
- neg_mul · prerequisite — 負號與乘法：(−u)v=−(uv)，(−u)(−v)=uv。
- forall_elim · prerequisite — ∀消去（代入特例）：若 ∀x∈D, P(x) 成立且 a∈D，則 P(a) 成立。
- and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
- contradiction · prerequisite — 反證法：若假設 ¬P 推出矛盾（某命題與其否定同時成立），則 P 成立。
- mko_complex_def · cited — 複數 z=a+bi 由實部 a 與虛部係數 b 唯一決定，可視為複平面有序對 (a,b)。加減逐分量進行，乘法由分配律與 i²=−1 導出。 · mko-complex-number
- complex_pair_eq · prerequisite — 對實數 a、b、c、d：a+bi=c+di 當且僅當 a=c 且 b=d；因此 a+bi 與有序對 (a,b) 一一對應。
- complex_addsub · prerequisite — 逐分量加減：(a+bi)+(c+di)=(a+c)+(b+d)i，(a+bi)−(c+di)=(a−c)+(b−d)i。
- i_squared · prerequisite — 虛數單位滿足 i²=i·i=−1。
- real_embedding · prerequisite — 實數 r 嵌入為複數 r+0i，對應有序對 (r,0)。
- L_complex_mul · lemma — 對所有實數 a、b、c、d：(a+bi)(c+di)=(ac−bd)+(ad+bc)i；以有序對表示即 (a,b)·(c,d)=(ac−bd, ad+bc)。





## 逐步主鏈

S01 · definition操作前

z=2+3i,\ w=4-5i

操作後

z\leftrightarrow(2,3),\ w\leftrightarrow(4,-5)

條件：無

規則：mko_complex_def · 依賴：G1, G2

葉節點依據：mko_complex_def + complex_pair_eq

依 MKO，複數 a+bi 由實部 a 與虛部係數 b 唯一決定，對應有序對 (a,b)。z 的實部是 2、虛部係數是 3；w=4−5i=4+(−5)i，虛部係數是 −5，負號屬於係數本身，不能丟掉。



S02 · equivalent操作前

z+w

操作後

(2+4)+(3+(-5))i=6-2i\leftrightarrow(6,-2)

條件：無

規則：complex_addsub · 依賴：S01, complex_addsub

葉節點依據：complex_addsub + numeric_evaluation

加法逐分量：實部 2+4=6，虛部係數 3+(−5)=−2，所以 z+w=6−2i，有序對為 (6,−2)。



S03 · equivalent操作前

z-w

操作後

(2-4)+(3-(-5))i=-2+8i\leftrightarrow(-2,8)

條件：無

規則：complex_addsub · 依賴：S01, complex_addsub

葉節點依據：complex_addsub + add_inverse + numeric_evaluation

減法也逐分量：實部 2−4=−2，虛部係數 3−(−5)=3+5=8。減去負數等於加上它的相反數，這是最容易弄錯符號的地方。



S04 · equivalent操作前

(a+bi)(c+di)

操作後

(ac-bd)+(ad+bc)i

條件：a,b,c,d\in\mathbb{R}

規則：L_complex_mul · 依賴：mko_complex_def, i_squared

葉節點依據：distributive + mul_assoc + mul_comm + i_squared + add_comm

MKO 說乘法由分配律與 i²=−1 導出，而不是逐分量相乘。先對任意實數 a、b、c、d 證明一般公式（引理 L_complex_mul），證明在子步 S04.1 到 S04.3；之後的乘積都由這個公式計算。



S05 · theorem_application操作前

zw=(2+3i)(4+(-5)i)

操作後

zw=(2\cdot 4-3\cdot(-5))+(2\cdot(-5)+3\cdot 4)i

條件：a=2,\ b=3,\ c=4,\ d=-5

規則：L_complex_mul · 依賴：S01, S04

葉節點依據：L_complex_mul + forall_elim

把 a=2、b=3、c=4、d=−5 代入引理。d 必須取 −5 而不是 5：w 的虛部係數要連同符號一起代入。



S06 · equivalent操作前

(2\cdot 4-3\cdot(-5))+(2\cdot(-5)+3\cdot 4)i

操作後

23+2i

條件：無

規則：numeric_evaluation · 依賴：S05

葉節點依據：numeric_evaluation

實部：8−(−15)=8+15=23；虛部係數：−10+12=2。所以 zw=23+2i。



S07 · equivalent操作前

(2+3i)(4-5i)

操作後

8-10i+12i-15i^2=8+2i+15=23+2i

條件：無

規則：i_squared · 依賴：S01, distributive, i_squared

葉節點依據：distributive + mul_assoc + mul_comm + i_squared + numeric_evaluation

不用公式，直接展開作交叉核對：分配律給出 2·4+2·(−5i)+3i·4+3i·(−5i)=8−10i+12i−15i²；i²=−1 把 −15i² 變成 +15；合併得 23+2i，與 S06 相同。



S08 · equivalent操作前

zw=23+2i

操作後

zw\leftrightarrow(23,2)

條件：無

規則：complex_pair_eq · 依賴：S06, complex_pair_eq

葉節點依據：complex_pair_eq

依 G2 把答案寫成有序對（實部, 虛部係數）=(23,2)。次序是語義資料：(2,23) 代表 2+23i，是另一個複數。



S09 · implies操作前

(23,2)\ \text{vs}\ (2,23)

操作後

(23,2)\neq(2,23)

條件：無

規則：complex_pair_eq · 依賴：S08, complex_pair_eq

葉節點依據：complex_pair_eq + numeric_evaluation

兩個有序對相等必須實部相等且虛部係數相等；23≠2，所以 (23,2)≠(2,23)。交換實部與虛部會得到另一個複數，這正是 MKO 指出的常見誤解。



S10 · definition操作前

23\in\mathbb{R}

操作後

23=23+0i\leftrightarrow(23,0)

條件：無

規則：real_embedding · 依賴：real_embedding

葉節點依據：real_embedding

要判定 zw 是否等於實數 23，先把 23 嵌入複數：23=23+0i，有序對為 (23,0)。比較必須在同一個集合 ℂ 中進行。



S11 · equivalent操作前

zw=23

操作後

23=23\ \land\ 2=0

條件：無

規則：complex_pair_eq · 依賴：S08, S10, complex_pair_eq

葉節點依據：complex_pair_eq + and_intro_elim

zw=23 等價於 (23,2)=(23,0)，再等價於兩個分量分別相等：23=23 且 2=0。



S12 · implies操作前

23=23\ \land\ 2=0

操作後

zw\neq 23

條件：無

規則：contradiction · 依賴：S11

葉節點依據：contradiction + and_intro_elim + numeric_evaluation

2=0 為假，所以合取為假；依 S11 的等價，zw=23 不成立。這正是 MKO 第三段：虛部係數不為零的複數不能等於任何實數，不論實部是否相同。



S13 · theorem_application操作前

wz=(4+(-5)i)(2+3i)

操作後

wz=(4\cdot 2-(-5)\cdot 3)+(4\cdot 3+(-5)\cdot 2)i=23+2i

條件：a=4,\ b=-5,\ c=2,\ d=3

規則：L_complex_mul · 依賴：S04, G1

葉節點依據：L_complex_mul + numeric_evaluation

反過來算 wz 作另一個核對：引理給出實部 8+15=23、虛部係數 12−10=2，與 zw 相同，和 ℂ 乘法的交換律一致。



S14 · implies操作前

z=2+3i,\ w=4-5i

操作後

z+w\leftrightarrow(6,-2),\ z-w\leftrightarrow(-2,8),\ zw\leftrightarrow(23,2),\ zw\neq 23

條件：無

規則：and_intro_elim · 依賴：S02, S03, S08, S12

葉節點依據：and_intro_elim

合併四個結論：和 (6,−2)、差 (−2,8)、積 (23,2)，而且積不等於實數 23。







## 局部子步與引理

S04.1 · equivalent操作前

(a+bi)(c+di)

操作後

ac+a(di)+(bi)c+(bi)(di)

條件：無

規則：distributive · 依賴：distributive, mul_comm

葉節點依據：distributive + mul_comm

對第二個因子用分配律：(a+bi)(c+di)=(a+bi)c+(a+bi)(di)；再對每一項各用一次分配律（右側分配用交換律轉成左側分配），得到四項 ac、a(di)、(bi)c、(bi)(di)。



S04.2 · equivalent操作前

ac+a(di)+(bi)c+(bi)(di)

操作後

ac+(ad)i+(bc)i+(bd)i^2

條件：無

規則：mul_assoc · 依賴：S04.1, mul_assoc, mul_comm

葉節點依據：mul_assoc + mul_comm

用乘法結合律與交換律重排每一項的因子：a(di)=(ad)i，(bi)c=(bc)i，(bi)(di)=(bd)(i·i)=(bd)i²。只改變因子的分組與次序，不改變值。



S04.3 · equivalent操作前

ac+(ad)i+(bc)i+(bd)i^2

操作後

(ac-bd)+(ad+bc)i

條件：無

規則：i_squared · 依賴：S04.2, i_squared, distributive

葉節點依據：i_squared + neg_mul + add_comm + add_assoc + distributive

代入 i²=−1：(bd)i²=(bd)(−1)=−bd，這一項不含 i，屬於實部。再用加法交換律與結合律把實數項 ac 與 −bd 放在一起，並用分配律把 (ad)i+(bc)i 合併成 (ad+bc)i。S04.1 到 S04.3 合起來證得引理 L_complex_mul；實部中的負號 −bd 正是來自 i²=−1。







## 逐步反向審查


- S14 · sufficient_goal_reduction · S02, S03, S08, S12, and_intro_elim — 目標 G：三個運算結果與相等判定。足夠條件 H：S02、S03、S08、S12 四個已證結論；H⇒G 由合取引入。H 由給定資料正向推出，沒有把 G 當作前提。
- S13 · premise_audit · L_complex_mul, mul_comm, numeric_evaluation — 這只是一組數的一致性核對，不用來證明交換律；交換律在本稿是前提。
- S12 · premise_audit · S11, contradiction, numeric_evaluation — 只用到一個分量 2≠0；實部相同（23=23）並不足以推出相等。
- S11 · inverse_equivalence · complex_pair_eq — 有序對相等的條件本身是雙向的，所以這一步兩個方向都成立。
- S10 · premise_audit · real_embedding — 此步只是嵌入的寫法，不推出新事實。
- S09 · premise_audit · complex_pair_eq, numeric_evaluation — 一個分量不同就足以推出不等；反向（不等推出某個指定分量不同）並未宣稱。
- S08 · inverse_equivalence · complex_pair_eq, G2 — a+bi 與 (a,b) 一一對應，所以寫成有序對與寫回 23+2i 互為反向。
- S07 · inverse_equivalence · distributive, i_squared, numeric_evaluation — 每個等號都是等值改寫；兩條獨立路徑得到同一結果，可抓出抄寫或符號錯誤。
- S06 · inverse_equivalence · numeric_evaluation — 整數算式的精確求值，可獨立重算（N5、N6）；兩邊是同一個數，雙向成立。
- S05 · premise_audit · S01, L_complex_mul, forall_elim — 引理對所有實數成立，整數 2、3、4、−5 是實數特例，所以可以代入；此步不宣稱可以由乘積反推出因子。
- S04.3 · inverse_equivalence · i_squared, distributive, add_comm, add_assoc — 每一步都把式子換成相等的式子（i² 換成 −1、項的重排與合併），反向依序還原，雙向成立。
- S04.2 · inverse_equivalence · mul_assoc, mul_comm — 結合律與交換律是對所有複數成立的恆等式，反向重排即回到原式。
- S04.1 · inverse_equivalence · distributive, mul_comm — 反向是依分配律把四項合併回兩個因子的乘積；分配律是等式，兩個方向都成立。
- S04 · inverse_equivalence · L_complex_mul — 兩邊是同一個複數的兩種寫法；子步中每一步都是等值改寫，所以整條等式雙向成立。
- S03 · inverse_equivalence · complex_addsub, numeric_evaluation — 反向：(−2+8i)+w=(−2+4)+(8+(−5))i=2+3i=z，還原了 z−w=−2+8i。
- S02 · inverse_equivalence · complex_addsub, numeric_evaluation — 反向：(6−2i)−w=(6−4)+(−2−(−5))i=2+3i=z，還原了 z+w=6−2i；兩式表示同一個複數。
- S01 · premise_audit · G1, G2, mko_complex_def, complex_pair_eq — 此步只把給定資料寫成有序對，不推出新事實；對應是一一的（complex_pair_eq），所以之後用有序對計算不會失去資訊。





## 錯誤控制與反例

忘記 i²=−1MKO 指出的誤解之一是乘法時忘記 i²=−1。若把 −15i² 當成 −15（等於把 i² 當成 1），會得到 (8−15)+2i=−7+2i；若乾脆丟掉 i² 項，會得到 8+2i。正確做法是 −15i²=−15·(−1)=+15，實部為 23。S04.3 顯示一般公式中的 −bd 正是這個負號。

交換實部與虛部MKO 的另一個誤解是交換實部與虛部。答案 (23,2) 表示 23+2i；寫成 (2,23) 就成了 2+23i，是另一個數（S09）。有序對的次序是語義資料，不能依圖上位置猜。

乘法不是逐分量加減是逐分量的，但乘法不是：(2,3)·(4,−5) 不等於 (2·4, 3·(−5))=(8,−15)。正確公式的實部 ac−bd 混合了兩個實部與兩個虛部係數，虛部係數 ad+bc 是交叉項之和。


- (2+3i)(4−5i)=8−15i，因為乘法逐分量進行 → reject — 乘法由分配律與 i²=−1 導出，正確結果是 23+2i。
- (2+3i)(4−5i)=−7+2i → reject — 這是把 i² 當成 +1 的結果；−15i²=+15，實部是 8+15=23。
- zw 的有序對是 (2,23) → reject — 次序是（實部, 虛部係數），zw=23+2i 對應 (23,2)，而 (2,23)≠(23,2)。
- 23+2i 的實部是 23，所以它等於實數 23 → reject — 23 嵌入為 (23,0)，相等還需要 2=0，不成立。





## 結論與限制

z+w=6−2i，即 (6,−2)；z−w=−2+8i，即 (−2,8)；z·w=23+2i，即 (23,2)，由一般公式 (a+bi)(c+di)=(ac−bd)+(ad+bc)i 與直接展開兩條路徑得到相同結果。因虛部係數 2≠0，z·w 不等於實數 23。


- ℂ 中加法與乘法的交換、結合、分配律是本稿的前提，沒有由有序對的定義推出；本稿也不處理複數除法、共軛、模與極式（MKO 的 formal next）。
- N13 用引理重算 i·i=−1 只是一致性核對；引理本身用到了 i²=−1，所以它不是 i²=−1 的證明。





## 驗證及來源綁定

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


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: 311fc9976ea86edccc67e94b6680145f12b64abe38568601a6bbabf8fd324b42
- original source SHA-256: 311fc9976ea86edccc67e94b6680145f12b64abe38568601a6bbabf8fd324b42
- Lean: NOT_RUN · independent AI: NOT_MEASURED

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