[proofplan]
For $y_1 \ne 0$, we determine the tangent line at $P$ algebraically by requiring that its intersection polynomial with the cubic have a double root at $x=x_1$. Comparing the coefficient of $x^2$ gives the third affine intersection point $R$, and the chord-tangent group law defines $2P$ as the reflection of $R$ across the $x$-axis. When $y_1=0$, the point is its own inverse because reflection across the $x$-axis fixes it, so $P+P=O$.
[/proofplan]
[step:Compute the tangent slope from the double root condition]
Assume first that $y_1 \ne 0$. Define the affine polynomial $F:\mathbb{R}^2 \to \mathbb{R}$ by
\begin{align*}
F(x,y)=y^2-x^3-ax-b.
\end{align*}
Since $P=(x_1,y_1)\in E(\mathbb{R})$, we have
\begin{align*}
F(x_1,y_1)=0.
\end{align*}
Let $m\in\mathbb{R}$ be the slope of a nonvertical line through $P$, and define the line as the map $\ell:\mathbb{R}\to\mathbb{R}$ given by
\begin{align*}
\ell(x)=m(x-x_1)+y_1.
\end{align*}
The affine intersections of this line with $E$ are the real roots of the cubic polynomial $q:\mathbb{R}\to\mathbb{R}$ defined by
\begin{align*}
q(x)=F(x,\ell(x)).
\end{align*}
Explicitly,
\begin{align*}
q(x)=\bigl(m(x-x_1)+y_1\bigr)^2-x^3-ax-b.
\end{align*}
The condition that the line be tangent to $E$ at $P$ is that $x=x_1$ be a double root of $q$. We already have $q(x_1)=F(x_1,y_1)=0$. Differentiating the polynomial $q$ gives
\begin{align*}
q'(x)=2m\bigl(m(x-x_1)+y_1\bigr)-3x^2-a.
\end{align*}
Therefore
\begin{align*}
q'(x_1)=2my_1-3x_1^2-a.
\end{align*}
Since $y_1\ne 0$, the equation $q'(x_1)=0$ is equivalent to
\begin{align*}
m=\frac{3x_1^2+a}{2y_1}.
\end{align*}
Thus this value of $m$ is exactly the slope of the tangent line to $E$ at $P$.
[guided]
We want the tangent line at $P$ without appealing to any unmentioned differential geometry. The algebraic meaning of tangency here is that the line meets the cubic with intersection multiplicity at least two at $P$. Since the line is not vertical when $y_1\ne 0$, we can write it as a graph over the $x$-axis.
Define $F:\mathbb{R}^2\to\mathbb{R}$ by
\begin{align*}
F(x,y)=y^2-x^3-ax-b.
\end{align*}
The curve $E$ is the zero set of $F$ together with the point at infinity. Since $P=(x_1,y_1)$ lies on $E$, the defining equation gives
\begin{align*}
F(x_1,y_1)=y_1^2-x_1^3-ax_1-b=0.
\end{align*}
Let $m\in\mathbb{R}$ be the slope of a nonvertical line through $P$. The corresponding line is the map $\ell:\mathbb{R}\to\mathbb{R}$ given by
\begin{align*}
\ell(x)=m(x-x_1)+y_1.
\end{align*}
Substituting this line into the equation of $E$ produces the polynomial $q:\mathbb{R}\to\mathbb{R}$ defined by
\begin{align*}
q(x)=F(x,\ell(x)).
\end{align*}
Thus
\begin{align*}
q(x)=\bigl(m(x-x_1)+y_1\bigr)^2-x^3-ax-b.
\end{align*}
The roots of $q$ are exactly the $x$-coordinates of affine intersection points between the line and the curve.
Because $P$ is on both the line and the curve, $x=x_1$ is a root:
\begin{align*}
q(x_1)=F(x_1,y_1)=0.
\end{align*}
For the line to be tangent at $P$, this root must be at least double, so we also impose $q'(x_1)=0$. Since $q$ is an ordinary polynomial in one real variable, we compute its derivative directly:
\begin{align*}
q'(x)=2m\bigl(m(x-x_1)+y_1\bigr)-3x^2-a.
\end{align*}
Evaluating at $x=x_1$ gives
\begin{align*}
q'(x_1)=2my_1-3x_1^2-a.
\end{align*}
The hypothesis $y_1\ne 0$ is used exactly here: it lets us solve uniquely for $m$. Setting $q'(x_1)=0$ gives
\begin{align*}
2my_1=3x_1^2+a,
\end{align*}
and hence
\begin{align*}
m=\frac{3x_1^2+a}{2y_1}.
\end{align*}
So the slope in the statement is precisely the tangent slope.
[/guided]
[/step]
[step:Find the third affine intersection by comparing the $x^2$ coefficient]
With
\begin{align*}
m=\frac{3x_1^2+a}{2y_1},
\end{align*}
the polynomial $q$ has $x=x_1$ as a double root. Since $q$ has leading coefficient $-1$, there exists a real number $x_R$ such that
\begin{align*}
q(x)=-(x-x_1)^2(x-x_R).
\end{align*}
Expanding the right-hand side gives
\begin{align*}
-(x-x_1)^2(x-x_R)
=
-x^3+(2x_1+x_R)x^2-(x_1^2+2x_1x_R)x+x_1^2x_R.
\end{align*}
On the other hand, the coefficient of $x^2$ in
\begin{align*}
q(x)=\bigl(m(x-x_1)+y_1\bigr)^2-x^3-ax-b
\end{align*}
is $m^2$. Comparing the coefficients of $x^2$ gives
\begin{align*}
2x_1+x_R=m^2.
\end{align*}
Therefore
\begin{align*}
x_R=m^2-2x_1.
\end{align*}
The third affine intersection point is
\begin{align*}
R=(x_R,y_R),
\qquad
y_R=\ell(x_R)=m(x_R-x_1)+y_1.
\end{align*}
[/step]
[step:Reflect the third intersection to obtain the double]
By the chord-tangent definition of the [Weierstrass group law](/page/Weierstrass%20Group%20Law), $P+P$ is the reflection across the $x$-axis of the third intersection point $R$ of the tangent line at $P$ with $E$. Thus
\begin{align*}
2P=-R=(x_R,-y_R).
\end{align*}
Set
\begin{align*}
x_3=x_R,
\qquad
y_3=-y_R.
\end{align*}
Using the formula for $x_R$ from the previous step gives
\begin{align*}
x_3=m^2-2x_1.
\end{align*}
Using $y_R=m(x_R-x_1)+y_1$ and $x_3=x_R$ gives
\begin{align*}
y_3=-\bigl(m(x_3-x_1)+y_1\bigr)
=
m(x_1-x_3)-y_1.
\end{align*}
Hence, when $y_1\ne 0$,
\begin{align*}
2P=(x_3,y_3),
\qquad
x_3=m^2-2x_1,
\qquad
y_3=m(x_1-x_3)-y_1.
\end{align*}
[/step]
[step:Handle the vertical tangent case]
It remains to consider the case $y_1=0$. Under the inverse formula in the [Weierstrass group law](/page/Weierstrass%20Group%20Law), the inverse of an affine point $(x,y)\in E(\mathbb{R})$ is its reflection across the $x$-axis:
\begin{align*}
-(x,y)=(x,-y).
\end{align*}
Therefore
\begin{align*}
-P=(x_1,-y_1)=(x_1,0)=P.
\end{align*}
Adding $P$ to both sides of $P=-P$ gives
\begin{align*}
P+P=O.
\end{align*}
Thus, if $y_1=0$, then
\begin{align*}
2P=O.
\end{align*}
Combining this with the preceding case proves the theorem.
[/step]
