[proofplan] We prove the theorem by invoking the modularity theorem of Wiles, Taylor-Wiles, and Breuil-Conrad-Diamond-Taylor in its final form for elliptic curves over $\mathbb Q$. For the given elliptic curve $E/\mathbb Q$, we name its conductor $N_E$ and its good-prime Frobenius trace $a_p(E)$. The cited modularity theorem produces a weight $2$ normalized newform of level $N_E$ whose associated Galois representation agrees with the Tate-module representation of $E$; comparing traces of Frobenius at every prime of good reduction gives the displayed coefficient formula. [/proofplan] [step:Name the conductor and the good-prime Frobenius traces] Let $E/\mathbb Q$ be the elliptic curve in the theorem statement. Let $N_E \in \mathbb N$ denote the conductor of $E$. For each prime number $p$ of good reduction for $E$, let $\widetilde{E}_p/\mathbb F_p$ denote the reduction of $E$ modulo $p$, and define the Frobenius trace of $E$ at $p$ by \begin{align*} a_p(E) := p + 1 - |\widetilde{E}_p(\mathbb F_p)|. \end{align*} Since $p$ is a prime of good reduction, $\widetilde{E}_p$ is an elliptic curve over $\mathbb F_p$, so the finite set $\widetilde{E}_p(\mathbb F_p)$ is well-defined. [/step] [step:Apply the modularity theorem for elliptic curves over $\mathbb Q$] We use the modularity theorem of Wiles, Taylor-Wiles, and Breuil-Conrad-Diamond-Taylor in the following form: for every elliptic curve $E/\mathbb Q$ with conductor $N_E$, there exists a weight $2$ normalized cuspidal newform $f \in S_2(\Gamma_0(N_E))$ whose associated compatible system of two-dimensional $\ell$-adic Galois representations agrees with the compatible system attached to $E$. The hypotheses of this theorem are exactly satisfied because the object in scope is an elliptic curve over $\mathbb Q$, and $N_E$ has been defined as its conductor. Hence there is a weight $2$ normalized newform $f$ of level $N_E$ attached to $E$. [/step] [step:Compare Frobenius traces to identify the Fourier coefficients] Write the Fourier expansion of the normalized newform $f$ at the cusp $\infty$ as \begin{align*} f(q) = \sum_{n=1}^{\infty} a_n(f) q^n, \end{align*} where normalization means $a_1(f)=1$. Let $p$ be a prime of good reduction for $E$. The trace compatibility in the modularity theorem states that the trace of arithmetic Frobenius at $p$ on the Galois representation attached to $f$ equals the trace of arithmetic Frobenius at $p$ on the $\ell$-adic Tate-module representation of $E$, for every auxiliary prime $\ell \neq p$. For an elliptic curve with good reduction at $p$, the latter trace is $a_p(E)$ by the standard Frobenius trace formula for the reduction $\widetilde{E}_p/\mathbb F_p$. Therefore \begin{align*} a_p(f) = a_p(E) = p + 1 - |\widetilde{E}_p(\mathbb F_p)|. \end{align*} Since $\widetilde{E}_p(\mathbb F_p)=E(\mathbb F_p)$ under the conventional notation for the good reduction of $E$ modulo $p$, this is precisely \begin{align*} a_p(f) = p + 1 - |E(\mathbb F_p)|. \end{align*} [/step] [step:Conclude modularity with the stated level] The newform $f$ obtained above has weight $2$, is normalized, and has level $N_E$, the conductor of $E$. The preceding trace comparison proves the required equality for every prime $p$ of good reduction. Hence $E/\mathbb Q$ is modular in the sense stated in the theorem. [/step]