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.
for all integers , the identity holding at and at as well
Statement
For all ,
(Common divisor, and the greatest common divisor , with the convention , The absolute value of an integer). The identity is asserted for every triple, including and , where both sides are .
Facts & Assumptions
Given: Integers , and , .
is a commutative ring: addition and multiplication are associative and commutative, , , , multiplication distributes over addition, and every has an additive inverse, with (The integers form a commutative ring, Arithmetic on the integers).
The order on is total, antisymmetric and transitive, and positives are closed under multiplication; means together with (The integers form a totally ordered ring, Order on the integers).
always, with when and by convention; is a common divisor of and (Common divisor, and the greatest common divisor , with the convention ).
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 implies and (Divisibility is reflexive and transitive on , and is linear: if and then for all integers ; also implies , and ).
If and then (If and then and ; hence the set of divisors of a nonzero integer is bounded above by ); means for some (Divisibility in : when for some integer ).
; exactly when ; when ; and is or (The absolute value of an integer, Absolute value in : ; exactly when ; ; ; ; and exactly when ).
A product of two nonzero integers is nonzero (The integers have no zero divisors; multiplicative cancellation).
Proof
If and then : for or the product is , and otherwise and , so .
Case : then , so the left side is ; and , so the right side is .
Case : then , so the left side is ; and , so the right side is .
Case and . Then , and one of is nonzero, say ; so by [L9] and hence and . Also , and by [L9].
In the case of step 1.4, is a common divisor of and . Indeed , say ; then , and is or by [L8], so or , and in either case . The same argument with gives .
Conversely, by [L5] fix with ; multiplying by gives . Since and , [L6] gives ; and is or , because is or , so as well.
Hence by [L4].
Both and are nonzero by step 1.4, and both are nonnegative, by [L3] and by step 1.1 and [L8]. From and , [L7] gives , that is ; from and , [L7] gives .
By antisymmetry in the case of step 1.4.
The three cases of steps 1.2, 1.3 and 1.4 exhaust the possibilities, since either , or , or neither; so for all .
Remarks
-
The boundary cases are the point, not an aside. The convention is the only value under which this identity extends to : it would read for every , and taking gives . That is a constraint on the choice, not a derivation from this lemma — steps 1.2 and 1.3 above read the boundary value off the convention rather than proving it. The choice is made where the convention is fixed (Common divisor, and the greatest common divisor , with the convention ) and instantiated on the companion page ( at the boundary: , , and the convention is exactly what makes true at ↗).
-
Why and not . is nonnegative by construction, so the right side must be too; with and the product is negative and could not be a greatest common divisor.
Depends on
- Common divisor, and the greatest common divisor $\gcd(a,b)$, with the convention $\gcd(0,0) := 0$
- 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
- 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
- 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$
- If $d \mid a$ and $a \ne 0$ then $d \ne 0$ and $|d| \le |a|$; hence the set of divisors of a nonzero integer is bounded above by $|a|$
- Divisibility in $\mathbb{Z}$: $d \mid a$ when $a = dq$ for some integer $q$
- The absolute value $|a|$ of an integer
- Absolute value in $\mathbb{Z}$: $|a| \ge 0$; $|a| = 0$ exactly when $a = 0$; $|-a| = |a|$; $|ab| = |a|\,|b|$; $-|a| \le a \le |a|$; and $|a| \le c$ exactly when $-c \le a \le c$
- The integers have no zero divisors; multiplicative cancellation
- The integers form a commutative ring
- Arithmetic on the integers
- The integers form a totally ordered ring
- Order on the integers
Used by
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 55 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
- Greatest common divisor (Wikipedia) (standard reference, not scraped)