The complex numbers are algebraically closed

By [L1], it is enough to prove that every nonconstant polynomial in $\mathbb{R}[x]$ splits over $\mathbb{C}$. Fix such a polynomial $f\in \mathbb{R}[x]$.

Put $h:=f(x)(x^2+1)$. By [L2], choose a splitting field $E\mathrm{/}\mathbb{R}$ of $h$. The roots of $h$ are algebraic over $\mathbb{R}$, and $E$ is generated by finitely many of them, so [L13] makes $E\mathrm{/}\mathbb{R}$ finite. Because $E$ is a splitting field of $h$, [L3] makes it normal, and [L4] makes it separable. Thus $E\mathrm{/}\mathbb{R}$ is finite Galois.

Let $G:=\mathrm{Gal}(E\mathrm{/}\mathbb{R})$. By [L7], choose a Sylow $2$-subgroup $H\le G$, and put $M:=E^H$. Then [L5] gives $[M:\mathbb{R}]=[G:H],$ which is odd by the definition of a Sylow $2$-subgroup.

Since $x^2+1$ splits in $E$, choose $j\in E$ with $j^2=-1$. By [L10], there is a unique real-field embedding $\iota :\mathbb{C}\to E$ sending $i$ to $j$. Identify $\mathbb{C}$ with its image, so that $\mathbb{R}\subseteq \mathbb{C}\subseteq E\mathrm{.}$

Let $\alpha \in M$. Since $\mathbb{R}\subseteq \mathbb{R}(\alpha )\subseteq M$, the tower law [L6] shows that $[\mathbb{R}(\alpha ):\mathbb{R}]$ divides $[M:\mathbb{R}]$, so $[\mathbb{R}(\alpha ):\mathbb{R}]$ is odd. Because $\alpha \in E$ and step 1.2 made $E\mathrm{/}\mathbb{R}$ finite, the element $\alpha$ is algebraic over $\mathbb{R}$. Fact [L14] therefore makes the minimal-polynomial degree of $\alpha$ over $\mathbb{R}$ equal to the same odd number $[\mathbb{R}(\alpha ):\mathbb{R}]$; by [L12] it must have degree $1$. Hence $\alpha \in \mathbb{R}$. Since every element of $M$ lies in $\mathbb{R}$, we get $M=\mathbb{R}$.

Because $M=E^H=\mathbb{R}=E^G$, the bijection in [L5] forces $H=G$. Therefore $G$ is a finite $2$-group.

Put $J:=\mathrm{Gal}(E\mathrm{/}\mathbb{C})$. Then $J\le G$, so step 3.1 makes $J$ a finite $2$-group. Suppose $J$ is nontrivial.

By [L8], the nontrivial $2$-group $J$ has a subgroup $K$ of index $2$. Put $L:=E^K$. Then $E^J=\mathbb{C}$ by [L5], and [L5] together with [L6] gives $[L:\mathbb{C}]=[J:K]=2.$

The field $\mathbb{C}$ has characteristic zero, hence not $2$, so [L11] makes the quadratic extension $L\mathrm{/}\mathbb{C}$ equal to $\mathbb{C}(\sqrt{d})$ for some $d\in \mathbb{C}$. By [L9], choose $e\in \mathbb{C}$ with $e^2=d$. Then $L=\mathbb{C}(\sqrt{d})=\mathbb{C}(e)=\mathbb{C},$ contradicting step 5.1. Therefore $J$ is trivial.

Since $\mathrm{Gal}(E\mathrm{/}\mathbb{C})=1$, the fixed field of the trivial subgroup is $E$; by [L5], that fixed field is also $\mathbb{C}$. Thus $E=\mathbb{C}$. Because $E$ is a splitting field of $h$ and $f$ divides $h$, the polynomial $f$ splits over $\mathbb{C}$. By step 1.1 and [L1], this proves that $\mathbb{C}$ is algebraically closed.