[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$.[/step]

[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: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)$.[/step]

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

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