Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passverified 2026-08-10 (gpt-5.6-terra-codex-subscription)
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 tends to ++\infty at ++\infty and to 00 at -\infty

Statement

exp(x)+(x+),exp(x)0(x),\exp(x)\to+\infty\quad(x\to+\infty),\qquad \exp(x)\to0\quad(x\to-\infty), and the range of exp\exp is contained in (0,)(0,\infty) and is unbounded above with infimum 00.

Facts & Assumptions

Given: The exponential series.

[L1]

For x0x\ge0, every exponential-series term is nonnegative, so its sum dominates every partial sum and in particular exp(x)1+x\exp(x)\ge1+x (The real exponential function and the number ee by a power series, A series of nonnegative terms converges iff its partial sums are bounded, and then the sum is their supremum).

[L2]

exp(x)=1/exp(x)>0\exp(-x)=1/\exp(x)>0 (The exponential is positive and satisfies exp(x)=1/exp(x)\exp(-x)=1/\exp(x)).

[L3]

Finite and infinite limits of functions at infinity have the quantified definitions in Limits at ++\infty and -\infty, and infinite limits at a point.

Proof

technique · direct
1.1

Given a real MM, every x>max{0,M1}x>\max\{0,M-1\} satisfies exp(x)1+x>M\exp(x)\ge1+x>M. Hence exp(x)+\exp(x)\to+\infty.

L1L3
1.2

Given ε>0\varepsilon>0, choose X>0X>0 with 1+X>1/ε1+X>1/\varepsilon. If x<Xx<-X, then x>X-x>X, so [L1] gives exp(x)1x>1+X>1/ε\exp(-x)\ge1-x>1+X>1/\varepsilon; [L2] yields 0<exp(x)<ε0<\exp(x)<\varepsilon.

L1L2choose
2.1

The range assertions follow from positivity and the two limit conclusions.

step 1.1step 1.2L2

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 82 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