The Dedekind reals form a field

For $A,B>0^{\ast }$, $A\cdot B$ is a cut: it is nonempty and proper, downward closed because any $0<y<ab$ equals $(y\mathrm{/}b)b$ with $0<y\mathrm{/}b<a$ in $A$ (so the positive part of $A\cdot B$ is exactly $\{ab:a\in A,b\in B,a,b>0\}$), and it has no greatest element because $A$ has none: given $ab$ with $a\in A$, $b\in B$, $a,b>0$, choose $a^{\mathrm{\prime }}\in A$ with $a^{\mathrm{\prime }}>a$, and then $a^{\mathrm{\prime }}b\in A\cdot B$ with $a^{\mathrm{\prime }}b>ab$ since $b>0$; and $0^{\ast }\cdot B=0^{\ast }$ by the sign rule, so multiplication of nonnegatives lands in $\mathbb{R}$.

On nonnegatives multiplication is commutative: $A\cdot B$ and $B\cdot A$ are the same set, since $\{ab\}=\{ba\}$ by commutativity of rational multiplication.

Identity on nonnegatives: $A\cdot 1^{\ast }=A$ for $A\ge 0^{\ast }$. For $x\in A$ with $x>0$ pick $a\in A$, $a>x$ (no greatest element), so $x=a\cdot (x\mathrm{/}a)$ with $0<x\mathrm{/}a<1$, giving $A\subseteq A\cdot 1^{\ast }$; conversely $ar<a\in A$ for $0<r<1$ forces $ar\in A$, so $A\cdot 1^{\ast }\subseteq A$; the $0^{\ast }$ case is the sign rule.

$1^{\ast }\mathrm{\ne }{0}^{\ast }$, as the embedding is injective and $1\mathrm{\ne }0$ in $\mathbb{Q}$.

For the reverse inclusion of distributivity, dispose of degenerate cases: if $A=0^{\ast }$ then $A\cdot B=A\cdot C=A\cdot (B+C)=0^{\ast }$, so $A\cdot B+A\cdot C=0^{\ast }=A\cdot (B+C)$; if $B=0^{\ast }$ then $A\cdot B=0^{\ast }$ and $B+C=0^{\ast }+C=C$ (additive identity), so $A\cdot B+A\cdot C=0^{\ast }+A\cdot C=A\cdot C=A\cdot (B+C)$, and symmetrically if $C=0^{\ast }$.

Sign rule: for all cuts $X,Y$, $(-X)\cdot Y=-(X\cdot Y)$ and $X\cdot (-Y)=-(X\cdot Y)$; indeed $\mathrm{\mid }-X\mathrm{\mid }=\mathrm{\mid }X\mathrm{\mid }$ so both sides keep magnitude $\mathrm{\mid }X\mathrm{\mid }\mathrm{\mid }Y\mathrm{\mid }$, while negating one factor toggles the same-sign versus opposite-sign classification of the pair and hence flips the product's sign in the definition $A\cdot B=0^{\ast }$ / $\mathrm{\mid }A\mathrm{\mid }\mathrm{\mid }B\mathrm{\mid }$ / $-(\mathrm{\mid }A\mathrm{\mid }\mathrm{\mid }B\mathrm{\mid })$ (the $0^{\ast }$ case being immediate), so in particular $X\cdot Y=-(\mathrm{\mid }X\mathrm{\mid }\cdot Y)$ whenever $X<0^{\ast }$.

On nonnegatives multiplication is associative: by step 1.1 the positive elements of $A\cdot B$ are exactly the products $ab$, so those of $(A\cdot B)\cdot C$ are the $(ab)c=abc$, and likewise $A\cdot (B\cdot C)$ has positive part the $a(bc)=abc$; both sides are thus $\{q\le 0\}\cup \{abc:a\in A,b\in B,c\in C,a,b,c>0\}$, by associativity of rational products.

