TheoremStatement: 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.

Every common multiple of $a$ and $b$ is a multiple of $lcm (a, b)$ , and $\gcd (a, b) \cdot lcm (a, b) = ∣ a b ∣$

Statement

Let $a, b \in Z$ , and write $d = \gcd (a, b)$ (Common divisor, and the greatest common divisor $\gcd (a, b)$ , with the convention $\gcd (0, 0) : = 0$ ) and $ℓ = lcm (a, b)$ (Common multiple, and the least common multiple $lcm (a, b)$ , taken to be $0$ when $a = 0$ or $b = 0$ ). Then:

every common multiple of $a$ and $b$ is a multiple of $ℓ$ , that is, $ℓ ∣ m$ whenever $a ∣ m$ and $b ∣ m$ ;
$d \cdot ℓ = ∣ a b ∣$ .

Both hold for every pair, including the pairs with $a = 0$ or $b = 0$ , where the two sides of clause 2 are $0$ .

Facts & Assumptions

Given: Integers $a$ and $b$ , $d : = \gcd (a, b)$ and $ℓ : = lcm (a, b)$ .

[L1]

$Z$ is a commutative ring: addition and multiplication are associative and commutative, $x \cdot 1 = x$ , $x \cdot 0 = 0$ , $x \cdot (- 1) = - x$ , multiplication distributes over addition, and every $x$ has an additive inverse, with $- (- x) = x$ (The integers form a commutative ring, Arithmetic on the integers).

[L2]

The order on $Z$ is total, antisymmetric and transitive; $x < y$ means $x \leq y$ together with $x \neq y$ (The integers form a totally ordered ring, Order on the integers).

[L3]

For $a, b$ both nonzero, $ℓ$ is the least positive common multiple of $a$ and $b$ ; if $a = 0$ or $b = 0$ then the only common multiple is $0$ and $ℓ = 0$ (Common multiple, and the least common multiple $lcm (a, b)$ , taken to be $0$ when $a = 0$ or $b = 0$ ).

[L4]

$d \geq 1$ when $(a, b) \neq (0, 0)$ , $\gcd (0, 0) = 0$ , and $d$ is a common divisor of $a$ and $b$ (Common divisor, and the greatest common divisor $\gcd (a, b)$ , with the convention $\gcd (0, 0) : = 0$ ).

[L5]

If $d \neq 0$ then $a = d a^{'}$ and $b = d b^{'}$ for unique integers $a^{'} = a / d$ , $b^{'} = b / d$ , and $\gcd (a^{'}, b^{'}) = 1$ (If $d = \gcd (a, b)$ is nonzero then $a / d$ and $b / d$ are coprime).

[L6]

$\gcd (u, v) = \gcd (v, u)$ ( $\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) \geq 1$ unless $a = b = 0$ ).

[L7]

If $\gcd (u, v) = 1$ and $u ∣ v w$ then $u ∣ w$ (If $\gcd (a, b) = 1$ and $a ∣ b c$ then $a ∣ c$ ; and if $a ∣ c$ , $b ∣ c$ and $\gcd (a, b) = 1$ then $a b ∣ c$ ).

[L8]

Divisibility is reflexive and transitive; $u ∣ v$ implies $u ∣ v w$ , $- u ∣ v$ and $u ∣ - v$ ; and $d ∣ u$ means $u = d q$ for some $q$ (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$ , Divisibility in $Z$ : $d ∣ a$ when $a = d q$ for some integer $q$ ).

[L9]

If $u ∣ v$ and $v \neq 0$ then $∣ u ∣ \leq ∣ v ∣$ (If $d ∣ a$ and $a \neq 0$ then $d \neq 0$ and $∣ d ∣ \leq ∣ a ∣$ ; hence the set of divisors of a nonzero integer is bounded above by $∣ a ∣$ ).

[L10]

$∣ x ∣ \geq 0$ ; $∣ x ∣ = 0$ exactly when $x = 0$ ; $∣ x ∣ = x$ when $x \geq 0$ ; $∣ x y ∣ = ∣ x ∣ ∣ y ∣$ ; and $x$ is $∣ x ∣$ or $- ∣ x ∣$ (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$ ).

[L11]

A product of two nonzero integers is nonzero, and $x z = y z$ with $z \neq 0$ gives $x = y$ (The integers have no zero divisors; multiplicative cancellation).

Proof

technique · cases

1.1

Case $a = 0$ or $b = 0$ . Then $ℓ = 0$ and the only common multiple of $a$ and $b$ is $0$ , so clause 1 reads $0 ∣ 0$ , which holds. And $a b = 0$ , so $∣ a b ∣ = 0 = d \cdot 0 = d ℓ$ : clause 2 holds.

assume-case degenerateL1L3L8L10

1.2

Case $a \neq 0$ and $b \neq 0$ . Then $(a, b) \neq (0, 0)$ , so $d \geq 1$ ; in particular $d \neq 0$ and $d \geq 0$ , so $∣ d ∣ = d$ . Fix $a^{'}, b^{'}$ with $a = d a^{'}$ , $b = d b^{'}$ and $\gcd (a^{'}, b^{'}) = 1$ .

assume-case genericL2L4L5L10

2.1

