Fundamental theorem of calculus: proving G′=f from continuity, then ∫_a^b f=F(b)−F(a)

Goal and scope

Let f:ℝ→ℝ be continuous on all of ℝ, a∈ℝ, and G(x)=∫_a^x f(t)dt an oriented integral. (1) Prove that G is differentiable at every point with G′(x)=f(x); (2) if F:ℝ→ℝ is differentiable with F′=f, prove ∫_a^b f(t)dt=F(b)−F(a) for arbitrary real a, b; (3) with f(t)=6t²−2t+1 and the candidate F(x)=2x³−x²+x+1/2, compute ∫_2^{−1} f(t)dt, and explain why G(2)=0 does not give G′(2)=0 and why bounds coinciding at x=0 do not give a zero derivative.

Works under the MKO's sufficient premises: f continuous on all of ℝ and F differentiable on all of ℝ. The ε–δ argument for part (1) is written out in full, but it rests on three general properties of the integral (additivity over oriented intervals, linearity, and an estimate from an upper bound on the integrand's absolute value); for general continuous functions these are cited from the literature (citation_verified) and not proved here. Part (2) also cites 'a function with zero derivative everywhere is constant' (a corollary of the Mean Value Theorem, citation_verified). The polynomial integral in the example is cross-checked with the moment formula of the definite-integral MKO. Merely integrable discontinuous functions, one-sided endpoint derivatives and Lebesgue integration are not treated; the canonical MKO and its English edition are not changed.

Givens and symbols

• continuity_def
• func_limit_def
• abs_rules
• order_basics
• numeric_evaluation

• G1 — f:ℝ→ℝ is continuous on all of ℝ; a∈ℝ; G(x)=∫_a^x f(t)dt. Integrals are oriented: for x<a, ∫_a^x f=−∫_x^a f, and ∫_a^a f=0 (MKO assumptions a1 and a2).
• G2 — F:ℝ→ℝ is differentiable on all of ℝ and F′(x)=f(x) for every real x.
• G3 — Example: f(t)=6t²−2t+1 (ascending integer coefficients [1,−2,6], degree 2); candidate F(x)=2x³−x²+x+1/2 (ascending rational coefficients [1/2,1,−1,2] with positive denominators); endpoints a=2, b=−1.

• G(x)=\int_a^x f(t)\,dt — the accumulation function (oriented integral)
• F — an antiderivative of f: F′=f
• x_0 — an arbitrary fixed point
• h — a nonzero increment
• Q(h) — the difference quotient (G(x_0+h)−G(x_0))/h
• \varepsilon,\ \delta — error bound and neighbourhood radius
• D=F-G — the difference of the two antiderivatives
• K(x)=\int_x^{2x} f(t)\,dt — an integral with both bounds moving

Rules and sources

