Thm) A1, A2, A3, ..., An를 각각 서로소인 양의 정수라고 하자. (서로 다른 i, j에 대해 Ai와 Aj의 최대공약수는 1.)
그리고 i=1, 2, ..., n에 대해
0≤ai＜Ai,
ai는 정수라고 하자.
그러면,
(모든 i=1, 2, .., n에 대해 M을 Ai로 나눈 나머지가 ai)를 만족하는 0 이상 A1*A2*A3*...*An 미만의 정수 m은 유일하게 존재한다.
pf)
(유일성)
x와 y를 각각 (모든 i=1, 2, .., n에 대해 M을 Ai로 나눈 나머지가 ai)를 만족하는 0 이상 A1*A2*A3*...*An 미만의 정수라고 하자.
그러면, 모든 i=1, 2, ..., n에 대해, |x-y|는 Ai의 배수이다. 따라서 |x-y|는 A1*A2*...*An의 배수이다.
이때, A1, A2, ..., An은 각각 서로소이므로 그 최대공배수는 A1*A2*....*An이 되며,
|x-y|는 0 이상, A1*A2*A3*...*An 미만의 정수이므로 |x-y|=0, x=y이다.
(존재성)
함수 f : { x | x는 0 이상 A1*A2*A3*...*An 미만의 정수}→ {(x1, x2, ..., xn) | 모든 i=1, 2, ..., n에 대해 0≤xi＜Ai},
f(x)=(x1, x2, .., xn), 모든 i=1, 2, ..., n에 대해 xi는 x를 Ai로 나눈 나머지
라고 정의하자.
그러면, 위의 유일성 증명에 따라 f는 일대일 함수(injection)이다.
그리고 f는 공역과 정의역이 서로 크기가 같은 유한 집합이다.
따라서 f는 일대일 대응 함수가 된다. (bijection)
즉, f(m)=(m1, m2, .., mn)=(a1, a2, ..., an)을 만족하는 정의역 상의 원소 x가 존재한다.
참고로 이 정리는 괴델의 불완전성 정리를 증명하기 위해 쓰인다.
