Alphabeta Math
LemmaStatement: Literature-sourcedProof: 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.

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∈Z, and d:=gcd⁡(m,n). The simultaneous system

x≡a(modm),x≡b(modn)

is solvable if and only if d∣(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

Proof

technique · direct
1.1

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

L1L4
1.2

Conversely suppose d∣(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≡a(modm), while x−b=(a−b)+dm′t=d(c−m′uc)=dcn′v, so x≡b(modn).

L2L3L4
1.3

If x,y are two solutions, then m∣(x−y), so x−y=dm′q for some integer q. Also n=dn′∣(x−y), hence cancellation of d gives n′∣m′q; multiplying a Bézout identity for m′,n′ by q shows n′∣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 · two levels

25 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