TheoremStatement: 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 $n \geq 1$ , $a x \equiv b (m o d n)$ is solvable exactly when $\gcd (a, n) ∣ b$ , and then has exactly $\gcd (a, n)$ solution classes modulo $n$

Statement

Let $a, b \in Z$ and $n \geq 1$ , and put $d : = \gcd (a, n)$ . The congruence

$a x \equiv b (m o d n)$

has an integer solution if and only if $d ∣ b$ . When it is solvable, it has exactly $d$ solution classes in $Z / n$ . More explicitly, if $a = d a^{'}$ , $n = d n^{'}$ , $b = d b^{'}$ and $x_{0}$ solves $a^{'} x_{0} \equiv b^{'} (m o d n^{'})$ , the solutions modulo $n$ are

$[x_{0} + j n^{'}]_{n} (0 \leq j < d) .$

Facts & Assumptions

Given: Integers $a, b$ , a positive integer $n$ , and $d : = \gcd (a, n)$ .

[L1]

The integer $d$ divides both $a$ and $n$ , and every common divisor of $a, n$ divides each integer linear combination of them (Common divisor, and the greatest common divisor $\gcd (a, b)$ , with the convention $\gcd (0, 0) : = 0$ , Divisibility is reflexive and transitive on $Z$ , and is linear: if $d ∣ a$ and $d ∣ b$ then $d ∣ a x + b y$ for all integers $x, y$ ; also $d ∣ a$ implies $d ∣ a c$ , $- d ∣ a$ and $d ∣ - a$ ).

[L2]

If $d ∣ b$ , the original congruence is equivalent to $a^{'} x \equiv b^{'} (m o d n^{'})$ , where $a = d a^{'}$ , $n = d n^{'}$ , $b = d b^{'}$ , $n^{'} > 0$ , and $a^{'}, n^{'}$ are coprime (If $n \geq 1$ , $d = \gcd (a, n)$ and $d ∣ b$ , then $a x \equiv b (m o d n)$ reduces to a congruence with coprime coefficient modulo $n / d$ ).

[L3]

Coprime integers $u, v$ admit integers $s, t$ with $s u + t v = 1$ ( $a$ and $b$ are coprime if and only if $a x + b y = 1$ for some integers $x, y$ ; and in that case the only common divisors of $a$ and $b$ are $1$ and $- 1$ , Bézout's identity: for integers $a, b$ not both zero, $\gcd (a, b)$ is the least positive element of ${a x + b y : x, y \in Z}$ ; in particular $a x + b y = \gcd (a, b)$ has an integer solution).

[L4]

Every class modulo a positive integer $c$ has a unique representative $r$ with $0 \leq r < c$ , and the quotient has cardinality $c$ (For $n \geq 1$ , every class in $Z / n$ has one representative $r$ with $0 \leq r < n$ , so $∣ Z / n ∣ = n$ ; while $Z / 0$ is in bijection with $Z$ , The cardinality $∣ A ∣$ of a finite set).

Proof

technique · direct

1.1

If $x$ solves the congruence, then $n ∣ a x - b$ , so $a x - b = n q$ for some $q$ and $b = a x - n q$ . Since $d ∣ a$ and $d ∣ n$ , it follows that $d ∣ b$ .

1.2

Conversely suppose $d ∣ b$ and use the notation of [L2]. Choose $u, v$ with $u a^{'} + v n^{'} = 1$ by [L3]. Then $x_{0} : = u b^{'}$ satisfies $a^{'} x_{0} - b^{'} = b^{'} (u a^{'} - 1) = - b^{'} v n^{'}$ , so it solves the reduced congruence and hence the original one.

L2L3

1.3

By [L4], every integer $q$ has a unique residue $j$ with $0 \leq j < d$ modulo $d$ . Thus every integer congruent to $x_{0}$ modulo $n^{'}$ is congruent modulo $d n^{'} = n$ to exactly one $x_{0} + j n^{'}$ with $0 \leq j < d$ .

2.1

Every solution $x$ of the reduced congruence is congruent to $x_{0}$ modulo $n^{'}$ . Indeed, $n^{'} ∣ a^{'} (x - x_{0})$ ; multiplying $u a^{'} + v n^{'} = 1$ by $x - x_{0}$ shows that $n^{'}$ divides $x - x_{0}$ . Conversely every $x \equiv x_{0} (m o d n^{'})$ solves the reduced congruence.

step 1.2L2L3

2.2

If $0 \leq i, j < d$ and $[x_{0} + i n^{'}]_{n} = [x_{0} + j n^{'}]_{n}$ , then $d n^{'} ∣ (i - j) n^{'}$ , so cancellation gives $d ∣ i - j$ ; uniqueness of the standard representatives modulo $d$ yields $i = j$ . Hence the displayed $d$ classes are distinct.

step 1.3L4

3.1

Steps 1.1 and 1.2 prove the solvability criterion. When it holds, steps 2.1, 1.3 and 2.2 show that the displayed list is exhaustive and contains exactly $d$ distinct solution classes.

step 1.1step 1.2step 2.1step 1.3step 2.2∎

Depends on

Used by

Dependency tree · two levels

34 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

Mathematics LibreTexts, Linear Congruences (standard reference, not scraped)

For n≥1n≥1, ax≡b(modn)ax≡b(modn) is solvable exactly when gcd⁡(a,n)∣bgcd(a,n)∣b, and then has exactly gcd⁡(a,n)gcd(a,n) solution classes modulo nn