CorollaryStatement: AI-adaptedProof: AI-adaptedSession-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.

If $d = \gcd(a,b)$ is nonzero then $a/d$ and $b/d$ are coprime

Statement

Let $a, b \in \mathbb{Z}$ and put $d := \gcd(a,b)$ (Common divisor, and the greatest common divisor $\gcd(a,b)$ , with the convention $\gcd(0,0) := 0$ ), and suppose $d \ne 0$ , equivalently $(a,b) \ne (0,0)$ . Since $d \mid a$ and $d \mid b$ , there are unique integers, written $a/d$ and $b/d$ , with

$a \;=\; d \cdot (a/d), \qquad b \;=\; d \cdot (b/d) ,$

uniqueness holding because $d \ne 0$ and $\mathbb{Z}$ has cancellation (The integers have no zero divisors; multiplicative cancellation). Then

$\gcd(a/d,\; b/d) \;=\; 1 ,$

that is, $a/d$ and $b/d$ are coprime (Coprime integers: $\gcd(a,b) = 1$ ).

Facts & Assumptions

Given: Integers $a, b$ with $(a,b) \ne (0,0)$ , and $d := \gcd(a,b)$ .

[L1]

$\gcd(u,v) \ge 1$ when $(u,v) \ne (0,0)$ , $\gcd(0,0) = 0$ , and $\gcd(u,v)$ is a common divisor of $u$ and $v$ (Common divisor, and the greatest common divisor $\gcd(a,b)$ , with the convention $\gcd(0,0) := 0$ ).

[L2]

$\gcd(cu, cv) = |c| \gcd(u,v)$ for all $c, u, v$ ( $\gcd(ca, cb) = |c|\,\gcd(a,b)$ for all integers $a, b, c$ , the identity holding at $c = 0$ and at $(a,b) = (0,0)$ as well).

[L3]

If $xz = yz$ and $z \ne 0$ then $x = y$ (The integers have no zero divisors; multiplicative cancellation).

[L4]

$d \mid u$ means $u = dq$ for some $q$ (Divisibility in $\mathbb{Z}$ : $d \mid a$ when $a = dq$ for some integer $q$ ).

[L5]

$|x| = x$ when $x \ge 0$ (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$ ).

[L6]

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

[L7]

$u$ and $v$ are coprime exactly when $\gcd(u,v) = 1$ (Coprime integers: $\gcd(a,b) = 1$ ).

Proof

technique · direct

1.1

Since $(a,b) \ne (0,0)$ we have $d \ge 1$ , so $d \ne 0$ and $d \ge 0$ , whence $|d| = d$ .

L1L5L6

2.1

$d$ is a common divisor of $a$ and $b$ , so there are integers $a'$ and $b'$ with $a = d a'$ and $b = d b'$ ; each is unique, since $d a' = d a''$ with $d \ne 0$ gives $a' = a''$ by cancellation. Write $a' = a/d$ and $b' = b/d$ .

step 1.1L1L3L4L6

3.1

By [L2] applied with $c = d$ , $u = a'$ and $v = b'$ : $d = \gcd(a,b) = \gcd(d a', d b') = |d| \gcd(a',b') = d\,\gcd(a',b')$ .

step 1.1step 2.1L2

4.1

Also $d = d \cdot 1$ , so $d \cdot \gcd(a',b') = d \cdot 1$ with $d \ne 0$ , and cancellation gives $\gcd(a',b') = 1$ : the integers $a/d$ and $b/d$ are coprime.

step 1.1step 3.1L3L6L7∎

Remarks

The hypothesis $d \ne 0$ is not a restriction in disguise. It fails only at $(a,b) = (0,0)$ , where $a/d$ and $b/d$ are not defined at all, since division by $0$ determines nothing.
This is the standard "reduce a fraction to lowest terms" statement, proved without any fractions: $a/d$ is defined as the unique integer solving $a = d \cdot x$ , and lives in $\mathbb{Z}$ throughout.

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 56 results over 19 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)

If d=gcd⁡(a,b)d = \gcd(a,b)d=gcd(a,b) is nonzero then a/da/da/d and b/db/db/d are coprime