• continuity_def · prerequisite — Continuity (ε-δ): f is continuous at a if for every ε>0 there is δ>0 such that |f(x)−f(a)|<ε for every domain point x with |x−a|<δ.
• func_limit_def · prerequisite — Limit of a function: lim_{x→a} f(x)=L means that for every ε>0 there is δ>0 such that |f(x)−L|<ε for every domain point x with 0<|x−a|<δ (a must be a limit point of the domain).
• abs_rules · prerequisite — Absolute value (reals): |u|=u if u≥0 and |u|=−u if u<0; |u|≥0; |uv|=|u||v|; triangle inequality |u+v|≤|u|+|v|; |u|<r ⇔ −r<u<r.
• order_basics · prerequisite — Order of the reals: exactly one of u<v, u=v, u>v holds; u<v and v<w give u<w; u<v gives u+w<v+w; u<v and w>0 give uw<vw; u<v and w<0 give uw>vw.
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• def_unfold · prerequisite — Unfolding a definition: replacing a defined term by its definition (or folding it back) does not change whether a statement is true.
• eq_congruence · prerequisite — Congruence of equality: if u=v, applying the same defined operation f to both sides gives f(u)=f(v). Operating on one side only is not an instance of this rule.
• add_inverse · prerequisite — Additive inverse: every u has −u with u+(−u)=0; u−v means u+(−v).
• case_analysis · prerequisite — Proof by cases: if P∨Q holds and both P⇒R and Q⇒R are proved, then R holds. The cases must cover every possibility.
• neg_mul · prerequisite — Signs and multiplication: (−u)v=−(uv) and (−u)(−v)=uv.
• mul_inverse_nonzero · prerequisite — Inverse of a nonzero number: in ℚ, ℝ or ℂ, if u≠0 there is 1/u with u·(1/u)=1, and v/u means v·(1/u). 0 has no inverse, so v/0 is undefined.
• distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu.
• eq_replace · prerequisite — Replacement of equals: an expression inside a statement may be replaced by an equal expression without changing whether the statement is true.
• forall_elim · prerequisite — ∀-elimination (instantiation): if ∀x∈D, P(x) holds and a∈D, then P(a) holds.
• frac_rules · prerequisite — Fraction rules (all denominators nonzero): a/c+b/c=(a+b)/c; (a/b)(c/d)=(ac)/(bd); (a/b)/(c/d)=(ad)/(bc) (also needing c≠0); a/b=(ak)/(bk) for k≠0.
• forall_intro · prerequisite — ∀-introduction (generalization): if a statement is proved for an arbitrary element x, with no extra assumption on x, it holds for every x in the domain.
• add_assoc · prerequisite — Associativity of addition: (u+v)+w=u+(v+w).
• add_comm · prerequisite — Commutativity of addition: u+v=v+u.
• add_zero · prerequisite — Additive identity: u+0=u.
• power_laws · prerequisite — Integer exponent laws (base nonzero, or exponents positive integers): a^m·a^n=a^{m+n}, (a^m)^n=a^{mn}, (ab)^n=a^n b^n, a^0=1.
• deriv_def · cited — For f:ℝ→ℝ, its derivative at x is lim_{h→0,h≠0}(f(x+h)−f(x))/h when this finite two-sided limit exists; a finite step h must be nonzero. · mko-derivative
• deriv_rules · cited — For real functions differentiable at the relevant points, (f+g)′=f′+g′, (cf)′=cf′ and (fg)′=f′g+fg′; if g is differentiable at x and f at g(x), then (f∘g)′(x)=f′(g(x))g′(x). · mko-derivative-rules
• mko_moment · cited — For continuous polynomials on a finite interval a≤b, I(x^n,a,b)=(b^{n+1}−a^{n+1})/(n+1); for f=Σc_k x^k the moments are summed coefficientwise. · mko-definite-integral
• mko_reverse · cited — Reversing endpoints changes the sign: I(f,a,b)=−I(f,b,a); equal endpoints give I(f,a,a)=0. · mko-definite-integral
• int_additive · cited — If f is continuous on ℝ, then for any reals p, q, r (in any order, with the orientation convention) ∫_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 — If f and g are continuous on ℝ, then for any reals p, q (orientation convention) ∫_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 — If p≤q, g is continuous on [p,q], and |g(t)|≤M for every t in [p,q], then |∫_p^q g(t)dt|≤M(q−p). · OpenStax, Calculus Volume 1, Section 5.2, Comparison Properties of Integrals
• thm_zero_deriv · cited — If H:ℝ→ℝ is differentiable on all of ℝ and H′(x)=0 for every x, then H is constant on ℝ. · OpenStax, Calculus Volume 1, Section 4.4, Theorem 4.6, Corollary 1
• poly_deriv · prerequisite — Polynomials differentiate term by term: (Σ_{k=0}^{m} c_k x^k)′=Σ_{k=1}^{m} k c_k x^{k−1} on all of ℝ; this follows by repeated use of the sum, constant-multiple and product rules of the derivative-rules MKO.
• L_const_int · lemma — For any reals c, x_0 and h≠0: ∫_{x_0}^{x_0+h} c dt=ch.

Main derivation

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

Substeps and lemmas

\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

Reverse audits

