[proofplan] The statement is exactly the good-prime characteristic-polynomial part of Deligne's construction of the Galois representation attached to the modular eigenform $f$. We first isolate the hypotheses inherited from Deligne's theorem and check that the chosen prime $p$ lies in the good range. Deligne's theorem then gives that $\rho_{f,\lambda}$ is unramified at $p$ and identifies the trace and determinant of geometric Frobenius; substituting those two values into the characteristic polynomial of a two-dimensional linear operator gives the desired formula. [/proofplan] [step:Check that the prime lies in the good range of Deligne's theorem] Let $E_{f,\lambda}$ denote the coefficient field completed at the place $\lambda$, and let \begin{align*} \rho_{f,\lambda}: \operatorname{Gal}(\overline{\mathbb{Q}}/\mathbb{Q}) &\to GL_2(E_{f,\lambda}) \end{align*} be the two-dimensional representation supplied by Deligne's theorem. The hypothesis $p \nmid Nl$ says simultaneously that $p$ is prime to the level $N$ and that $p$ is not the rational prime below $\lambda$. Hence $p$ is a prime of good reduction for the modular curve of level $N$ and is away from the coefficient characteristic of the $\lambda$-adic representation. [/step] [step:Apply Deligne's good-prime Frobenius formula] By Deligne's theorem for the representation attached to the eigenform $f$, the representation $\rho_{f,\lambda}$ is unramified at every prime $p \nmid Nl$. Therefore the conjugacy class of \begin{align*} \rho_{f,\lambda}(\operatorname{Frob}_p) \in GL_2(E_{f,\lambda}) \end{align*} is defined. Deligne's theorem further identifies its trace and determinant as \begin{align*} \operatorname{tr}\left(\rho_{f,\lambda}(\operatorname{Frob}_p)\right) &= a_p(f), \\ \det\left(\rho_{f,\lambda}(\operatorname{Frob}_p)\right) &= \varepsilon(p)p. \end{align*} Here $a_p(f)$ is the $p$-th Hecke eigenvalue of $f$, and $\varepsilon(p)$ is the value at $p$ of the nebentypus character of $f$. [guided] The condition $p \nmid Nl$ is exactly the condition under which Deligne's good-prime theorem applies. Since $p$ is prime to $N$, the modular curve has good reduction at $p$; since $p \ne l$, the $\lambda$-adic representation can be evaluated at a Frobenius conjugacy class at $p$ without ramification interference. Deligne's theorem therefore gives two pieces of data for the linear operator \begin{align*} \rho_{f,\lambda}(\operatorname{Frob}_p): E_{f,\lambda}^2 &\to E_{f,\lambda}^2. \end{align*} First, the representation is unramified at $p$, so $\operatorname{Frob}_p$ is meaningful up to conjugacy and the trace and determinant are independent of the chosen representative. Second, the theorem computes those invariants: \begin{align*} \operatorname{tr}\left(\rho_{f,\lambda}(\operatorname{Frob}_p)\right) &= a_p(f), \\ \det\left(\rho_{f,\lambda}(\operatorname{Frob}_p)\right) &= \varepsilon(p)p. \end{align*} The first scalar is the Hecke eigenvalue of $f$ at $p$, and the second scalar is the nebentypus value at $p$ multiplied by $p$. [/guided] [/step] [step:Convert trace and determinant into the characteristic polynomial] Let \begin{align*} A := \rho_{f,\lambda}(\operatorname{Frob}_p) \in GL_2(E_{f,\lambda}). \end{align*} For any $2 \times 2$ matrix $A$ over a field, the characteristic polynomial is \begin{align*} \det(XI-A)=X^2-\operatorname{tr}(A)X+\det(A). \end{align*} Substituting the trace and determinant computed above gives \begin{align*} \det\left(XI-\rho_{f,\lambda}(\operatorname{Frob}_p)\right) &=X^2-\operatorname{tr}\left(\rho_{f,\lambda}(\operatorname{Frob}_p)\right)X +\det\left(\rho_{f,\lambda}(\operatorname{Frob}_p)\right) \\ &=X^2-a_p(f)X+\varepsilon(p)p. \end{align*} This is the asserted characteristic polynomial. [/step]