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 dominates every fixed nonnegative integer power at
Statement
For every and every real ,
Facts & Assumptions
Given: and .
Every term of the exponential series is nonnegative at a nonnegative argument (The real exponential function and the number by a power series).
The exponential reciprocal identity is The exponential is positive and satisfies , and limits at infinity are Limits at and , and infinite limits at a point.
Proof
For , retain term of the series at : .
Hence .
The upper bound tends to , so the quotient tends to .
Depends on
- The real exponential function and the number $e$ by a power series
- The exponential is positive and satisfies $\exp(-x)=1/\exp(x)$
- Limits at $+\infty$ and $-\infty$, and infinite limits at a point
- The factorial $n!$ and the falling factorial $n^{\underline{k}}$, defined by recursion in $\mathbb{N}$
- The canonical natural $\iota(n) = n \cdot 1_F$ of a field
- Laws of finite sums and finite products
Used by
- A smooth flat refinement has a strict minimum on every line through the origin but no local extremum Counterexample
- The exponential is not uniformly continuous on ℝ Counterexample
- Concrete logarithmic, polynomial, and exponential growth comparisons Example
- The one-sided flat function is C^∞ with identically zero Taylor series Example
- The exponential roadmap and its circularity hazards Remark
- The logarithm grows more slowly than every positive real power Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 89 results over 24 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)
- MIT 18.102, Chapter 4 notes (standard reference, not scraped)