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

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.

Rational root theorem

Statement

Let $f = a_{n} x^{n} + \dots + a_{1} x + a_{0} \in Z [x]$ with $a_{n} \neq 0$ . If a reduced rational number $r / s$ , where $r, s \in Z$ , $s > 0$ , and $\gcd (r, s) = 1$ , is a root of $f$ , then

$r ∣ a_{0} and s ∣ a_{n} .$

Facts & Assumptions

Given: An integer polynomial $f = a_{n} x^{n} + \dots + a_{0}$ with $a_{n} \neq 0$ and a root $r / s \in Q$ with $s > 0$ and $\gcd (r, s) = 1$ .

[L1]

Evaluation substitutes the chosen ring element into the finite coefficient expression, and a root has value zero (Evaluation and roots of a polynomial in a commutative target ring).

[L2]

Coprime integers have gcd $1$ (Coprime integers: $\gcd (a, b) = 1$ ).

[L3]

If $a, b$ are coprime and $a ∣ b c$ , then $a ∣ c$ (If $\gcd (a, b) = 1$ and $a ∣ b c$ then $a ∣ c$ ; and if $a ∣ c$ , $b ∣ c$ and $\gcd (a, b) = 1$ then $a b ∣ c$ ).

[L4]

The leading coefficient is the nonzero coefficient at the degree of a nonzero polynomial (Degree, leading coefficient and monic polynomial, with the zero polynomial having no degree).

[L5]

The rational numbers form a field, so multiplication by the nonzero denominator power preserves the root equation (The rationals form a field).

[L6]

The integers embed in the rationals preserving addition and multiplication (The integers embed in the rationals).

[L7]

The induction principle permits iteration of a divisibility implication through a positive power (The principle of mathematical induction).

Proof

technique · direct

1.1

By [L1], [L5], and the coefficient embedding [L6], multiplying $f (r / s) = 0$ by $s^{n}$ gives $a_{n} r^{n} + a_{n - 1} r^{n - 1} s + \dots + a_{1} r s^{n - 1} + a_{0} s^{n} = 0$ .

givenL1L4L5L6algebra

2.1

The equation shows $r ∣ a_{0} s^{n}$ ; [L2], [L3], and [L7] remove the coprime factor $s$ one power at a time and give $r ∣ a_{0}$ , including $r = 0$ , when the root equation itself gives $a_{0} = 0$ .

step 1.1L2L3L7

3.1

The same equation shows $s ∣ a_{n} r^{n}$ ; [L2], [L3], and [L7] remove the coprime factor $r$ one power at a time and give $s ∣ a_{n}$ , proving both conclusions.

step 1.1L2L3L4L7∎

Depends on

Used by

The rational algebraic integers are exactly the integers Corollary
The polynomial x²-2 is irreducible over ℚ Example
x³-3x+1 has discriminant 81 and Galois group A₃ over ℚ Example
x⁴-x-1 has Galois group S₄ over ℚ Example
x⁴+8x+12 has Galois group A₄ over ℚ Example

Dependency tree · two levels

29 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

Thomas W. Judson, Abstract Algebra: Theory and Applications, Theorem 17.15 (standard reference, not scraped)
Neil Donaldson, Math 120B Notes, Theorem 23.8(3) (standard reference, not scraped)