ExampleConstruction: AI-adaptedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (z-ai/glm-5.2)audited 2026-07-28

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.

$ax + by = c$ has an integer solution exactly when $\gcd(a,b) \mid c$ : $6x + 15y = 9$ is solvable and $6x + 15y = 7$ is not

Example

For integers $a, b, c$ , the equation

$ax + by = c$

has a solution $(x,y) \in \mathbb{Z} \times \mathbb{Z}$ if and only if $\gcd(a,b) \mid c$ (Common divisor, and the greatest common divisor $\gcd(a,b)$ , with the convention $\gcd(0,0) := 0$ , Divisibility in $\mathbb{Z}$ : $d \mid a$ when $a = dq$ for some integer $q$ ).

With $a = 6$ and $b = 15$ , where $\gcd(6,15) = 3$ :

$6x + 15y = 9$ is solvable, since $3 \mid 9$ ; explicitly $6 \cdot (-1) + 15 \cdot 1 = 9$ ;
$6x + 15y = 7$ has no solution, since $3 \nmid 7$ : dividing, $7 = 2 \cdot 3 + 1$ with remainder $1 \ne 0$ .

Numerals. For $k \in \mathbb{N}$ the symbol $k$ inside $\mathbb{Z}$ means $\iota(k)$ , the embedding of The naturals embed in the integers; the numerical identities below are the images of the corresponding identities in $\mathbb{N}$ .

Facts & Assumptions

Given: Integers $a, b, c$ , and $g := \gcd(a,b)$ .

[L1]

$\mathbb{Z}$ is a commutative ring: addition and multiplication are associative and commutative, $x \cdot 1 = x$ , $x \cdot 0 = 0$ , $x \cdot (-1) = -x$ , multiplication distributes over addition, and every $x$ has an additive inverse (The integers form a commutative ring, Arithmetic on the integers, The integers as equivalence classes of pairs of naturals).

[L2]

The order on $\mathbb{Z}$ is total, antisymmetric and transitive (The integers form a totally ordered ring, Order on the integers).

[L3]

$g$ is a common divisor of $a$ and $b$ , $g \ge 0$ , and $\gcd(0,0) = 0$ (Common divisor, and the greatest common divisor $\gcd(a,b)$ , with the convention $\gcd(0,0) := 0$ ).

[L4]

For $(a,b) \ne (0,0)$ there are $x_0,y_0$ with $a x_0 + b y_0 = g$ (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).

[L5]

$d = \gcd(u,v)$ exactly when $d \ge 0$ , $d \mid u$ , $d \mid v$ and every common divisor of $u$ and $v$ divides $d$ (Every common divisor of $a$ and $b$ divides $\gcd(a,b)$ ; consequently $d = \gcd(a,b)$ exactly when $d \ge 0$ , $d \mid a$ , $d \mid b$ , and every common divisor of $a$ and $b$ divides $d$ — a characterisation that holds at $(a,b) = (0,0)$ as well).

[L6]

If $d \mid u$ and $d \mid v$ then $d \mid ux + vy$ for all $x,y$ (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$ ).

[L7]

$d \mid u$ means $u = dq$ for some $q$ ; $0 \mid u$ only for $u = 0$ (Divisibility in $\mathbb{Z}$ : $d \mid a$ when $a = dq$ for some integer $q$ ).

[L8]

For $u \in \mathbb{Z}$ and $v > 0$ there is exactly one pair $(q,r)$ with $u = qv + r$ and $0 \le r < v$ , and $v \mid u$ holds exactly when $r = 0$ (Division with remainder in $\mathbb{Z}$ : for $a \in \mathbb{Z}$ and $b > 0$ there are unique $q, r \in \mathbb{Z}$ with $a = qb + r$ and $0 \le r < b$ ).

Verification

technique · direct

1.1

If $ax + by = c$ has a solution, then $g \mid a$ and $g \mid b$ give $g \mid ax + by = c$ by [L6].

L3L6

1.2

Conversely suppose $g \mid c$ , say $c = gk$ . If $(a,b) \ne (0,0)$ , take $x_0, y_0$ with $a x_0 + b y_0 = g$ and multiply by $k$ : $a(x_0 k) + b(y_0 k) = gk = c$ , a solution.

L1L4L7

1.3

If instead $(a,b) = (0,0)$ then $g = 0$ , so $0 \mid c$ forces $c = 0$ , and $a \cdot 0 + b \cdot 0 = 0 = c$ is a solution. The two cases are exhaustive.

L1L3L7

1.4

$\gcd(6,15) = 3$ . Indeed $3 \ge 0$ ; $6 = 3 \cdot 2$ and $15 = 3 \cdot 5$ , so $3 \mid 6$ and $3 \mid 15$ ; and $6 \cdot (-2) + 15 \cdot 1 = -12 + 15 = 3$ , so every common divisor of $6$ and $15$ divides $3$ by [L6]. By [L5] this is exactly the characterisation of $\gcd(6,15)$ .

L1L5L6L7algebra

2.1

So solvability of $ax + by = c$ is equivalent to $g \mid c$ .

step 1.1step 1.2step 1.3

3.1

$3 \mid 9$ , since $9 = 3 \cdot 3$ ; so $6x + 15y = 9$ is solvable by step 2.1, and $6 \cdot (-1) + 15 \cdot 1 = -6 + 15 = 9$ exhibits a solution.

step 2.1step 1.4L1L7algebra

4.1

$3 \nmid 7$ : since $3 > 0$ , [L8] applies, and $7 = 2 \cdot 3 + 1$ with $0 \le 1 < 3$ is the unique such representation, so the remainder is $1 \ne 0$ and $3$ does not divide $7$ . Hence $6x + 15y = 7$ has no integer solution by step 2.1.

step 2.1step 1.4L1L2L8algebra∎

Remarks

The criterion is decidable by the Euclidean algorithm: compute $\gcd(a,b)$ by The Euclidean algorithm: for $a \in \mathbb{Z}$ and $b > 0$ the remainder descent from $(a,b)$ terminates, and the last nonzero remainder is $\gcd(a,b)$ , test whether it divides $c$ by division with remainder, and, when it does, obtain a solution by scaling the Bézout pair that The extended Euclidean algorithm: the same descent produces integers $x, y$ with $ax + by = \gcd(a,b)$ , so Bézout coefficients are computed and not merely shown to exist computes.
Solutions are never unique when $a$ and $b$ are both nonzero; the family is described in Bézout coefficients are not unique: $1071 \cdot (-3) + 462 \cdot 7 = 21$ and $1071 \cdot 19 + 462 \cdot (-44) = 21$ , and for nonzero $a, b$ every solution has the form $(x_0 + t b/d,\; y_0 - t a/d)$ , and scaling that description by $k = c/\gcd(a,b)$ describes the solutions of $ax + by = c$ .
The unsolvable case is genuinely unsolvable, not merely hard. Every value of $6x + 15y$ is a multiple of $3$ , and $7$ is not one; no search is involved.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 54 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

Diophantine equation (Wikipedia) (standard reference, not scraped)

ax+by=cax + by = cax+by=c has an integer solution exactly when gcd⁡(a,b)∣c\gcd(a,b) \mid cgcd(a,b)∣c: 6x+15y=96x + 15y = 96x+15y=9 is solvable and 6x+15y=76x + 15y = 76x+15y=7 is not