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 nonzero value of a nonconstant complex polynomial cannot be a local minimum of its modulus

Statement

If $p$ is nonconstant and $p (a) \neq 0$ , then $∣ p ∣$ is not minimal on any neighbourhood of $a$ . 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, The $n$ -th roots of a complex number and the $n$ distinct roots of unity for every $n \geq 1$ , The binomial theorem over the complex field, Laws of finite sums and finite products.

Facts & Assumptions

Given: A nonconstant polynomial $p$ and a point $a$ with $p (a) \neq 0$ .

[L1]

The $n$ -th roots of a complex number and the $n$ distinct roots of unity for every $n \geq 1$ supplies an $m$ th root of every nonzero complex number when $m \geq 1$ .

[L2]

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

[L3]

The binomial theorem over the complex field gives the finite expansion of $(a + z)^{n}$ in complex coefficients.

Proof

technique · constructive

1.1

By [L3], expanding $p (a + z) - p (a)$ gives a nonzero polynomial in $z$ (its top coefficient is the nonzero leading coefficient of $p$ ). Let $m \geq 1$ be its first nonzero degree, so $p (a + z) = p (a) + c_{m} z^{m} + z^{m + 1} q (z)$ with $c_{m} \neq 0$ . Choose by [L1] a unit complex number $u$ with $u^{m} = - p (a) \overline{c_{m}} / (∣ p (a) ∣ ∣ c_{m} ∣)$ . Then $\overline{p (a)} c_{m} u^{m} = - ∣ p (a) ∣ ∣ c_{m} ∣$ .

L1L3constructalgebra

1.2

Write $M$ for the sum of the moduli of the finitely many coefficients of $q$ . For $0 < t \leq 1$ , [L2] gives $∣ t^{m + 1} q (t u) ∣ \leq M t^{m + 1}$ . With $λ : = ∣ p (a) ∣ ∣ c_{m} ∣$ and $B : = 2 ∣ p (a) ∣ M + (∣ c_{m} ∣ + M)^{2} > 0$ , choose $0 < t < \min {1, λ / B}$ .

L2choose

2.1

Put $R = t^{m + 1} q (t u)$ . By step 1.1 and [L2], $∣ p (a + t u) ∣^{2} \leq ∣ p (a) ∣^{2} - 2 λ t^{m} + 2 ∣ p (a) ∣ M t^{m + 1} + (∣ c_{m} ∣ + M)^{2} t^{2 m} \leq ∣ p (a) ∣^{2} - 2 λ t^{m} + B t^{m + 1} < ∣ p (a) ∣^{2}$ . Thus $a + t u$ is arbitrarily close to $a$ and has strictly smaller modulus.

L2step 1.1step 1.2discharge-construct∎

Depends on

Used by

Fundamental theorem of algebra: every nonconstant complex polynomial has a complex root Theorem

Dependency tree · two levels

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