• S17.2 · premise_audit · S17.1, deriv_rules, S14 — A consistency check of two computations; the chain rule's premises (F, u and l differentiable) all hold.
• S17.1 · premise_audit · poly_deriv, numeric_evaluation — Only polynomial differentiation is used (N8).
• S17 · premise_audit · S13, S14, forall_elim — S13 holds for arbitrary real endpoints, so it applies for every x; for x<0 the endpoints are reversed, and that is covered too.
• S16 · premise_audit · S10, G3, forall_elim, numeric_evaluation — It needs only S10 at x=2 and the value of f(2) (N5).
• S15.2 · inverse_equivalence · add_inverse, add_assoc — An identity, valid both ways (N9).
• S15.1 · premise_audit · mko_moment, mko_reverse, numeric_evaluation — A numeric cross-check by another route (N4), not a proof of the FTC.
• S15 · premise_audit · S13, S14, forall_elim, numeric_evaluation — It needs S14's check F′=f first; reversed endpoints need no special treatment because a and b in S13 are arbitrary.
• S14 · premise_audit · G3, poly_deriv — Equal coefficient lists give equal functions; no finite sampling is used (MKO assumption a3). Uniqueness of the antiderivative is not claimed: F+7 and others also work.
• S13.2 · inverse_equivalence · add_assoc, add_comm, add_inverse — An identity for all reals, so it holds both ways.
• S13.1 · inverse_equivalence · G1, def_unfold — Unfolding the definition and the convention are equalities, valid both ways.
• S13 · inverse_equivalence · S12, G1, eq_replace — Every move replaces equals by equals, so reading right to left works as well.
• S12 · premise_audit · S11, thm_zero_deriv — The corollary needs zero derivative throughout an interval; on two separated intervals one could only conclude 'constant on each piece'. The MKO's premise that the domain is all of ℝ avoids this.
• S11 · premise_audit · G2, S10, deriv_rules — The rules need both functions differentiable at the point, provided by G2 and S10. No converse is claimed.
• S10 · premise_audit · S09, forall_intro — Generalization needs x_0 not to have been specialized; checked: neither x_0≠a nor a sign of h was assumed.
• S09 · sufficient_goal_reduction · S05, S08, func_limit_def, deriv_def — Goal G: G′(x_0)=f(x_0). Sufficient condition H: the ε–δ statement above; H⇒G by the definitions of a function limit and of the derivative. H is proved forwards in S05 to S08; G is never used as a premise.
• S08 · premise_audit · S04, S07, abs_rules, frac_rules — h≠0 is needed to divide by |h|; the conclusion holds for every 0<|h|<δ. This is a one-way inequality.
• S07 · premise_audit · S06, int_bound, G1, abs_rules — The bound needs p≤q, g continuous and |g|≤M; for h<0 the orientation convention of G1 first turns it into a forward interval. Only an upper bound is obtained; equality is not claimed.
• S06 · premise_audit · S05, abs_rules, order_basics, case_analysis — It needs |h|<δ; the two cases cover every h≠0. This is a one-way estimate.
• S05 · premise_audit · G1, continuity_def — It needs continuity of f at x_0; with integrability alone such a δ may fail to exist (see the step-function negative control). No converse is claimed.
• S04 · inverse_equivalence · S02, S03, int_linear, mul_inverse_nonzero — Backward: split the integral by linearity and restore with S03 and S02; every move is an equality and the premise h≠0 is unchanged.
• S03.2 · premise_audit · mko_reverse, mko_moment, order_basics — It needs the reversal rule and the moment formula, both from the definite-integral MKO; the two cases cover every h≠0.
• S03.1 · premise_audit · mko_moment — The moment formula needs endpoints a≤b, which h>0 guarantees; the case h<0 is not claimed here.
• S03 · inverse_equivalence · L_const_int — Both expressions are the same number, so the step is two-way; both cases of the lemma are proved.
• S02 · inverse_equivalence · int_additive, eq_congruence, add_inverse — Backward: add G(x_0) to both sides to return to the additivity equation; both expressions name the same number.
• S01 · premise_audit · G1, deriv_def — This step only states the goal and derives nothing new. x_0 is arbitrary, which allows the generalization in S10; in particular x_0=a is not excluded.

