TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-27

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.

Every odd-degree real polynomial has a real root

Statement

Let $f (x) = a_{n} x^{n} + a_{n - 1} x^{n - 1} + \dots + a_{0} \in R [x]$ have odd degree $n \geq 1$ . Then there exists $c \in R$ with $f (c) = 0$ .

Facts & Assumptions

Given: A real polynomial $f (x) = a_{n} x^{n} + \dots + a_{0}$ of odd degree $n \geq 1$ .

[F1]

The degree hypothesis means $a_{n} \neq 0$ and $a_{i} = 0$ for every $i > n$ (Degree, leading coefficient and monic polynomial, with the zero polynomial having no degree).

[L1]

Every real polynomial function is continuous on $R$ (Sums, scalar multiples, products, absolute values, maxima, minima and quotients with nonvanishing denominator of continuous functions are continuous, as are constants, the identity and every polynomial function).

[L2]

A continuous function on a closed interval takes every intermediate value between its endpoint values (Intermediate value theorem, by bisection with a canonical left-half rule: a continuous function on $[a, b]$ takes every value between $f (a)$ and $f (b)$ ).

[F2]

The real numbers form an ordered field, so absolute values and the order laws behave as usual (The reals form a totally ordered field).

Proof

technique · direct

1.1F1F2algebra

Put $S : = \sum_{i < n} ∣ a_{i} ∣$ and $R : = 1 + \frac{S}{∣ a_{n} ∣} .$ Then $R > 1$ , and therefore $\sum_{i < n} ∣ a_{i} ∣ R^{i} \leq S R^{n - 1} < ∣ a_{n} ∣ R^{n} .$

2.1step 1.1F2algebra

The estimate in step 1.1 gives $∣ \sum_{i < n} a_{i} R^{i} ∣ \leq \sum_{i < n} ∣ a_{i} ∣ R^{i} < ∣ a_{n} ∣ R^{n} .$ Hence $f (R) = a_{n} R^{n} + \sum_{i < n} a_{i} R^{i}$ has the same sign as $a_{n}$ .

2.2step 1.1F1F2algebra

Because $n$ is odd, $(- R)^{n} = - R^{n}$ . Also $∣ \sum_{i < n} a_{i} (- R)^{i} ∣ \leq \sum_{i < n} ∣ a_{i} ∣ R^{i} < ∣ a_{n} ∣ R^{n},$ so $f (- R) = a_{n} (- R)^{n} + \sum_{i < n} a_{i} (- R)^{i}$ has the opposite sign from $a_{n}$ . Thus $f (- R)$ and $f (R)$ have opposite signs.

3.1L1L2step 2.2∎

By [L1], the polynomial function $f$ is continuous on $[- R, R]$ . Since step 2.2 shows that $0$ lies between $f (- R)$ and $f (R)$ , [L2] gives a point $c \in [- R, R]$ with $f (c) = 0$ .

Every odd-degree real polynomial has a real root

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources