The p-adic numbers as a metric completion

Let $p$ be a prime. The space of $p$-adic numbers ${\mathbb{Q}}_p$ is the Cauchy-sequence quotient and metric constructed in assertions 1--4 of Every metric space has a completion, constructed as the equivalence classes of its Cauchy sequences for the metric

$d_p(x,y):=\mathrm{\mid }x-y{\mathrm{\mid }}_p,$

where $\mathrm{\mid }\cdot {\mathrm{\mid }}_p$ is the absolute value of The p-adic absolute value on the rationals. Thus its points are equivalence classes of rational $d_p$-Cauchy sequences, two sequences being equivalent when their termwise distance tends to $0$. Assertions 1--4 are choice-free and give ${\mathbb{Q}}_p$ its metric and its named dense isometric embedding of $\mathbb{Q}$. The general theorem's Countable-Choice-dependent completeness assertion is not used in this definition. The next theorem equips this metric space with the field operations extending those of $\mathbb{Q}$ and proves its completeness choice-free from the fixed countable enumeration of $\mathbb{Q}$.