CorollaryStatement: AI-adaptedProof: AI-generatedprecheck passverified 2026-08-02 (claude-opus-5)

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.

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

Statement

Let $a, b \in Z$ . Every common divisor of $a$ and $b$ divides $\gcd (a, b)$ (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$ ).

Consequently, for $d \in Z$ the following are equivalent:

$d = \gcd (a, b)$ ;
$d \geq 0$ , $d ∣ a$ , $d ∣ b$ , and every common divisor of $a$ and $b$ divides $d$ .

This characterisation holds for every pair $(a, b)$ , the pair $(0, 0)$ included, where it returns the value $\gcd (0, 0) = 0$ fixed by convention.

Facts & Assumptions

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

[L1]

For $(a, b) \neq (0, 0)$ , $g$ is the greatest element of the set $D (a, b)$ of common divisors, so in particular $g \in D (a, b)$ , and $g \geq 1$ ; at $(a, b) = (0, 0)$ , $g = 0$ by convention. In both cases $g \geq 0$ (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} \in Z$ 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).

[L3]

Every integer divides $0$ (Divisibility in $Z$ : $d ∣ a$ when $a = d q$ for some integer $q$ ).

[L4]

If $c ∣ a$ and $c ∣ b$ then $c ∣ a x + b 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$ ).

[L5]

If $u ∣ v$ and $v ∣ u$ then $∣ u ∣ = ∣ v ∣$ (For integers $a$ and $b$ the following are equivalent: $a ∣ b$ and $b ∣ a$ ; $b = u a$ for a unit $u$ ; $∣ a ∣ = ∣ b ∣$ . Being associates is an equivalence relation whose class of $a$ is ${a, - a}$ ).

[L6]

$∣ x ∣ = x$ when $x \geq 0$ (The absolute value $∣ a ∣$ of an integer, Absolute value in $Z$ : $∣ a ∣ \geq 0$ ; $∣ a ∣ = 0$ exactly when $a = 0$ ; $∣ - a ∣ = ∣ a ∣$ ; $∣ a b ∣ = ∣ a ∣ ∣ b ∣$ ; $- ∣ a ∣ \leq a \leq ∣ a ∣$ ; and $∣ a ∣ \leq c$ exactly when $- c \leq a \leq c$ ).

Proof

technique · direct

1.1

Suppose $(a, b) \neq (0, 0)$ and let $c$ be a common divisor of $a$ and $b$ . By [L2] fix $x_{0}, y_{0}$ with $a x_{0} + b y_{0} = g$ ; then $c ∣ g$ by [L4].

L2L4

1.2

Suppose instead $(a, b) = (0, 0)$ . Then $g = 0$ , and every integer, in particular every common divisor $c$ , divides $0 = g$ .

L1L3

1.3

$g$ itself is a common divisor of $a$ and $b$ : for $(a, b) \neq (0, 0)$ this is $g \in D (a, b)$ , and for $(a, b) = (0, 0)$ it is $0 ∣ 0$ . And $g \geq 0$ in both cases.

L1L3

2.1

In both cases every common divisor of $a$ and $b$ divides $g$ ; since the two cases are exhaustive, this is the first assertion.

step 1.1step 1.2

3.1

Claim 1 implies claim 2: if $d = g$ then $d \geq 0$ , $d ∣ a$ and $d ∣ b$ by step 1.3, and every common divisor divides $d$ by step 2.1.

step 2.1step 1.3

3.2

Claim 2 implies claim 1: suppose $d \geq 0$ , $d ∣ a$ , $d ∣ b$ , and every common divisor of $a$ and $b$ divides $d$ . Then $d$ is a common divisor, so $d ∣ g$ by step 2.1; and $g$ is a common divisor by step 1.3, so $g ∣ d$ by hypothesis. Hence $∣ d ∣ = ∣ g ∣$ by [L5], and since $d \geq 0$ and $g \geq 0$ this reads $d = ∣ d ∣ = ∣ g ∣ = g$ .

step 2.1step 1.3L1L5L6

4.1

The two claims are therefore equivalent, for every pair $(a, b)$ including $(0, 0)$ , where step 1.2 and step 1.3 were proved directly from the convention rather than from a maximum.

step 1.2step 1.3step 3.1step 3.2∎

Remarks

This is the statement later pages should cite. "Greatest in the order of $Z$ " is how $\gcd$ was defined, but it is not a property that survives at $(0, 0)$ and it is not what any later argument uses. "Nonnegative, a common divisor, and divisible by every common divisor" is uniform, and it is the definition that generalises beyond $Z$ .
Both halves of claim 2 are needed. Dropping $d \geq 0$ leaves $d$ determined only up to sign, since $- g$ also divides $a$ and $b$ and is divided by every common divisor (For integers $a$ and $b$ the following are equivalent: $a ∣ b$ and $b ∣ a$ ; $b = u a$ for a unit $u$ ; $∣ a ∣ = ∣ b ∣$ . Being associates is an equivalence relation whose class of $a$ is ${a, - a}$ ). Dropping "every common divisor divides $d$ " leaves every nonnegative common divisor a candidate.

Depends on

Used by

Dependency tree · two levels

23 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

Greatest common divisor (Wikipedia) (standard reference, not scraped)

Every common divisor of aa and bb divides gcd⁡(a,b)gcd(a,b); consequently d=gcd⁡(a,b)d=gcd(a,b) exactly when d≥0d≥0, d∣ad∣a, d∣bd∣b, and every common divisor of aa and bb divides dd — a characterisation that holds at (a,b)=(0,0)(a,b)=(0,0) as well