[proofplan]
The statement is a transfer of the [Root Bound for Integral Domains](/theorems/1708) from $\mathbb{Z}[X]$ to $\mathbb{F}_p[X]$ via the mod-$p$ reduction homomorphism. The hypothesis $p \nmid (\text{leading coefficient})$ ensures the reduced polynomial $\bar f$ still has degree $n$ in $\mathbb{F}_p[X]$. Since $p$ is prime, $\mathbb{F}_p$ is a field, hence an integral domain, so Theorem 1708 applies to $\bar f$ and bounds its roots by $n$. Roots of $\bar f$ in $\mathbb{F}_p$ are in bijection with residue classes of solutions to $f(x) \equiv 0 \pmod p$.
[/proofplan]
[step:Pass from $\mathbb{Z}[X]$ to $\mathbb{F}_p[X]$ via the reduction homomorphism]
The reduction-mod-$p$ map $\mathbb{Z} \to \mathbb{F}_p = \mathbb{Z}/p\mathbb{Z}$, $a \mapsto \bar a$, extends coefficientwise to a ring homomorphism
\begin{align*}
\pi_p : \mathbb{Z}[X] &\to \mathbb{F}_p[X] \\
\sum_{i=0}^{n} a_i X^i &\mapsto \sum_{i=0}^{n} \bar{a}_i X^i.
\end{align*}
Write $\bar f := \pi_p(f)$. Since $\pi_p$ is a ring homomorphism, $\bar f(\bar x) = \overline{f(x)}$ for all $x \in \mathbb{Z}$; in particular,
\begin{align*}
f(x) \equiv 0 \pmod{p} \iff \bar{f}(\bar{x}) = 0 \text{ in } \mathbb{F}_p.
\end{align*}
Therefore the number of solutions of $f(x) \equiv 0 \pmod p$ modulo $p$ equals the number of roots of $\bar f$ in $\mathbb{F}_p$:
\begin{align*}
\#\{\bar{x} \in \mathbb{F}_p : f(x) \equiv 0 \pmod{p}\} = \#\{\bar{x} \in \mathbb{F}_p : \bar{f}(\bar{x}) = 0\} = \#Z(\bar{f}).
\end{align*}
[/step]
[step:Verify that $\bar f$ is non-zero of degree $n$ in $\mathbb{F}_p[X]$]
Let $a_n \in \mathbb{Z}$ be the leading coefficient of $f$, so $f(X) = a_n X^n + (\text{lower-order terms})$ with $a_n \neq 0$ and $\deg(f) = n$. The hypothesis is $p \nmid a_n$, which means precisely $\bar{a}_n \neq 0$ in $\mathbb{F}_p$. Consequently the $X^n$-coefficient of $\bar f$ is $\bar{a}_n \neq 0$, so
\begin{align*}
\deg(\bar{f}) = n \quad \text{and} \quad \bar{f} \neq 0 \text{ in } \mathbb{F}_p[X].
\end{align*}
[guided]
We need both non-vanishing and preservation of degree to invoke the root-bound theorem. Observe that $\pi_p$ can lower degree: the polynomial $pX + 1 \in \mathbb{Z}[X]$ has degree $1$, but reducing mod $p$ gives the constant polynomial $1 \in \mathbb{F}_p[X]$, of degree $0$. This degree collapse happens precisely when $p$ divides the leading coefficient — which is exactly what the hypothesis $p \nmid a_n$ rules out.
Checking explicitly: $p \nmid a_n$ is the same as $a_n \not\equiv 0 \pmod p$, which is the same as $\bar{a}_n \neq 0$ in $\mathbb{F}_p$. So the $X^n$-coefficient of $\bar f$ is the non-zero element $\bar a_n$, and all higher-order coefficients are zero (because they are zero already in $f$). Therefore $\deg(\bar f) = n$ and $\bar f \neq 0$.
Without this hypothesis the conclusion is false in general: over $\mathbb{Z}/4\mathbb{Z}$ (not a field, but the point is the same) the polynomial $2X$ has degree $1$ but every even integer is a root, so more than one residue class satisfies the congruence.
[/guided]
[/step]
[step:Apply the Root Bound for Integral Domains over $\mathbb{F}_p$]
Since $p$ is prime, $\mathbb{F}_p = \mathbb{Z}/p\mathbb{Z}$ is a field, and every field is an integral domain. The [Root Bound for Integral Domains](/theorems/1708) applied to $\bar f \in \mathbb{F}_p[X]$ — which we have just verified is non-zero of degree $n$ — yields
\begin{align*}
\#Z(\bar{f}) \leq n.
\end{align*}
Combining with the bijection from the first step:
\begin{align*}
\#\{\bar{x} \in \mathbb{F}_p : f(x) \equiv 0 \pmod{p}\} = \#Z(\bar{f}) \leq n,
\end{align*}
which is the stated bound on the number of solutions modulo $p$.
[/step]
