LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-02

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.

A nonconstant complex polynomial tends to infinite modulus and attains a global minimum modulus

Statement

If $p$ is a nonconstant complex polynomial, then $∣ p (z) ∣ \to \infty$ as $∣ z ∣ \to \infty$ , and $∣ p ∣$ attains a global minimum on $C$ . The conventions and prerequisite facts used below are recorded in Formal complex polynomials, evaluation, degree, leading coefficient, and monic polynomials, Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive, Heine-Borel in $R^{n}$ : with the Euclidean metric a subset of $R^{n}$ 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, A vector-valued function has a limit, or is continuous, if and only if each of its components does; with the algebra of continuous vector-valued functions, Laws of finite sums and finite products.

Facts & Assumptions

Given: A nonconstant polynomial $p (z) = a_{n} z^{n} + \sum_{k < n} a_{k} z^{k}$ with $a_{n} \neq 0$ .

[L1]

Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive gives $∣ u v ∣ = ∣ u ∣ ∣ v ∣$ and $∣ u + v ∣ \leq ∣ u ∣ + ∣ v ∣$ .

[L2]

Heine-Borel in $R^{n}$ : with the Euclidean metric a subset of $R^{n}$ 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 says that every closed box in $R^{2}$ is compact.

[L3]

A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value gives a minimum for a continuous real-valued function on a nonempty compact metric space.

[L4]

A vector-valued function has a limit, or is continuous, if and only if each of its components does; with the algebra of continuous vector-valued functions makes a map into $R^{2}$ continuous exactly when its two components are continuous.

Proof

technique · direct

1.1

Put $C : = \sum_{k < n} ∣ a_{k} ∣$ . For $r = ∣ z ∣ \geq 1$ , [L1] gives $∣ p (z) ∣ \geq ∣ a_{n} ∣ r^{n} - \sum_{k < n} ∣ a_{k} ∣ r^{k} \geq r^{n} (∣ a_{n} ∣ - C / r) .$ Thus for $r \geq 2 C / ∣ a_{n} ∣$ the right side is at least $(∣ a_{n} ∣ / 2) r^{n}$ , which tends to $+ \infty$ .

L1algebra

1.2

Writing $z = x + i y$ , each coordinate projection is continuous because $∣ x - x_{0} ∣, ∣ y - y_{0} ∣ \leq ∥ (x, y) - (x_{0}, y_{0}) ∥$ . The identity $u v - u_{0} v_{0} = u (v - v_{0}) + v_{0} (u - u_{0})$ proves continuity of products, so induction over the finite expression makes both coordinate polynomials of $p (x + i y)$ continuous. Then [L4] makes $p$ and $∣ p ∣$ continuous.

2.1

Choose $R \geq 1$ so that the lower bound of step 1.1 is $> ∣ p (0) ∣$ when $∣ z ∣ > R$ . The closed square $K = [- R, R]^{2} \subseteq R^{2} = C$ is nonempty and compact by [L2]; outside $K$ one has $∣ z ∣ > R$ . By [L3] and step 1.2, let $a \in K$ minimize $∣ p ∣$ on $K$ .

L2L3step 1.1step 1.2

3.1

Since $0 \in K$ , this minimizer satisfies $∣ p (a) ∣ \leq ∣ p (0) ∣$ . Step 2.1 makes every point outside $K$ have strictly larger modulus, so $a$ is a global minimizer.

step 2.1∎

Depends on

Used by

Dependency tree · two levels

70 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

J. Lebl, Basic Analysis I: The Fundamental Theorem of Algebra (standard reference, not scraped)