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

目標與範圍

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

逐步主鏈

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)

G(x_0+h)-G(x_0)

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

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

f(x_0)\,h

\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

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}

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}

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

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

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

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

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

G'(x_0)=f(x_0)

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

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

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

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

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

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

F(b)-F(a)

\int_a^b f(t)\,dt

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

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

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

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

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

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

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

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

局部子步與引理

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

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

\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

G(a)

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

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

G(b)-G(a)

\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

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

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

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

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

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

逐步反向審查

• 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 不等於導數為 0

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

上下限重合不等於導數為 0

K(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、反控制與修訂記錄）