# 微積分基本定理：由連續性證明 G′=f，再推出 ∫_a^b f=F(b)−F(a)

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

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

derivation-mko-fundamental-theorem-calculus-01 · production-20261019-adopted-96



## 目標與範圍

設 f:ℝ→ℝ 在全 ℝ 連續，a∈ℝ，G(x)=∫_a^x f(t)dt 為有向積分。(1) 證明 G 在每一點可微且 G′(x)=f(x)；(2) 若 F:ℝ→ℝ 可微且 F′=f，證明對任意實數 a、b 有 ∫_a^b f(t)dt=F(b)−F(a)；(3) 以 f(t)=6t²−2t+1 與候選 F(x)=2x³−x²+x+1/2 算出 ∫_2^{−1} f(t)dt，並說明 G(2)=0 不推出 G′(2)=0、上下限在 x=0 重合也不推出導數為 0。

在 MKO 的充分前提下工作：f 在全 ℝ 連續、F 在全 ℝ 可微。第一部分的 ε–δ 論證完整寫出，但依賴三條一般積分性質（有向區間可加、線性、以上界估計積分）；這些性質對一般連續函數以外部文獻引用（citation_verified），不在本稿證明。第二部分另引用「導數處處為 0 的函數為常數」（均值定理推論，citation_verified）。例題中的多項式積分另以 MKO 定積分的矩公式交叉核對。不處理只可積而不連續的函數、端點單側導數或 Lebesgue 積分；不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- continuity_def
- func_limit_def
- abs_rules
- order_basics
- numeric_evaluation


- G1 — f:ℝ→ℝ 在全 ℝ 連續；a∈ℝ；G(x)=∫_a^x f(t)dt。積分是有向的：x<a 時 ∫_a^x f=−∫_x^a f，且 ∫_a^a f=0（MKO 假設 a1、a2）。
- G2 — F:ℝ→ℝ 在全 ℝ 可微，且對每個實數 x 有 F′(x)=f(x)。
- G3 — 例題：f(t)=6t²−2t+1（升冪整數係數 [1,−2,6]，次數 2）；候選 F(x)=2x³−x²+x+1/2（升冪有理係數 [1/2,1,−1,2]，分母為正）；端點 a=2、b=−1。


- G(x)=\int_a^x f(t)\,dt — 累積函數（有向積分）
- F — f 的原函數：F′=f
- x_0 — 任意取定的一點
- h — 非零增量
- Q(h) — 差商 (G(x_0+h)−G(x_0))/h
- \varepsilon,\ \delta — 誤差界與鄰域半徑
- D=F-G — 兩個原函數之差
- K(x)=\int_x^{2x} f(t)\,dt — 上下限都移動的積分





## 規則與來源


