TheoremStatement: 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 $n\ge1$ , $ax\equiv b\pmod n$ is solvable exactly when $\gcd(a,n)\mid b$ , and then has exactly $\gcd(a,n)$ solution classes modulo $n$

Statement

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

$ax\equiv b\pmod n$

has an integer solution if and only if $d\mid b$ . When it is solvable, it has exactly $d$ solution classes in $\mathbb Z/n$ . More explicitly, if $a=da'$ , $n=dn'$ , $b=db'$ and $x_0$ solves $a'x_0\equiv b'\pmod{n'}$ , the solutions modulo $n$ are

$[x_0+jn']_n\qquad(0\le 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 $\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$ ).

[L2]

If $d\mid b$ , the original congruence is equivalent to $a'x\equiv b'\pmod{n'}$ , where $a=da'$ , $n=dn'$ , $b=db'$ , $n'>0$ , and $a',n'$ are coprime (If $n\ge1$ , $d=\gcd(a,n)$ and $d\mid b$ , then $ax\equiv b\pmod n$ reduces to a congruence with coprime coefficient modulo $n/d$ ).

[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$ , Bézout's identity: for integers $a, b$ not both zero, $\gcd(a,b)$ is the least positive element of $\{\, ax + by : x, y \in \mathbb{Z} \,\}$ ; in particular $ax + by = \gcd(a,b)$ has an integer solution).

[L4]

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

Proof

technique · direct

1.1

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

1.2

Conversely suppose $d\mid b$ and use the notation of [L2]. Choose $u,v$ with $ua'+vn'=1$ by [L3]. Then $x_0:=ub'$ satisfies $a'x_0-b'=b'(ua'-1)=-b'vn'$ , 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\le j<d$ modulo $d$ . Thus every integer congruent to $x_0$ modulo $n'$ is congruent modulo $dn'=n$ to exactly one $x_0+jn'$ with $0\le j<d$ .

2.1

Every solution $x$ of the reduced congruence is congruent to $x_0$ modulo $n'$ . Indeed, $n'\mid a'(x-x_0)$ ; multiplying $ua'+vn'=1$ by $x-x_0$ shows that $n'$ divides $x-x_0$ . Conversely every $x\equiv x_0\pmod{n'}$ solves the reduced congruence.

step 1.2L2L3

2.2

If $0\le i,j<d$ and $[x_0+in']_n=[x_0+jn']_n$ , then $dn'\mid(i-j)n'$ , so cancellation gives $d\mid 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

The congruence 14x≡30pmod100 has exactly the two solutions x≡45,95pmod100 Example

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 75 results over 20 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

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

For n≥1n\ge1n≥1, ax≡b(modn)ax\equiv b\pmod nax≡b(modn) is solvable exactly when gcd⁡(a,n)∣b\gcd(a,n)\mid bgcd(a,n)∣b, and then has exactly gcd⁡(a,n)\gcd(a,n)gcd(a,n) solution classes modulo nnn