ExampleConstruction: AI-adaptedVerification: 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.

$12\mathbb{Z} + 18\mathbb{Z} = 6\mathbb{Z}$ and $12\mathbb{Z} \cap 18\mathbb{Z} = 36\mathbb{Z}$ , the arithmetic of $\gcd$ and $\operatorname{lcm}$ read off the subgroups of $(\mathbb{Z},+)$

Example

Take $a = 12$ and $b = 18$ . Then $\gcd(12,18) = 6$ and $\operatorname{lcm}(12,18) = 36$ , and $a\mathbb{Z} + b\mathbb{Z} = \gcd(a,b)\,\mathbb{Z}$ and $a\mathbb{Z} \cap b\mathbb{Z} = \operatorname{lcm}(a,b)\,\mathbb{Z}$ ; equivalently, in $(\mathbb{Z},+)$ the subgroup generated by $\{a,b\}$ is $\langle \gcd(a,b) \rangle$ and $\langle a \rangle \cap \langle b \rangle = \langle \operatorname{lcm}(a,b) \rangle$ turns these two numbers into two statements about subgroups of $(\mathbb{Z},+)$ :

$12\mathbb{Z} + 18\mathbb{Z} \;=\; 6\mathbb{Z}, \qquad 12\mathbb{Z} \cap 18\mathbb{Z} \;=\; 36\mathbb{Z} .$

The first says that the integers expressible as $12x + 18y$ are exactly the multiples of $6$ ; the smallest positive one is $6 = 12 \cdot (-1) + 18 \cdot 1$ . The second says that the integers divisible by both $12$ and $18$ are exactly the multiples of $36$ . The product check is $\gcd \cdot \operatorname{lcm} = 6 \cdot 36 = 216 = |12 \cdot 18|$ .

Numerals. For $k \in \mathbb{N}$ the symbol $k$ inside $\mathbb{Z}$ means $\iota(k)$ , the embedding of The naturals embed in the integers.

Facts & Assumptions

Given: The integers $12$ , $18$ , $6$ , $36$ and $216$ , and $g\mathbb{Z} = \{\, gk : k \in \mathbb{Z} \,\}$ .

[L1]

$\mathbb{Z}$ is a commutative ring: multiplication is associative and commutative, $x \cdot 1 = x$ , $x \cdot (-1) = -x$ , and multiplication distributes over addition (The integers form a commutative ring, Arithmetic on the integers, The integers as equivalence classes of pairs of naturals).

[L2]

$d = \gcd(u,v)$ exactly when $d \ge 0$ , $d \mid u$ , $d \mid v$ and every common divisor of $u$ and $v$ divides $d$ (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, Common divisor, and the greatest common divisor $\gcd(a,b)$ , with the convention $\gcd(0,0) := 0$ ).

[L3]

If $d \mid u$ and $d \mid v$ then $d \mid ux + vy$ for all $x, y$ (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$ ); $d \mid u$ means $u = dq$ for some $q$ (Divisibility in $\mathbb{Z}$ : $d \mid a$ when $a = dq$ for some integer $q$ ).

[L4]

$\gcd(u,v)\operatorname{lcm}(u,v) = |uv|$ , and every common multiple of $u$ and $v$ is a multiple of $\operatorname{lcm}(u,v)$ (Every common multiple of $a$ and $b$ is a multiple of $\operatorname{lcm}(a,b)$ , and $\gcd(a,b) \cdot \operatorname{lcm}(a,b) = |ab|$ , Common multiple, and the least common multiple $\operatorname{lcm}(a,b)$ , taken to be $0$ when $a = 0$ or $b = 0$ ).

[L5]

$|x| = x$ for $x \ge 0$ , and $|xy| = |x|\,|y|$ (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]

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

[L7]

$a\mathbb{Z} + b\mathbb{Z} = \gcd(a,b)\mathbb{Z}$ and $a\mathbb{Z} \cap b\mathbb{Z} = \operatorname{lcm}(a,b)\mathbb{Z}$ , and these are subgroups of $(\mathbb{Z},+)$ ( $a\mathbb{Z} + b\mathbb{Z} = \gcd(a,b)\,\mathbb{Z}$ and $a\mathbb{Z} \cap b\mathbb{Z} = \operatorname{lcm}(a,b)\,\mathbb{Z}$ ; equivalently, in $(\mathbb{Z},+)$ the subgroup generated by $\{a,b\}$ is $\langle \gcd(a,b) \rangle$ and $\langle a \rangle \cap \langle b \rangle = \langle \operatorname{lcm}(a,b) \rangle$ , Subgroup, Group and abelian group, The subgroup $\langle S \rangle$ generated by a subset, the cyclic subgroup $\langle g \rangle$ , and cyclic groups).