- continuity_def · prerequisite — 連續（ε-δ）：f 在 a 連續表示對每個 ε>0，存在 δ>0，使所有滿足 |x−a|<δ 的定義域點 x 都有 |f(x)−f(a)|<ε。
- func_limit_def · prerequisite — 函數極限：lim_{x→a} f(x)=L 表示對每個 ε>0，存在 δ>0，使所有滿足 0<|x−a|<δ 的定義域點 x 都有 |f(x)−L|<ε（a 須為定義域的極限點）。
- abs_rules · prerequisite — 絕對值（實數）：|u|=u（u≥0）、|u|=−u（u<0）；|u|≥0；|uv|=|u||v|；三角不等式 |u+v|≤|u|+|v|；|u|<r ⇔ −r<u<r。
- 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。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
- eq_congruence · prerequisite — 等式同用：若 u=v，對兩邊做同一個有定義的運算 f，得 f(u)=f(v)。只對一邊做運算不屬於此規則。
- add_inverse · prerequisite — 加法反元素：每個 u 都有 −u，使 u+(−u)=0；u−v 定義為 u+(−v)。
- case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
- neg_mul · prerequisite — 負號與乘法：(−u)v=−(uv)，(−u)(−v)=uv。
- mul_inverse_nonzero · prerequisite — 非零數的倒數：在 ℚ、ℝ、ℂ 中，若 u≠0，存在 1/u 使 u·(1/u)=1；對 u≠0 定義 v/u 為 v·(1/u)。u=0 時沒有倒數，v/0 不定義。
- distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。
- eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。
- forall_elim · prerequisite — ∀消去（代入特例）：若 ∀x∈D, P(x) 成立且 a∈D，則 P(a) 成立。
- 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）。
- forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
- add_assoc · prerequisite — 加法結合律：(u+v)+w=u+(v+w)。
- add_comm · prerequisite — 加法交換律：u+v=v+u。
- add_zero · prerequisite — 加法單位元：u+0=u。
- power_laws · prerequisite — 整數指數律（底數非零或指數為正整數）：a^m·a^n=a^{m+n}，(a^m)^n=a^{mn}，(ab)^n=a^n b^n，a^0=1。
- deriv_def · cited — 對 f:ℝ→ℝ，f 在 x 的導數是 lim_{h→0,h≠0}(f(x+h)−f(x))/h，若此兩側有限極限存在；有限步 h 須非零。 · mko-derivative
- deriv_rules · cited — 在相應點可微的實函數有 (f+g)′=f′+g′、(cf)′=cf′、(fg)′=f′g+fg′；若 g 在 x 可微且 f 在 g(x) 可微，則 (f∘g)′(x)=f′(g(x))g′(x)。 · mko-derivative-rules
- mko_moment · cited — 對連續多項式與有限區間 a≤b，I(x^n,a,b)=(b^{n+1}−a^{n+1})/(n+1)；對 f=Σc_k x^k 逐係數相加。 · mko-definite-integral
- mko_reverse · cited — 反向端點換號：I(f,a,b)=−I(f,b,a)；相同端點 I(f,a,a)=0。 · mko-definite-integral
- int_additive · cited — 若 f 在 ℝ 上連續，則對任意實數 p、q、r（大小次序不限，採有向約定）有 ∫_p^r f=∫_p^q f+∫_q^r f。 · OpenStax, Calculus Volume 1, Section 5.2, Properties of the Definite Integral, rules 1, 2 and 6
- int_linear · cited — 若 f、g 在 ℝ 上連續，則對任意實數 p、q（有向約定）有 ∫_p^q (f(t)−g(t))dt=∫_p^q f(t)dt−∫_p^q g(t)dt。 · OpenStax, Calculus Volume 1, Section 5.2, Properties of the Definite Integral, rule 4
- int_bound · cited — 若 p≤q，g 在 [p,q] 上連續，且對 [p,q] 中每個 t 有 |g(t)|≤M，則 |∫_p^q g(t)dt|≤M(q−p)。 · OpenStax, Calculus Volume 1, Section 5.2, Comparison Properties of Integrals
- thm_zero_deriv · cited — 若 H:ℝ→ℝ 在全 ℝ 可微，且對每個 x 有 H′(x)=0，則 H 在 ℝ 上是常數。 · OpenStax, Calculus Volume 1, Section 4.4, Theorem 4.6, Corollary 1
- poly_deriv · prerequisite — 多項式逐項求導：(Σ_{k=0}^{m} c_k x^k)′=Σ_{k=1}^{m} k c_k x^{k−1}，在全 ℝ 成立；它由 MKO 導數規則的和、常數倍與乘積規則逐次得到。
- L_const_int · lemma — 對任意實數 c、x_0 與 h≠0：∫_{x_0}^{x_0+h} c dt=ch。





## 逐步主鏈

S01 · definition操作前

G'(x_0)=f(x_0)

操作後

\lim_{h\to 0,\ h\neq 0}\frac{G(x_0+h)-G(x_0)}{h}=f(x_0)

條件：x_0\in\mathbb{R}

規則：deriv_def · 依賴：G1, deriv_def

