ExampleConstruction: AI-adaptedVerification: AI-adaptedprecheck 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.

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

Example

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

$a x + b y = c$

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

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

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

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

Facts & Assumptions

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

[L1]

$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 $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 \geq 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) \neq (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 ${a x + b y : x, y \in Z}$ ; in particular $a x + b y = \gcd (a, b)$ has an integer solution).

[L5]

$d = \gcd (u, v)$ exactly when $d \geq 0$ , $d ∣ u$ , $d ∣ 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 \geq 0$ , $d ∣ a$ , $d ∣ 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 ∣ u$ and $d ∣ v$ then $d ∣ u x + v y$ for all $x, y$ (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$ ).

[L7]

$d ∣ u$ means $u = d q$ for some $q$ ; $0 ∣ u$ only for $u = 0$ (Divisibility in $Z$ : $d ∣ a$ when $a = d q$ for some integer $q$ ).

[L8]

For $u \in Z$ and $v > 0$ there is exactly one pair $(q, r)$ with $u = q v + r$ and $0 \leq r < v$ , and $v ∣ u$ holds exactly when $r = 0$ (Division with remainder in $Z$ : for $a \in Z$ and $b > 0$ there are unique $q, r \in Z$ with $a = q b + r$ and $0 \leq r < b$ ).

Verification

technique · direct

1.1

If $a x + b y = c$ has a solution, then $g ∣ a$ and $g ∣ b$ give $g ∣ a x + b y = c$ by [L6].

L3L6

1.2

Conversely suppose $g ∣ c$ , say $c = g k$ . If $(a, b) \neq (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) = g k = c$ , a solution.

L1L4L7

1.3

If instead $(a, b) = (0, 0)$ then $g = 0$ , so $0 ∣ 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 \geq 0$ ; $6 = 3 \cdot 2$ and $15 = 3 \cdot 5$ , so $3 ∣ 6$ and $3 ∣ 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 $a x + b y = c$ is equivalent to $g ∣ c$ .

step 1.1step 1.2step 1.3

3.1

$3 ∣ 9$ , since $9 = 3 \cdot 3$ ; so $6 x + 15 y = 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 ∤ 7$ : since $3 > 0$ , [L8] applies, and $7 = 2 \cdot 3 + 1$ with $0 \leq 1 < 3$ is the unique such representation, so the remainder is $1 \neq 0$ and $3$ does not divide $7$ . Hence $6 x + 15 y = 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 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 $a x + b y = \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 $a x + b y = c$ .
The unsolvable case is genuinely unsolvable, not merely hard. Every value of $6 x + 15 y$ 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 · two levels

36 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

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

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