%This proof is used in Emboss to propagate alignment restrictions through
%multiplication: if a and b are non-constant integers, their product can still
%have a known alignment.
%
%Forgive me on the details and formatting, math majors, I never completed my
%math degree.  --bolms
%
%Thanks to Aaron Webster for helping me format this as an actual proof.
\documentclass{article}
\usepackage[utf8]{inputenc}
\usepackage[english]{babel}
\usepackage{amssymb,amsmath,amsthm}
\title{Modular Congruence of the Product of Two Values with Known Modular Congruences}
\author{Emboss Authors}
\date{2017}

\begin{document}
\maketitle

\newtheorem{theorem}{Theorem}

%(Draft)
%TODO(webstera): Try to simplify this proof.

\begin{theorem}
Given

\begin{align*}
  &{a} \equiv {r} \pmod{{m}} \\
  &{b} \equiv {s} \pmod{{n}} \\
  &{a}, {r}, {m}, {b}, {s}, {n} \in \mathbb{Z}
\end{align*}

then

\begin{align*}
  &{a}{b} \equiv {r}{s} \pmod{G\left(\dfrac{{m}}{G\left({m}, {r}\right)},
\dfrac{{n}}{G\left({n}, {s}\right)}\right) \cdot G\left({m}, {r}\right) \cdot
G\left({n}, {s}\right)}
\end{align*}

where $G$ is the greatest common divisor function.
\end{theorem}

\begin{proof}
\begin{align}
  \text{Let }{q} &= G\left({m}, {r}\right) \label{eq:qdef} \\
             {p} &= G\left({n}, {s}\right) \label{eq:pdef} \\
             {z} &= G\left(\dfrac{{m}}{{q}}, \dfrac{{n}}{{p}}\right) =
                    G\left(\dfrac{{m}}{G\left({m}, {r}\right)},
                    \dfrac{{n}}{G\left({n}, {s}\right)}\right) \label{eq:zdef}
\end{align}

by the definition of modular congruence:
\begin{align}
  &\exists {x} \in \mathbb{Z} : {a} = {m}{x} + {r} \\
  &\exists {y} \in \mathbb{Z} : {b} = {n}{y} + {s}
\end{align}

multiplying $\dfrac{{q}}{{q}}$ and distributing $\dfrac{1}{{q}}$:
\begin{align}
  &{a} = {q}\left(\dfrac{{m}{x}}{q} + \dfrac{{r}}{q}\right)
\end{align}

by the definition of ${q}$ in \eqref{eq:qdef}:
\begin{align}
  &\dfrac{{m}{x}}{q}, \dfrac{{r}}{q} \in \mathbb{Z} \label{eq:rqinz}
\end{align}

multiplying $\dfrac{{p}}{{p}}$ and distributing $\dfrac{1}{{p}}$:
\begin{align}
  &{b} = {p}\left(\dfrac{{n}{y}}{{p}} + \dfrac{{s}}{{p}}\right)
\end{align}

by the definition of ${p}$ in \eqref{eq:pdef}:
\begin{align}
  &\dfrac{{n}{y}}{{p}}, \dfrac{{s}}{{p}} \in \mathbb{Z} \label{eq:spinz}
\end{align}

multiplying $\dfrac{{z}}{{z}}$:
\begin{align}
  &{a} = {q}\left({z} \cdot \dfrac{{m}{x}}{{q}{z}} + \dfrac{{r}}{{q}}\right) \label{eq:aeqq}
\end{align}

by the definition of ${z}$ in \eqref{eq:zdef}:
\begin{align}
  &\dfrac{{m}{x}}{{q}{z}} \in \mathbb{Z} \label{eq:mxqzinz}
\end{align}

multiplying $\dfrac{{z}}{{z}}$:
\begin{align}
  &{b} = {p}\left({z} \cdot \dfrac{{n}{y}}{{p}{z}} + \dfrac{{s}}{{p}}\right) \label{eq:beqp}
\end{align}

