# 絕對值：由分段定義證明非負性、零點與 |a−b|=|b−a|

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

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

derivation-mko-absolute-value-01 · production-20261019-adopted-96



## 目標與範圍

只用分段定義（x≥0 時 |x|=x，x<0 時 |x|=−x）與實數的序和加法，證明對所有實數 x、a、b：(1) |x|≥0；(2) |x|=0 ⇔ x=0；(3) |−x|=|x|；(4) |a−b|=|b−a|。並計算 |−3|、|2−7|、|7−2|，說明「|x|=x 對所有 x 成立」是錯的。

在 MKO 的範圍內：實數及其標準線性序與加法反元素（假設 a1），以分段定義的函數 A(x)=|x|。所有性質都由分段定義推出，不使用現成的絕對值規則；不處理三角不等式、不等式解法、複數模或範數（MKO 指出這些是後續內容）；不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- order_basics
- add_inverse
- add_assoc
- add_comm
- add_zero
- numeric_evaluation


- G1 — x、a、b 是實數；ℝ 具有標準線性序與加法反元素（MKO 假設 a1）。
- G2 — 定義：若 x≥0，則 |x|=x；若 x<0，則 |x|=−x。


- |x| — x 的絕對值 A(x)
- -x — x 的加法反元素
- a,\ b — 數線上的兩個實數
- |a-b| — a 與 b 的距離





## 規則與來源


- 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。
- add_inverse · prerequisite — 加法反元素：每個 u 都有 −u，使 u+(−u)=0；u−v 定義為 u+(−v)。
- add_assoc · prerequisite — 加法結合律：(u+v)+w=u+(v+w)。
- add_comm · prerequisite — 加法交換律：u+v=v+u。
- add_zero · prerequisite — 加法單位元：u+0=u。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
- eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。
- case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
- forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
- contrapositive · prerequisite — 逆否命題：P⇒Q 與 ¬Q⇒¬P 等價。逆命題 Q⇒P 一般不與 P⇒Q 等價。
- iff_intro · prerequisite — 雙條件：P⇒Q 與 Q⇒P 都成立時，P⇔Q 成立；反之亦然。
- forall_elim · prerequisite — ∀消去（代入特例）：若 ∀x∈D, P(x) 成立且 a∈D，則 P(a) 成立。
- quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。
- exists_intro · prerequisite — ∃引入：若找到 a∈D 使 P(a) 成立，則 ∃x∈D, P(x)。
- and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
- mko_abs_def · cited — 函數 A:ℝ→ℝ 定義為：若 x≥0，則 A(x)=x；若 x<0，則 A(x)=−x。慣用記號為 |x|，且 |x|≥0。 · mko-absolute-value
- L_sign · lemma — 對實數 x：若 x<0 則 0<−x；若 0<x 則 −x<0。
- L_inv_unique · lemma — 對實數 u、v：若 u+v=0，則 v=−u。特別地 −(−x)=x，且 −0=0。





## 逐步主鏈

S01 · definition操作前

|x|

操作後

|x|=x\ \ (x\geq 0),\qquad |x|=-x\ \ (x<0)

條件：無

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

葉節點依據：mko_abs_def + order_basics

依 MKO 寫出分段定義。依實數序的三一律，每個 x 恰好滿足 x<0、x=0、x>0 之一，而 x≥0 表示 x>0 或 x=0；所以每個 x 恰好落在一個分支，|x| 有唯一的值，A 確實是 ℝ→ℝ 的函數。判斷用哪個分支，看的是 x 這個數的正負，不是式子裡有沒有負號。



S02 · implies操作前

x\geq 0

操作後

|x|=x\geq 0

條件：x\geq 0

規則：def_unfold · 依賴：S01

葉節點依據：def_unfold

情況一：x≥0。依第一分支 |x|=x，而 x≥0 是本情況的假設，所以 |x|≥0。



S03 · implies操作前

x<0

操作後

|x|=-x>0

條件：x<0

規則：L_sign · 依賴：S01, L_sign

葉節點依據：def_unfold + order_basics + add_inverse

情況二：x<0。依第二分支 |x|=−x；依引理 L_sign，x<0 推出 0<−x。所以此時 |x|>0。式子 −x 前面有負號，但它表示的數是正的。



S04 · implies操作前

x\geq 0\ \lor\ x<0

操作後

