[proofplan]
The nonsingularity hypothesis makes the projective closure of the displayed cubic an [elliptic curve](/page/Elliptic%20Curve), so the chord-and-tangent construction gives a well-defined group law with identity $O$. The hypothesis $\operatorname{char}(k)\ne 3$ is not used in the coefficient-comparison argument itself; it is retained because the theorem is stated in the standard short Weierstrass modelling convention for the equation $y^2=x^3+ax+b$. The proof below uses $\operatorname{char}(k)\ne 2$ for reflection across the $x$-axis and for the tangent denominator $2y_1$. The chord-and-tangent group law defines $P+Q$ by taking the third intersection point $R$ of the appropriate line with the cubic and then reflecting $R$ across the $x$-axis. In the non-vertical cases, the line has slope $m$, so substituting its equation into the cubic gives a degree-three polynomial whose three roots are the $x$-coordinates of the intersection points, counted with multiplicity. Comparing the coefficient of $x^2$ gives the formula for the third $x$-coordinate, and reflection gives the formula for $y_3$. The vertical case $Q=-P$ is exactly the case where the chord meets the point at infinity, so the group law gives $P+Q=O$.
[/proofplan]
[step:Identify the vertical case with the point at infinity]
Let $P=(x_1,y_1) \in E(k)$ and $Q=(x_2,y_2) \in E(k)$ be affine points. Since $\operatorname{char}(k)\ne 2$, the inverse of $P$ in the chord-and-tangent construction is
\begin{align*}
-P=(x_1,-y_1).
\end{align*}
If $Q=-P$, then $x_2=x_1$ and $y_2=-y_1$. If $P\ne Q$, the relevant chord is the vertical line $x=x_1$; if $P=Q$, then $y_1=0$ and the relevant tangent is also the vertical line $x=x_1$. Let $[X:Y:Z]$ denote homogeneous coordinates on the projective plane $\mathbb{P}^2_k$. Define the projective cubic $\overline{E}\subset\mathbb{P}^2_k$ by
\begin{align*}
Y^2Z=X^3+aXZ^2+bZ^3.
\end{align*}
The nonsingularity of $E$ ensures that this projective cubic is the [elliptic curve](/page/Elliptic%20Curve) to which the chord-and-tangent group law applies, with identity point $O=[0:1:0]$. Base change to an [algebraic closure](/page/Algebraic%20Closure) $\overline{k}$ of $k$ for the intersection count. The vertical projective line $X=x_1Z$ is not a component of $\overline{E}_{\overline{k}}$, because substituting $X=x_1Z$ into $Y^2Z=X^3+aXZ^2+bZ^3$ gives the nonzero homogeneous polynomial $Y^2Z-(x_1^3+ax_1+b)Z^3$. Hence the line-cubic intersection consequence of [Bézout's Theorem](/page/Bezout%27s%20Theorem) applies: this line meets $\overline{E}_{\overline{k}}$ in three points counted with intersection multiplicity. These points are the affine points represented by $P$ and $Q$, counted with the appropriate multiplicities, together with $O$. The reflection of $O$ is $O$, so the chord-and-tangent definition gives
\begin{align*}
P+Q=O.
\end{align*}
[/step]
[step:Write the non-vertical chord or tangent as a line of slope $m$]
Assume now that $Q\ne -P$. If $P\ne Q$, then $x_2\ne x_1$; otherwise $x_2=x_1$ would force $y_2^2=y_1^2$, hence $y_2=\pm y_1$, and the alternatives would be $Q=P$ or $Q=-P$. Thus the slope
\begin{align*}
m=\frac{y_2-y_1}{x_2-x_1}
\end{align*}
is defined in $k$. Define the affine line $\ell:k\to k^2$ by
\begin{align*}
\ell(x)=\bigl(x,\;m(x-x_1)+y_1\bigr).
\end{align*}
This is the chord through $P$ and $Q$.
If $P=Q$, then $Q\ne -P$ implies $P\ne -P$, hence $y_1\ne 0$. Since $\operatorname{char}(k)\ne 2$, the element $2y_1\in k$ is nonzero, so the tangent slope
\begin{align*}
m=\frac{3x_1^2+a}{2y_1}
\end{align*}
is defined. Define the tangent line at $P$ by the map $\ell:k\to k^2$ given by
\begin{align*}
\ell(x)=\bigl(x,\;m(x-x_1)+y_1\bigr).
\end{align*}
[guided]
We first need a single equation for the line used by the group law. In the secant case $P\ne Q$, the line is not vertical because $Q\ne -P$. Indeed, if $x_2=x_1$, then the two points satisfy
\begin{align*}
y_1^2=x_1^3+ax_1+b=y_2^2,
\end{align*}
so
\begin{align*}
(y_2-y_1)(y_2+y_1)=0.
\end{align*}
Since $k$ is a field, this gives either $y_2=y_1$, hence $Q=P$, or $y_2=-y_1$, hence $Q=-P$. The first option contradicts $P\ne Q$, and the second contradicts the present non-vertical assumption. Therefore $x_2-x_1\ne 0$, so
\begin{align*}
m=\frac{y_2-y_1}{x_2-x_1}
\end{align*}
is a well-defined element of $k$.
In the tangent case $P=Q$, the assumption $Q\ne -P$ says $P\ne -P$. Since $-P=(x_1,-y_1)$, this means $y_1\ne -y_1$, equivalently $2y_1\ne 0$. Because $\operatorname{char}(k)\ne 2$, this is the same as $y_1\ne 0$, and therefore
\begin{align*}
m=\frac{3x_1^2+a}{2y_1}
\end{align*}
is defined. This is the usual implicit-differentiation slope of the cubic at $P$: differentiating $y^2=x^3+ax+b$ gives $2y\,dy=(3x^2+a)\,dx$, so the tangent slope at $(x_1,y_1)$ is $(3x_1^2+a)/(2y_1)$.
Thus in both non-vertical cases the relevant line is the map $\ell:k\to k^2$ defined as follows: for each $x\in k$, the point $\ell(x)$ is
\begin{align*}
\ell(x)=\bigl(x,\;m(x-x_1)+y_1\bigr).
\end{align*}
No raw TeX row-break command is needed in this display, so the line equation is rendered as a single display equation.
[/guided]
[/step]
[step:Compare the cubic intersection polynomial with its roots]
Let $\overline{k}$ denote an algebraic closure of $k$. Define the polynomial $F\in k[x]$ by
\begin{align*}
F(x)=\bigl(m(x-x_1)+y_1\bigr)^2-\bigl(x^3+ax+b\bigr).
\end{align*}
After base change from $k$ to $\overline{k}$, the zeros of $F$ are exactly the $x$-coordinates of the affine intersection points of the line $\ell$ with $E$, counted with intersection multiplicity. The projective closure of this non-vertical line has equation
\begin{align*}
Y=mX+(y_1-mx_1)Z.
\end{align*}
Substituting $O=[0:1:0]$ into this equation gives $1=0$, so the line does not contain $O$. The projective line is not a component of $\overline{E}_{\overline{k}}$: after substitution, the intersection equation is the nonzero cubic polynomial $F(x)$, whose leading term is $-x^3$. Therefore the line-cubic intersection consequence of [Bézout's Theorem](/page/Bezout%27s%20Theorem) applies over $\overline{k}$, and the projective line meets the projective cubic $\overline{E}_{\overline{k}}$ in three points counted with multiplicity. Since the line does not contain $O$, all three intersections are affine. Expanding the leading terms gives
\begin{align*}
F(x)=-x^3+m^2x^2+\text{terms of degree at most }1.
\end{align*}
Over $\overline{k}$, let $\alpha\in\overline{k}$ denote the remaining root of $F$ after the roots contributed by $P$ and $Q$ are counted with their prescribed multiplicities. In the secant case, $x_1$, $x_2$, and $\alpha$ are the three roots of $F$. In the tangent case, $x_1$ occurs with multiplicity two. Indeed, let $F'\in k[x]$ denote the formal derivative of $F$. Since $P=(x_1,y_1)$ lies on $E$, we have $F(x_1)=0$, and differentiating the displayed polynomial gives
\begin{align*}
F'(x)=2m\bigl(m(x-x_1)+y_1\bigr)-(3x^2+a).
\end{align*}
Evaluating at $x_1$ gives
\begin{align*}
F'(x_1)=2my_1-(3x_1^2+a)=0,
\end{align*}
because in the tangent case $m=(3x_1^2+a)/(2y_1)$. Thus the three roots are $x_1$, $x_1$, and $\alpha$. In both cases we may write in $\overline{k}[x]$
\begin{align*}
F(x)=-(x-x_1)(x-x_2)(x-\alpha),
\end{align*}
where in the tangent case $x_2=x_1$. Comparing the coefficient of $x^2$ gives
\begin{align*}
m^2=x_1+x_2+\alpha.
\end{align*}
Hence
\begin{align*}
\alpha=m^2-x_1-x_2.
\end{align*}
Since $m$, $x_1$, and $x_2$ lie in $k$, this equality shows that $\alpha\in k$. Define $x_R=\alpha\in k$ and define $y_R\in k$ by
\begin{align*}
y_R=m(x_R-x_1)+y_1.
\end{align*}
Then $R=(x_R,y_R)$ is the third affine intersection point of $\ell$ with $E$, counted with multiplicity, and
\begin{align*}
x_R=m^2-x_1-x_2.
\end{align*}
[/step]
[step:Reflect the third intersection point to obtain the sum]
Since $R$ lies on the line $\ell$, its $y$-coordinate is
\begin{align*}
y_R=m(x_R-x_1)+y_1.
\end{align*}
By definition of the chord-and-tangent group law, $P+Q$ is the reflection of $R$ across the $x$-axis. Since $\operatorname{char}(k)\ne 2$, this reflection sends $(x_R,y_R)$ to $(x_R,-y_R)$. Therefore, writing
\begin{align*}
P+Q=(x_3,y_3),
\end{align*}
we have
\begin{align*}
x_3=x_R=m^2-x_1-x_2
\end{align*}
and
\begin{align*}
y_3=-y_R=-m(x_R-x_1)-y_1=m(x_1-x_3)-y_1.
\end{align*}
This is exactly the claimed addition formula.
[/step]