葉節點依據：deriv_def + def_unfold

取定任意一點 x_0∈ℝ，除了 x_0∈ℝ 不加任何假設。依導數定義，第 (1) 小題在 x_0 的意思是：差商 Q(h)=(G(x_0+h)−G(x_0))/h（h≠0）在 h→0 時有有限極限，且極限等於 f(x_0)。



S02 · equivalent操作前

G(x_0+h)-G(x_0)

操作後

\int_{x_0}^{x_0+h} f(t)\,dt

條件：h\neq 0

規則：int_additive · 依賴：G1, int_additive

葉節點依據：int_additive + eq_congruence + add_inverse

取 p=a、q=x_0、r=x_0+h，可加性給 ∫_a^{x_0+h} f=∫_a^{x_0} f+∫_{x_0}^{x_0+h} f，即 G(x_0+h)=G(x_0)+∫_{x_0}^{x_0+h} f；兩邊同減 G(x_0)。因為採有向約定，a、x_0、x_0+h 的大小次序不限，h<0 也適用。



S03 · equivalent操作前

\int_{x_0}^{x_0+h} f(x_0)\,dt

操作後

f(x_0)\,h

條件：h\neq 0

規則：L_const_int · 依賴：L_const_int

葉節點依據：mko_moment + mko_reverse + case_analysis

x_0 已取定，被積函數 t↦f(x_0) 是常數 c=f(x_0)；依引理 L_const_int（S03.1、S03.2 證明），其積分是 f(x_0)h。



S04 · equivalent操作前

\frac{G(x_0+h)-G(x_0)}{h}-f(x_0)

操作後

\frac{1}{h}\int_{x_0}^{x_0+h}\bigl(f(t)-f(x_0)\bigr)\,dt

條件：h\neq 0

規則：int_linear · 依賴：S02, S03, int_linear

葉節點依據：int_linear + mul_inverse_nonzero + distributive + eq_replace

由 S02，分子是 ∫_{x_0}^{x_0+h} f；由 S03，f(x_0)=f(x_0)h/h=(1/h)∫_{x_0}^{x_0+h} f(x_0)dt（h≠0 才能除）。兩項都有因子 1/h，再依積分線性把兩個積分合成 ∫_{x_0}^{x_0+h}(f(t)−f(x_0))dt。



S05 · implies操作前

f\ \text{continuous at}\ x_0,\ \varepsilon>0

操作後

\exists\delta>0\ \forall t:\ |t-x_0|<\delta\Rightarrow|f(t)-f(x_0)|<\tfrac{\varepsilon}{2}

條件：\varepsilon>0

規則：continuity_def · 依賴：G1, continuity_def

葉節點依據：continuity_def + forall_elim

任取 ε>0。f 在 x_0 連續（G1），把連續的定義用在正數 ε/2 上，得到一個 δ>0 滿足上式。這是證明中唯一直接展開點連續 ε–δ 定義的地方；積分可加性、線性與上界估計的引用也依賴各自的連續性前提，S07 另核對誤差函數連續。



S06 · implies操作前

0<|h|<\delta,\ t\ \text{between}\ x_0\ \text{and}\ x_0+h

操作後

|t-x_0|\le|h|<\delta,\quad |f(t)-f(x_0)|<\tfrac{\varepsilon}{2}

條件：0<|h|<\delta

規則：abs_rules · 依賴：S05

葉節點依據：abs_rules + order_basics + case_analysis

分兩種情況：h>0 時 x_0≤t≤x_0+h，所以 0≤t−x_0≤h=|h|；h<0 時 x_0+h≤t≤x_0，所以 0≤x_0−t≤−h=|h|。兩種情況都有 |t−x_0|≤|h|<δ，再由 S05 得 |f(t)−f(x_0)|<ε/2。



S07 · implies操作前

\left|\int_{x_0}^{x_0+h}\bigl(f(t)-f(x_0)\bigr)\,dt\right|