[L8]

Every subgroup of $(\mathbb{Z},+)$ has exactly one nonnegative generator (Every subgroup of $(\mathbb{Z}, +)$ is $\langle n \rangle = n\mathbb{Z}$ for exactly one natural number $n$ ).

Verification

technique · direct

1.1

$\gcd(12,18) = 6$ . Indeed $6 \ge 0$ ; $12 = 6 \cdot 2$ and $18 = 6 \cdot 3$ , so $6 \mid 12$ and $6 \mid 18$ ; and $12 \cdot (-1) + 18 \cdot 1 = -12 + 18 = 6$ , so every common divisor of $12$ and $18$ divides $6$ by [L3]. By [L2] this characterises $\gcd(12,18)$ .

L1L2L3algebra

2.1

$\operatorname{lcm}(12,18) = 36$ . By [L4], $\gcd(12,18)\operatorname{lcm}(12,18) = |12 \cdot 18| = |216| = 216$ ; with step 1.1 this reads $6 \cdot \operatorname{lcm}(12,18) = 216$ . Since $6 \cdot 36 = 216$ and $6 \ne 0$ , cancellation gives $\operatorname{lcm}(12,18) = 36$ .

step 1.1L1L4L5L6algebra

3.1

Applying [L7] with $a = 12$ and $b = 18$ : $12\mathbb{Z} + 18\mathbb{Z} = \gcd(12,18)\mathbb{Z} = 6\mathbb{Z}$ and $12\mathbb{Z} \cap 18\mathbb{Z} = \operatorname{lcm}(12,18)\mathbb{Z} = 36\mathbb{Z}$ .

step 1.1step 2.1L7

4.1

Both right-hand sides are written with their canonical generator: $6 \ge 0$ and $36 \ge 0$ , and by [L8] no other nonnegative integer generates the same subgroup, so the two identities pin the subgroups down rather than merely exhibiting one description of each.

step 3.1L8

5.1

The two statements read concretely: an integer is of the form $12x + 18y$ exactly when it is a multiple of $6$ — with $6 = 12 \cdot (-1) + 18 \cdot 1$ the smallest positive such value — and an integer is divisible by both $12$ and $18$ exactly when it is a multiple of $36$ , which is the divisibility clause of [L4] instantiated here.

step 1.1step 3.1L3L4∎

Remarks

The example is the seam in miniature. On the left of each identity is a construction in the group $(\mathbb{Z},+)$ — a sum of subgroups, an intersection of subgroups — and on the right is a number computed by arithmetic. $a\mathbb{Z} + b\mathbb{Z} = \gcd(a,b)\,\mathbb{Z}$ and $a\mathbb{Z} \cap b\mathbb{Z} = \operatorname{lcm}(a,b)\,\mathbb{Z}$ ; equivalently, in $(\mathbb{Z},+)$ the subgroup generated by $\{a,b\}$ is $\langle \gcd(a,b) \rangle$ and $\langle a \rangle \cap \langle b \rangle = \langle \operatorname{lcm}(a,b) \rangle$ is what makes the two sides the same object.
$36 = 12 \cdot 3 = 18 \cdot 2$ , so $36$ is visibly a common multiple; what is not visible without the theorem is that every common multiple is a multiple of it, which is why $12\mathbb{Z} \cap 18\mathbb{Z}$ is exactly $36\mathbb{Z}$ and not merely contains it.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

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

Cyclic group (Wikipedia) (standard reference, not scraped)
Bézout's identity (Wikipedia) (standard reference, not scraped)
Least common multiple (Wikipedia) (standard reference, not scraped)

12Z+18Z=6Z12\mathbb{Z} + 18\mathbb{Z} = 6\mathbb{Z}12Z+18Z=6Z and 12Z∩18Z=36Z12\mathbb{Z} \cap 18\mathbb{Z} = 36\mathbb{Z}12Z∩18Z=36Z, the arithmetic of gcd⁡\gcdgcd and lcm⁡\operatorname{lcm}lcm read off the subgroups of (Z,+)(\mathbb{Z},+)(Z,+)