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 complex exponential series converges absolutely for every complex argument
Statement
For every , the series converges absolutely.
Facts & Assumptions
Given: .
A complex series converges absolutely when its real modulus series converges (Complex series, absolute convergence, complex power series, and radius of convergence).
Complex modulus is multiplicative, and natural factorials are positive and nonzero (Conjugation is an involutive real-field automorphism, , and modulus is definite, multiplicative, and subadditive, Integer powers in the complex field, The factorial and the falling factorial , defined by recursion in , Canonical naturals are positive and strictly increasing).
For every real , the real series converges absolutely (The exponential series converges absolutely for every real argument).
Absolute convergence of a complex series implies convergence (Every absolutely convergent complex series converges, and rearrangements preserve its sum).
Proof
Each factorial denominator is nonzero, and multiplicativity of modulus gives . Thus its modulus series is the real exponential series at the nonnegative real .
By [F3] this modulus series converges; [F1] makes the complex series absolutely convergent, and [F4] gives convergence as well.
Depends on
Complex series, absolute convergence, complex power series, and radius of convergence
Integer powers in the complex field
The factorial and the falling factorial , defined by recursion in
Canonical naturals are positive and strictly increasing
Conjugation is an involutive real-field automorphism, , and modulus is definite, multiplicative, and subadditive
The exponential series converges absolutely for every real argument
Every absolutely convergent complex series converges, and rearrangements preserve its sum