LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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.

For coprime positive $m,n$ , every pair of residue classes modulo $m$ and $n$ has a unique simultaneous class modulo $mn$

Statement

Let $m,n$ be positive integers, $a,b\in\mathbb Z$ , and $d:=\gcd(m,n)$ . The simultaneous system

$x\equiv a\pmod m,\qquad x\equiv b\pmod n$

is solvable if and only if $d\mid(a-b)$ . If it is solvable, all its solutions form one congruence class modulo $mn/d$ .

In particular, when $m,n$ are coprime, every pair of classes $[a]_m,[b]_n$ determines a unique simultaneous class $[x]_{mn}$ . This includes $m=1$ or $n=1$ .

Facts & Assumptions

Given: Positive integers $m,n$ , integers $a,b$ , and $d:=\gcd(m,n)$ .

[L1]

The gcd $d$ is a positive common divisor of $m,n$ (Common divisor, and the greatest common divisor $\gcd(a,b)$ , with the convention $\gcd(0,0) := 0$ ).

[L2]

Writing $m=dm'$ and $n=dn'$ , the positive integers $m',n'$ are coprime (If $d = \gcd(a,b)$ is nonzero then $a/d$ and $b/d$ are coprime, The integers have no zero divisors; multiplicative cancellation).

[L3]

Coprime integers $u,v$ admit integers $s,t$ with $su+tv=1$ ( $a$ and $b$ are coprime if and only if $ax + by = 1$ for some integers $x, y$ ; and in that case the only common divisors of $a$ and $b$ are $1$ and $-1$ ).

[L4]

Congruence means divisibility of a difference, and divisors are preserved by integer linear combinations (Congruence modulo an integer: $a\equiv b\pmod n$ when $n\mid(a-b)$ , including the moduli $0$ and $1$ , Divisibility is reflexive and transitive on $\mathbb{Z}$ , and is linear: if $d \mid a$ and $d \mid b$ then $d \mid ax + by$ for all integers $x, y$ ; also $d \mid a$ implies $d \mid ac$ , $-d \mid a$ and $d \mid -a$ ).

[L5]

The quotient $\mathbb Z/c$ consists of the congruence classes modulo $c$ (The congruence class $[a]_n$ and the quotient set $\mathbb{Z}/n$ ).

Proof

technique · direct

1.1

If $x$ solves both congruences, then $m\mid(x-a)$ and $n\mid(x-b)$ . Since $d$ divides $m,n$ , it divides both differences and therefore their difference $b-a$ ; equivalently $d\mid(a-b)$ .

L1L4

1.2

Conversely suppose $d\mid(a-b)$ and write $a-b=dc$ , $m=dm'$ , $n=dn'$ as in [L2]. Choose $u,v$ with $um'+vn'=1$ by [L3], put $t:=-uc$ , and set $x:=a+mt$ . Then $x\equiv a\pmod m$ , while $x-b=(a-b)+d m't=d(c-m'uc)=dcn'v$ , so $x\equiv b\pmod n$ .

L2L3L4

1.3

If $x,y$ are two solutions, then $m\mid(x-y)$ , so $x-y=dm'q$ for some integer $q$ . Also $n=dn'\mid(x-y)$ , hence cancellation of $d$ gives $n'\mid m'q$ ; multiplying a Bézout identity for $m',n'$ by $q$ shows $n'\mid q$ . Thus $dm'n'=mn/d$ divides $x-y$ .

L2L3L4

1.4

Conversely, if $mn/d=dm'n'$ divides $x-y$ , then both $m=dm'$ and $n=dn'$ divide $x-y$ , so $x$ and $y$ satisfy exactly the same two residue conditions. Hence, when compatible, the solution set is one class modulo $mn/d$ .

L2L4L5

2.1

When $\gcd(m,n)=1$ , one has $d=1$ and the compatibility condition is automatic; the modulus $mn/d$ is $mn$ , so steps 1.1 through 1.4 give the stated bijection between pairs of residue classes and simultaneous classes. The same proof applies when either modulus is $1$ .

step 1.1step 1.2step 1.3step 1.4L5∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 64 results over 18 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

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

For coprime positive m,nm,nm,n, every pair of residue classes modulo mmm and nnn has a unique simultaneous class modulo mnmnmn