操作後

\le\tfrac{\varepsilon}{2}\,|h|

條件：0<|h|<\delta

規則：int_bound · 依賴：S06, int_bound, G1

葉節點依據：int_bound + abs_rules + case_analysis

令 g(t)=f(t)−f(x_0)。g 連續，因為 |g(t)−g(s)|=|f(t)−f(s)|。由 S06，在 x_0 與 x_0+h 之間的閉區間上 |g|≤ε/2。h>0 時以 p=x_0、q=x_0+h 套用估計，得 |∫|≤(ε/2)h；h<0 時有向積分等於 −∫_{x_0+h}^{x_0} g，絕對值不變，估計給 (ε/2)(−h)。兩者都是 (ε/2)|h|。



S08 · implies操作前

\left|\frac{G(x_0+h)-G(x_0)}{h}-f(x_0)\right|

操作後

\le\tfrac{\varepsilon}{2}<\varepsilon\quad(0<|h|<\delta)

條件：0<|h|<\delta

規則：abs_rules · 依賴：S04, S07

葉節點依據：abs_rules + frac_rules + order_basics

由 S04，左邊等於 |1/h|·|∫_{x_0}^{x_0+h}(f(t)−f(x_0))dt|=(1/|h|)·|∫|；由 S07，它 ≤(1/|h|)(ε/2)|h|=ε/2<ε。用到 |uv|=|u||v| 與 |h|>0。



S09 · implies操作前

\forall\varepsilon>0\ \exists\delta>0\ \forall h:\ 0<|h|<\delta\Rightarrow|Q(h)-f(x_0)|<\varepsilon

操作後

G'(x_0)=f(x_0)

條件：無

規則：func_limit_def · 依賴：S05, S08, func_limit_def

葉節點依據：func_limit_def + deriv_def + forall_intro

ε>0 是任取的，S05 到 S08 對它找到了合用的 δ；這正是 lim_{h→0} Q(h)=f(x_0) 的定義（0 是 Q 的定義域 ℝ∖{0} 的極限點）。依 S01，G 在 x_0 可微且 G′(x_0)=f(x_0)。



S10 · implies操作前

G'(x_0)=f(x_0)\ \text{for an arbitrary}\ x_0\in\mathbb{R}

操作後

\forall x\in\mathbb{R}:\ G'(x)=f(x)

條件：無

規則：forall_intro · 依賴：S09

葉節點依據：forall_intro

S01 到 S09 除了 x_0∈ℝ 沒有用到 x_0 的任何性質，基點 a 也是任意的，所以全稱推廣：對每個 a 與每個 x，G 在 x 可微且 G′(x)=f(x)。第 (1) 小題在所引用的積分性質下得證。



S11 · implies操作前

D(x)=F(x)-G(x)

操作後

D'(x)=F'(x)-G'(x)=f(x)-f(x)=0\quad\forall x\in\mathbb{R}

條件：無

規則：deriv_rules · 依賴：G2, S10, deriv_rules

葉節點依據：deriv_rules + add_inverse

F 在每點可微（G2），G 在每點可微（S10）。把 D 寫成 F+(−1)·G，由和與常數倍的導數規則，D 在每點可微，且 D′=F′−G′=f−f=0。



S12 · theorem_application操作前

D'(x)=0\quad\forall x\in\mathbb{R}

操作後

\exists C\in\mathbb{R}\ \forall x\in\mathbb{R}:\ F(x)=G(x)+C

條件：D\ \text{differentiable on}\ \mathbb{R}

規則：thm_zero_deriv · 依賴：S11, thm_zero_deriv

葉節點依據：thm_zero_deriv

D 在整個 ℝ（一個區間）上可微且導數處處為 0；依引用的均值定理推論，D 是常數 C，即 F=G+C。



S13 · equivalent操作前

F(b)-F(a)

操作後

\int_a^b f(t)\,dt

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

規則：eq_replace · 依賴：S12, G1

