[proofplan]
The hypothesis that $E$ is nonsingular ensures that the standard chord-and-tangent definition of the [elliptic curve group law](/page/Elliptic%20Curve%20Group%20Law) applies to this Weierstrass cubic, and the hypothesis $P+Q \ne O$ ensures that the sum is an affine point with coordinates $(x_3,y_3)$. That group-law construction says that the line through $P$ and $Q$, or the tangent line at $P$ when $P=Q$, meets the cubic in a third point $R$, and $P+Q$ is the reflection of $R$ across the $x$-axis. We substitute the corresponding line into the Weierstrass equation and obtain a cubic polynomial whose known roots are $x_1$ and $x_2$, with $x_1$ counted twice in the tangent case. Comparing the coefficient of $X^2$ over an [algebraic closure](/page/Algebraic%20Closure) first identifies the third root and then shows it is rational; reflecting the third intersection point gives the displayed formula for $y_3$.
[/proofplan]
[step:Define the relevant line through the known point or tangent direction]
First suppose $P \ne Q$ and $x_1 \ne x_2$. Define $\lambda \in \mathbb{Q}$ by
\begin{align*}
\lambda=\frac{y_2-y_1}{x_2-x_1}.
\end{align*}
Define the affine line map $L: \mathbb{Q} \to \mathbb{Q}^2$ as follows: for every $X \in \mathbb{Q}$,
\begin{align*}
L(X)=\bigl(X,\, y_1+\lambda(X-x_1)\bigr).
\end{align*}
Since $x_1,x_2,y_1,y_2 \in \mathbb{Q}$ and $x_2-x_1 \ne 0$, we have $\lambda \in \mathbb{Q}$. Moreover $L(x_1)=P$ and $L(x_2)=Q$.
Now suppose $P=Q$ and $2y_1 \ne 0$. Define $\lambda \in \mathbb{Q}$ by
\begin{align*}
\lambda=\frac{3x_1^2+a}{2y_1}.
\end{align*}
Define the affine line map $L: \mathbb{Q} \to \mathbb{Q}^2$ as follows: for every $X \in \mathbb{Q}$,
\begin{align*}
L(X)=\bigl(X,\, y_1+\lambda(X-x_1)\bigr).
\end{align*}
Again $\lambda \in \mathbb{Q}$, and $L(x_1)=P$.
In both cases, $L$ is the secant line through $P$ and $Q$ in the first case and the tangent line to $E$ at $P$ in the second case.
[/step]
[step:Substitute the line into the cubic and identify the known roots]
Define the polynomial $F \in \mathbb{Q}[X]$ by
\begin{align*}
F(X)=\bigl(y_1+\lambda(X-x_1)\bigr)^2-\bigl(X^3+aX+b\bigr).
\end{align*}
The zeros of $F$ are exactly the $X$-coordinates of the affine intersection points of the line $L$ with the cubic $E$.
In the secant case, $F(x_1)=0$ because $P \in E(\mathbb{Q})$, and $F(x_2)=0$ because $Q \in E(\mathbb{Q})$. In the tangent case, $F(x_1)=0$, and
\begin{align*}
F'(X)=2\lambda\bigl(y_1+\lambda(X-x_1)\bigr)-(3X^2+a).
\end{align*}
Therefore
\begin{align*}
F'(x_1)=2\lambda y_1-(3x_1^2+a)=0
\end{align*}
by the definition of $\lambda$. Hence $x_1$ is a root of $F$ with multiplicity at least two in the tangent case.
[guided]
The purpose of introducing $F$ is to translate a geometric intersection problem into a root-counting problem for one polynomial. A point of the line $L$ has the form
\begin{align*}
\bigl(X,\, y_1+\lambda(X-x_1)\bigr).
\end{align*}
This point lies on $E$ exactly when its coordinates satisfy the equation $y^2=x^3+ax+b$, which is exactly the condition
\begin{align*}
\bigl(y_1+\lambda(X-x_1)\bigr)^2-\bigl(X^3+aX+b\bigr)=0.
\end{align*}
Thus the roots of $F$ record the $X$-coordinates of the intersections of $L$ with $E$.
In the secant case, the line has been chosen so that it passes through both $P=(x_1,y_1)$ and $Q=(x_2,y_2)$. Since both points lie on $E$, substituting $X=x_1$ and $X=x_2$ into $F$ gives
\begin{align*}
F(x_1)=y_1^2-(x_1^3+ax_1+b)=0.
\end{align*}
It also gives
\begin{align*}
F(x_2)=y_2^2-(x_2^3+ax_2+b)=0.
\end{align*}
The condition $x_1 \ne x_2$ ensures that these are two distinct roots.
In the tangent case, the line must meet the cubic at $P$ with multiplicity at least two. We verify this algebraically by checking that both $F(x_1)$ and $F'(x_1)$ vanish. First,
\begin{align*}
F(x_1)=y_1^2-(x_1^3+ax_1+b)=0
\end{align*}
because $P \in E(\mathbb{Q})$. Differentiating the polynomial $F$ gives
\begin{align*}
F'(X)=2\lambda\bigl(y_1+\lambda(X-x_1)\bigr)-(3X^2+a).
\end{align*}
Evaluating at $X=x_1$ gives
\begin{align*}
F'(x_1)=2\lambda y_1-(3x_1^2+a).
\end{align*}
Since in the tangent case
\begin{align*}
\lambda=\frac{3x_1^2+a}{2y_1}
\end{align*}
and $2y_1 \ne 0$, this becomes
\begin{align*}
F'(x_1)=0.
\end{align*}
Therefore $x_1$ is counted twice as an intersection root in the tangent case.
[/guided]
[/step]
[step:Compare the quadratic coefficient to determine the third intersection]
Let $\overline{\mathbb{Q}}$ denote an algebraic closure of $\mathbb{Q}$. Since $F \in \mathbb{Q}[X]$ has degree three, it factors into three linear factors over $\overline{\mathbb{Q}}$. Let $x_R \in \overline{\mathbb{Q}}$ denote the remaining root of $F$, counted with multiplicity, so that in the secant case the roots are $x_1,x_2,x_R$, and in the tangent case the roots are $x_1,x_1,x_R$. Since the tangent case has $P=Q$, we may write $x_2=x_1$ there, so both cases are uniformly described by the roots $x_1,x_2,x_R$ counted with multiplicity.
Expanding the square in the definition of $F$ gives a cubic polynomial whose leading term is $-X^3$ and whose quadratic term is $\lambda^2X^2$. Thus
\begin{align*}
F(X)=-X^3+\lambda^2X^2+\text{terms of degree at most }1.
\end{align*}
Since the leading coefficient is $-1$, the factorization of $F$ over $\overline{\mathbb{Q}}$ is
\begin{align*}
F(X)=-(X-x_1)(X-x_2)(X-x_R).
\end{align*}
The coefficient of $X^2$ in the right-hand side is
\begin{align*}
x_1+x_2+x_R.
\end{align*}
Comparing the coefficient of $X^2$ with the expanded form of $F$ gives
\begin{align*}
x_1+x_2+x_R=\lambda^2.
\end{align*}
Therefore
\begin{align*}
x_R=\lambda^2-x_1-x_2.
\end{align*}
Because $x_1,x_2,\lambda \in \mathbb{Q}$, this formula shows $x_R \in \mathbb{Q}$.
[/step]
[step:Reflect the third intersection point to obtain the sum]
Define $y_R \in \mathbb{Q}$ by
\begin{align*}
y_R=y_1+\lambda(x_R-x_1).
\end{align*}
Then $R=(x_R,y_R)$ is the third affine intersection point of $L$ with $E$, counted with intersection multiplicity: in the secant case the three counted $X$-roots are $x_1,x_2,x_R$, and in the tangent case they are $x_1,x_1,x_R$. At this point the proof uses the standard chord-and-tangent construction in the [elliptic curve group law](/page/Elliptic%20Curve%20Group%20Law) as an established definition of addition on a nonsingular Weierstrass cubic. Its hypotheses are met because $E$ is nonsingular and because $L$ is the secant line through $P,Q$ in the case $P \ne Q$ and the tangent line at $P$ in the case $P=Q$. In that definition, the group sum is obtained by taking the third intersection point with multiplicity and reflecting it across the $x$-axis. Therefore $P+Q$ is the reflection of $R$. Since the theorem assumes $P+Q \ne O$, this reflected point is affine, so we may write $P+Q=(x_3,y_3)$. Hence $x_3=x_R$ and $y_3=-y_R$. Using the expression for $x_R$ obtained above,
\begin{align*}
x_3=\lambda^2-x_1-x_2.
\end{align*}
Finally, substituting the definition of $y_R$ and then using $x_R=x_3$ gives
\begin{align*}
y_3=-y_1+\lambda(x_1-x_3).
\end{align*}
This proves the stated rational addition formulas.
[/step]
