The p-adic completion is a complete valued field

By the specific construction fixed in [L3] and supplied by [L1], an element of ${\mathbb{Q}}_p$ is represented by a $d_p$-Cauchy sequence $(x_n)$ in $\mathbb{Q}$, and the distance between classes is ${\widehat{d}}_p([x],[y])={\lim }_n\mathrm{\mid }{x}_n-y_n{\mathrm{\mid }}_p\mathrm{.}$ Define $[x]+[y]:=[x_n+y_n],[x][y]:=[x_n{y}_n],\mathrm{\mid }[x]{\mathrm{\mid }}_p:={\lim }_n\mathrm{\mid }{x}_n{\mathrm{\mid }}_p\mathrm{.}$

The nonarchimedean inequality in [L2] shows that sums and differences of Cauchy sequences are Cauchy. A Cauchy sequence in a nonarchimedean metric is bounded, so products of Cauchy sequences are again Cauchy, and equivalent representatives give equivalent sums and products because $x_n{y}_n-x_n^{\mathrm{\prime }}{y}_n^{\mathrm{\prime }}=x_n(y_n-y_n^{\mathrm{\prime }})+y_n^{\mathrm{\prime }}(x_n-x_n^{\mathrm{\prime }})\mathrm{.}$ Passing to the limit through [L2] proves representative independence of the extended absolute value as well.

Let $[x]\in {\mathbb{Q}}_p$ be nonzero. Then $\mathrm{\mid }[x]{\mathrm{\mid }}_p>0$, and step 1.1 says $\mathrm{\mid }{x}_n{\mathrm{\mid }}_p\to \mathrm{\mid }[x]{\mathrm{\mid }}_p$ in $\mathbb{R}$. So there are a real constant $c>0$ and an index $N$ with $\mathrm{\mid }{x}_n{\mathrm{\mid }}_p\ge c$ for all $n\ge N$. In particular $x_n\mathrm{\ne }0$ eventually. For $n,m\ge N$, $\mathrm{\mid }{x}_n^{-1}-x_m^{-1}{\mathrm{\mid }}_p=\frac{\mathrm{\mid }{x}_n-x_m{\mathrm{\mid }}_p}{\mathrm{\mid }{x}_n{\mathrm{\mid }}_p\mathrm{\mid }{x}_m{\mathrm{\mid }}_p}\le c^{-2}\mathrm{\mid }{x}_n-x_m{\mathrm{\mid }}_p,$ and the right-hand side tends to $0$ because $(x_n)$ is Cauchy. Thus $(x_n^{-1})$ is eventually defined and Cauchy, so every nonzero class has an inverse.

Multiplicativity and the strong triangle inequality on ${\mathbb{Q}}_p$ follow by taking limits of the corresponding rational identities from [L2].

With the valued-field structure established in step 4.1, it remains to prove completeness without invoking assertion 5 of the general completion theorem. Fix once and for all a bijection $e:\mathbb{N}\to \mathbb{Q}$ from [L4]; fixing this single supplied bijection is ordinary existential instantiation, not a family of choices. Let $({\xi }_n)$ be a Cauchy sequence in ${\mathbb{Q}}_p$. By density in [L1], each set $S_n:=\{k\in \mathbb{N}:{\widehat{d}}_p(\iota (e(k)),{\xi }_n)<2^{-n}\}$ is nonempty. Define $k_n:=\min S_n$ and $q_n:=e(k_n)$. The least-index rule in [L5] determines the whole sequence $(q_n)$ and makes no choice.

The rational sequence $(q_n)$ is $d_p$-Cauchy. Indeed, given $\epsilon >0$, use [L6] and Cauchyness of $({\xi }_n)$ to choose $N$ such that $2^{-n}<\epsilon \mathrm{/}3$ for $n\ge N$ and ${\widehat{d}}_p({\xi }_m,{\xi }_n)<\epsilon \mathrm{/}3$ for $m,n\ge N$. Since $\iota$ is isometric by [L1], for such $m,n$ the triangle inequality gives $d_p(q_m,q_n)={\widehat{d}}_p(\iota (q_m),\iota (q_n))<\epsilon \mathrm{.}$ Thus $x:=[(q_n)]$ is a point of ${\mathbb{Q}}_p$.

The embedded sequence $\iota (q_n)$ converges to $x$. For fixed $n$, the quotient metric of [L1] gives ${\widehat{d}}_p(\iota (q_n),x)={\lim }_{m\to \mathrm{\infty }}{d}_p(q_n,q_m)\mathrm{.}$ Given $\epsilon >0$, Cauchyness of $(q_n)$ supplies $N$ such that $d_p(q_n,q_m)<\epsilon \mathrm{/}2$ whenever $m,n\ge N$. Hence for every fixed $n\ge N$ the displayed real sequence is eventually bounded above by $\epsilon \mathrm{/}2$, so [L7] gives ${\widehat{d}}_p(\iota (q_n),x)\le \epsilon \mathrm{/}2<\epsilon$. This is convergence to $x$.

Finally, step 5.1 and the triangle inequality give ${\widehat{d}}_p({\xi }_n,x)\le {\widehat{d}}_p({\xi }_n,\iota (q_n))+{\widehat{d}}_p(\iota (q_n),x)<2^{-n}+{\widehat{d}}_p(\iota (q_n),x)\mathrm{.}$ Given $\epsilon >0$, [L6] and step 7.1 make the two terms on the right smaller than $\epsilon \mathrm{/}2$ for all sufficiently large $n$, so ${\widehat{d}}_p({\xi }_n,x)<\epsilon$. Thus every Cauchy sequence in ${\mathbb{Q}}_p$ converges, so ${\mathbb{Q}}_p$ is complete. Together with steps 1.1--4.1, it is a complete nonarchimedean valued field, with no choice principle used.