Solution (source code)

= Solution

Write the <rational number> as $r=p/q$ with <coprime integers> $p,q$ and $q>0$. Substituting into the <monic polynomial> and multiplying by $q^n$ gives
$$
p^n+a_{n-1}p^{n-1}q+\cdots+a_1pq^{n-1}+a_0q^n=0.
$$
All terms except the first are divisible by $q$, so $q\mid p^n$. If $q>1$, it has a <prime factor> dividing $p^n$, and the <Euclid lemma> implies that this prime divides $p$, contradicting <coprimality>. Thus $q=1$, proving this special case of the <rational root theorem>:
$$
\boxed{r\in\mathbb Q\ \Longrightarrow\ r\in\mathbb Z.}
$$