TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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_nx^n+\cdots+a_1x+a_0\in\mathbb Z[x]$ with $a_n\ne0$ . If a reduced rational number $r/s$ , where $r,s\in\mathbb Z$ , $s>0$ , and $\gcd(r,s)=1$ , is a root of $f$ , then

$r\mid a_0\qquad\text{and}\qquad s\mid a_n.$

Facts & Assumptions

Given: An integer polynomial $f=a_nx^n+\cdots+a_0$ with $a_n\ne0$ and a root $r/s\in\mathbb 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\mid bc$ , then $a\mid c$ (If $\gcd(a,b) = 1$ and $a \mid bc$ then $a \mid c$ ; and if $a \mid c$ , $b \mid c$ and $\gcd(a,b) = 1$ then $ab \mid 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_nr^n+a_{n-1}r^{n-1}s+\cdots+a_1rs^{n-1}+a_0s^n=0$ .

givenL1L4L5L6algebra

2.1

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

step 1.1L2L3L7

3.1

The same equation shows $s\mid a_nr^n$ ; [L2], [L3], and [L7] remove the coprime factor $r$ one power at a time and give $s\mid a_n$ , proving both conclusions.

step 1.1L2L3L4L7∎

Depends on

Used by

The polynomial x²-2 is irreducible over ℚ Example

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 67 results over 21 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click 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)