(Draft)
TODO(webstera): Try to simplify this proof.
$$\text{If}$$
$${a} \equiv {r} \pmod{{m}}$$
$${b} \equiv {s} \pmod{{n}}$$
$${a}, {r}, {m}, {b}, {s}, {n} \in ℤ$$
$$\text{then}$$
$${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)}$$
$$\text{where }G\text{ is the greatest common divisor function.}$$
$$\text{Proof:}$$
$$\exists {x} \in ℤ : {a} = {m}{x} + {r} \text{ by the definition of modular congruence}$$
$$\exists {y} \in ℤ : {b} = {n}{y} + {s} \text{ by the definition of modular congruence}$$
$$\text{Let }{q} = G\left({m}, {r}\right)$$
$$\text{Let }{p} = G\left({n}, {s}\right)$$
$$\text{Let }{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)$$
$${a} = {q}\left(\dfrac{{m}{x}}{q} + \dfrac{{r}}{q}\right) \text{ by multiplying } \dfrac{{q}}{{q}} \text{ and distributing } \dfrac{1}{{q}}$$
$$\dfrac{{m}{x}}{q}, \dfrac{{r}}{q} \in ℤ \text{ by the definition of } {q} \text{ in (3) }$$
$${b} = {p}\left(\dfrac{{n}{y}}{{p}} + \dfrac{{s}}{{p}}\right) \text{ by multiplying } \dfrac{{p}}{{p}} \text{ and distributing } \dfrac{1}{{p}}$$
$$\dfrac{{n}{y}}{{p}}, \dfrac{{s}}{{p}} \in ℤ \text{ by the definition of } {p} \text{ in (4) }$$
$${a} = {q}\left({z} \cdot \dfrac{{m}{x}}{{q}{z}} + \dfrac{{r}}{{q}}\right) \text{ by multiplying } \dfrac{{z}}{{z}}$$
$$\dfrac{{m}{x}}{{q}{z}} \in ℤ \text{ by the definition of } {z} \text{ in (5) }$$
$${b} = {p}\left({z} \cdot \dfrac{{n}{y}}{{p}{z}} + \dfrac{{s}}{{p}}\right) \text{ by multiplying } \dfrac{{z}}{{z}}$$
$$\dfrac{{n}{y}}{{p}{z}} \in ℤ \text{ by the definition of } {z} \text{ in (5)}$$
$${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) \text{ by (10) and (12)}$$
$${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) \text{ by partially distributing (14)}$$
$${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} \text{ by extracting the } \dfrac{{r}{s}}{{q}{p}} \text{ term from (15) and cancelling } \dfrac{{q}{p}}{{q}{p}}$$
$${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} \text{ by factoring } {z} \text{ from (16)}$$
$${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 ℤ \text{ because } {z}, \dfrac{{r}}{q}, \dfrac{{s}}{{p}}, \dfrac{{m}{x}}{{q}{z}}, \dfrac{{n}{y}}{{p}{z}}, {z} \in ℤ \text{ per (5), (7), (9), (11), (13)}$$
$${a}{b} \equiv {r}{s} \pmod{{q}{p}{z}} \text{ by the definition of modulus}$$
$${a}{b} ≡ {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)} \text{ by the definitions of } {q} \text{, } {p} \text{, and } {z} \text{ in (3), (4), and (5)}$$