by the definition of ${z}$ in \eqref{eq:zdef}:
\begin{align}
  &\dfrac{{n}{y}}{{p}{z}} \in \mathbb{Z} \label{eq:nypzinz}
\end{align}

\eqref{eq:aeqq} and \eqref{eq:beqp}:
\begin{align}
  &{a}{b} = {q}{p}\left({z} \cdot \dfrac{{m}{x}}{{q}{z}} +
    \dfrac{{r}}{{q}}\right)\left({z} \cdot \dfrac{{n}{y}}{{p}{z}} +
    \dfrac{{s}}{{p}}\right) \label{eq:abeqqp}
\end{align}

partially distributing \eqref{eq:abeqqp}:
\begin{align}
  &{a}{b} = {q}{p}\left({z}^2 \cdot \dfrac{{m}{x}}{{q}{z}} \cdot
    \dfrac{{n}{y}}{{p}{z}} + {z} \cdot \dfrac{{r}}{{q}} \cdot
    \dfrac{{n}{y}}{{p}{z}} + {z} \cdot \dfrac{{m}{x}}{{q}{z}} \cdot
    \dfrac{{s}}{{p}} + \dfrac{{r}}{{q}} \cdot \dfrac{{s}}{{p}}\right) \label{eq:abeqqpexp}
\end{align}

extracting the $\dfrac{{r}{s}}{{q}{p}}$ term from \eqref{eq:abeqqpexp} and cancelling $\dfrac{{q}{p}}{{q}{p}}$:
\begin{align}
  &{a}{b} = {q}{p}\left({z}^2 \cdot \dfrac{{m}{x}}{{q}{z}} \cdot
    \dfrac{{n}{y}}{{p}{z}} + {z} \cdot \dfrac{{r}}{{q}} \cdot
    \dfrac{{n}{y}}{{p}{z}} + {z} \cdot \dfrac{{m}{x}}{{q}{z}} \cdot
    \dfrac{{s}}{{p}}\right) + {r}{s} \label{eq:abeqqpextr}
\end{align}

factoring ${z}$ from \eqref{eq:abeqqpextr}:
\begin{align}
  &{a}{b} = {q}{p}{z}\left({z} \cdot \dfrac{{m}{x}}{{q}{z}} \cdot
    \dfrac{{n}{y}}{{p}{z}} + \dfrac{{r}}{{q}} \cdot \dfrac{{n}{y}}{{p}{z}} +
    \dfrac{{m}{x}}{{q}{z}} \cdot \dfrac{{s}}{{p}}\right) + {r}{s}
\end{align}

because ${z}, \dfrac{{r}}{q}, \dfrac{{s}}{{p}}, \dfrac{{m}{x}}{{q}{z}},
  \dfrac{{n}{y}}{{p}{z}} \in \mathbb{Z}$, per \eqref{eq:zdef}, \eqref{eq:rqinz}, \eqref{eq:spinz}, \eqref{eq:mxqzinz}, \eqref{eq:nypzinz}:
\begin{align}
  &{z} \cdot \dfrac{{m}{x}}{{q}{z}} \cdot \dfrac{{n}{y}}{{p}{z}} +
    \dfrac{{r}}{{q}} \cdot \dfrac{{n}{y}}{{p}{z}} + \dfrac{{m}{x}}{{q}{z}} \cdot
    \dfrac{{s}}{{p}} \in \mathbb{Z}
\end{align}

by the definition of modulus:
\begin{align}
  &{a}{b} \equiv {r}{s} \pmod{{q}{p}{z}}
\end{align}

by the definitions of ${q}$, ${p}$, and ${z}$ in \eqref{eq:qdef}, \eqref{eq:pdef}, and \eqref{eq:zdef}:
\begin{align}
  &{a}{b} \equiv {r}{s} \pmod{G\left(\dfrac{{m}}{G\left({m}, {r}\right)},
    \dfrac{{n}}{G\left({n}, {s}\right)}\right) \cdot G\left({m}, {r}\right)
    \cdot G\left({n}, {s}\right)}
\end{align}

\end{proof}
\end{document}