Proof that real multiplication distributes over addition using Dedekind cuts? Proving $\forall x,y,z\in \mathbb R,\:x(y+z)=xy+xz$
There is a very concise proof of this in ProofWiki using Cauchy sequences, but I was wondering whether the same would be possible using Dedekind cuts.

There is, but as with most of the checks of the field axioms using Dedekind Cuts, it isn't pretty.
First recall that multiplication is given by, for $A,B$ positive
\begin{equation}
A\cdot B =\{a\cdot b \mid a\in A \wedge 0<a \wedge b \in B \wedge 0<b \} \cup \{ q\in \mathbb{Q}\mid q\leq 0\}.
\end{equation}
More generally, we define
\begin{equation}
A\cdot B=
\begin{cases}
\overline{0} & \text{If $A=\overline{0}$ or $B=\overline{0}$,} \\
-(A\cdot (-B)) & \text{If $\overline{0}<A$ and $B<\overline{0}$,} \\
-((-A)\cdot B) & \text{If $A<\overline{0}$ and $\overline{0}<B$,} \\
(-A)\cdot (-B) & \text{If $A<\overline{0}$ and $B<\overline{0}$.} 
\end{cases} 
\end{equation}
We want to show that $A\cdot (B+C)=A\cdot B+A\cdot C$.  Sadly, since this means that we now must take into account three variables, we have ourselves a case-by-case nightmare.  
First let us suppose that $A$, $B$, and $C$ are all positive.  Let $d\in A\cdot (B+C)$; if $d\leq 0$, then $d \in A\cdot B+A\cdot C$ since it is the sum of two positive Dedekind cuts.  Otherwise we have $0<d$; $d$ can hence be written as $d=a\cdot (b+c)$ where $0<a \in A$, $b \in B$, and $c \in C$ where $0<b+c$.  We can assume that $b$ and $c$ are positive because at least one must be positive; without loss of generality assume $b$ is positive.  If $c$ is negative, then $b+c<b$, so that because $B$ is downwards closed it follows that $b+c\in B$.  Then take a positive element $c'<b+c$ of $C$ and let $b'=b+c-c'$ which is necessarily positive by our choice of $c'$.  Then $b'+c'=b+c$ with $0<b'\in B$ and $0<c'\in C$.  Thus, we will simply assume that $b$ and $c$ are positive.   Hence, $ab\in A\cdot B$ and $ac\in A\cdot C$ and thus $d=ab+ac\in A\cdot B+A\cdot C$, so that $A\cdot (B+C) \subset A\cdot B + A\cdot C$.  
Similarly, if $d\in A\cdot B+A\cdot C$, then there exists $d_1\in A\cdot B$ and $d_2\in A\cdot C$ such that $d=d_1+d_2$.  If $d_1$ and $d_2$ are positive, then there are $0<a,a'\in A$, $0<b\in B$, and $0<c\in C$ such that $ab=d_1$ and $a'c=d_2$.  We may assume that $a=a'$, as otherwise we can let $a''=\frac{ab+a'c}{a+a'}$ which gives us $a''b+a''c=d$ and replace $a$ and $a'$ with $a''$.  Then $ab+a'c=ab+ac=a(b+c)$ so that $d=a(b+c)\in A\cdot (B+C)$.  If $d_1$ and $d_2$ are both non-positive, then $d_1+d_2$ is non-positive and thus lies in $A\cdot (B+C)$.  Finally, if one of $d_1$ and $d_2$ is non-positive while the other is positive -- say $d_1$ is positive and $d_2$ non-positive -- then $d_1=ab$ for $0<a\in A$ and $0<b\in B$, so taking $c$ to be any positive rational number in $C$ we find that $d_1+d_2<ab+ac=a(b+c)\in A\cdot (B+C)$, so that because $A\cdot (B+C)$ is downwards closed, we see that $d=d_1+d_2\in A\cdot (B+C)$, thus establishing the fact that $A\cdot B+A\cdot C\subset A\cdot (B+C)$.
A tool we shall make use of in the remaining cases is that $-(A+B)=(-A)+(-B)$:  $(A+B)+(-(A+B))=\overline{0}$ and $A+B+(-A)+(-B)=\overline{0}$, so that $(A+B)+(-(A+B))=(A+B)+(-A)+(-B)$, and cancellation of the term $A+B$ gives us the desired result.


*

*If $A=\overline{0}$, then $A\cdot (B+C)=A\cdot B=A\cdot C=\overline{0}$, and thus $A\cdot B+A\cdot C=\overline{0}=A\cdot (B+C)$.

*When $A$, $B$, and $C$ are all negative, $B+C$ is negative, so $A\cdot (B+C)=(-A)\cdot (-(B+C))=(-A)\cdot ((-B)+(-C))=(-A)\cdot (-B)+(-A)\cdot (-C)=A\cdot B+A\cdot C$.
\item When $A$ is negative and $B$ and $C$ are positive, $B+C$ is positive and $A\cdot (B+C)=-((-A)\cdot (B+C))=-((-A)\cdot B+(-A)\cdot C)=(-((-A)\cdot B))+(-((-A)\cdot C))=A\cdot B+A\cdot C$.  

*If $B=\overline{0}$, then $A\cdot (B+C)=A\cdot (\overline{0}+C)=A\cdot C=A\cdot \overline{0}+A\cdot C=A\cdot B+A\cdot C$.  The same argument shows the case for $C=\overline{0}$.

*If $A$ and $C$ are negative and $B$ is positive, then we have three cases: if $B+C$ is positive, negative, or zero. In the last case, $B=(-C)$ and $A\cdot (B+C)=A\cdot \overline{0}=\overline{0}=(A\cdot B)+(-(A\cdot B))=A\cdot B+A\cdot (-B)=A\cdot B+A\cdot C$.  If $B+C$ is negative, then
\begin{align}
A\cdot C
& =A\cdot ((B+C)+(-B)) \\
& =(-A)\cdot (-((B+C)+(-B))) \\
& =(-A)\cdot ((-(B+C))+B) \\
& = (-A)\cdot (-(B+C))+(-A)\cdot B \\
& = A\cdot (B+C)+(-(A\cdot B))
\end{align}
Adding $A\cdot B$ to both sides gives us the desired result.
If $B+C$ is positive, then
\begin{align}
A\cdot B & =A\cdot ((B+C)+(-C)) \\
& =-((-A)\cdot ((B+C)+(-C))) \\
& = -((-A)\cdot (B+C)+(-A)\cdot (-C)) \\
& = -((-(A\cdot (B+C)))+A\cdot C) \\
& = A\cdot (B+C)+(-(A\cdot C)).
\end{align}
Adding $A\cdot C$ to both sides gives us the desired result.
The same arguments hold for $B$ negative and $C$ positive by interchanged the roles of $B$ and $C$ above.

*If $A$ and $B$ are positive and $C$ is negative, then we have three cases: if $B+C$ is positive, negative, or zero. In the last case, $B=(-C)$ and $A\cdot (B+C)=A\cdot \overline{0}=\overline{0}=(A\cdot B)+(-(A\cdot B))=A\cdot B+A\cdot (-B)=A\cdot B+A\cdot C$.  If $B+C$ is negative, then
\begin{align}
A\cdot C
& = A\cdot ((B+C)+(-B)) \\
& = -(A\cdot (-((B+C)+(-B)))) \\
& = -(A\cdot ((-(B+C))+B)) \\
& = -(A\cdot (-(B+C))+A\cdot B) \\
& = (-(A\cdot(-(B+C))))+(-(A\cdot B)) \\
& = A\cdot (B+C)+(-(A\cdot B))
\end{align}
Adding $A\cdot B$ to both sides gives us the desired result.
If $B+C$ is positive, then
\begin{align}
A\cdot B & =A\cdot ((B+C)+(-C)) \\
& = A\cdot ((B+C)+(-C)) \\
& = A\cdot (B+C)+A\cdot (-C)) \\
& = A\cdot (B+C)+(-(A\cdot C)) 
\end{align}
Adding $A\cdot C$ to both sides gives us the desired result.
The same arguments hold for $B$ negative and $C$ positive by interchanging the roles of $B$ and $C$ above.
(If there's a prettier way to prove this with Dedekind Cuts, I certainly don't know it.  At first glance the proof that Rudin gives in Principles of Mathematical Analysis is shorter, but that's because he doesn't actually do it all (rather, says "similar to our above proofs"))