葉節點依據：eq_replace + add_inverse + def_unfold

由 S12，F(b)−F(a)=(G(b)+C)−(G(a)+C)=G(b)−G(a)（S13.2）；G(b)=∫_a^b f，且 G(a)=0（S13.1），所以等於 ∫_a^b f。b 可以小於、等於或大於 a，因為 G 用的是有向積分。



S14 · implies操作前

F(x)=\tfrac{1}{2}+x-x^2+2x^3

操作後

F'(x)=1-2x+6x^2=f(x)

條件：無

規則：poly_deriv · 依賴：G3, poly_deriv

葉節點依據：poly_deriv + numeric_evaluation

逐係數求導：常數 1/2 的導數是 0；x 給 1；−x² 給 −2x；2x³ 給 6x²。F′ 的升冪係數 [1,−2,6] 與 f 的 [1,−2,6] 逐項相同，所以 F′=f 作為多項式相等，於每個實數 x 都成立。F 是多項式，在全 ℝ 可微，所以 G2 的前提對這個 F 成立。



S15 · theorem_application操作前

\int_2^{-1} f(t)\,dt

操作後

F(-1)-F(2)=-\tfrac{7}{2}-\tfrac{29}{2}=-18

條件：F'=f\ \text{on}\ \mathbb{R}

規則：forall_elim · 依賴：S13, S14, G3

葉節點依據：forall_elim + numeric_evaluation

S13 對任意實數端點成立，取 a=2、b=−1（端點反向）。F(−1)=2(−1)³−(−1)²+(−1)+1/2=−2−1−1+1/2=−7/2；F(2)=16−4+2+1/2=29/2；差為 −36/2=−18。



S16 · implies操作前

G(x)=\int_2^x f(t)\,dt

操作後

G(2)=0,\quad G'(2)=f(2)=21\neq 0

條件：無

規則：forall_elim · 依賴：S10, S13, G3

葉節點依據：forall_elim + numeric_evaluation

取基點 a=2。G(2)=∫_2^2 f=0，但由 S10，G′(2)=f(2)=6·4−2·2+1=21≠0。函數值為 0 只說明累積量從 0 開始；導數是此刻的變化率。由 S13 也可寫 G(x)=F(x)−F(2)，所以 G′=F′=f，一致。



S17 · implies操作前

K(x)=\int_x^{2x} f(t)\,dt

操作後

K(x)=F(2x)-F(x)=14x^3-3x^2+x

條件：無

規則：forall_elim · 依賴：S13, S14, G3

葉節點依據：forall_elim + distributive + power_laws

對每個 x，以 a=x、b=2x 套用 S13：K(x)=F(2x)−F(x)=(16x³−4x²+2x+1/2)−(2x³−x²+x+1/2)=14x³−3x²+x（N6 為次數 3 的恆等式核對）。在 x=0，上下限都是 0，K(0)=0。







## 局部子步與引理

S03.1 · theorem_application操作前

\int_{x_0}^{x_0+h} c\,dt\quad(h>0)

操作後

c\cdot\frac{(x_0+h)^1-x_0^1}{1}=ch

條件：h>0

規則：mko_moment · 依賴：mko_moment

葉節點依據：mko_moment + add_inverse

h>0 時 x_0<x_0+h。常數 c 是多項式 c·x⁰，套用矩公式 n=0：c((x_0+h)−x_0)/1=ch。



S03.2 · theorem_application操作前

\int_{x_0}^{x_0+h} c\,dt\quad(h<0)

操作後

-\int_{x_0+h}^{x_0} c\,dt=-c\bigl(x_0-(x_0+h)\bigr)=ch

條件：h<0

規則：mko_reverse · 依賴：mko_reverse, mko_moment

葉節點依據：mko_reverse + mko_moment + neg_mul + order_basics

