[proofplan]
We work inside the field $\mathbb{F}_p$, with $p \ne 2$ so that reflection across the $x$-axis is the map $(x,y) \mapsto (x,-y)$ and with $p \ne 3$ so the displayed short-Weierstrass equation has the usual derivative $3x^2+a$. The nonsingularity condition $4a^3+27b^2 \ne 0$ is the hypothesis that makes this cubic a nonsingular [projective closure](/page/Projective%20Closure) of an elliptic curve. We use the [chord-and-tangent law](/page/Chord-and-Tangent%20Law) in its projective-intersection form: for a line through the two input points, counted with intersection multiplicity, the sum is the reflection of the third intersection point, and the [point at infinity](/page/Point%20at%20Infinity) $O$ is fixed by reflection. For a nonvertical line through $P$ and $Q$, we substitute the line equation into $y^2=x^3+ax+b$ and obtain a cubic polynomial whose roots are the $x$-coordinates of the intersection points. Vieta's relation gives the third $x$-coordinate, and reflecting the third intersection point across the $x$-axis gives the stated point $(x_3,y_3)$. The doubling case is the same computation with $x_1$ counted twice, where the tangent slope is characterized by making $x_1$ a double root.
[/proofplan]
[step:Verify that the slope is defined in the nonvertical cases]
Assume first that $P \ne Q$ and $Q \ne -P$. Since $P=(x_1,y_1)$ and $Q=(x_2,y_2)$ are distinct, if $x_1=x_2$ then $y_1 \ne y_2$. Because both points lie on $E$, we have
\begin{align*}
y_1^2=x_1^3+ax_1+b=x_2^3+ax_2+b=y_2^2.
\end{align*}
Thus $(y_1-y_2)(y_1+y_2)=0$ in $\mathbb{F}_p$. Since $y_1 \ne y_2$, we get $y_1=-y_2$, so $Q=-P$, contrary to the assumption. Hence $x_1 \ne x_2$, and $x_2-x_1$ is invertible in $\mathbb{F}_p$.
Assume next that $P=Q$ and $Q \ne -P$. Then $P \ne -P$, so $y_1 \ne -y_1$. Since $p \ne 2$, this is equivalent to $2y_1 \ne 0$. Hence $2y_1$ is invertible in $\mathbb{F}_p$. Therefore the displayed formula for $\lambda$ is defined in every case with $Q \ne -P$.
[/step]
[step:Substitute a nonvertical line and identify the third intersection]
Let $\nu \in \mathbb{F}_p$ be defined by
\begin{align*}
\nu := y_1-\lambda x_1.
\end{align*}
Define the affine line map $\ell: \mathbb{F}_p \to \mathbb{F}_p$ by sending each $x \in \mathbb{F}_p$ to $\ell(x):=\lambda x+\nu$.
Then $\ell(x_1)=y_1$. In the case $P \ne Q$, the definition of $\lambda$ also gives $\ell(x_2)=y_2$.
Define the cubic polynomial function $f: \mathbb{F}_p \to \mathbb{F}_p$ by sending each $x \in \mathbb{F}_p$ to
\begin{align*}
f(x):=x^3+ax+b-(\lambda x+\nu)^2.
\end{align*}
Expanding gives
\begin{align*}
f(x)=x^3-\lambda^2x^2+(a-2\lambda\nu)x+(b-\nu^2).
\end{align*}
The points of intersection between the line $y=\ell(x)$ and the affine curve $E$ are exactly the roots of $f$, because
\begin{align*}
\ell(x)^2=x^3+ax+b
\end{align*}
is equivalent to $f(x)=0$.
[guided]
The goal is to convert the geometric statement "the line meets the cubic in three points" into a finite-field polynomial computation. We define
\begin{align*}
\nu := y_1-\lambda x_1,
\end{align*}
so the affine line through $P$ is represented by the map $\ell: \mathbb{F}_p \to \mathbb{F}_p$ defined by $\ell(x):=\lambda x+\nu$ for each $x \in \mathbb{F}_p$.
This definition gives $\ell(x_1)=\lambda x_1+y_1-\lambda x_1=y_1$. If $P \ne Q$, then
\begin{align*}
\lambda=\frac{y_2-y_1}{x_2-x_1},
\end{align*}
and therefore
\begin{align*}
\ell(x_2)=\lambda x_2+\nu=y_1+\lambda(x_2-x_1)=y_1+(y_2-y_1)=y_2.
\end{align*}
So in the chord case the line passes through both $P$ and $Q$.
Now we substitute the line equation $y=\ell(x)$ into the curve equation. Define $f: \mathbb{F}_p \to \mathbb{F}_p$ by $f(x):=x^3+ax+b-(\lambda x+\nu)^2$ for each $x \in \mathbb{F}_p$.
A value $x \in \mathbb{F}_p$ is a root of $f$ exactly when
\begin{align*}
0=f(x)=x^3+ax+b-\ell(x)^2,
\end{align*}
which is exactly the condition that $(x,\ell(x))$ lies on $E$. Expanding the square gives
\begin{align*}
f(x)=x^3+ax+b-(\lambda^2x^2+2\lambda\nu x+\nu^2)=x^3-\lambda^2x^2+(a-2\lambda\nu)x+(b-\nu^2).
\end{align*}
Thus the coefficient of $x^2$ is $-\lambda^2$. This coefficient is the only coefficient needed for the root-sum calculation.
[/guided]
[/step]
[step:Use the chord case to compute the reflected third point]
Assume $P \ne Q$ and $Q \ne -P$. By the previous step, $f(x_1)=0$ and $f(x_2)=0$. Since $f$ is monic of degree $3$, there exists a third root $x' \in \mathbb{F}_p$ counted with multiplicity such that
\begin{align*}
f(x)=(x-x_1)(x-x_2)(x-x').
\end{align*}
Comparing the coefficient of $x^2$ with the expanded expression for $f$ gives
\begin{align*}
-(x_1+x_2+x')=-\lambda^2,
\end{align*}
hence
\begin{align*}
x'=\lambda^2-x_1-x_2.
\end{align*}
Thus $x'=x_3$.
The third affine intersection point is therefore
\begin{align*}
R=(x_3,\ell(x_3)).
\end{align*}
Since $\ell(x_3)=\lambda x_3+\nu=\lambda x_3+y_1-\lambda x_1$, we have
\begin{align*}
-\ell(x_3)=\lambda(x_1-x_3)-y_1=y_3.
\end{align*}
The chord-and-tangent rule defines $P+Q$ as the reflection of $R$ across the $x$-axis, so
\begin{align*}
P+Q=(x_3,-\ell(x_3))=(x_3,y_3).
\end{align*}
Because $R \in E(\mathbb{F}_p)$ and the equation of $E$ is invariant under $y \mapsto -y$, the reflected point $(x_3,y_3)$ also lies in $E(\mathbb{F}_p)$.
[guided]
Assume $P \ne Q$ and $Q \ne -P$. The previous step constructed the line map $\ell: \mathbb{F}_p \to \mathbb{F}_p$ and the monic cubic polynomial function $f: \mathbb{F}_p \to \mathbb{F}_p$ whose roots are exactly the $x$-coordinates of affine intersections between the line $y=\ell(x)$ and the curve $E$. Since $\ell(x_1)=y_1$ and $\ell(x_2)=y_2$, we have $f(x_1)=0$ and $f(x_2)=0$.
Because $f$ is monic of degree $3$, the remaining intersection has an $x$-coordinate $x' \in \mathbb{F}_p$, counted with multiplicity, such that
\begin{align*}
f(x)=(x-x_1)(x-x_2)(x-x').
\end{align*}
Expanding only the coefficient needed for Vieta's relation gives the coefficient of $x^2$ as $-(x_1+x_2+x')$. The direct expansion from the previous step gives the coefficient of $x^2$ as $-\lambda^2$. Comparing these coefficients yields
\begin{align*}
-(x_1+x_2+x')=-\lambda^2,
\end{align*}
and therefore
\begin{align*}
x'=\lambda^2-x_1-x_2=x_3.
\end{align*}
The third affine intersection point is $R=(x_3,\ell(x_3))$. Since $\nu=y_1-\lambda x_1$, we compute
\begin{align*}
-\ell(x_3)=-(\lambda x_3+\nu)=-(\lambda x_3+y_1-\lambda x_1)=\lambda(x_1-x_3)-y_1=y_3.
\end{align*}
The chord-and-tangent convention says that $P+Q$ is the reflection of the third intersection point $R$ across the $x$-axis. Hence
\begin{align*}
P+Q=(x_3,-\ell(x_3))=(x_3,y_3).
\end{align*}
Finally, $R$ lies on $E$ by construction, and replacing $\ell(x_3)$ by $-\ell(x_3)$ preserves the equation $y^2=x^3+ax+b$, so $(x_3,y_3) \in E(\mathbb{F}_p)$.
[/guided]
[/step]
[step:Use the tangent condition to compute the doubled point]
Assume $P=Q$ and $Q \ne -P$. Define $\nu=y_1-\lambda x_1$ and $f$ as above. We show that the chosen value
\begin{align*}
\lambda=\frac{3x_1^2+a}{2y_1}
\end{align*}
makes $x_1$ a double root of $f$.
Since $P \in E(\mathbb{F}_p)$, $f(x_1)=0$. The formal derivative of $f$ is
\begin{align*}
f'(x)=3x^2-2\lambda(\lambda x+\nu)+a.
\end{align*}
Using $\lambda x_1+\nu=y_1$, we obtain
\begin{align*}
f'(x_1)=3x_1^2-2\lambda y_1+a=3x_1^2+a-2y_1\frac{3x_1^2+a}{2y_1}=0.
\end{align*}
Therefore $x_1$ is a root of multiplicity at least $2$. Since $f$ is monic of degree $3$, there exists a third root $x' \in \mathbb{F}_p$ counted with multiplicity such that
\begin{align*}
f(x)=(x-x_1)^2(x-x').
\end{align*}
Comparing the coefficient of $x^2$ gives
\begin{align*}
-(2x_1+x')=-\lambda^2,
\end{align*}
so
\begin{align*}
x'=\lambda^2-2x_1=\lambda^2-x_1-x_2.
\end{align*}
Since $P=Q$, this is precisely $x'=x_3$.
The tangent intersection point other than the doubled contact point is
\begin{align*}
R=(x_3,\ell(x_3)).
\end{align*}
Reflecting across the $x$-axis gives
\begin{align*}
P+P=(x_3,-\ell(x_3)).
\end{align*}
As in the chord case,
\begin{align*}
-\ell(x_3)=\lambda(x_1-x_3)-y_1=y_3,
\end{align*}
so
\begin{align*}
P+P=(x_3,y_3).
\end{align*}
[/step]
[step:Handle the vertical line case and conclude the formula]
If $Q=-P$, then $Q=(x_1,-y_1)$. Let $\mathbb{P}^2_{\mathbb{F}_p}$ denote the projective plane over $\mathbb{F}_p$, whose points are equivalence classes $[X:Y:Z]$ of nonzero triples $(X,Y,Z) \in \mathbb{F}_p^3$ under nonzero scalar multiplication. Define the [projective closure](/page/Projective%20Closure) $\overline{E} \subset \mathbb{P}^2_{\mathbb{F}_p}$ by the homogeneous equation
\begin{align*}
Y^2Z=X^3+aXZ^2+bZ^3,
\end{align*}
and define the [point at infinity](/page/Point%20at%20Infinity) by $O=[0:1:0] \in \overline{E}(\mathbb{F}_p)$. The affine point $(x,y)$ corresponds to $[x:y:1]$. The vertical affine line $x=x_1$ has projective closure $L \subset \mathbb{P}^2_{\mathbb{F}_p}$ defined by
\begin{align*}
X-x_1Z=0.
\end{align*}
Substituting $X=x_1Z$ into the homogeneous equation of $\overline{E}$ gives
\begin{align*}
Y^2Z=x_1^3Z^3+ax_1Z^3+bZ^3.
\end{align*}
On the affine chart $Z \ne 0$, this is exactly
\begin{align*}
y^2=x_1^3+ax_1+b=y_1^2.
\end{align*}
Equivalently, along the affine vertical line define the polynomial function $g: \mathbb{F}_p \to \mathbb{F}_p$ by
\begin{align*}
g(y):=y^2-y_1^2.
\end{align*}
The affine intersections are the roots of $g$. If $y_1 \ne 0$, then $g(y)=(y-y_1)(y+y_1)$ has the two distinct roots $y_1$ and $-y_1$, because $p \ne 2$. If $y_1=0$, then $g(y)=y^2$, so $y=0$ is a root of multiplicity two. Hence the affine intersections are $[x_1:y_1:1]=P$ and $[x_1:-y_1:1]=Q$, with the affine point counted twice in the tangent case $y_1=0$. On the line at infinity $Z=0$, the equation $X-x_1Z=0$ gives $X=0$, and the unique projective point on $L$ with $Z=0$ is $[0:1:0]=O$. At $O=[0:1:0]$, use the affine projective chart $Y \ne 0$ with local coordinates $u=X/Y$ and $v=Z/Y$. In these coordinates $O$ is $(u,v)=(0,0)$, the vertical line equation becomes $u-x_1v=0$, and the homogeneous curve equation becomes
\begin{align*}
v=u^3+auv^2+bv^3.
\end{align*}
Substituting $u=x_1v$ gives
\begin{align*}
v=x_1^3v^3+ax_1v^3+bv^3,
\end{align*}
or equivalently
\begin{align*}
v\bigl(1-(x_1^3+ax_1+b)v^2\bigr)=0.
\end{align*}
The factor in parentheses has value $1$ at $v=0$, so it is nonzero at $O$; hence $v=0$ occurs with multiplicity one. Thus $O$ is the third projective intersection point with the correct multiplicity. The [chord-and-tangent law](/page/Chord-and-Tangent%20Law) defines $P+Q$ as the reflection of this third point. Since $O$ is fixed by negation, this gives
\begin{align*}
P+Q=O.
\end{align*}
[guided]
We now make the vertical-line exception explicit rather than referring only to the projective closure abstractly. The symbol $\mathbb{P}^2_{\mathbb{F}_p}$ denotes the projective plane over $\mathbb{F}_p$, meaning the set of equivalence classes $[X:Y:Z]$ of nonzero triples $(X,Y,Z) \in \mathbb{F}_p^3$ under multiplication by nonzero scalars in $\mathbb{F}_p$. The [projective closure](/page/Projective%20Closure) $\overline{E} \subset \mathbb{P}^2_{\mathbb{F}_p}$ is the cubic
\begin{align*}
Y^2Z=X^3+aXZ^2+bZ^3,
\end{align*}
and its [point at infinity](/page/Point%20at%20Infinity) is $O=[0:1:0]$. The affine chart $Z \ne 0$ identifies $(x,y) \in \mathbb{F}_p^2$ with $[x:y:1]$.
If $Q=-P$, then $Q=(x_1,-y_1)$. The relevant affine line is vertical, so its projective closure $L$ is defined by
\begin{align*}
X-x_1Z=0.
\end{align*}
To find its intersections with $\overline{E}$, substitute $X=x_1Z$ into the projective equation. This gives
\begin{align*}
Y^2Z=x_1^3Z^3+ax_1Z^3+bZ^3.
\end{align*}
On the affine chart $Z \ne 0$, dividing by $Z^3$ gives
\begin{align*}
y^2=x_1^3+ax_1+b=y_1^2.
\end{align*}
To justify the multiplicities, restrict the curve equation to the affine vertical line. Define $g: \mathbb{F}_p \to \mathbb{F}_p$ by
\begin{align*}
g(y):=y^2-y_1^2.
\end{align*}
The affine intersections of $L$ with $E$ are exactly the roots of $g$. If $y_1 \ne 0$, then
\begin{align*}
g(y)=(y-y_1)(y+y_1),
\end{align*}
and the two roots $y_1$ and $-y_1$ are distinct because $p \ne 2$. If $y_1=0$, then
\begin{align*}
g(y)=y^2,
\end{align*}
so $y=0$ is a double root. This proves that in the vertical tangent case the affine point $P=[x_1:0:1]$ is counted with multiplicity two. On the line at infinity, $Z=0$ and $X-x_1Z=0$ force $X=0$, so the only projective point of $L$ at infinity is $[0:1:0]=O$. We also verify its multiplicity. Work in the affine projective chart $Y \ne 0$ and define local coordinates $u=X/Y$ and $v=Z/Y$; in this chart $O$ is $(u,v)=(0,0)$. The line equation becomes $u-x_1v=0$, while the homogeneous equation of $\overline{E}$ becomes
\begin{align*}
v=u^3+auv^2+bv^3.
\end{align*}
Substituting $u=x_1v$ along the line gives
\begin{align*}
v=x_1^3v^3+ax_1v^3+bv^3,
\end{align*}
so
\begin{align*}
v\bigl(1-(x_1^3+ax_1+b)v^2\bigr)=0.
\end{align*}
The second factor equals $1$ at $v=0$, so it does not vanish at $O$. Therefore the intersection multiplicity of $L$ and $\overline{E}$ at $O$ is one. Combined with the two affine intersections already counted, this proves that the third point in the [chord-and-tangent law](/page/Chord-and-Tangent%20Law) is $O$ in the secant case and also in the tangent case. Since negation fixes $O$, reflecting the third point gives
\begin{align*}
P+Q=O.
\end{align*}
[/guided]
It remains to record the identity cases involving $O$. Let $P=(x_1,y_1) \in E(\mathbb{F}_p)$ be an affine point. The projective line through $P=[x_1:y_1:1]$ and $O=[0:1:0]$ is the vertical line $X-x_1Z=0$, because both points satisfy this linear equation. The computation above shows that the third affine intersection is $-P=[x_1:-y_1:1]$, counted with multiplicity in the case $y_1=0$. Reflecting this third point gives $P$. Hence the chord-and-tangent law gives
\begin{align*}
P+O=P
\end{align*}
and, by the same line with the two inputs interchanged,
\begin{align*}
O+P=P.
\end{align*}
Also $O+O=O$ because $O$ is defined as the identity point of the projective group law.
For $Q \ne -P$, the chord case and tangent case prove that the third intersection point has $x$-coordinate
\begin{align*}
x_3=\lambda^2-x_1-x_2
\end{align*}
and that its reflection has $y$-coordinate
\begin{align*}
y_3=\lambda(x_1-x_3)-y_1.
\end{align*}
Hence the chord-and-tangent addition law on $E(\mathbb{F}_p)$ is exactly
\begin{align*}
P+Q=(x_3,y_3),
\end{align*}
with the exceptional vertical case giving $P+Q=O$.
[/step]
