LemmaStatement: AI-adaptedProof: 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$ 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$

Statement

Let $a, b \in Z$ . Then $a$ and $b$ are coprime (Coprime integers: $\gcd (a, b) = 1$ ) if and only if

$a x + b y = 1 for some x, y \in Z .$

When this holds, the set of common divisors of $a$ and $b$ is exactly ${1, - 1}$ .

Facts & Assumptions

Given: Integers $a$ and $b$ .

[L1]

$a$ and $b$ are coprime when $\gcd (a, b) = 1$ (Coprime integers: $\gcd (a, b) = 1$ , Common divisor, and the greatest common divisor $\gcd (a, b)$ , with the convention $\gcd (0, 0) : = 0$ ).

[L2]

For $(a, b) \neq (0, 0)$ there are $x_{0}, y_{0}$ with $a x_{0} + b y_{0} = \gcd (a, b)$ (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).

[L3]

$d = \gcd (a, b)$ exactly when $d \geq 0$ , $d ∣ a$ , $d ∣ b$ , and every common divisor of $a$ and $b$ 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).

[L4]

If $c ∣ a$ and $c ∣ b$ then $c ∣ a x + b y$ for all $x, y$ ; and $1 ∣ a$ for every $a$ (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$ , Divisibility in $Z$ : $d ∣ a$ when $a = d q$ for some integer $q$ ).

[L5]

$c ∣ 1$ exactly when $c = 1$ or $c = - 1$ , and $1 \neq - 1$ ( $(Z, \cdot, 1)$ is a commutative monoid whose group of units is ${1, - 1}$ ; equivalently $u ∣ 1$ holds exactly for $u = 1$ and $u = - 1$ ).

[L6]

$Z$ is a commutative ring, with $x \cdot 0 = 0$ , $x + 0 = x$ , $- (- x) = x$ and $(- x) (- y) = x y$ (The integers form a commutative ring, Arithmetic on the integers); its order is total, antisymmetric and transitive and is compatible with addition, and positives are closed under multiplication (The integers form a totally ordered ring, Order on the integers).

[L7]

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

Proof

technique · direct

1.1

$1 \neq 0$ and $0 \leq 1$ . If $1 = 0$ then $- 1 = - 0 = 0 = 1$ , contradicting $1 \neq - 1$ in [L5]. By totality either $0 \leq 1$ or $1 \leq 0$ ; in the second case adding $- 1$ gives $0 \leq - 1$ , and $- 1 \neq 0$ since otherwise $1 = 0$ , so $0 < - 1$ and hence $0 < (- 1) (- 1) = 1$ , which with $1 \leq 0$ contradicts antisymmetry.

L5L6

1.2

Conversely, suppose $a x + b y = 1$ for some $x, y$ . Every common divisor $c$ of $a$ and $b$ divides $a x + b y = 1$ by [L4], hence $c = 1$ or $c = - 1$ by [L5].

L4L5

2.1

Suppose $a$ and $b$ are coprime, so $\gcd (a, b) = 1$ . Then $(a, b) \neq (0, 0)$ , since $\gcd (0, 0) = 0 \neq 1$ ; so [L2] supplies $x_{0}, y_{0}$ with $a x_{0} + b y_{0} = \gcd (a, b) = 1$ .

step 1.1L1L2L7

2.2

The integer $1$ then satisfies all four conditions of [L3]: $1 \geq 0$ by step 1.1, $1 ∣ a$ and $1 ∣ b$ by [L4], and every common divisor of $a$ and $b$ divides $1$ by step 1.2. Hence $\gcd (a, b) = 1$ , that is, $a$ and $b$ are coprime.

step 1.1step 1.2L1L3L4

3.1

So coprimality and the solvability of $a x + b y = 1$ are equivalent, by step 2.1 and step 2.2.

step 2.1step 2.2

4.1

When they hold, step 1.2 shows every common divisor is $1$ or $- 1$ ; conversely $1$ and $- 1$ are common divisors of any pair, since $1 ∣ a$ , $1 ∣ b$ , $- 1 ∣ a$ and $- 1 ∣ b$ . So the set of common divisors is exactly ${1, - 1}$ , and it has two elements since $1 \neq - 1$ .

step 1.2L4L5∎

Remarks

The criterion is the practical form of coprimality. Verifying $\gcd (a, b) = 1$ from the definition means examining all common divisors; exhibiting one pair $(x, y)$ with $a x + b y = 1$ settles it in a line, and the extended Euclidean algorithm produces such a pair (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).
The analogous statement with $1$ replaced by a general $c$ is false, and the correct version is that $a x + b y = c$ is solvable exactly when $\gcd (a, b) ∣ c$ ; that is worked out on the companion page ( $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 ↗).

Depends on

Used by

Dependency tree · two levels

44 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

Coprime integers (Wikipedia) (standard reference, not scraped)

aa and bb are coprime if and only if ax+by=1ax+by=1 for some integers x,yx,y; and in that case the only common divisors of aa and bb are 11 and −1−1