CorollaryStatement: AI-adaptedProof: AI-adaptedprecheck 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 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 \neq 0$ , equivalently $(a, b) \neq (0, 0)$ . Since $d ∣ a$ and $d ∣ b$ , there are unique integers, written $a / d$ and $b / d$ , with

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

uniqueness holding because $d \neq 0$ and $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) \neq (0, 0)$ , and $d : = \gcd (a, b)$ .

[L1]

$\gcd (u, v) \geq 1$ when $(u, v) \neq (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 (c u, c v) = ∣ c ∣ \gcd (u, v)$ for all $c, u, v$ ( $\gcd (c a, c b) = ∣ 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 $x z = y z$ and $z \neq 0$ then $x = y$ (The integers have no zero divisors; multiplicative cancellation).

[L4]

$d ∣ u$ means $u = d q$ for some $q$ (Divisibility in $Z$ : $d ∣ a$ when $a = d q$ for some integer $q$ ).

[L5]

$∣ 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$ ).

[L6]

$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) \neq (0, 0)$ we have $d \geq 1$ , so $d \neq 0$ and $d \geq 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 \neq 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 \neq 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 \neq 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 $Z$ throughout.

Depends on

Used by

Dependency tree · two levels

35 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)

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