Alphabeta MathHow 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 is positive and satisfies
Statement
For every real , and
Facts & Assumptions
Given: .
Every nonzero square in an ordered field is positive (Squares of nonzero elements are positive).
Proof
Setting in [L1] gives , so both factors are nonzero.
Also , so it is nonnegative; by step 1.1 and [L2] it is positive.
Dividing the identity in step 1.1 by gives the reciprocal formula.
Depends on
Used by
- exp(x+iy)=eˣ(cos y+i sin y), |exp(x+iy)|=eˣ, and e^iπ+1=0 Corollary
- A discontinuous positive solution of F(x+y)=F(x)F(y) Counterexample
- The six hyperbolic functions and their natural domains Definition
- Fubini computes ∫₀¹∫₋₁¹ x exp(xy) dx dy by reversing the order Example
- The log-free product limit (1-2/n)ⁿ→exp(-2) Example
- The one-sided flat function is C^∞ with identically zero Taylor series Example
- Addition formulas, identities, parity, and derivatives of the hyperbolic functions Theorem
- Holder's inequality for finite sums and conjugate real exponents Theorem
- Minkowski's inequality for finite sums and real exponent p greater than one 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 exponent, product, quotient, and iterated-power laws for positive real bases and real exponents Theorem
- The exponential dominates every fixed nonnegative integer power at +∞ Theorem
- The exponential function is strictly increasing Theorem
- The exponential is the unique solution of y'=y with y(0)=1 Theorem
- The exponential tends to +∞ at +∞ and to 0 at -∞ Theorem
- Young's inequality for conjugate real exponents Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 73 results over 15 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)
- J. K. Hunter, An Introduction to Real Analysis, Chapter 10 (standard reference, not scraped)
- S. G. Johnson, Exponential Functions (standard reference, not scraped)