Error controls and negative controls

A zero value is not a zero derivative

The misconception the MKO names: since the integral is 0 at the starting point, the derivative must be 0. G(2)=∫_2^2 f=0 only says the accumulation starts at 0; G′(2)=f(2)=21 is the rate of change at that moment (S16).

Coinciding bounds do not force a zero derivative

K(x)=∫_x^{2x} f has both bounds equal to 0 at x=0, so K(0)=0; but the upper bound moves at speed 2 and the lower at speed 1, so K′(0)=2f(0)−f(0)=f(0)=1 (S17).

Check F′=f first, and coefficientwise

Part (2) needs the premise F′=f. The candidate F₃(x)=1/2+x−(3/2)x²+2x³+(1/4)x⁴ satisfies F₃′=f at x=−1, 0, 1, but F₃′−f=x³−x equals 6 at x=2; using it gives the endpoint difference F₃(−1)−F₃(2)=−81/4 instead of −18. Finite sampling cannot replace the coefficientwise check (MKO assumption a3).

Continuity is invoked directly once and also supports the integral rules

The definition of pointwise continuity is used directly only in S05 to control f(t)−f(x_0); G1's continuity hypothesis also supports the cited integral properties and S07. If f is merely integrable, for example f(t)=0 for t<0 and f(t)=1 for t≥0 with a=0, then G(x)=max(x,0), whose right quotient at 0 is 1 and left quotient is 0, so G′(0) does not exist.

• G(x)=∫_2^x f(t)dt has G(2)=0, so G′(2)=0 → reject — By part (1), G′(2)=f(2)=21.
• K(x)=∫_x^{2x} f(t)dt has coinciding bounds at x=0, so K′(0)=0 → reject — K(x)=14x³−3x²+x, so K′(0)=1.
• F₃(x)=1/2+x−(3/2)x²+2x³+(1/4)x⁴ has F₃′=f at x=−1, 0, 1, so ∫_2^{−1} f=F₃(−1)−F₃(2) → reject — F₃′−f=x³−x is 6≠0 at x=2, so the premise F₃′=f fails; F₃(−1)−F₃(2)=−81/4≠−18.
• For every integrable f (not necessarily continuous), G(x)=∫_0^x f is differentiable everywhere with G′=f → reject — f(t)=0 for t<0 and 1 for t≥0 gives G(x)=max(x,0), and G′(0) does not exist.
• ∫_a^b f=F(b)−F(a) holds only when a<b → reject — S13 holds for arbitrary real a, b; S15 computes −18 with a=2>b=−1, confirmed by the moment formula.

Result and limitations

With f continuous on ℝ (and citing additivity, linearity and the bound for integrals), G(x)=∫_a^x f is differentiable everywhere with G′=f; if F′=f on ℝ, then ∫_a^b f=F(b)−F(a) for arbitrary real a, b (also citing 'zero derivative everywhere implies constant'). Example: ∫_2^{−1}(6t²−2t+1)dt=−18, confirmed independently by the moment formula; the accumulation function with a=2 has G(2)=0 but G′(2)=21; K(x)=∫_x^{2x} f has K(0)=0 but K′(0)=1.

• Part (1) is derived from three cited integral properties (int_additive, int_linear, int_bound); for general continuous functions they are not materialized in OCME and are not proved here. Existence of the integral for a continuous integrand is likewise a premise.
• Part (2) cites the Mean Value Theorem corollary thm_zero_deriv, which is not proved here.
• The Spivak chapter locations are given from memory and have not been checked against the book; chapter or theorem numbers may need correction.
• The example's numbers hold for this f and F only and cannot replace the general proof. N11 is only a finite check at x=−1, 0, 1, used to show that sampling is insufficient.

Verification and source binding

14 declared checks for this guide; only the listed expressions are covered.

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

Same-source full JSON (formulas, ASTs, controls and revision log)