\forall x\in\mathbb{R}:\ |x|\geq 0

條件：無

規則：case_analysis · 依賴：S02, S03, order_basics

葉節點依據：case_analysis + order_basics + forall_intro

依三一律每個實數都滿足 x≥0 或 x<0；兩種情況下分別由 S02 得 |x|≥0、由 S03 得 |x|>0（因此也 ≥0）。x 是任意的，所以對所有實數 |x|≥0。這就是 MKO 中「|x|≥0」的證明。



S05 · implies操作前

x\neq 0

操作後

|x|>0,\ \text{hence}\ |x|\neq 0;\ \text{so}\ |x|=0\Rightarrow x=0

條件：無

規則：contrapositive · 依賴：S02, S03, order_basics

葉節點依據：contrapositive + case_analysis + order_basics

設 x≠0，則 x>0 或 x<0。x>0 時 |x|=x>0（S02）；x<0 時 |x|=−x>0（S03）。兩種情況都有 |x|>0，所以 |x|≠0。這證明了 x≠0 ⇒ |x|≠0，其逆否命題就是 |x|=0 ⇒ x=0。



S06 · implies操作前

x=0

操作後

|0|=0;\ \ \text{hence}\ |x|=0\Leftrightarrow x=0

條件：無

規則：iff_intro · 依賴：S01, S05

葉節點依據：iff_intro + def_unfold

0≥0，所以 0 落在第一分支，|0|=0，即 x=0 ⇒ |x|=0。與 S05 合起來得 |x|=0 ⇔ x=0：絕對值只在 0 處為 0。



S07 · implies操作前

x>0

操作後

|-x|=-(-x)=x=|x|

條件：x>0

規則：def_unfold · 依賴：S01, L_sign, L_inv_unique

葉節點依據：def_unfold + L_sign + L_inv_unique

證 |−x|=|x| 的情況 x>0：依 L_sign，−x<0，所以對數 −x 用第二分支：|−x|=−(−x)。依引理 L_inv_unique，−(−x)=x；而 x>0 時 |x|=x。所以 |−x|=|x|。



S08 · implies操作前

x<0

操作後

|-x|=-x=|x|

條件：x<0

規則：def_unfold · 依賴：S01, L_sign

葉節點依據：def_unfold + L_sign

情況 x<0：依 L_sign，−x>0，所以對 −x 用第一分支：|−x|=−x。而 x<0 時 |x|=−x（第二分支）。兩者相同，|−x|=|x|。



S09 · implies操作前

x>0\ \lor\ x<0\ \lor\ x=0

操作後

\forall x\in\mathbb{R}:\ |-x|=|x|

條件：無

規則：case_analysis · 依賴：S07, S08, L_inv_unique

葉節點依據：case_analysis + order_basics + forall_intro

剩下的情況 x=0：依 L_inv_unique，−0=0，所以 |−0|=|0|。三種情況由三一律涵蓋全部實數，依分情況論證與全稱推廣，對所有實數 |−x|=|x|。



S10 · implies操作前

(a-b)+(b-a)

操作後

(a-b)+(b-a)=0,\ \text{hence}\ b-a=-(a-b)

條件：無

規則：L_inv_unique · 依賴：L_inv_unique, add_assoc, add_comm, add_inverse, add_zero

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

(a−b)+(b−a)=a+(−b)+b+(−a)，依結合律與交換律重排為 (a+(−a))+(b+(−b))=0+0=0。依引理 L_inv_unique（u=a−b、v=b−a），b−a=−(a−b)。



S11 · implies操作前

|b-a|

操作後

|b-a|=|-(a-b)|=|a-b|

條件：無

規則：forall_elim · 依賴：S09, S10

葉節點依據：forall_elim + eq_replace

依 S10 把 b−a 換成相等的 −(a−b)，再把 S09 用在 x=a−b：|−(a−b)|=|a−b|。所以對所有實數 a、b，|a−b|=|b−a|：數線上兩點的距離不因交換端點而改變。



S12 · implies操作前

|-3|

操作後

|-3|=-(-3)=3

條件：-3<0

規則：def_unfold · 依賴：S01, L_inv_unique

葉節點依據：def_unfold + L_inv_unique + numeric_evaluation

−3<0，所以用第二分支：|−3|=−(−3)=3（L_inv_unique）。結果 3≥0，符合 S04。