h<0 時 x_0+h<x_0。先用反向規則 ∫_{x_0}^{x_0+h} c dt=−∫_{x_0+h}^{x_0} c dt，再對正向區間用矩公式：−c(x_0−(x_0+h))=−c(−h)=ch。依三分律，h≠0 表示 h>0 或 h<0，所以 S03.1 與 S03.2 合起來證得引理 L_const_int。



S13.1 · equivalent操作前

G(a)

操作後

\int_a^a f(t)\,dt=0

條件：無

規則：def_unfold · 依賴：G1

葉節點依據：def_unfold

依 G 的定義 G(a)=∫_a^a f，再依 G1 的有向約定（相同端點的積分為 0）得 0。



S13.2 · equivalent操作前

(G(b)+C)-(G(a)+C)

操作後

G(b)-G(a)

條件：無

規則：add_inverse · 依賴：S12

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

C 與 −C 相消（加法結合律、交換律與反元素）。這也說明為什麼原函數加常數不改端點差。



S15.1 · theorem_application操作前

\int_{-1}^{2} f(t)\,dt

操作後

6\cdot\tfrac{2^3-(-1)^3}{3}-2\cdot\tfrac{2^2-(-1)^2}{2}+\bigl(2-(-1)\bigr)=18

條件：-1\le 2

規則：mko_moment · 依賴：G3, mko_moment, mko_reverse

葉節點依據：mko_moment + mko_reverse + numeric_evaluation

獨立核對：用定積分 MKO 的矩公式（不用 FTC）：6·9/3−2·3/2+3=18−3+3=18；再依反向規則 ∫_2^{−1} f=−18，與 S15 一致。



S15.2 · equivalent操作前

\bigl(F(-1)+7\bigr)-\bigl(F(2)+7\bigr)

操作後

F(-1)-F(2)=-18

條件：無

規則：add_inverse · 依賴：S15

葉節點依據：add_inverse + add_assoc + add_comm

換用原函數 F+7：(F(−1)+7)−(F(2)+7)=F(−1)−F(2)=−18。加常數不改端點差，與 S13.2 消去 C 是同一件事。



S17.1 · implies操作前

K(x)=14x^3-3x^2+x

操作後

K'(x)=42x^2-6x+1,\quad K'(0)=1\neq 0

條件：無

規則：poly_deriv · 依賴：S17, poly_deriv

葉節點依據：poly_deriv + numeric_evaluation

逐項求導得 K′(x)=42x²−6x+1，所以 K′(0)=1≠0：上下限在 x=0 重合並不使導數為 0，因為上限以速度 2、下限以速度 1 移動。



S17.2 · implies操作前

f(u(x))\,u'(x)-f(l(x))\,l'(x),\quad u(x)=2x,\ l(x)=x

操作後

2f(2x)-f(x)=42x^2-6x+1

條件：無

規則：deriv_rules · 依賴：S17.1, S14, deriv_rules

葉節點依據：deriv_rules + poly_deriv + numeric_evaluation

MKO 假設 a2 的移動上下限公式給 f(2x)·2−f(x)·1=2(24x²−4x+1)−(6x²−2x+1)=42x²−6x+1，與 S17.1 相同（N7 為次數 2 的恆等式核對）。這也就是對 K(x)=F(2x)−F(x) 用合成規則：K′(x)=2F′(2x)−F′(x)。







## 逐步反向審查


