[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*}[/step]

[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: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]