Serre's modularity conjecture for weight two over number fields

Let $K$ be a number field, let $p$ be a rational prime unramified in $K$, and let $G_K$ denote the absolute Galois group of $K$. Let $\overline{\rho}:G_K\rightarrow \operatorname{GL}_2(\overline{\mathbb{F}}_p)$ be an odd, irreducible, continuous representation with Serre conductor $\mathfrak N$ and determinant $\chi_p$, the mod $p$ cyclotomic character. Assume that, for every prime $\mathfrak p\mid p$, the restriction $\overline{\rho}\mid_{G_{\mathbb Q_{\mathfrak p}}}$ arises from a finite-flat group scheme over $\mathcal O_{\mathbb Q_{\mathfrak p}}$. Serre's modularity conjecture. There is a weight two, mod $p$ eigenform $\theta$ over $K$ of level $\mathfrak N$ such that, for every prime $\mathfrak q$ coprime to $p\mathfrak N$,

$$\operatorname{Tr}(\overline{\rho}(\operatorname{Frob}_{\mathfrak q}))=\theta(T_{\mathfrak q}).$$

This is presented as a special case of Serre's modularity conjecture over number fields and is used to relate residual representations attached to elliptic curves to mod $p$ eigenforms; the source gives no resolution status.