- S17.2 · premise_audit · S17.1, deriv_rules, S14 — 這是兩種算法的一致性核對；合成規則的前提（F、u、l 可微）都成立。
- S17.1 · premise_audit · poly_deriv, numeric_evaluation — 只用多項式求導（N8）。
- S17 · premise_audit · S13, S14, forall_elim — S13 對任意實數端點成立，所以對每個 x 都可用；x<0 時端點是反向的，也被涵蓋。
- S16 · premise_audit · S10, G3, forall_elim, numeric_evaluation — 只需 S10 在 x=2 的特例與 f(2) 的計算（N5）。
- S15.2 · inverse_equivalence · add_inverse, add_assoc — 恆等式，雙向成立（N9）。
- S15.1 · premise_audit · mko_moment, mko_reverse, numeric_evaluation — 這是另一條路的數值核對（N4），不是 FTC 的證明。
- S15 · premise_audit · S13, S14, forall_elim, numeric_evaluation — 需要 S14 先確認 F′=f；端點反向不需另外處理，因為 S13 的 a、b 是任意的。
- S14 · premise_audit · G3, poly_deriv — 係數表相等推出函數相等；這一步沒有用有限個點取樣（MKO 假設 a3）。不宣稱原函數唯一：F+7 等其他原函數也可用。
- S13.2 · inverse_equivalence · add_assoc, add_comm, add_inverse — 對所有實數成立的恆等式，雙向成立。
- S13.1 · inverse_equivalence · G1, def_unfold — 展開定義與約定都是等式，兩向成立。
- S13 · inverse_equivalence · S12, G1, eq_replace — 每一步都是等值代換，從右讀到左同樣成立。
- S12 · premise_audit · S11, thm_zero_deriv — 推論要求在一個區間上導數處處為 0；若定義域是兩段分離的區間，結論只能是「在每一段上為常數」。MKO 採全 ℝ 前提，正好避開這個問題。
- S11 · premise_audit · G2, S10, deriv_rules — 導數規則要求兩函數在該點都可微，由 G2 與 S10 提供。不宣稱反向。
- S10 · premise_audit · S09, forall_intro — 推廣需要 x_0 未被特殊化；已檢查：沒有假設 x_0≠a，也沒有假設 h 的符號。
- S09 · sufficient_goal_reduction · S05, S08, func_limit_def, deriv_def — 目標 G：G′(x_0)=f(x_0)。足夠條件 H：上面的 ε–δ 敘述；H⇒G 由函數極限與導數的定義。H 由 S05 到 S08 正向證成，沒有把 G 當作前提。
- S08 · premise_audit · S04, S07, abs_rules, frac_rules — 需要 h≠0 才能除以 |h|；結論對每個 0<|h|<δ 成立。這是單向不等式。
- S07 · premise_audit · S06, int_bound, G1, abs_rules — 估計需要 p≤q、g 連續、|g|≤M；h<0 時先用 G1 的有向約定換成正向區間。只得到上界，不宣稱相等。
- S06 · premise_audit · S05, abs_rules, order_basics, case_analysis — 需要 |h|<δ；兩種情況涵蓋所有 h≠0。這是單向估計。
- S05 · premise_audit · G1, continuity_def — 需要 f 在 x_0 連續；若只有可積而無連續，這樣的 δ 可能不存在（見負面對照的階梯函數）。不宣稱反向。
- S04 · inverse_equivalence · S02, S03, int_linear, mul_inverse_nonzero — 反向：依線性把積分拆回兩項，再用 S03 與 S02 還原；每一步都是等式，前提 h≠0 不變。
- S03.2 · premise_audit · mko_reverse, mko_moment, order_basics — 需要反向規則與矩公式，兩者都來自 MKO 定積分；兩種情況覆蓋所有 h≠0。
- S03.1 · premise_audit · mko_moment — 矩公式要求端點 a≤b，此處由 h>0 保證；這一步不宣稱 h<0 的情形。
- S03 · inverse_equivalence · L_const_int — 兩式是同一個數，雙向成立；引理的兩種情況都已證。
- S02 · inverse_equivalence · int_additive, eq_congruence, add_inverse — 反向：兩邊同加 G(x_0) 回到可加性的等式；兩式表示同一個數。
- S01 · premise_audit · G1, deriv_def — 此步只寫出目標，不推出新事實。x_0 是任意的，S10 才能做全稱推廣；特別地不排除 x_0=a。





## 錯誤控制與反例

函數值為 0 不等於導數為 0MKO 指出的誤解：起點積分值為 0 就以為導數為 0。G(2)=∫_2^2 f=0 只說明累積從 0 開始；G′(2)=f(2)=21 是此刻的變化率（S16）。

