TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-07-31

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Chinese remainder theorem for a finite pairwise-coprime list: simultaneous residues determine one class modulo the product, and the resulting bijection preserves addition and multiplication

Statement

Let $n_{0}, \dots, n_{r - 1}$ be a finite pairwise-coprime list of positive integers and let $N : = \prod_{i < r} n_{i}$ . The map

$Φ : Z / N ⟶ \prod_{i < r} Z / n_{i}, [x]_{N} ⟼ ([x]_{n_{i}})_{i < r},$

is a bijection. It preserves addition, multiplication, $[0]$ , and $[1]$ componentwise. For the empty list, $N = 1$ and both sides have one element.

Facts & Assumptions

Given: A natural $r$ , a finite pairwise-coprime list of positive integers $n_{0}, \dots, n_{r - 1}$ , and $N : = \prod_{i < r} n_{i}$ .

[L1]

Every initial product $P_{k} : = \prod_{i < k} n_{i}$ is coprime to $n_{k}$ , and the full product divides every common multiple of all list entries (For a finite pairwise-coprime list of positive integers, the product divides every common multiple, and each initial product is coprime to every remaining modulus).

[L2]

For coprime positive $m, n$ , each pair of residue classes modulo $m, n$ determines exactly one class modulo $m n$ (For coprime positive $m, n$ , every pair of residue classes modulo $m$ and $n$ has a unique simultaneous class modulo $m n$ ).

[L3]

Finite products have empty value $1$ and satisfy $P_{k + 1} = P_{k} n_{k}$ (The product $g_{0} g_{1} \dots g_{n - 1}$ of a finite list in a monoid, by recursion, with the empty product ( $n = 0$ ) equal to the identity, Generalised associativity: in a monoid the product of a finite list does not depend on the bracketing, and in a commutative monoid it does not depend on the order of the factors either).

[L4]

Congruence modulo a divisor follows from congruence modulo the dividend, and modular addition and multiplication are computed on representatives (Congruence modulo an integer: $a \equiv b (m o d n)$ when $n ∣ (a - b)$ , including the moduli $0$ and $1$ , Addition and multiplication on $Z / n$ by $[a]_{n} + [b]_{n} = [a + b]_{n}$ and $[a]_{n} [b]_{n} = [a b]_{n}$ ).

[L5]

A map is bijective exactly when it is both injective and surjective (Injection, surjection, bijection).

[L6]

Induction proves a statement at every natural number from its base case and successor implication (The principle of mathematical induction).

[F1]

The quotient $Z / c$ is the set of congruence classes modulo $c$ (The congruence class $[a]_{n}$ and the quotient set $Z / n$ ).

Proof

technique · induction

1.1

For $r = 0$ , $N = P_{0} = 1$ . The quotient $Z / 1$ has one class because congruence modulo $1$ is universal, and the empty Cartesian product has its single empty tuple; hence $Φ$ is a bijection and all componentwise preservation assertions are vacuous.

baseL3L4F1

1.2

Assume the simultaneous-residue assertion for the first $k$ moduli. Given classes modulo the first $k + 1$ moduli, the induction hypothesis supplies a unique class $[y]_{P_{k}}$ having the first $k$ residues. Since $\gcd (P_{k}, n_{k}) = 1$ by [L1], [L2] supplies a unique class $[x]_{P_{k} n_{k}} = [x]_{P_{k + 1}}$ reducing to $[y]_{P_{k}}$ and to the prescribed class modulo $n_{k}$ . It therefore has all prescribed residues.

ihL1L2L3

1.3

If $x \equiv y (m o d N)$ , every $n_{i}$ divides $N$ and hence divides $x - y$ , so $Φ$ is well defined. For representatives $x, y$ , its $i$ th coordinate sends $[x + y]_{N}$ to $[x + y]_{n_{i}} = [x]_{n_{i}} + [y]_{n_{i}}$ and sends $[x y]_{N}$ to $[x y]_{n_{i}} = [x]_{n_{i}} [y]_{n_{i}}$ ; it similarly sends $[0]_{N}, [1]_{N}$ to the componentwise identities.

L3L4

2.1

If two classes modulo $P_{k + 1}$ have the same first $k + 1$ residues, their representatives have difference divisible by every $n_{i}$ for $i < k + 1$ , hence by $P_{k + 1}$ using [L1]; the two classes are equal. Thus the class constructed in step 1.2 is unique.

ihstep 1.2L1L4

3.1

Induction gives existence and uniqueness for every finite length $r$ . Therefore $Φ$ is surjective and injective, hence bijective by [L5].

step 1.1step 1.2step 2.1L5L6

4.1

Steps 3.1 and 1.3 prove all assertions, including the empty-list boundary case from step 1.1.

step 1.1step 3.1step 1.3discharge-induction∎

Depends on

Used by

Dependency tree · two levels

42 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

K. Conrad, The Chinese Remainder Theorem (standard reference, not scraped)