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.
and are coprime if and only if for some integers ; and in that case the only common divisors of and are and
Statement
Let . Then and are coprime (Coprime integers: ) if and only if
When this holds, the set of common divisors of and is exactly .
Facts & Assumptions
Given: Integers and .
and are coprime when (Coprime integers: , Common divisor, and the greatest common divisor , with the convention ).
exactly when , , , and every common divisor of and divides (Every common divisor of and divides ; consequently exactly when , , , and every common divisor of and divides — a characterisation that holds at as well).
If and then for all ; and for every (Divisibility is reflexive and transitive on , and is linear: if and then for all integers ; also implies , and , Divisibility in : when for some integer ).
exactly when or , and ( is a commutative monoid whose group of units is ; equivalently holds exactly for and ).
is a commutative ring, with , , and (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).
by convention (Common divisor, and the greatest common divisor , with the convention ).
Proof
and . If then , contradicting in [L5]. By totality either or ; in the second case adding gives , and since otherwise , so and hence , which with contradicts antisymmetry.
Conversely, suppose for some . Every common divisor of and divides by [L4], hence or by [L5].
Suppose and are coprime, so . Then , since ; so [L2] supplies with .
The integer then satisfies all four conditions of [L3]: by step 1.1, and by [L4], and every common divisor of and divides by step 1.2. Hence , that is, and are coprime.
So coprimality and the solvability of are equivalent, by step 2.1 and step 2.2.
When they hold, step 1.2 shows every common divisor is or ; conversely and are common divisors of any pair, since , , and . So the set of common divisors is exactly , and it has two elements since .
Remarks
-
The criterion is the practical form of coprimality. Verifying from the definition means examining all common divisors; exhibiting one pair with settles it in a line, and the extended Euclidean algorithm produces such a pair (The extended Euclidean algorithm: the same descent produces integers with , so Bézout coefficients are computed and not merely shown to exist).
-
The analogous statement with replaced by a general is false, and the correct version is that is solvable exactly when ; that is worked out on the companion page ( has an integer solution exactly when : is solvable and is not ↗).
Depends on
Coprime integers:
Bézout's identity: for integers not both zero, is the least positive element of ; in particular has an integer solution
Every common divisor of and divides ; consequently exactly when , , , and every common divisor of and divides — a characterisation that holds at as well
Common divisor, and the greatest common divisor , with the convention
Divisibility is reflexive and transitive on , and is linear: if and then for all integers ; also implies , and
is a commutative monoid whose group of units is ; equivalently holds exactly for and
Divisibility in : when for some integer
The integers form a commutative ring
Arithmetic on the integers
The integers form a totally ordered ring
Order on the integers