上下限重合不等於導數為 0K(x)=∫_x^{2x} f 在 x=0 時上下限都是 0，K(0)=0；但上限移動速度 2、下限速度 1，K′(0)=2f(0)−f(0)=f(0)=1（S17）。

先核對 F′=f，而且要逐係數第二部分需要 F′=f 這個前提。候選 F₃(x)=1/2+x−(3/2)x²+2x³+(1/4)x⁴ 在 x=−1、0、1 三點有 F₃′=f，但 F₃′−f=x³−x 在 x=2 等於 6；用它算端點差會得 F₃(−1)−F₃(2)=−81/4，而不是 −18。有限取樣不能代替逐係數核對（MKO 假設 a3）。

連續性定義直接用一次，積分規則也依賴此假設點連續的定義只在 S05 直接展開，以控制 f(t)−f(x_0)；G1 的連續性亦供所引用的積分性質與 S07 使用。若 f 只可積不連續，例如 f(t)=0（t<0）、f(t)=1（t≥0），a=0，則 G(x)=max(x,0)，在 0 的右差商為 1、左差商為 0，G′(0) 不存在。


- G(x)=∫_2^x f(t)dt 滿足 G(2)=0，所以 G′(2)=0 → reject — 由第一部分，G′(2)=f(2)=21。
- K(x)=∫_x^{2x} f(t)dt 在 x=0 上下限重合，所以 K′(0)=0 → reject — K(x)=14x³−3x²+x，K′(0)=1。
- F₃(x)=1/2+x−(3/2)x²+2x³+(1/4)x⁴ 在 x=−1、0、1 都有 F₃′=f，所以 ∫_2^{−1} f=F₃(−1)−F₃(2) → reject — F₃′−f=x³−x，在 x=2 為 6≠0，前提 F₃′=f 不成立；F₃(−1)−F₃(2)=−81/4≠−18。
- 對任何可積函數 f（不必連續），G(x)=∫_0^x f 處處可微且 G′=f → reject — f(t)=0（t<0）、1（t≥0）給 G(x)=max(x,0)，G′(0) 不存在。
- ∫_a^b f=F(b)−F(a) 只在 a<b 時成立 → reject — S13 對任意實數 a、b 成立；S15 以 a=2>b=−1 算得 −18，並經矩公式核對。





## 結論與限制

在 f 於 ℝ 連續的前提下（並引用積分的可加、線性與估計性質），G(x)=∫_a^x f 處處可微且 G′=f；若 F′=f 於 ℝ，則對任意實數 a、b，∫_a^b f=F(b)−F(a)（另引用「導數處處為 0 則為常數」）。例：∫_2^{−1}(6t²−2t+1)dt=−18，矩公式獨立核對一致；以 a=2 的累積函數有 G(2)=0 但 G′(2)=21；K(x)=∫_x^{2x} f 有 K(0)=0 但 K′(0)=1。


- 第一部分由三條引用的積分性質（int_additive、int_linear、int_bound）推出；這些性質對一般連續函數未在 OCME 中物化，本稿也未證明。被積函數連續時積分存在，同樣是前提。
- 第二部分引用均值定理推論 thm_zero_deriv，本稿未證明。
- Spivak 的章節位置依記憶標示，尚未對原書核對，章節或定理編號可能需要修正。
- 例題數字只對這個 f 與 F 有效，不能取代一般證明。N11 只是 x=−1、0、1 三點的有限核對，用來顯示取樣不足。





## 驗證及來源綁定

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


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: f34b050fd0264c3575761dfd055ea69e5a8e7f1e68756823ca33ed236d0e4f17
- original source SHA-256: ddfe7d1b1540889b94b73bb5fa4bb929138d1e74fc22af8ec30063b704076861
- Lean: NOT_RUN · independent AI: NOT_MEASURED

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