Primitive nonvertical coprime pair has finite explicitly bounded intersection

Let $p$ and $q$ be bivariate real polynomials of total degree at most $d_1$ and $d_2$ respectively ($h_{pdeg}$, $h_{qdeg}$), with primitive curries ($h_{pprim}$, $h_{qprim}$), both genuinely depending on the first variable ($h_{p0deg} : 0 < (\mathrm{Curry0}\,p).\mathrm{natDegree}$, $h_{q0deg}$ likewise), and coprime curries ($h_{rel} : \mathrm{IsRelPrime}\,(\mathrm{Curry0}\,p)\,(\mathrm{Curry0}\,q)$). Then their common zero set is finite with an explicit bound:

This is the workhorse resultant-based intersection estimate of the preliminaries: the resultant in the coefficient variable has degree at most $(d_1+d_2)^2$, its roots index the nonempty fibers, and each fiber has at most $\max d_1 d_2$ points. Summing over components upgrades it to the finite Bezout bound for arbitrary (reducible) curves.