S13 · implies操作前

|2-7|,\ |7-2|

操作後

|2-7|=|-5|=5,\ \ |7-2|=|5|=5

條件：無

規則：def_unfold · 依賴：S01, S11

葉節點依據：def_unfold + numeric_evaluation

先算括號內的數：2−7=−5<0，用第二分支得 |−5|=−(−5)=5；7−2=5≥0，用第一分支得 |5|=5。兩者相等，符合 S11（a=2、b=7）：2 與 7 在數線上相距 5。



S14 · implies操作前

\forall x\in\mathbb{R}:\ |x|=x

操作後

\text{false, since}\ |-3|=3\neq -3

條件：無

規則：quantifier_negation · 依賴：S12

葉節點依據：quantifier_negation + exists_intro + order_basics

反例：命題「對所有實數 x，|x|=x」的否定是「存在 x 使 |x|≠x」。x=−3 就是這樣的 x：|−3|=3，而 3>0>−3，所以 3≠−3。這個反例已否定對所有 x 的等式，所以不能不分情況把 |x|=x 當作一般規則；本步不由單一反例推導全部成立情形。



S15 · implies操作前

S04,\ S06,\ S09,\ S11

操作後

|x|\geq 0,\ \ |x|=0\Leftrightarrow x=0,\ \ |-x|=|x|,\ \ |a-b|=|b-a|

條件：無

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

葉節點依據：and_intro_elim

四個目標分別由 S04、S06、S09、S11 證成，全部只依賴分段定義、實數的序與加法。







## 局部子步與引理

S03.1 · implies操作前

x<0

操作後

x+(-x)<0+(-x)

條件：無

規則：order_basics · 依賴：order_basics

葉節點依據：order_basics

依 order_basics（u<v 推出 u+w<v+w），兩邊同加 w=−x。同理，對 0<x 兩邊同加 −x 得 0+(−x)<x+(−x)，這是引理的第二部分。



S03.2 · equivalent操作前

x+(-x)<0+(-x)

操作後

0<-x

條件：無

規則：eq_replace · 依賴：S03.1, add_inverse, add_zero, add_comm

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

化簡兩邊：x+(−x)=0（加法反元素），0+(−x)=(−x)+0=−x（交換律與單位元）。第二部分同理化簡為 −x<0。S03.1 與 S03.2 合起來證得引理 L_sign。



S07.1 · implies操作前

u+v=0

操作後

v=-u

條件：無

規則：eq_replace · 依賴：add_zero, add_inverse, add_assoc, add_comm

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

v=v+0=v+(u+(−u))=(v+u)+(−u)=(u+v)+(−u)=0+(−u)=−u，依序用到單位元、反元素、結合律、交換律、假設 u+v=0 與單位元。取 u=−x、v=x：(−x)+x=0，所以 x=−(−x)。取 u=v=0：0+0=0，所以 0=−0。此子步證得引理 L_inv_unique。







## 逐步反向審查