In the case of step 1.2 put $M : = d ∣ a^{'} b^{'} ∣$ . Both $a^{'}$ and $b^{'}$ are nonzero, since $a = d a^{'} \neq 0$ and $b = d b^{'} \neq 0$ ; hence $a^{'} b^{'} \neq 0$ , so $∣ a^{'} b^{'} ∣ \geq 0$ and $∣ a^{'} b^{'} ∣ \neq 0$ , and $M \neq 0$ .

step 1.2L1L10L11

3.1

$M$ is a common multiple of $a$ and $b$ . Indeed $d a^{'} b^{'} = (d a^{'}) b^{'} = a b^{'}$ and $d a^{'} b^{'} = (d b^{'}) a^{'} = b a^{'}$ , so $a ∣ d a^{'} b^{'}$ and $b ∣ d a^{'} b^{'}$ ; and $M = d ∣ a^{'} b^{'} ∣$ equals $d a^{'} b^{'}$ or $- (d a^{'} b^{'})$ , since $∣ a^{'} b^{'} ∣$ is $a^{'} b^{'}$ or $- (a^{'} b^{'})$ . So $a ∣ M$ and $b ∣ M$ .

step 1.2step 2.1L1L8L10

3.2

$M > 0$ : $d \geq 1 > 0$ and $∣ a^{'} b^{'} ∣ \geq 0$ with $∣ a^{'} b^{'} ∣ \neq 0$ , so $∣ a^{'} b^{'} ∣ > 0$ and the product of two positives is positive.

step 1.2step 2.1L2L10

3.3

Every common multiple $m$ of $a$ and $b$ is a multiple of $M$ . Write $m = a s = d a^{'} s$ . From $b ∣ m$ , that is $d b^{'} ∣ d a^{'} s$ , we get $d a^{'} s = d b^{'} t$ for some $t$ , and cancelling $d \neq 0$ gives $a^{'} s = b^{'} t$ , so $b^{'} ∣ a^{'} s$ . Since $\gcd (b^{'}, a^{'}) = \gcd (a^{'}, b^{'}) = 1$ , [L7] gives $b^{'} ∣ s$ , say $s = b^{'} u$ ; then $m = d a^{'} b^{'} u$ , so $d a^{'} b^{'} ∣ m$ and hence $M ∣ m$ , because $M$ is $d a^{'} b^{'}$ or $- (d a^{'} b^{'})$ .

step 1.2step 2.1L1L6L7L8L10L11

4.1

$M = ℓ$ . By steps 3.1 and 3.2, $M$ is a positive common multiple. If $p$ is any positive common multiple, then $M ∣ p$ by step 3.3 and $p \neq 0$ , so $∣ M ∣ \leq ∣ p ∣$ by [L9], that is $M \leq p$ since both are positive. So $M$ is the least positive common multiple, which is $ℓ$ .

step 3.1step 3.2step 3.3L3L9L10

5.1

Clause 1 in this case now follows from step 3.3, since $ℓ = M$ .

step 3.3step 4.1

5.2

Clause 2 in this case: $d ℓ = d \cdot d ∣ a^{'} b^{'} ∣ = ∣ d ∣ ∣ d ∣ ∣ a^{'} ∣ ∣ b^{'} ∣ = ∣ d a^{'} ∣ ∣ d b^{'} ∣ = ∣ (d a^{'}) (d b^{'}) ∣ = ∣ a b ∣$ , using $∣ d ∣ = d$ and multiplicativity of the absolute value throughout.

step 1.2step 4.1L1L10

6.1

The two cases of steps 1.1 and 1.2 are exhaustive, so clauses 1 and 2 hold for every pair $a, b$ .

step 1.1step 5.1step 5.2cases-exhaustive∎

Remarks

Clause 1 is the clause later pages use. "Least positive common multiple" is how $lcm$ was defined, but the useful property is that it divides every common multiple, which is what identifies $a Z \cap b Z$ with $lcm (a, b) Z$ in $a Z + b Z = \gcd (a, b) Z$ and $a Z \cap b Z = lcm (a, b) Z$ ; equivalently, in $(Z, +)$ the subgroup generated by ${a, b}$ is $⟨ \gcd (a, b) ⟩$ and $⟨ a ⟩ \cap ⟨ b ⟩ = ⟨ lcm (a, b) ⟩$ .
The absolute value in clause 2 is not decorative. The unsigned form $\gcd (a, b) lcm (a, b) = a b$ is false, and $(- 2, 3)$ refutes it: the companion page records this as FALSE: For all integers $a$ and $b$ , $\gcd (a, b) \cdot lcm (a, b) = a b$ ↗.
Where coprimality enters. The only substantial step is step 3.3, which proves that every common multiple is a multiple of $M$ ; what it uses is that $a / d$ and $b / d$ are coprime (If $d = \gcd (a, b)$ is nonzero then $a / d$ and $b / d$ are coprime) together with the coprime divisibility lemma (If $\gcd (a, b) = 1$ and $a ∣ b c$ then $a ∣ c$ ; and if $a ∣ c$ , $b ∣ c$ and $\gcd (a, b) = 1$ then $a b ∣ c$ ). Without those the argument gives only that $M$ is a common multiple, not the least one.

Depends on

Used by

Dependency tree · two levels

41 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

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

Every common multiple of aa and bb is a multiple of lcm⁡(a,b)lcm(a,b), and gcd⁡(a,b)⋅lcm⁡(a,b)=∣ab∣gcd(a,b)⋅lcm(a,b)=∣ab∣