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

目標與範圍

設 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)。

逐步主鏈

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

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

z+w

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

z-w

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

(a+bi)(c+di)

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

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

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

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

23+2i

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

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

zw=23+2i

zw\leftrightarrow(23,2)

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

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

23\in\mathbb{R}

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

zw=23

23=23\ \land\ 2=0

23=23\ \land\ 2=0

zw\neq 23

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

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

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

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

局部子步與引理

(a+bi)(c+di)

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

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

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

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

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

逐步反向審查

• 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²=−1

MKO 指出的誤解之一是乘法時忘記 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、反控制與修訂記錄）