- S15 · sufficient_goal_reduction · S04, S06, S09, S11, and_intro_elim — 目標 G：(1) 到 (4) 同時成立。足夠條件 H：S04、S06、S09、S11 各自成立；H⇒G 由合取引入。H 由定義正向證成，沒有把 G 當作前提；S12 到 S14 是例子與反例。
- S14 · premise_audit · S12, quantifier_negation, order_basics — 推翻全稱命題只需要一個反例；這不宣稱 |x|=x 對其他 x 是否成立。
- S13 · premise_audit · S01, S11, numeric_evaluation — 必須先求出 2−7 的值再判定分支；不能看到式子中的減號就直接刪掉。
- S12 · premise_audit · S01, L_inv_unique, numeric_evaluation — 先判定 −3 的正負才選分支；N1 重算 −(−3)=3。
- S11 · premise_audit · S09, S10, forall_elim, eq_replace — S09 對所有實數成立，所以可代入 x=a−b；N6 只是 a、b 在 −6 到 6 的有限核對，不是證明。
- S10 · premise_audit · L_inv_unique, add_assoc, add_comm, add_inverse — 重排只用加法的結合律與交換律；N5 以多項式恆等式核對 (a−b)+(b−a)=0。
- S09 · premise_audit · S07, S08, case_analysis, order_basics — 三種情況必須都處理；只看 x>0 不能推出一般結論。
- S08 · premise_audit · S01, L_sign — 兩次展開定義所用的分支不同（−x 用第一分支、x 用第二分支），各自由相應數值的正負判定。
- S07.1 · premise_audit · add_zero, add_inverse, add_assoc, add_comm, eq_replace — 每一步都是對所有實數成立的恆等式或假設 u+v=0 的代換；結論只說反元素唯一。
- S07 · premise_audit · L_sign, L_inv_unique, S01 — 分支是依 −x 這個數的正負選的，不是依 x 的正負；這正是容易弄錯的地方。
- S06 · premise_audit · S05, iff_intro, def_unfold — 雙條件需要兩個方向都已證：⇐ 在此步，⇒ 在 S05。
- S05 · premise_audit · S02, S03, contrapositive, case_analysis — 逆否命題與原命題等價；此步只得到一個方向，另一方向在 S06。
- S04 · premise_audit · S02, S03, case_analysis, forall_intro — 分情況論證要求情況涵蓋全部可能；x≥0 與 x<0 由三一律涵蓋所有實數。
- S03.2 · inverse_equivalence · add_inverse, add_zero, add_comm, eq_replace — 只把式子換成相等的式子，不等式的真假不變，雙向成立。
- S03.1 · premise_audit · order_basics — 兩邊加同一個數保持嚴格不等號的方向，對任何實數 w 都成立，沒有附加條件。
- S03 · premise_audit · S01, L_sign — 需要本情況的假設 x<0 與引理；引理在 S03.1、S03.2 證明。
- S02 · premise_audit · S01, def_unfold — 只在 x≥0 的情況下使用第一分支；不宣稱 x<0 時 |x|=x。
- S01 · premise_audit · G2, mko_abs_def, order_basics — 此步只寫出定義；分支互斥且涵蓋全部實數，靠的是三一律。





## 錯誤控制與反例

|x| 不一律等於 xMKO 指出的第一個誤解是把 |x| 一律寫成 x。|x|=x 只是 x≥0 時的分支；x<0 時 |x|=−x。反例：x=−3 時 |x|=3，而 x=−3。使用絕對值前，先判定裡面那個數的正負。

絕對值不是刪除負號的文字規則MKO 指出的第二個誤解是把絕對值當成刪除負號。把 |2−7| 的減號刪掉得 2+7=9，但 2−7=−5，|−5|=5。又如 x=−2 時 |−x|=|2|=2，而刪除負號會得到 x=−2。定義看的是數值的正負，不是符號的外觀。

|x| 不會是負數，而 −x 不一定是負數MKO 指出的第三個誤解是認為 |x| 可以是負數。第二分支寫成 |x|=−x，看起來帶負號，但它只在 x<0 時使用，而依 L_sign，此時 −x>0；例如 x=−3 時 −x=3。所以 S04 證明 |x|≥0 對所有實數成立。


- 對所有實數 x，|x|=x → reject — x=−3 時 |x|=3≠−3。
- |2−7|=2+7=9 → reject — 2−7=−5，|−5|=5。
- 對所有實數 x，|−x|=x → reject — x=−2 時 |−x|=|2|=2≠−2；正確的是 |−x|=|x|。
- 存在實數 x 使 |x|<0 → reject — S04 證明對所有實數 |x|≥0。
- 因為 a−b≠b−a（a≠b 時），所以 |a−b| 與 |b−a| 一般不相等 → reject — b−a=−(a−b)，而 |−x|=|x|（S11）；例如 |2−7|=|7−2|=5。





## 結論與限制

由分段定義可證：對所有實數 |x|≥0；|x|=0 ⇔ x=0；|−x|=|x|；|a−b|=|b−a|。例子：|−3|=3，|2−7|=|7−2|=5；|x|=x 在 x=−3 時不成立，所以不是一般規則。


- N6 與 N10 是整數點上的有限核對（分別為 a、b 從 −6 到 6，x 從 −10 到 10），只支持這些點；一般結論來自 S04 與 S11 的證明。





## 驗證及來源綁定

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


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: ca5b2649a099d99d3fc2f80cd2245c776c98a9a136217dfab0d702504caa791f
- original source SHA-256: 34445117b994db885a5ef32034463f123a04ed40293eda3d29414fa6e7d493f6
- Lean: NOT_RUN · independent AI: NOT_MEASURED

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