LemmaStatement: AI-adaptedProof: AI-generatedSession-authored (Fable 5 assisted)precheck 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.

$\gcd$ is symmetric and unchanged by signs: $\gcd(a,b) = \gcd(b,a) = \gcd(|a|,|b|)$ ; moreover $\gcd(a,0) = |a|$ , $\gcd(a,1) = 1$ , $\gcd(a,a) = |a|$ , and $\gcd(a,b) \ge 1$ unless $a = b = 0$

Statement

For all $a, b \in \mathbb{Z}$ , with $\gcd$ as in Common divisor, and the greatest common divisor $\gcd(a,b)$ , with the convention $\gcd(0,0) := 0$ :

$\gcd(a,b) = \gcd(b,a)$ ;
$\gcd(a,b) = \gcd(|a|,|b|)$ ;
$\gcd(a,0) = |a|$ , and in particular $\gcd(0,0) = 0$ ;
$\gcd(a,1) = 1$ ;
$\gcd(a,a) = |a|$ ;
$\gcd(a,b) \ge 1$ unless $a = b = 0$ , in which case $\gcd(a,b) = 0$ .

Facts & Assumptions

Given: Integers $a$ and $b$ , and the set $D(a,b) = \{\, d : d \mid a \text{ and } d \mid b \,\}$ of common divisors (Common divisor, and the greatest common divisor $\gcd(a,b)$ , with the convention $\gcd(0,0) := 0$ ).

[L1]

For $(a,b) \ne (0,0)$ , $\gcd(a,b)$ is the unique greatest element of $D(a,b)$ and satisfies $\gcd(a,b) \ge 1$ ; and $\gcd(0,0) = 0$ by convention (Common divisor, and the greatest common divisor $\gcd(a,b)$ , with the convention $\gcd(0,0) := 0$ ).

[L2]

$d \mid a$ means $a = dq$ for some $q$ ; every $d$ satisfies $d \mid 0$ ; $0 \mid a$ only for $a = 0$ ; and $1 \mid a$ , $a \mid a$ for every $a$ (Divisibility in $\mathbb{Z}$ : $d \mid a$ when $a = dq$ for some integer $q$ ).

[L3]

$d \mid a$ , $d \mid -a$ , $-d \mid a$ and $-d \mid -a$ are equivalent (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$ ).

[L4]

If $d \mid a$ and $a \ne 0$ then $d \le |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|$ ).

[L5]

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

[L6]

$|x| = x$ when $x \ge 0$ and $|x| = -x$ when $x \le 0$ (The absolute value $|a|$ of an integer); $|x| \ge 0$ and $|x| = 0$ exactly when $x = 0$ (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$ ).

[L7]

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

Proof

technique · direct

1.1

$1 \ne 0$ and $-1 \le 0 \le 1$ . If $1 = 0$ then $-1 = -0 = 0 = 1$ , contradicting $1 \ne -1$ . By totality $0 \le 1$ or $1 \le 0$ ; in the second case adding $-1$ gives $0 \le -1$ , and $-1 \ne 0$ , so $0 < -1$ and hence $0 < (-1)(-1) = 1$ , contradicting $1 \le 0$ by antisymmetry. So $0 \le 1$ , and adding $-1$ gives $-1 \le 0$ .

L5L7

1.2

$|x| \mid x$ for every $x$ : by totality $x \ge 0$ , when $x = |x| = |x| \cdot 1$ , or $x \le 0$ , when $|x| = -x$ and so $x = -(-x) = -|x| = |x| \cdot (-1)$ .

L6L7

1.3

For every $d$ and $x$ : $d \mid x$ if and only if $d \mid |x|$ , because $|x|$ is $x$ or $-x$ and the two conditions $d \mid x$ , $d \mid -x$ are equivalent.

L3L6

1.4

Claim 1. The condition defining $D(a,b)$ is unchanged when $a$ and $b$ are interchanged, so $D(a,b) = D(b,a)$ ; and $(a,b) = (0,0)$ exactly when $(b,a) = (0,0)$ . Hence the two greatest elements coincide in the first case, and both values are $0$ in the second.

1.5

Claim 5. $D(a,a) = \{\, d : d \mid a \,\} = D(a,0)$ , and $(a,a) = (0,0)$ exactly when $(a,0) = (0,0)$ , so $\gcd(a,a) = \gcd(a,0)$ .

L1L2

1.6

Claim 6 is [L1] restated: for $(a,b) \ne (0,0)$ the value $\gcd(a,b)$ is $\ge 1$ because $1$ is a common divisor and $\gcd(a,b)$ is greatest, and at $(0,0)$ the value is $0$ by convention.

L1L2

2.1

Claim 2. By step 1.3, $D(a,b) = D(|a|,|b|)$ ; and $|a| = 0$ exactly when $a = 0$ , so $(a,b) = (0,0)$ exactly when $(|a|,|b|) = (0,0)$ . Hence the values agree in both cases.

step 1.3L1L6

2.2

Claim 3. $D(a,0) = \{\, d : d \mid a \,\}$ , since every $d$ divides $0$ . If $a = 0$ this is $\mathbb{Z}$ and $\gcd(0,0) = 0 = |0|$ by the convention. If $a \ne 0$ , then $|a| \in D(a,0)$ by step 1.2, and every $d \in D(a,0)$ satisfies $d \le |a|$ by [L4], so $|a|$ is the greatest element of $D(a,0)$ and $\gcd(a,0) = |a|$ .

step 1.2L1L2L4L6

2.3

Claim 4. Every $d \in D(a,1)$ satisfies $d \mid 1$ , hence $d = 1$ or $d = -1$ ; and $1 \in D(a,1)$ since $1 \mid a$ and $1 \mid 1$ . Also $(a,1) \ne (0,0)$ because $1 \ne 0$ . Since $-1 \le 1$ by step 1.1, the greatest element of $D(a,1)$ is $1$ , so $\gcd(a,1) = 1$ .

step 1.1L1L2L5L7

3.1

Claim 3's second half and claim 5 now read off: $\gcd(0,0) = 0 = |0|$ , and $\gcd(a,a) = \gcd(a,0) = |a|$ .

step 2.2step 1.5

4.1

Claims 1 to 6 are established.

step 1.4step 2.1step 2.2step 2.3step 3.1step 1.6∎

Remarks

Claim 2 is what lets every later argument assume the arguments are nonnegative, and claim 1 lets it assume they are in either order. Both are used without comment below.
Every clause is checked at the boundary. Claim 3 covers $a = 0$ , where it returns the convention $\gcd(0,0) = 0$ rather than contradicting it; claim 4 holds at $a = 0$ , giving $\gcd(0,1) = 1$ ; and claim 5 holds at $a = 0$ , giving $\gcd(0,0) = 0$ . There is no pair at which a clause above is silent.

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 58 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)