Alphabeta Math
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)=anxn+an−1xn−1+⋯+a0∈R[x] have odd degree n≥1. Then there exists c∈R with f(c)=0.

Facts & Assumptions

Given: A real polynomial f(x)=anxn+⋯+a0 of odd degree n≥1.

[F1]

The degree hypothesis means an≠0 and ai=0 for every i>n (Degree, leading coefficient and monic polynomial, with the zero polynomial having no degree).

[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:=∑i<n∣ai∣ and R:=1+S∣an∣. Then R>1, and therefore ∑i<n∣ai∣Ri≤SRn−1<∣an∣Rn.

2.1step 1.1F2algebra

The estimate in step 1.1 gives ∣∑i<naiRi∣≤∑i<n∣ai∣Ri<∣an∣Rn. Hence f(R)=anRn+∑i<naiRi has the same sign as an.

2.2step 1.1F1F2algebra

Because n is odd, (−R)n=−Rn. Also ∣∑i<nai(−R)i∣≤∑i<n∣ai∣Ri<∣an∣Rn, so f(−R)=an(−R)n+∑i<nai(−R)i has the opposite sign from an. 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∈[−R,R] with f(c)=0.

Depends on

Used by

Dependency tree · two levels

35 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