はじめに
競技プログラミングで中国剰余定理（Chinese Remainder Theorem; CRT）を使う問題が出てきたので，証明を含む概要を備忘録として記した．
本記事は以下を参照して作成した．
https://qiita.com/drken/items/ae02240cd1f8edfc86fd
また，拡張ユークリッドの互除法を事前説明なしに用いている．
中国剰余定理とは
中国剰余定理は以下のように表される.
$m_1, m_2, m_3, \dots, m_n$をどの2つも互いに素な自然数とする．
この時，任意の整数$b_1, b_2,b_3,\dots,b_n$に対して，
x\equiv b_1 \ ({\rm mod}\ m_1)\\
x\equiv b_2 \ ({\rm mod}\ m_2)\\
\vdots\\
x\equiv b_n \ ({\rm mod}\ m_n)
を満たす整数$x$が存在する．また，$M=m_1m_2\dots m_n$とすると，上記を満たす0以上$M$未満の$x$はただ一つ存在し，特にそれを$r$とすると以下が成立する．
x\equiv b_1 \ ({\rm mod}\ m_1)\\
x\equiv b_2 \ ({\rm mod}\ m_2)\\
\vdots\\
x\equiv b_n \ ({\rm mod}\ m_n)\\
\Leftrightarrow x\equiv r\ ({\rm mod}\ M)
この定理は法が互いに素である複数の合同式による条件を一つにまとめることができることを述べている．
例えば，「3で割ると2余り，かつ7で割ると4余る」という条件を満たす整数は，$11,32,53,74,95$などである．つまり，
x\equiv 2 \ ({\rm mod}\ 3)\\
x\equiv 4 \ ({\rm mod}\ 7)
という条件と
$$x\equiv 11 \ ({\rm mod}\ 21)$$
という条件が同値となる．
中国剰余定理の証明（2元ver. ）
ここでは，2元の場合である
x\equiv b_1 \ ({\rm mod}\ m_1)\\
x\equiv b_2 \ ({\rm mod}\ m_2)
を満たすxが0以上$m_1m_2$未満の間にただ一つ存在することを示す．3元以上の場合も同様に示すことができる．
ここでは，まず解の存在性を示し，その後，解の一意性を示す．
解の存在性
実際に解を構成することで存在を示す．
$m_1$と$m_2$は互いに素であるため，最大公約数は1である．したがって，拡張ユークリッドの互除法より，
$$m_1p+m_2q=1$$
を満たす整数の組$(p,q)$を構成できる．
この時，$m_2q=-m_1p+1,m_1p=-m_2q+1$なので，
m_2q\equiv 1\ ({\rm mod}\ m_1)\\
m_1p\equiv 1\ ({\rm mod}\ m_2)
が成り立つ．
したがって，$x=b_2m_1p+b_1m_2q$とすれば，
x\equiv b_1\ ({\rm mod}\ m_1)\\
x\equiv b_2\ ({\rm mod}\ m_2)
となる．したがって，この$x$を$m_1m_2$で割った余りが解なので存在が示された．
解の一意性
0以上$m_1m_2$未満の間に解が2つ存在したと仮定する．
この解を$x,y\ (<m_1m_2)$とすると，
x\equiv b_1,y\equiv b_1\ ({\rm mod}\ m_1)\\
x\equiv b_2,y\equiv b_2\ ({\rm mod}\ m_2)
が成立するので，$x-y$は$m_1$と$m_2$で割り切れる．
いま，$m_1,m_2$は互いに素なので，$x-y$は最小公倍数である$m_1m_2$で割り切れることとなり，
$$x\equiv y\ ({\rm mod}\ m_1m_2)$$
が成り立つ．$x,y<m_1m_2$より，$x=y$となるが，これは仮定に反する．
したがって，一意性が示された．
合同式をまとめる部分の証明
次に，
x\equiv b_1 \ ({\rm mod}\ m_1)\\
x\equiv b_2 \ ({\rm mod}\ m_2)\\
\Leftrightarrow x\equiv r\ ({\rm mod}\ m_1m_2)
を示す．
必要性(→)
これまでの議論から，
r\equiv b_1 \ ({\rm mod}\ m_1)\\
r\equiv b_2 \ ({\rm mod}\ m_2)
を満たす$r$が0以上$m_1m_2$未満の範囲にただ一つ存在する．
ここで，この$r$とは異なる0以上$m_1m_2$未満の整数を$r'$とし，
x\equiv b_1 \ ({\rm mod}\ m_1)\\
x\equiv b_2 \ ({\rm mod}\ m_2)\\
x\equiv r'\ ({\rm mod}\ m_1m_2)
を満たす$x$が存在したと仮定する．
この時，$x$は整数$x'$を用いて$x=m_1m_2x'+r'$と表すことができるので，
x\equiv r'\equiv b_1 \ ({\rm mod}\ m_1)\\
x\equiv r'\equiv b_2 \ ({\rm mod}\ m_2)\\
となるが，これは$r$の一意性に反する．したがって，
x\equiv b_1 \ ({\rm mod}\ m_1)\\
x\equiv b_2 \ ({\rm mod}\ m_2)\\
\Rightarrow x\equiv r\ ({\rm mod}\ m_1m_2)
である．
十分性(←)
0以上$m_1m_2$未満の整数$r$が
r\equiv b_1 \ ({\rm mod}\ m_1)\\
r\equiv b_2 \ ({\rm mod}\ m_2)
を満たすとする．この時，
$$x\equiv r\ ({\rm mod}\ m_1m_2)$$
を満たす任意の整数$x$を考える．
$x$は整数$x'$を用いて$x=m_1m_2x'+r'$と表すことができるので，
x\equiv r\equiv b_1 \ ({\rm mod}\ m_1)\\
x\equiv r\equiv b_2 \ ({\rm mod}\ m_2)
が成り立つ．
したがって，
x\equiv b_1 \ ({\rm mod}\ m_1)\\
x\equiv b_2 \ ({\rm mod}\ m_2)\\
\Leftarrow x\equiv r\ ({\rm mod}\ m_1m_2)
である．