The Cauchy-sequence reals have the least-upper-bound property

Fix $s_0\in S$ (possible as $S\mathrm{\ne }\mathrm{\varnothing }$); by [L6] choose a real $a_0<s_0$, so $a_0$ is not an upper bound of $S$, and put $b_0=U$, an upper bound of $S$.

Define $(a_k),(b_k)$ by bisection: given $a_k$ (not an upper bound) and $b_k$ (an upper bound), let $m=(a_k+b_k)\mathrm{/}2$; if $m$ is an upper bound set $a_{k+1}=a_k,b_{k+1}=m$, otherwise set $a_{k+1}=m,b_{k+1}=b_k$.

An induction on $k$ shows each $b_k$ is an upper bound of $S$, each $a_k$ is not, $a_k\le a_{k+1}\le b_{k+1}\le b_k$, and $b_k-a_k=(b_0-a_0)\mathrm{/}{2}^k$.

Given rational $\epsilon >0$, by [L4] choose $k$ with $(b_0-a_0)<2^k\widehat{\epsilon }$; then for all $j\ge k$, $b_j-a_j=(b_0-a_0)\mathrm{/}{2}^j\le (b_0-a_0)\mathrm{/}{2}^k<\widehat{\epsilon }$.

For $j,l\ge k$ both $a_j,a_l,b_j,b_l$ lie in the nested interval $[a_k,b_k]$, so $\mathrm{\mid }{a}_j-a_l\mathrm{\mid }\le b_k-a_k<\widehat{\epsilon }$ and likewise $\mathrm{\mid }{b}_j-b_l\mathrm{\mid }<\widehat{\epsilon }$; hence $(a_k)$ and $(b_k)$ are Cauchy sequences of reals.

By [L2], $(a_k)$ converges to a real $s$ and $(b_k)$ to a real $s^{\mathrm{\prime }}$. If $s<s^{\mathrm{\prime }}$, choose by [L6] a positive rational $\epsilon$ with $3\widehat{\epsilon }<s^{\mathrm{\prime }}-s$. For all large $k$, convergence and step 4.1 give $\mathrm{\mid }{a}_k-s\mathrm{\mid }<\widehat{\epsilon }$, $\mathrm{\mid }{b}_k-s^{\mathrm{\prime }}\mathrm{\mid }<\widehat{\epsilon }$ and $b_k-a_k<\widehat{\epsilon }$, whence $s^{\mathrm{\prime }}-s\le \mathrm{\mid }{s}^{\mathrm{\prime }}-b_k\mathrm{\mid }+(b_k-a_k)+\mathrm{\mid }{a}_k-s\mathrm{\mid }<3\widehat{\epsilon }$, a contradiction. If $s^{\mathrm{\prime }}<s$, choose $2\widehat{\epsilon }<s-s^{\mathrm{\prime }}$; for all large $k$, $a_k\le b_k$ and the two convergence bounds give $s-s^{\mathrm{\prime }}\le \mathrm{\mid }s-a_k\mathrm{\mid }+(a_k-b_k)+\mathrm{\mid }{b}_k-s^{\mathrm{\prime }}\mathrm{\mid }<2\widehat{\epsilon }$, again a contradiction. Thus $s=s^{\mathrm{\prime }}$. For fixed $k$ and every $j\ge k$, step 3.1 gives $a_k\le a_j\le b_j\le b_k$. If $s<a_k$, choose $0<\widehat{\epsilon }<a_k-s$ and use $a_j\to s$; if $b_k<s$, choose $0<\widehat{\epsilon }<s-b_k$ and use $b_j\to s$. Each choice contradicts the displayed inequalities for all large $j$, so $a_k\le s\le b_k$.

Every $t\in S$ satisfies $t\le b_k$ for all $k$, since each $b_k$ is an upper bound. If $s<t$, choose by [L6] a positive rational $\epsilon$ with $\widehat{\epsilon }<t-s$. Since $b_k\to s$, eventually $\mathrm{\mid }{b}_k-s\mathrm{\mid }<\widehat{\epsilon }$, hence $b_k<s+\widehat{\epsilon }<t$, contradicting $t\le b_k$. Therefore $t\le s$, so $s$ is an upper bound of $S$.

If $v$ is any upper bound of $S$, then for each $k$ some element of $S$ exceeds $a_k$, because $a_k$ is not an upper bound; hence $a_k<v$. If $v<s$, choose by [L6] a positive rational $\epsilon$ with $\widehat{\epsilon }<s-v$. Since $a_k\to s$, eventually $\mathrm{\mid }{a}_k-s\mathrm{\mid }<\widehat{\epsilon }$, so $a_k>s-\widehat{\epsilon }>v$, a contradiction. Thus $s\le v$, and $s$ is the least upper bound.

Hence $s=\sup S$ exists in ${\mathbb{R}}_C$; as $S$ was an arbitrary nonempty bounded-above set, ${\mathbb{R}}_C$ has the least-upper-bound property and is a complete ordered field.