Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-21
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 p.

[L1]

If P,Q are complex polynomials, then P/Q is holomorphic on the open set where Q does not vanish (Complex polynomials are entire with the power-rule derivative, and rational functions are holomorphic wherever their denominator is nonzero).

[L2]

If p is a nonconstant complex polynomial, then ∣p(z)∣→∞ as ∣z∣→∞ (A nonconstant complex polynomial tends to infinite modulus and attains a global minimum modulus).

[L3]

A complex differentiable function is continuous (Complex differentiability at a point implies continuity there).

[L4]

Complex modulus is multiplicative, nonnegative, and zero exactly at zero, and it satisfies the triangle inequality (Conjugation is an involutive real-field automorphism, zz‾=∣z∣2, and modulus is definite, multiplicative, and subadditive).

[L5]

Under C=R2, the metric dC(z,w)=∣z−w∣ is the Euclidean metric (The Euclidean metric, convergence, Cauchy sequences, and continuity on the complex plane).

[L7]

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).

[L8]

Every bounded entire function is constant (Liouville's theorem: every bounded entire function is constant).

Proof

technique · contradiction
1.1givenassume-contra

Suppose, for contradiction, that p has no complex root.

2.1step 1.1L1

The denominator p is then nonzero throughout C, so [L1] makes g:=1/p entire.

3.1step 2.1L2L4choosealgebra

By [L2], choose R≥1 such that ∣p(z)∣≥1 whenever ∣z∣≥R; then step 2.1 and [L4] give ∣g(z)∣=1/∣p(z)∣≤1 on that exterior region.

3.2step 2.1L3L4algebra

By step 2.1 and [L3], g is continuous; the inequality ∣∣u∣−∣v∣∣≤∣u−v∣ derived from [L4] makes the real-valued function ∣g∣ continuous.

4.1step 3.1L4L5L6algebra

The closed disc K={z:∣z∣≤R} contains 0, is bounded, and is closed because ∣∣z∣−∣w∣∣≤∣z−w∣; by [L5] it is a nonempty closed bounded subset of R2, so [L6] makes it compact.

5.1step 3.2step 4.1L7

Applying [L7] to the continuous function ∣g∣ from step 3.2 on the compact set from step 4.1 gives a finite maximum M≥0 with ∣g(z)∣≤M for z∈K.

6.1step 3.1step 5.1algebra

If ∣z∣≤R, step 5.1 gives ∣g(z)∣≤M, while if ∣z∣≥R, step 3.1 gives ∣g(z)∣≤1; hence ∣g(z)∣≤max⁡{M,1} on the whole plane, with the boundary ∣z∣=R covered by both estimates.

7.1step 2.1step 6.1L8

The function g is entire by step 2.1 and bounded by step 6.1, so [L8] makes it constant.

8.1step 1.1step 2.1step 7.1L4algebradischarge-contradiction∎

The constant value of g=1/p is nonzero by [L4], so p=1/g is constant, contradicting the given nonconstancy; the assumption of step 1.1 is false, and p has a complex root.

Depends on

Used by

Dependency tree · two levels

63 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources