How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced — the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted — a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated — a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
The exponential function is strictly increasing
Statement
The exponential function is continuous and strictly increasing on .
Facts & Assumptions
Given: The exponential function.
Its derivative equals itself (The exponential function is smooth and ) and it is everywhere positive (The exponential is positive and satisfies ).
The mean value theorem applies to a continuous function on a closed interval and converts a positive interior derivative into strict increase (The mean value theorem, as the case of Cauchy's: for continuous on with and differentiable on there is with ). A power-series sum is continuous at every point strictly inside its convergence interval, and the exponential series has infinite radius (The sum of a real power series is continuous at every point strictly inside its interval of convergence, The exponential series converges absolutely for every real argument).
Proof
If , the mean value theorem gives for some .
Both factors on the right are positive, so . Continuity is the cited power-series conclusion.
Depends on
- The exponential series converges absolutely for every real argument
- The exponential function is smooth and $(\exp)'=\exp$
- The exponential is positive and satisfies $\exp(-x)=1/\exp(x)$
- The mean value theorem, as the case $g(x) = x$ of Cauchy's: for $f$ continuous on $[a,b]$ with $a < b$ and differentiable on $(a,b)$ there is $c \in (a,b)$ with $f(b) - f(a) = f'(c)(b-a)$
- The sum of a real power series is continuous at every point strictly inside its interval of convergence
Used by
- The exponential is a continuous bijection from ℝ onto (0,∞) Corollary
- A discontinuous positive solution of F(x+y)=F(x)F(y) Counterexample
- f(x+iy)=eˣ(cos 2y+isin 2y) is continuous, satisfies f(z+w)=f(z)f(w) and f(1)=e, but is not the standard complex exponential Counterexample
- The exponential is not uniformly continuous on ℝ Counterexample
- The six hyperbolic functions and their natural domains Definition
- xˣ tends to one as x tends to zero from the right Example
- ker(exp)=2π iℤ, and exp z=exp w exactly when z-w∈2π iℤ Theorem
- Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm Theorem
- Regular normalized multiplicative Cauchy equations characterize the exponential Theorem
- The rational-supremum construction of real powers agrees with the exponential construction Theorem
- The two-point convexity inequality for the exponential function Theorem
- Under square summability, the signed product of (1+pₙ) converges iff the series of pₙ converges Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 90 results over 18 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.
Sources
- MIT OpenCourseWare 18.100B Real Analysis, Spring 2025 full lecture notes (standard reference, not scraped)
- J. Lebl, Basic Analysis, Logarithm and Exponential (standard reference, not scraped)