Distributivity on nonnegatives, inclusion $\subseteq$ for $A,B,C\ge 0^{\ast }$: a positive element of $A\cdot (B+C)$ is $a\cdot w$ with $a\in A$, $w\in B+C$, $a,w>0$, and $w=b+c$ for some $b\in B$, $c\in C$; then $a\cdot w=ab+ac$ where $ab\in A\cdot B$ and $ac\in A\cdot C$ (each product lies in the positive part of its factor product when positive, otherwise in that product's $\{q\le 0\}$ clause), so $a\cdot w\in A\cdot B+A\cdot C$; with the $\{q\le 0\}$ clause this gives $A\cdot (B+C)\subseteq A\cdot B+A\cdot C$.

For the reverse inclusion assume $A,B,C>0^{\ast }$, the degenerate cases being step 1.5; then $A\cdot B$ and $A\cdot C$ each contain a positive rational and, being downward-closed cuts (step 1.1), contain positive rationals arbitrarily close to $0$.

Every $A\mathrm{\ne }{0}^{\ast }$ has a multiplicative inverse: for $A>0^{\ast }$ the reciprocal $A^{-1}$ satisfies $A\cdot A^{-1}=1^{\ast }$; for $A<0^{\ast }$ we have $-A>0^{\ast }$ and $A^{-1}=-((-A{)}^{-1})$, so applying the sign rule to both factors gives $A\cdot A^{-1}=(-A)\cdot (-A{)}^{-1}=1^{\ast }$ by the reciprocal of the positive cut $-A$.

Take $u\in A\cdot B+A\cdot C$ with $u>0$, say $u=s+t$ with $s\in A\cdot B$, $t\in A\cdot C$: if $t\le 0$, pick a positive $t^{\mathrm{\prime }}\in A\cdot C$ with $t^{\mathrm{\prime }}<u$ (available by step 2.3) and set $s^{\mathrm{\prime }}:=u-t^{\mathrm{\prime }}$, so $0<s^{\mathrm{\prime }}\le s$ (since $t\le 0$ gives $s\ge u>s^{\mathrm{\prime }}$) and $s^{\mathrm{\prime }}\in A\cdot B$ by downward closure, then replace $(s,t)$ by $(s^{\mathrm{\prime }},t^{\mathrm{\prime }})$; symmetrically if $s\le 0$; so we may assume $s,t>0$.

The nonnegative laws now extend by signs: $A\cdot B$ and $B\cdot A$ share magnitude $\mathrm{\mid }A\mathrm{\mid }\mathrm{\mid }B\mathrm{\mid }=\mathrm{\mid }B\mathrm{\mid }\mathrm{\mid }A\mathrm{\mid }$ and the same sign, hence are equal (step 1.2); $(A\cdot B)\cdot C$ and $A\cdot (B\cdot C)$ share magnitude $\mathrm{\mid }A\mathrm{\mid }\mathrm{\mid }B\mathrm{\mid }\mathrm{\mid }C\mathrm{\mid }$ and the sign given by the product of the three factor signs, hence are equal (step 2.1); and $A\cdot 1^{\ast }=A$, since $1^{\ast }>0^{\ast }$ leaves the sign of $A$ unchanged and $\mathrm{\mid }A\mathrm{\mid }\cdot 1^{\ast }=\mathrm{\mid }A\mathrm{\mid }$ (step 1.3).

With $s,t>0$ from step 3.1, step 1.1 gives $s=a_1{b}_1$ and $t=a_2{c}_1$ with $a_1,a_2\in A$, $b_1\in B$, $c_1\in C$ all positive; set $a:=\max (a_1,a_2)$, so $a\in A$ and $a>0$.

Put $b:=s\mathrm{/}a$ and $c:=t\mathrm{/}a$: then $0<b=a_1{b}_1\mathrm{/}a\le b_1$, so $b\in B$, and $0<c=a_2{c}_1\mathrm{/}a\le c_1$, so $c\in C$, both by downward closure; hence $u=s+t=ab+ac=a(b+c)$ with $b+c\in B+C$, $b+c>0$, $a\in A$, $a>0$, so $u\in A\cdot (B+C)$.

Hence for $A,B,C>0^{\ast }$ and $u\in A\cdot B+A\cdot C$: if $u\le 0$ then $u\in A\cdot (B+C)$ by its $\{q\le 0\}$ clause, and if $u>0$ then $u\in A\cdot (B+C)$ by step 5.1, so $A\cdot B+A\cdot C\subseteq A\cdot (B+C)$; with step 2.2 this gives $A\cdot (B+C)=A\cdot B+A\cdot C$, an equality that also holds in the degenerate cases of step 1.5, so distributivity holds for all $A,B,C\ge 0^{\ast }$.

Distributivity for $A\ge 0^{\ast }$ with $B,C\le 0^{\ast }$: writing $B=-\mathrm{\mid }B\mathrm{\mid }$, $C=-\mathrm{\mid }C\mathrm{\mid }$ so that $B+C=(-\mathrm{\mid }B\mathrm{\mid })+(-\mathrm{\mid }C\mathrm{\mid })=-(\mathrm{\mid }B\mathrm{\mid }+\mathrm{\mid }C\mathrm{\mid })$ by [L10], the sign rule and nonnegative distributivity give $A\cdot (B+C)=-(A\cdot (\mathrm{\mid }B\mathrm{\mid }+\mathrm{\mid }C\mathrm{\mid }))=-(A\cdot \mathrm{\mid }B\mathrm{\mid }+A\cdot \mathrm{\mid }C\mathrm{\mid })=(-(A\cdot \mathrm{\mid }B\mathrm{\mid }))+(-(A\cdot \mathrm{\mid }C\mathrm{\mid }))=A\cdot B+A\cdot C$, the last equality using that negation is an additive homomorphism.

Distributivity for $A\ge 0^{\ast }$ with $B\ge 0^{\ast }\ge C$ and $D:=B+C\ge 0^{\ast }$: then $B=D+\mathrm{\mid }C\mathrm{\mid }$ with $D,\mathrm{\mid }C\mathrm{\mid }\ge 0^{\ast }$, so $A\cdot B=A\cdot D+A\cdot \mathrm{\mid }C\mathrm{\mid }$ by nonnegative distributivity, whence $A\cdot D=A\cdot B-A\cdot \mathrm{\mid }C\mathrm{\mid }=A\cdot B+A\cdot C$ because $A\cdot C=-(A\cdot \mathrm{\mid }C\mathrm{\mid })$ by the sign rule; that is $A\cdot (B+C)=A\cdot B+A\cdot C$.

Distributivity for $A\ge 0^{\ast }$ with $B\ge 0^{\ast }\ge C$ and $D:=B+C<0^{\ast }$: then $\mathrm{\mid }C\mathrm{\mid }=B+\mathrm{\mid }D\mathrm{\mid }$ with $B,\mathrm{\mid }D\mathrm{\mid }\ge 0^{\ast }$, so $A\cdot \mathrm{\mid }C\mathrm{\mid }=A\cdot B+A\cdot \mathrm{\mid }D\mathrm{\mid }$ by nonnegative distributivity, giving $A\cdot C=-(A\cdot \mathrm{\mid }C\mathrm{\mid })=(-(A\cdot B))+(-(A\cdot \mathrm{\mid }D\mathrm{\mid }))$ and $A\cdot D=-(A\cdot \mathrm{\mid }D\mathrm{\mid })$ by the sign rule, whence $A\cdot B+A\cdot C=-(A\cdot \mathrm{\mid }D\mathrm{\mid })=A\cdot D=A\cdot (B+C)$.

Distributivity for $A\ge 0^{\ast }$ and arbitrary $B,C$: if $B,C\ge 0^{\ast }$ this is step 6.1; if $B,C\le 0^{\ast }$ it is step 7.1; otherwise one factor is $\ge 0^{\ast }$ and the other $\le 0^{\ast }$, say $B\ge 0^{\ast }\ge C$ (else exchange $B,C$ using commutativity of $+$), and then it is step 7.2 or step 7.3 according as $B+C\ge 0^{\ast }$ or $B+C<0^{\ast }$; by the sign trichotomy these cases are exhaustive, so $A\cdot (B+C)=A\cdot B+A\cdot C$.

Distributivity for $A<0^{\ast }$: the sign rule gives $A\cdot (B+C)=-(\mathrm{\mid }A\mathrm{\mid }\cdot (B+C))$ and $A\cdot B+A\cdot C=(-(\mathrm{\mid }A\mathrm{\mid }\cdot B))+(-(\mathrm{\mid }A\mathrm{\mid }\cdot C))=-(\mathrm{\mid }A\mathrm{\mid }\cdot B+\mathrm{\mid }A\mathrm{\mid }\cdot C)$, while $\mathrm{\mid }A\mathrm{\mid }\ge 0^{\ast }$ makes step 8.1 apply to give $\mathrm{\mid }A\mathrm{\mid }\cdot (B+C)=\mathrm{\mid }A\mathrm{\mid }\cdot B+\mathrm{\mid }A\mathrm{\mid }\cdot C$, so the two negated cuts coincide and $A\cdot (B+C)=A\cdot B+A\cdot C$.

By the sign trichotomy every cut $A$ is either $\ge 0^{\ast }$ (step 8.1) or $<0^{\ast }$ (step 9.1), so $A\cdot (B+C)=A\cdot B+A\cdot C$ holds for all cuts $A,B,C$.

Thus $(\mathbb{R},+)$ is an abelian group (L5), multiplication is commutative and associative with identity $1^{\ast }\mathrm{\ne }{0}^{\ast }$ (step 3.2, step 1.4), distributes over addition (step 10.1), and every nonzero cut is invertible (step 2.4): $\mathbb{R}$ is a field.