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.
Fundamental theorem of algebra by Liouville's theorem
Statement
Every nonconstant complex polynomial has a complex root.
This proof uses Liouville's theorem and is independent of the minimum-modulus proof cited in the accompanying agreement remark.
Facts & Assumptions
Given: A nonconstant complex polynomial .
If are complex polynomials, then is holomorphic on the open set where does not vanish (Complex polynomials are entire with the power-rule derivative, and rational functions are holomorphic wherever their denominator is nonzero).
If is a nonconstant complex polynomial, then as (A nonconstant complex polynomial tends to infinite modulus and attains a global minimum modulus).
A complex differentiable function is continuous (Complex differentiability at a point implies continuity there).
Complex modulus is multiplicative, nonnegative, and zero exactly at zero, and it satisfies the triangle inequality (Conjugation is an involutive real-field automorphism, , and modulus is definite, multiplicative, and subadditive).
Under , the metric is the Euclidean metric (The Euclidean metric, convergence, Cauchy sequences, and continuity on the complex plane).
A subset of Euclidean space is compact if and only if it is closed and bounded (Heine-Borel in : with the Euclidean metric a subset of is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line).
A continuous real-valued function on a nonempty compact metric space is bounded and attains a maximum (A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value).
Every bounded entire function is constant (Liouville's theorem: every bounded entire function is constant).
Proof
Suppose, for contradiction, that has no complex root.
The denominator is then nonzero throughout , so [L1] makes entire.
By [L2], choose such that whenever ; then step 2.1 and [L4] give on that exterior region.
By step 2.1 and [L3], is continuous; the inequality derived from [L4] makes the real-valued function continuous.
The closed disc contains , is bounded, and is closed because ; by [L5] it is a nonempty closed bounded subset of , so [L6] makes it compact.
Applying [L7] to the continuous function from step 3.2 on the compact set from step 4.1 gives a finite maximum with for .
If , step 5.1 gives , while if , step 3.1 gives ; hence on the whole plane, with the boundary covered by both estimates.
The function is entire by step 2.1 and bounded by step 6.1, so [L8] makes it constant.
The constant value of is nonzero by [L4], so is constant, contradicting the given nonconstancy; the assumption of step 1.1 is false, and has a complex root.
Depends on
Liouville's theorem: every bounded entire function is constant
Complex polynomials are entire with the power-rule derivative, and rational functions are holomorphic wherever their denominator is nonzero
A nonconstant complex polynomial tends to infinite modulus and attains a global minimum modulus
Complex differentiability at a point implies continuity there
Conjugation is an involutive real-field automorphism, , and modulus is definite, multiplicative, and subadditive
The Euclidean metric, convergence, Cauchy sequences, and continuity on the complex plane
Heine-Borel in : with the Euclidean metric a subset of is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line
A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value