Alphabeta Math
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.

✓ 20 results · all verified · 16 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 4 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Divisibility, Greatest Common Divisors and Bézout's Identity

1 · Prerequisites

2 · Summary

Objective. This page opens the number theory track, and it is built entirely on Z as the library constructed it: the ordered commutative ring of The integers form a commutative ring and The integers form a totally ordered ring, with the embedding ι:N→Z of The naturals embed in the integers and the division algorithm Division with remainder in Z: for a∈Z and b>0 there are unique q,r∈Z with a=qb+r and 0≤r<b. What is developed here is the divisibility relation and everything that follows from Bézout's identity: greatest common divisors, the Euclidean algorithm and its extended form, coprime integers, least common multiples, and the identification of the subgroups of (Z,+) with the sets of multiples. Primes, Euclid's lemma and unique factorisation are not proved here; they belong to a later page, and no argument below assumes them.

Absolute value on Z, minted here. The library's other absolute value, Absolute value in an ordered field, is stated for an ordered field, and Z is not one, so it does not apply. The absolute value ∣a∣ of an integer therefore defines ∣a∣ for an integer directly, by the case split the total order of Z makes legitimate, and Absolute value in Z: ∣a∣≥0; ∣a∣=0 exactly when a=0; ∣−a∣=∣a∣; ∣ab∣=∣a∣ ∣b∣; −∣a∣≤a≤∣a∣; and ∣a∣≤c exactly when −c≤a≤c proves the six facts recorded here for later use: positivity, vanishing exactly at 0, invariance under negation, multiplicativity, the bound −∣a∣≤a≤∣a∣, and the characterisation of ∣a∣≤c by −c≤a≤c. The Remarks of The absolute value ∣a∣ of an integer record that this agrees with Absolute value in an ordered field along the embedding of Z in Q, and nothing on this page depends on that observation. The absolute value is load-bearing rather than convenient: Division with remainder in Z: for a∈Z and b>0 there are unique q,r∈Z with a=qb+r and 0≤r<b is stated for a positive divisor, so every use of it below first replaces a divisor b by ∣b∣.

Divisibility, which the library already had. Division with remainder in Z: for a∈Z and b>0 there are unique q,r∈Z with a=qb+r and 0≤r<b introduces the relation "b divides a" inside its own Statement, for use on its own page, and its Remarks leave the systematic theory to a later page, which "must record that its general divisibility in a ring restricts on Z to the relation defined here, rather than introduce a second notion silently". This is that page: Divisibility in Z: d∣a when a=dq for some integer q states the same relation, quotes the source, and adds the three boundary values that a page over a ring containing 0 has to state — d∣0 for every d including 0, 0∣a only for a=0, and 1∣a and a∣a always. It is a dictionary item, not new vocabulary. Division with remainder for any nonzero divisor: for a∈Z and b≠0 there are unique q,r∈Z with a=qb+r and 0≤r<∣b∣ then discharges the other promise made in those Remarks, extending division with remainder to every nonzero divisor with 0≤r<∣b∣, which is possible here precisely because the absolute value has just arrived.

The arithmetic of the relation. Divisibility is reflexive and transitive on Z, and is linear: if d∣a and d∣b then d∣ax+by for all integers x,y; also d∣a implies d∣ac, −d∣a and d∣−a proves that divisibility is reflexive, transitive and linear, the linearity clause being the step used by almost every later proof. If d∣a and a≠0 then d≠0 and ∣d∣≤∣a∣; hence the set of divisors of a nonzero integer is bounded above by ∣a∣ supplies the one place where divisibility constrains size — d∣a with a≠0 forces ∣d∣≤∣a∣ — and it is what makes the set of divisors of a nonzero integer bounded above. (Z,⋅,1) is a commutative monoid whose group of units is {1,−1}; equivalently u∣1 holds exactly for u=1 and u=−1 identifies the units: (Z,⋅,1) is a commutative monoid whose group of units is {1,−1}, obtained from the published The invertible elements of a monoid form a group under the restricted operation. Associates in Z: integers each of which divides the other and For integers a and b the following are equivalent: a∣b and b∣a; b=ua for a unit u; ∣a∣=∣b∣. Being associates is an equivalence relation whose class of a is {a,−a} then show that divisibility cannot distinguish a from −a and nothing more: mutual divisibility, differing by a unit and having equal absolute value are the same condition, and the classes are the pairs {a,−a}.

A greatest element, which well-ordering does not give. The definition of gcd⁡ needs a greatest element of a set of integers bounded above, whereas The well-ordering principle gives a least element of a set of naturals. A nonempty set of integers bounded above has a greatest element, and a nonempty set of integers bounded below has a least element bridges the two, by reflecting the set through an upper bound into N; it is general infrastructure, homed here because this is the first page that needs it.

Greatest common divisors, and the convention at (0,0). Common divisor, and the greatest common divisor gcd⁡(a,b), with the convention gcd⁡(0,0):=0 defines gcd⁡(a,b) as the greatest common divisor, discharging in the definition itself the obligation that one exists: the common divisors are nonempty because 1 divides everything and bounded above by If d∣a and a≠0 then d≠0 and ∣d∣≤∣a∣; hence the set of divisors of a nonzero integer is bounded above by ∣a∣, so A nonempty set of integers bounded above has a greatest element, and a nonempty set of integers bounded below has a least element applies. At (0,0) there is no greatest element at all, and the value is fixed by the convention gcd⁡(0,0)=0, argued where it is made rather than in a footnote: 0 is greatest in the divisibility ordering, and it is the only value under which gcd⁡(ca,cb)=∣c∣gcd⁡(a,b) holds at c=0. The companion page carries the witness that makes the convention necessary rather than decorative. 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)≥1 unless a=b=0 then records symmetry, invariance under signs, and the values at (a,0), (a,1) and (a,a), each checked at 0.

Bézout's identity and its corollary. Bézout's identity: for integers a,b not both zero, gcd⁡(a,b) is the least positive element of { ax+by:x,y∈Z }; in particular ax+by=gcd⁡(a,b) has an integer solution proves that for a,b not both zero the least positive element of {ax+by} is gcd⁡(a,b), by well-ordering and the division algorithm; the last step, that every common divisor is below the gcd and not merely divides it, is where If d∣a and a≠0 then d≠0 and ∣d∣≤∣a∣; hence the set of divisors of a nonzero integer is bounded above by ∣a∣ is needed. Every common divisor of a and b divides gcd⁡(a,b); consequently d=gcd⁡(a,b) exactly when d≥0, d∣a, d∣b, and every common divisor of a and b divides d — a characterisation that holds at (a,b)=(0,0) as well converts the definition into the form later pages should cite: d=gcd⁡(a,b) exactly when d≥0, d is a common divisor, and every common divisor divides d — a characterisation that, unlike the maximum, holds at (0,0) too.

The algorithm. If a=qb+r then a,b and b,r have exactly the same common divisors, so gcd⁡(a,b)=gcd⁡(b,r) is the whole content of the Euclidean algorithm: a=qb+r makes a,b and b,r have literally the same common divisors, with no inequality on r assumed. The Euclidean algorithm: for a∈Z and b>0 the remainder descent from (a,b) terminates, and the last nonzero remainder is gcd⁡(a,b) turns that into a terminating procedure, defining the remainder descent by The recursion theorem rather than by an informal "iterate", proving termination from the 0≤r<b clause of the division algorithm, and identifying the last nonzero remainder as the gcd. The extended Euclidean algorithm: the same descent produces integers x,y with ax+by=gcd⁡(a,b), so Bézout coefficients are computed and not merely shown to exist runs the same recursion carrying two coefficient pairs alongside the remainders, so that Bézout coefficients are computed rather than merely shown to exist.

Coprimality. Coprime integers: gcd⁡(a,b)=1 is gcd⁡(a,b)=1, with its three boundary pairs stated; a and b are coprime if and only if ax+by=1 for some integers x,y; and in that case the only common divisors of a and b are 1 and −1 gives the usable form, solvability of ax+by=1; and If gcd⁡(a,b)=1 and a∣bc then a∣c; and if a∣c, b∣c and gcd⁡(a,b)=1 then ab∣c is the lemma that carries the weight, that gcd⁡(a,b)=1 and a∣bc force a∣c. It is proved here, from Bézout and with no primality whatever, because primality is only a way of guaranteeing the coprimality it actually uses. 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 and If d=gcd⁡(a,b) is nonzero then a/d and b/d are coprime complete the arithmetic: gcd⁡(ca,cb)=∣c∣gcd⁡(a,b) at every triple, and a/d, b/d are coprime when d=gcd⁡(a,b) is nonzero.

Least common multiples. Common multiple, and the least common multiple lcm⁡(a,b), taken to be 0 when a=0 or b=0 defines lcm⁡(a,b) as the least positive common multiple when both arguments are nonzero, and as 0 otherwise — where 0 is not a free choice but the only common multiple there is. Every common multiple of a and b is a multiple of lcm⁡(a,b), and gcd⁡(a,b)⋅lcm⁡(a,b)=∣ab∣ proves the two facts that matter: every common multiple is a multiple of the lcm, and gcd⁡(a,b)lcm⁡(a,b)=∣ab∣. The absolute value is not decorative, and the companion page refutes the version without it.

The seam with the group theory. Every subgroup of (Z,+) is ⟨n⟩=nZ for exactly one natural number n classifies the subgroups of (Z,+): each is nZ=⟨n⟩ for exactly one natural n. The published example on the examples companion of Binary Operations, Monoids, Groups and Subgroups gives that classification for some such n, but examples pages are leaves in this library's reading order, so nothing here may rest on it — which is why that companion is deliberately absent from the Prerequisites above, while the spine page it accompanies is present. The classification is therefore re-proved here on a spine where later pages can cite it, and re-proved in the stronger form the uses need: its Remarks set out exactly how the two statements differ. aZ+bZ=gcd⁡(a,b) Z and aZ∩bZ=lcm⁡(a,b) Z; equivalently, in (Z,+) the subgroup generated by {a,b} is ⟨gcd⁡(a,b)⟩ and ⟨a⟩∩⟨b⟩=⟨lcm⁡(a,b)⟩ is then the item that joins the two halves of the page: aZ+bZ=gcd⁡(a,b)Z and aZ∩bZ=lcm⁡(a,b)Z. Both inclusions come from Bézout and divisibility alone; the classification is used for exactly one thing, the uniqueness of the nonnegative generator, which is what lets these be read as identifications of subgroups rather than coincidences between sets.

What is deliberately absent. No primes, no Euclid's lemma for a prime divisor, no unique factorisation: those rest on this page and are developed after it. No greatest common divisor of a list longer than a pair, since nothing here needs one. No bound on the number of divisions the Euclidean algorithm performs — the companion page computes the count for one family and proves no worst-case theorem. Twenty-six items make up this page: six definitions, twelve lemmas, four theorems and four corollaries, ten of them marked as landmarks in the flowchart above.

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (z-ai/glm-5.2)audited 2026-07-28Open item page →

The absolute value ∣a∣ of an integer

Definition

Let a∈Z (The integers as equivalence classes of pairs of naturals). The absolute value of a is

∣a∣  :=  {aif a≥0,−aif a<0,

where ≤ is the order of Order on the integers and −a is the additive inverse supplied by The integers form a commutative ring for the operations of Arithmetic on the integers.

Why the two clauses define a function. The order on Z is total and antisymmetric (The integers form a totally ordered ring), so for each a exactly one of a≥0 and a<0 holds: totality gives at least one of 0≤a and a≤0, and if both hold then a=0 by antisymmetry, in which case a≥0 and a<0 fails, since a<0 means a≤0 together with a≠0. The two clauses therefore never both apply and never both fail, and −a is a single element of Z because additive inverses are unique in a commutative ring: if a+u=0 and a+v=0 then u=u+0=u+(a+v)=(u+a)+v=0+v=v.

At the boundary, ∣0∣=0 by the first clause, and the second clause also gives −a whenever a≤0: for a<0 that is the definition, and for a=0 both readings give 0.

Remarks

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-28Open item page →

Absolute value in Z: ∣a∣≥0; ∣a∣=0 exactly when a=0; ∣−a∣=∣a∣; ∣ab∣=∣a∣ ∣b∣; −∣a∣≤a≤∣a∣; and ∣a∣≤c exactly when −c≤a≤c

Statement

Let a,b,c∈Z and let ∣⋅∣ be as in The absolute value ∣a∣ of an integer. Then

  1. ∣a∣≥0;
  2. ∣a∣=0 if and only if a=0;
  3. ∣−a∣=∣a∣;
  4. ∣ab∣=∣a∣ ∣b∣;
  5. −∣a∣≤a≤∣a∣;
  6. ∣a∣≤c if and only if −c≤a≤c.

Facts & Assumptions

Given: Integers a,b,c, and the absolute value of The absolute value ∣a∣ of an integer.

[L1]

Z is a commutative ring: addition and multiplication are associative and commutative, x+0=x, x⋅1=x, multiplication distributes over addition, and every x has an additive inverse −x; we write u−v for u+(−v). Its standard consequences are used freely: −(−x)=x, (−x)y=−(xy), (−x)(−y)=xy, x⋅0=0 and −0=0 (The integers form a commutative ring, Arithmetic on the integers).

[L2]

The order on Z is total, antisymmetric and transitive, is compatible with addition (x≤y implies x+z≤y+z), and positives are closed under multiplication (0<x and 0<y imply 0<xy); x<y means x≤y together with x≠y (The integers form a totally ordered ring, Order on the integers).

[L3]

∣x∣=x when x≥0, and ∣x∣=−x when x≤0; the second clause covers x=0 as well, since −0=0 (The absolute value ∣a∣ of an integer).

Proof

technique · cases
1.1

For every x: 0≤x if and only if −x≤0, and x≤0 if and only if 0≤−x. Adding −x to 0≤x gives −x≤0, and adding x to −x≤0 gives back 0≤x; the second equivalence is the same computation with x and −x interchanged, using −(−x)=x.

L1L2
1.2

If 0≤u and 0≤v then 0≤uv. If u=0 or v=0 then uv=0; otherwise 0<u and 0<v, so 0<uv because positives are closed under multiplication.

L1L2
1.3

By totality, at least one of 0≤a and a≤0 holds, and correspondingly ∣a∣=a or ∣a∣=−a; this is the case split used throughout, and it is exhaustive.

L2L3cases-exhaustive
1.4

Case a≥0: ∣a∣=a≥0.

assume-case nonnegL3
2.1

Case a≤0: ∣a∣=−a, and 0≤−a by step 1.1, so ∣a∣≥0.

assume-case nonposstep 1.1L3
2.2

If a=0 then ∣a∣=0 by the first clause. Conversely, if ∣a∣=0 then in the case a≥0 we get a=∣a∣=0, and in the case a≤0 we get −a=∣a∣=0, whence a=−(−a)=−0=0. This is claim 2.

step 1.3L1L3
2.3

Claim 3. If a≥0 then −a≤0 by step 1.1, so ∣−a∣=−(−a)=a=∣a∣. If a≤0 then 0≤−a by step 1.1, so ∣−a∣=−a=∣a∣.

step 1.1L1L3
2.4

Claim 4, case a≥0 and b≥0: ab≥0 by step 1.2, so ∣ab∣=ab=∣a∣ ∣b∣.

assume-case posposstep 1.2L3
2.5

Claim 4, case a≥0 and b≤0: 0≤−b by step 1.1, so 0≤a(−b)=−(ab) by step 1.2, hence ab≤0 by step 1.1 again; therefore ∣ab∣=−(ab)=a(−b)=∣a∣ ∣b∣.

assume-case posnegstep 1.1step 1.2L1L3
2.6

Claim 4, case a≤0 and b≥0: the same computation with the factors interchanged, using commutativity of multiplication, gives ∣ab∣=(−a)b=∣a∣ ∣b∣.

assume-case negposstep 1.1step 1.2L1L3
2.7

Claim 4, case a≤0 and b≤0: 0≤−a and 0≤−b by step 1.1, so 0≤(−a)(−b)=ab by step 1.2, hence ∣ab∣=ab=(−a)(−b)=∣a∣ ∣b∣.

assume-case negnegstep 1.1step 1.2L1L3
2.8

Claim 5. If a≥0 then ∣a∣=a, so a≤∣a∣; and −∣a∣=−a≤0≤a by step 1.1, so −∣a∣≤a by transitivity. If a≤0 then ∣a∣=−a and 0≤−a by step 1.1, so a≤0≤∣a∣ by transitivity; and −∣a∣=−(−a)=a≤a.

step 1.1step 1.3L1L2L3
2.9

Claim 6, from right to left: suppose −c≤a≤c. If a≥0 then ∣a∣=a≤c. If a≤0 then ∣a∣=−a, and adding c−a to −c≤a gives −a≤c, that is ∣a∣≤c.

step 1.3L1L2L3
3.1

Claim 1 holds: ∣a∣≥0 in both cases.

step 1.3step 1.4step 2.1cases
3.2

The four sign combinations of step 2.4 to step 2.7 exhaust the possibilities by totality, so claim 4 holds for all a,b.

step 1.3step 2.4step 2.5step 2.6step 2.7cases
3.3

Claim 6, from left to right: suppose ∣a∣≤c. Then a≤∣a∣≤c by step 2.8 and transitivity. Adding −c−∣a∣ to ∣a∣≤c gives −c≤−∣a∣, and −∣a∣≤a by step 2.8, so −c≤a by transitivity.

step 2.8L1L2
4.1

Every one of the six claims is now established, claim 6 by its two halves.

step 3.1step 2.2step 2.3step 3.2step 2.8step 3.3step 2.9∎

Remarks

  • Claim 6 is stated with ≤ on both sides deliberately, and the strict form follows from it: ∣a∣<c holds exactly when −c<a<c. From left to right, a≤∣a∣<c and −c<−∣a∣≤a by claim 5. From right to left, −c<a<c gives ∣a∣≤c by claim 6, and ∣a∣=c is impossible, since ∣a∣ is a or −a and both a=c and −a=c are excluded by the two strict inequalities.

  • The list does not include the triangle inequality, which is not used anywhere on this page. What the proofs below actually reach for is claim 1, claim 2, claim 4 and the bound a≤∣a∣ of claim 5; claim 3 is used once, in the identification of the associate classes, and claim 6 is recorded for completeness rather than because something later needs it.

DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (z-ai/glm-5.2)audited 2026-07-28Open item page →

Divisibility in Z: d∣a when a=dq for some integer q

Definition

Let d,a∈Z (The integers as equivalence classes of pairs of naturals). We say d divides a, and write d∣a, when

a  =  dqfor some q∈Z,

the product being that of Arithmetic on the integers. We write d∤a when this fails. In this situation d is called a divisor, or a factor, of a, and a is called a multiple of d.

This is the relation the library already has, not a second one. The published Division with remainder in Z: for a∈Z and b>0 there are unique q,r∈Z with a=qb+r and 0≤r<b introduces it in its own Statement, in these words: "We say b divides a, written b∣a, when a=qb for some q∈Z." Since multiplication on Z is commutative (The integers form a commutative ring), a=qd and a=dq are the same condition, so the definition above is that relation verbatim and the two usages agree everywhere. The theorem defined it for use on its own page and left the systematic theory to a later page; this is that page, and this item records the agreement rather than introducing a rival notion.

The remainder test. For b>0 the same Statement records that b∣a holds exactly when the remainder r in a=qb+r, 0≤r<b, is 0.

Boundary values. Each is one line from the ring axioms, and each is used below, so all three are recorded here rather than assumed:

  • d∣0 for every integer d, including d=0, since 0=d⋅0;
  • 0∣a only for a=0, since a=0⋅q forces a=0;
  • 1∣a and a∣a for every a, since a=1⋅a and a=a⋅1.

Remarks

CorollaryStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-28Open item page →

Division with remainder for any nonzero divisor: for a∈Z and b≠0 there are unique q,r∈Z with a=qb+r and 0≤r<∣b∣

Statement

Let a,b∈Z with b≠0. Then there is exactly one pair (q,r) of integers with

a  =  qb+r,0≤r<∣b∣,

the absolute value being that of The absolute value ∣a∣ of an integer. Moreover b∣a (Divisibility in Z: d∣a when a=dq for some integer q) holds exactly when r=0.

Facts & Assumptions

Given: Integers a and b with b≠0.

[L1]

For a∈Z and b′>0 there is exactly one pair (Q,r) of integers with a=Qb′+r and 0≤r<b′ (Division with remainder in Z: for a∈Z and b>0 there are unique q,r∈Z with a=qb+r and 0≤r<b).

[L2]

Z is a commutative ring: addition and multiplication are associative and commutative, x+0=x, x⋅1=x, multiplication distributes over addition, and every x has an additive inverse −x, with −(−x)=x and (−x)(−y)=xy (The integers form a commutative ring, Arithmetic on the integers).

[L3]

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

[L5]

b∣a means a=bs for some s∈Z (Divisibility in Z: d∣a when a=dq for some integer q).

Proof

technique · cases
1.1

0<∣b∣: indeed ∣b∣≥0, and ∣b∣≠0 because b≠0.

L4given
1.2

Case b>0: put ε:=1. Then ∣b∣=b, so ε∣b∣=b, and ε2=1.

assume-case posL2L4
1.3

Case b<0: put ε:=−1. Then ∣b∣=−b, so ε∣b∣=−(−b)=b, and ε2=(−1)(−1)=1.

assume-case negL2L4
2.1

Since b≠0, totality gives 0≤b or b≤0, hence b>0 or b<0; so in either case there is an integer ε with b=ε∣b∣ and ε2=1.

step 1.2step 1.3L3givencases
2.2

By [L1] applied to a and the positive integer ∣b∣, there is exactly one pair (Q,r) of integers with a=Q∣b∣+r and 0≤r<∣b∣.

step 1.1L1
3.1

Existence. Put q:=εQ. Then qb=εQ⋅ε∣b∣=ε2Q∣b∣=Q∣b∣, so a=qb+r with 0≤r<∣b∣.

step 2.1step 2.2L2
3.2

Uniqueness. Suppose a=q1b+r1=q2b+r2 with 0≤ri<∣b∣ for i=1,2. Since b=ε∣b∣, this reads a=(εq1)∣b∣+r1=(εq2)∣b∣+r2, two representations of the form required by [L1] for the divisor ∣b∣; hence εq1=εq2 and r1=r2. Multiplying the first equation by ε and using ε2=1 gives q1=q2.

step 2.1step 2.2L1L2
4.1

The remainder test. If r=0 then a=qb, so b∣a. Conversely, if b∣a, say a=bs, then a=sb+0 and 0≤0<∣b∣ by step 1.1, so this is a representation of the required form and uniqueness forces r=0.

step 1.1step 3.1step 3.2L2L5
5.1

Existence is step 3.1, uniqueness is step 3.2, and the remainder test is step 4.1, which is the full statement.

step 3.1step 3.2step 4.1∎

Remarks

  • What this discharges. Division with remainder in Z: for a∈Z and b>0 there are unique q,r∈Z with a=qb+r and 0≤r<b is stated for a positive divisor, and its own Remarks record that "the version for b≠0, with 0≤r<∣b∣, follows once absolute values are in hand". Absolute values on Z arrive on this page (The absolute value ∣a∣ of an integer), so the promise is discharged here.

  • The remainder is still taken nonnegative, and that is a choice. With a=−7 and b=−3 the statement above gives −7=3⋅(−3)+2, so q=3 and r=2, whereas truncating the quotient toward zero would give q=2 and r=−1, which the constraint 0≤r excludes. The clause 0≤r<∣b∣ is the one every use below makes, and no other convention is introduced anywhere on this page.

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-28Open item page →

Divisibility is reflexive and transitive on Z, and is linear: if d∣a and d∣b then d∣ax+by for all integers x,y; also d∣a implies d∣ac, −d∣a and d∣−a

Statement

Let a,b,c,d,x,y∈Z and let ∣ be divisibility (Divisibility in Z: d∣a when a=dq for some integer q). Then

  1. reflexivity: a∣a;
  2. transitivity: d∣a and a∣b imply d∣b;
  3. linearity: d∣a and d∣b imply d∣ax+by; in particular d∣a+b and d∣a−b;
  4. d∣a implies d∣ac;
  5. d∣a implies −d∣a and d∣−a.

Consequently the four statements d∣a, −d∣a, d∣−a and −d∣−a are equivalent.

Facts & Assumptions

Given: Integers a,b,c,d,x,y.

[L1]

d∣a means a=dq for some q∈Z; a=a⋅1 exhibits a∣a (Divisibility in Z: d∣a when a=dq for some integer q).

[L2]

Z is a commutative ring: addition and multiplication are associative and commutative, x+0=x, x⋅1=x, multiplication distributes over addition, and every x has an additive inverse −x, with −(−x)=x, (−x)y=−(xy) and (−x)(−y)=xy; we write u−v for u+(−v) (The integers form a commutative ring, Arithmetic on the integers).

Proof

technique · direct
1.1

Reflexivity: a=a⋅1, so a∣a.

L1L2
1.2

Transitivity: suppose a=dm and b=an. Then b=(dm)n=d(mn) by associativity, so d∣b.

L1L2
1.3

Linearity: suppose a=dm and b=dn. Then ax+by=(dm)x+(dn)y=d(mx+ny) by associativity, commutativity and distributivity, so d∣ax+by.

L1L2
1.4

Clause 4: suppose a=dm. Then ac=(dm)c=d(mc), so d∣ac.

L1L2
1.5

Clause 5: suppose a=dm. Then a=(−d)(−m), so −d∣a; and −a=−(dm)=d(−m), so d∣−a.

L1L2
2.1

The two special cases in clause 3: taking x=y=1 gives d∣a+b, and taking x=1, y=−1 gives d∣a⋅1+b⋅(−1)=a−b.

step 1.3L2
2.2

The four equivalent forms: clause 5 gives d∣a⇒−d∣a and d∣a⇒d∣−a; applying each to −d in place of d, or to −a in place of a, and using −(−x)=x, gives the reverse implications, so all four statements are equivalent.

step 1.5L2
3.1

Clauses 1 to 5 and the two consequences are established.

step 1.1step 1.2step 1.3step 1.4step 1.5step 2.1step 2.2∎

Remarks

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-28Open item page →

If d∣a and a≠0 then d≠0 and ∣d∣≤∣a∣; hence the set of divisors of a nonzero integer is bounded above by ∣a∣

Statement

Let a,d∈Z with d∣a (Divisibility in Z: d∣a when a=dq for some integer q) and a≠0. Then d≠0 and

∣d∣  ≤  ∣a∣.

Consequently, for a≠0 the set { d∈Z:d∣a } of divisors of a is bounded above by ∣a∣: every divisor d of a satisfies d≤∣a∣.

Facts & Assumptions

Given: Integers a and d with a=dq for some q∈Z and a≠0; and the embedding ι:N→Z, ι(k)=[(k,0)], of The naturals embed in the integers.

[L1]

Z is a commutative ring: addition and multiplication are associative and commutative, x+0=x, x⋅1=x, x⋅0=0, multiplication distributes over addition, and every x has an additive inverse −x; we write u−v for u+(−v) (The integers form a commutative ring, Arithmetic on the integers).

[L2]

The order on Z is total, antisymmetric and transitive, is compatible with addition, and positives are closed under multiplication; x<y means x≤y together with x≠y (The integers form a totally ordered ring, Order on the integers).

[L3]

ι is injective, preserves addition, multiplication and order, and its image is exactly the set of nonnegative integers; ι(0)=0 and ι(1)=1 (The naturals embed in the integers, The integers as equivalence classes of pairs of naturals).

[L4]

On N: m<n if and only if σ(m)≤n (Discreteness: σ(n) is the immediate successor); 1=σ(0) (The natural numbers N (von Neumann)); and 0≤k for every k, since 0+k=k (Order on the natural numbers).

[L6]

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

Proof

technique · direct
1.1

Write a=dq. If d=0 then a=0⋅q=0, and if q=0 then a=d⋅0=0; both contradict a≠0, so d≠0 and q≠0.

givenL1L6
1.2

If 0≤u and 0≤v then 0≤uv: if u=0 or v=0 then uv=0, and otherwise 0<u and 0<v, so 0<uv because positives are closed under multiplication.

L1L2
1.3

Discreteness of Z: if 0<x then 1≤x. Indeed x≥0, so x=ι(k) for some k∈N; k≠0 because ι(0)=0≠x; hence 0<k in N, so 1=σ(0)≤k, and applying ι, which preserves the order, gives 1=ι(1)≤ι(k)=x.

L2L3L4
2.1

∣a∣=∣d∣ ∣q∣, and ∣q∣>0 because ∣q∣≥0 and ∣q∣≠0, the latter since q≠0.

step 1.1L5
3.1

Hence 1≤∣q∣, so 0≤∣q∣−1 by compatibility of the order with addition.

step 1.3step 2.1L2
4.1

Since ∣d∣≥0 and 0≤∣q∣−1, the product ∣d∣ (∣q∣−1) is nonnegative, and it equals ∣d∣ ∣q∣−∣d∣=∣a∣−∣d∣ by distributivity; adding ∣d∣ gives ∣d∣≤∣a∣.

step 1.2step 2.1step 3.1L1L2L5
5.1

Finally, every divisor d of a satisfies d≤∣d∣ and ∣d∣≤∣a∣, hence d≤∣a∣ by transitivity: ∣a∣ is an upper bound for the set of divisors of a.

step 4.1L2L5∎

Remarks

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-28Open item page →

(Z,⋅,1) is a commutative monoid whose group of units is {1,−1}; equivalently u∣1 holds exactly for u=1 and u=−1

Statement

(Z,⋅,1), with the multiplication of Arithmetic on the integers, is a commutative monoid (Semigroup and monoid). Its group of units (Left inverse, right inverse, and invertible element of a monoid, The invertible elements of a monoid form a group under the restricted operation) is

Z×  =  { 1, −1 },

and these are two distinct elements. Equivalently, for u∈Z the condition u∣1 (Divisibility in Z: d∣a when a=dq for some integer q) holds exactly when u=1 or u=−1.

Facts & Assumptions

Given: Z with the operations of Arithmetic on the integers, and the embedding ι:N→Z, ι(k)=[(k,0)], of The naturals embed in the integers.

[L1]

Z is a commutative ring: multiplication is a function Z×Z→Z and is associative and commutative, x⋅1=x, and every x has an additive inverse −x, with −(−x)=x and (−x)(−y)=xy (The integers form a commutative ring, Arithmetic on the integers).

[L2]

The order on Z is total, antisymmetric and transitive, and positives are closed under multiplication; x<y means x≤y together with x≠y (The integers form a totally ordered ring, Order on the integers).

[L3]

A binary operation on a set S is a function S×S→S; a monoid is a set with an associative binary operation and a two-sided identity, and it is commutative when the operation is (Binary operation on a set; associativity, commutativity, and a subset closed under the operation, Left identity, right identity, and two-sided identity for a binary operation, Semigroup and monoid).

[L4]

In a monoid M, u is a unit when it has a two-sided inverse, and M× denotes the set of units; M× is a group under the restricted operation (Left inverse, right inverse, and invertible element of a monoid, The invertible elements of a monoid form a group under the restricted operation, Group and abelian group).

[L5]

u∣a means a=uv for some v∈Z (Divisibility in Z: d∣a when a=dq for some integer q).

[L8]

ι is injective, preserves addition, multiplication and order, and its image is exactly the set of nonnegative integers; ι(0)=0 and ι(1)=1 (The naturals embed in the integers, The integers as equivalence classes of pairs of naturals).

[L9]

On N: m<n if and only if σ(m)≤n (Discreteness: σ(n) is the immediate successor); 0=∅, 1=σ(0)={0} and 2=σ(1)={0,1}, so 1≠0 and 2≠0 (The natural numbers N (von Neumann)); and 0≤k for every k (Order on the natural numbers).

Proof

technique · direct
1.1

Multiplication on Z is a function Z×Z→Z, hence a binary operation, and it is associative and commutative; 1 is a two-sided identity, since x⋅1=x and, by commutativity, 1⋅x=x. So (Z,⋅,1) is a commutative monoid.

L1L3
1.2

For u∈Z, being a unit of this monoid means uv=1 for some v, the two equations uv=1 and vu=1 being the same by commutativity; and uv=1 for some v is precisely u∣1. So Z×={ u:u∣1 }.

L1L4L5
1.3

Both 1 and −1 lie in Z×: 1⋅1=1 and (−1)(−1)=1⋅1=1.

L1L4
1.4

0≤1, since 1=ι(1) lies in the image of ι, which is the set of nonnegative integers; hence ∣1∣=1. Also 1≠0, since ι is injective and 1≠0 in N.

L7L8
1.5

Discreteness of Z: if 0<x then 1≤x. Indeed x≥0, so x=ι(k) for some k∈N; k≠0 because ι(0)=0≠x; hence 0<k in N, so 1=σ(0)≤k, and applying ι, which preserves the order, gives 1=ι(1)≤ι(k)=x.

L2L8L9
1.6

1≠−1: otherwise 1+1=1+(−1)=0, whereas 1+1=ι(1)+ι(1)=ι(1+1)=ι(2) and ι(2)≠ι(0)=0 because ι is injective and 2≠0 in N.

L1L8L9
2.1

Let u∣1. Since 1≠0, [L6] gives u≠0 and ∣u∣≤∣1∣=1.

step 1.4L6
3.1

Also ∣u∣≥0 and ∣u∣≠0, so 0<∣u∣, whence 1≤∣u∣; with step 2.1 and antisymmetry this gives ∣u∣=1.

step 1.5step 2.1L2L7
4.1

From ∣u∣=1: if u≥0 then u=∣u∣=1, and if u≤0 then −u=∣u∣=1, so u=−(−u)=−1. By totality one of the two holds, so u=1 or u=−1.

step 3.1L1L2L7
5.1

Combining, Z×={ u:u∣1 }={1,−1}, a two-element set, and by [L4] it is a group under multiplication, with identity 1 and with each of its elements its own inverse.

step 1.2step 1.3step 4.1step 1.6L4∎

Remarks

DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (z-ai/glm-5.2)audited 2026-07-28Open item page →

Associates in Z: integers each of which divides the other

Definition

Integers a and b are associates, written a∼b, when each divides the other (Divisibility in Z: d∣a when a=dq for some integer q):

a∼b:⟺a∣b  and  b∣a.

As a binary relation in the sense of Equivalence relation, equivalence class, and the quotient set A/∼ this is the subset

R  =  { (a,b)∈Z×Z  :  a∣b  and  b∣a }

of Z×Z, and a∼b abbreviates (a,b)∈R.

Nothing is claimed here beyond the definition. That R is an equivalence relation — reflexive, symmetric and transitive — is a statement about R that has to be proved, and it is proved next, in For integers a and b the following are equivalent: a∣b and b∣a; b=ua for a unit u; ∣a∣=∣b∣. Being associates is an equivalence relation whose class of a is {a,−a}, together with the identification of the class of a as {a,−a}. Until then the symbol ∼ is notation for membership of R and carries no further content; in particular the language of equivalence classes is not used above.

Remarks

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passverified 2026-08-02 (claude-opus-5)Open item page →

For integers a and b the following are equivalent: a∣b and b∣a; b=ua for a unit u; ∣a∣=∣b∣. Being associates is an equivalence relation whose class of a is {a,−a}

Statement

Let a,b∈Z. The following are equivalent:

  1. a∣b and b∣a, that is, a∼b (Associates in Z: integers each of which divides the other);
  2. b=ua for some unit u∈Z×={1,−1} ((Z,⋅,1) is a commutative monoid whose group of units is {1,−1}; equivalently u∣1 holds exactly for u=1 and u=−1);
  3. ∣a∣=∣b∣ (The absolute value ∣a∣ of an integer).

Moreover ∼ is an equivalence relation on Z (Equivalence relation, equivalence class, and the quotient set A/∼), and the class of a is

[a]  =  { a, −a },

which is {0} when a=0 and has exactly two elements otherwise.

Facts & Assumptions

Given: Integers a and b, and the relation ∼ of Associates in Z: integers each of which divides the other.

[L1]

Z is a commutative ring, with −(−x)=x, (−x)y=−(xy), x⋅1=x and x⋅0=0 (The integers form a commutative ring, Arithmetic on the integers).

[L2]

The order on Z is total, antisymmetric and transitive, is compatible with addition (x≤y implies x+z≤y+z), and positives are closed under multiplication (0<x and 0<y imply 0<xy) (The integers form a totally ordered ring, Order on the integers).

[L3]

d∣a means a=dq for some q; 0∣a only for a=0 (Divisibility in Z: d∣a when a=dq for some integer q).

[L6]

Z×={1,−1}: an integer u is a unit exactly when u=1 or u=−1, and 1≠−1 ((Z,⋅,1) is a commutative monoid whose group of units is {1,−1}; equivalently u∣1 holds exactly for u=1 and u=−1).

[L8]

A relation is an equivalence relation when it is reflexive, symmetric and transitive, and then the class of a is [a]={ b:a∼b } (Equivalence relation, equivalence class, and the quotient set A/∼).

Proof

technique · direct
1.1

Every integer x satisfies x=∣x∣ or x=−∣x∣: by totality either x≥0, when ∣x∣=x, or x≤0, when ∣x∣=−x and so x=−(−x)=−∣x∣.

L1L2L7
1.2

1≠0, 0<1, ∣1∣=1 and ∣−1∣=1. Indeed 1=0 would give −1=−0=0=1, contradicting 1≠−1 in [L6]. By totality either 0≤1 or 1≤0; in the second case adding −1 gives 0≤−1, and −1≠0 (else 1=0), so 0<−1, hence 0<(−1)(−1)=1, which with 1≤0 contradicts antisymmetry. So 0≤1, and 0<1 since 1≠0; then ∣1∣=1, while 0≤1 gives −1≤0 by compatibility with addition, so ∣−1∣=−(−1)=1.

L1L2L6L7
1.3

Claim 1 implies claim 3. Suppose a∣b and b∣a. If a=0 then 0∣b forces b=0, so ∣a∣=0=∣b∣. If a≠0, then b∣a with a≠0 gives b≠0 and ∣b∣≤∣a∣, and a∣b with b≠0 gives ∣a∣≤∣b∣; antisymmetry gives ∣a∣=∣b∣.

L2L3L5L7
1.4

∼ is reflexive, since a∣a; symmetric, since its defining condition is unchanged when a and b are interchanged; and transitive, since a∣b, b∣c give a∣c and c∣b, b∣a give c∣a. So it is an equivalence relation.

L4L8
2.1

Claim 3 implies claim 1. Suppose ∣a∣=∣b∣. By step 1.1, b is ∣b∣ or −∣b∣, that is ∣a∣ or −∣a∣; and, again by step 1.1, ∣a∣ is a or −a. Hence b=a or b=−a. If b=a then a∣b and b∣a by reflexivity. If b=−a then a∣−a=b by [L4]; and b=−a gives a=−(−a)=−b, so b∣−b=a, again by [L4].

step 1.1L1L4
2.2

Claim 2 implies claim 3. If b=ua with u a unit then u=1 or u=−1, so ∣u∣=1 by step 1.2, and ∣b∣=∣u∣ ∣a∣=∣a∣.

step 1.2L6L7
3.1

Claim 3 implies claim 2. By step 2.1, ∣a∣=∣b∣ gives b=a=1⋅a or b=−a=(−1)a, and 1 and −1 are units.

step 2.1L1L6
4.1

The three claims are equivalent: claim 3 implies claim 1 by step 2.1 and claim 1 implies claim 3 by step 1.3, while claim 3 implies claim 2 by step 3.1 and claim 2 implies claim 3 by step 2.2.

step 2.1step 1.3step 2.2step 3.1
5.1

The class of a is [a]={ b:a∼b }={ b:∣b∣=∣a∣ }={a,−a}: the middle equality is the equivalence of claims 1 and 3, and the last holds because ∣−a∣=∣a∣ by [L7], while conversely ∣b∣=∣a∣ gives b=a or b=−a by step 2.1. At a=0 this set is {0}, since −0=0; and for a≠0 it has exactly two elements, since by totality either 0<a, when adding −a gives −a<0<a, or a<0, when adding −a gives a<0<−a; in both cases a≠−a.

step 2.1step 4.1L1L2L7L8
6.1

By [L9] the classes {a,−a} are nonempty, cover Z, and any two are equal or disjoint; together with steps 4.1, 1.4 and 5.1 this is the full statement.

step 4.1step 1.4step 5.1L9∎

Remarks

  • This is the "up to sign" of elementary number theory made precise. Every statement below that fixes a sign — gcd⁡(a,b)≥0, lcm⁡(a,b)≥0, the nonnegative generator of a subgroup of (Z,+) — is choosing one representative from a class {a,−a}, and claim 3 is what says the choice is between exactly two candidates.

  • The equivalence of claims 1 and 2 is the general ring-theoretic statement, and it is the reason associates are defined by mutual divisibility rather than by "differ by a sign": mutual divisibility is the formulation that survives when the unit group is larger than {1,−1}.

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-28Open item page →

A nonempty set of integers bounded above has a greatest element, and a nonempty set of integers bounded below has a least element

Statement

Let S⊆Z be nonempty. Call b∈Z an upper bound for S when s≤b for every s∈S, and a lower bound when b≤s for every s∈S; call m a greatest element of S when m∈S and s≤m for every s∈S, and a least element when m∈S and m≤s for every s∈S.

If S has an upper bound, it has a greatest element. If S has a lower bound, it has a least element. In each case the element is unique.

Facts & Assumptions

Given: A nonempty S⊆Z, and the embedding ι:N→Z, ι(k)=[(k,0)], of The naturals embed in the integers.

[L1]

Z is a commutative ring: addition is associative and commutative, x+0=x, and every x has an additive inverse −x, with −(−x)=x; we write u−v for u+(−v) (The integers form a commutative ring, Arithmetic on the integers, The integers as equivalence classes of pairs of naturals).

[L2]

The order on Z is total, antisymmetric and transitive, and is compatible with addition: x≤y implies x+z≤y+z (The integers form a totally ordered ring, Order on the integers).

[L3]

ι is injective, preserves addition, multiplication and order, and its image is exactly the set of nonnegative integers, so every x≥0 is ι(k) for a unique k∈N (The naturals embed in the integers, The natural numbers N (von Neumann)).

[L4]

Every nonempty subset of N has a least element (The well-ordering principle, Order on the natural numbers).

Proof

technique · direct
1.1

Suppose b is an upper bound for S. For every s∈S we have s≤b, and adding −s gives 0≤b−s; so b−s is nonnegative and therefore equals ι(k) for a unique k∈N.

givenL1L2L3
1.2

Now suppose instead that c is a lower bound for S, and put S′:={ −s:s∈S }, a nonempty subset of Z. For s∈S, adding −s−c to c≤s gives −s≤−c, so −c is an upper bound for S′.

givenL1L2
2.1

Put T:={ k∈N:b−ι(k)∈S }. It is nonempty: choosing s∈S and the k of step 1.1 with ι(k)=b−s, we get b−ι(k)=b−(b−s)=s∈S, so k∈T.

step 1.1L1given
3.1

By well-ordering let k0 be the least element of T, and put m:=b−ι(k0), so that m∈S.

step 2.1L4choose
4.1

Let s∈S. By step 1.1 there is k∈N with ι(k)=b−s, and then b−ι(k)=s∈S, so k∈T and hence k0≤k.

step 1.1step 2.1step 3.1L1
5.1

Applying ι, which preserves the order, gives ι(k0)≤ι(k)=b−s; adding s−ι(k0) to this inequality gives s≤b−ι(k0)=m.

step 3.1step 4.1L1L2L3
6.1

So m∈S and s≤m for every s∈S: m is a greatest element of S. If m′ were another one, then m≤m′ and m′≤m, so m=m′ by antisymmetry.

step 3.1step 5.1L2
7.1

By the first part S′ has a greatest element, which has the form −ℓ with ℓ∈S; then for every s∈S we have −s≤−ℓ, and adding s+ℓ gives ℓ≤s. So ℓ is a least element of S, and it is unique by antisymmetry as in step 6.1.

step 6.1step 1.2L1L2∎

Remarks

DefinitionDefinition: AI-adaptedProof: Not applicableverified 2026-08-02 (claude-opus-5)Open item page →

Common divisor, and the greatest common divisor gcd⁡(a,b), with the convention gcd⁡(0,0):=0

Definition

Let a,b∈Z. An integer d is a common divisor of a and b when d∣a and d∣b (Divisibility in Z: d∣a when a=dq for some integer q). Write

D(a,b)  :=  { d∈Z  :  d∣a  and  d∣b }

for the set of common divisors.

Case (a,b)≠(0,0): the greatest element exists. D(a,b) is nonempty, since 1∣a and 1∣b for every a and b (Divisibility in Z: d∣a when a=dq for some integer q). It is bounded above: at least one of a and b is nonzero, say a≠0 (if instead b≠0, argue with b throughout), and every d∈D(a,b) divides a, so d≤∣a∣ by If d∣a and a≠0 then d≠0 and ∣d∣≤∣a∣; hence the set of divisors of a nonzero integer is bounded above by ∣a∣. A nonempty set of integers bounded above has a unique greatest element (A nonempty set of integers bounded above has a greatest element, and a nonempty set of integers bounded below has a least element), and we define

gcd⁡(a,b)  :=  the greatest element of D(a,b).

Since 1∈D(a,b) and gcd⁡(a,b) is greatest, gcd⁡(a,b)≥1; in particular gcd⁡(a,b)>0.

Case (a,b)=(0,0): a convention, fixed here. Every integer divides 0 (Divisibility in Z: d∣a when a=dq for some integer q), so D(0,0)=Z, which has no greatest element at all: the clause above defines nothing, and leaving gcd⁡(0,0) undefined would put a hole in every identity below. We therefore set

gcd⁡(0,0)  :=  0.

With both cases together, gcd⁡(a,b) is defined for every pair of integers, and gcd⁡(a,b)≥0 always.

Why 0, and not some other value. The convention is not arbitrary, and the reasons are recorded here rather than deferred:

Remarks

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-28Open item page →

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)≥1 unless a=b=0

Statement

For all a,b∈Z, with gcd⁡ as in Common divisor, and the greatest common divisor gcd⁡(a,b), with the convention gcd⁡(0,0):=0:

  1. gcd⁡(a,b)=gcd⁡(b,a);
  2. gcd⁡(a,b)=gcd⁡(∣a∣,∣b∣);
  3. gcd⁡(a,0)=∣a∣, and in particular gcd⁡(0,0)=0;
  4. gcd⁡(a,1)=1;
  5. gcd⁡(a,a)=∣a∣;
  6. gcd⁡(a,b)≥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∣a and d∣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)≠(0,0), gcd⁡(a,b) is the unique greatest element of D(a,b) and satisfies gcd⁡(a,b)≥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∣a means a=dq for some q; every d satisfies d∣0; 0∣a only for a=0; and 1∣a, a∣a for every a (Divisibility in Z: d∣a when a=dq for some integer q).

[L7]

Z is a commutative ring with x⋅1=x, x⋅(−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≠0 and −1≤0≤1. If 1=0 then −1=−0=0=1, contradicting 1≠−1. By totality 0≤1 or 1≤0; in the second case adding −1 gives 0≤−1, and −1≠0, so 0<−1 and hence 0<(−1)(−1)=1, contradicting 1≤0 by antisymmetry. So 0≤1, and adding −1 gives −1≤0.

L5L7
1.2

∣x∣∣x for every x: by totality x≥0, when x=∣x∣=∣x∣⋅1, or x≤0, when ∣x∣=−x and so x=−(−x)=−∣x∣=∣x∣⋅(−1).

L6L7
1.3

For every d and x: d∣x if and only if d∣∣x∣, because ∣x∣ is x or −x and the two conditions d∣x, d∣−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.

L1
1.5

Claim 5. D(a,a)={ d:d∣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)≠(0,0) the value gcd⁡(a,b) is ≥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∣a }, since every d divides 0. If a=0 this is Z and gcd⁡(0,0)=0=∣0∣ by the convention. If a≠0, then ∣a∣∈D(a,0) by step 1.2, and every d∈D(a,0) satisfies d≤∣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∈D(a,1) satisfies d∣1, hence d=1 or d=−1; and 1∈D(a,1) since 1∣a and 1∣1. Also (a,1)≠(0,0) because 1≠0. Since −1≤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.

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-28Open item page →

Bézout's identity: for integers a,b not both zero, gcd⁡(a,b) is the least positive element of { ax+by:x,y∈Z }; in particular ax+by=gcd⁡(a,b) has an integer solution

Statement

Let a,b∈Z, not both 0, and put

I  :=  { ax+by  :  x,y∈Z }.

Then I contains a positive element, and its least positive element is gcd⁡(a,b) (Common divisor, and the greatest common divisor gcd⁡(a,b), with the convention gcd⁡(0,0):=0). In particular there are integers x0,y0 with

ax0+by0  =  gcd⁡(a,b),

so the equation ax+by=gcd⁡(a,b) is solvable in Z.

Facts & Assumptions

Given: Integers a and b, not both 0; the set I={ ax+by:x,y∈Z }; and the embedding ι:N→Z, ι(k)=[(k,0)], of The naturals embed in the integers.

[L1]

Z is a commutative ring: addition and multiplication are associative and commutative, x+0=x, x⋅1=x, x⋅0=0, multiplication distributes over addition, and every x has an additive inverse −x, with −(−x)=x and (−x)(−y)=xy; we write u−v for u+(−v) (The integers form a commutative ring, Arithmetic on the integers, The integers as equivalence classes of pairs of naturals).

[L2]

The order on Z is total, antisymmetric and transitive, is compatible with addition, and positives are closed under multiplication; x<y means x≤y together with x≠y (The integers form a totally ordered ring, Order on the integers).

[L3]

ι is injective, preserves addition, multiplication and order, and its image is exactly the nonnegative integers (The naturals embed in the integers, The natural numbers N (von Neumann)).

[L4]

Every nonempty subset of N has a least element (The well-ordering principle, Order on the natural numbers).

[L5]

For a∈Z and b′>0 there are integers q,r with a=qb′+r and 0≤r<b′ (Division with remainder in Z: for a∈Z and b>0 there are unique q,r∈Z with a=qb+r and 0≤r<b).

[L6]

For (a,b)≠(0,0), gcd⁡(a,b) is the unique greatest element of the set D(a,b) of common divisors of a and b (Common divisor, and the greatest common divisor gcd⁡(a,b), with the convention gcd⁡(0,0):=0).

[L10]

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

Proof

technique · direct
1.1

If 0≤u and 0≤v then 0≤uv, and if moreover u≠0 and v≠0 then 0<uv: for u=0 or v=0 the product is 0, and otherwise 0<u and 0<v, so 0<uv because positives are closed under multiplication.

L1L2
1.2

If 0<u and 0≤v then 0<u+v: adding u to 0≤v gives u≤u+v, so 0≤u+v by transitivity, and u+v=0 would give u≤0 and hence u=0 by antisymmetry, contrary to 0<u.

L1L2
2.1

x⋅x≥0 for every x, with x⋅x>0 when x≠0. By totality either 0≤x, and step 1.1 applies directly, or x≤0, in which case 0≤−x by compatibility with addition and x⋅x=(−x)(−x)≥0 by step 1.1; the strict form follows since x≠0 gives −x≠0.

step 1.1L1L2
3.1

I contains a positive element: a⋅a+b⋅b∈I, and one of a,b is nonzero, so one of a⋅a, b⋅b is positive and the other is nonnegative, whence the sum is positive by step 1.2.

step 2.1step 1.2given
4.1

Let P be the set of positive elements of I and put T:={ k∈N:ι(k)∈P }. Every p∈P satisfies p≥0, hence p=ι(k) for some k∈N with k∈T; so T is nonempty by step 3.1.

step 3.1L3
5.1

By well-ordering let k0 be the least element of T and put d:=ι(k0), so d∈P and d>0; fix x0,y0∈Z with d=ax0+by0.

step 4.1L4choose
6.1

d is the least element of P: given p∈P, write p=ι(k) with k∈T as in step 4.1; then k0≤k, and applying ι, which preserves the order, gives d=ι(k0)≤ι(k)=p.

step 4.1step 5.1L3L4
7.1

d∣a. By [L5] with divisor d>0 write a=qd+r with 0≤r<d. Then r=a−qd=a−q(ax0+by0)=a(1−qx0)+b(−qy0), so r∈I. If r were positive it would lie in P, so d≤r by step 6.1, which with r<d contradicts antisymmetry. Hence r is not positive; with 0≤r this forces r=0, so a=qd and d∣a.

step 5.1step 6.1L1L2L5L10
7.2

d∣b, by the same argument with b in place of a: dividing b by d gives b=q′d+r′ with 0≤r′<d, and r′=b(1−q′y0)+a(−q′x0)∈I, so r′=0 as before.

step 5.1step 6.1L1L2L5L10
8.1

So d is a common divisor of a and b. Moreover every common divisor c of a and b divides ax0+by0=d by [L7].

step 5.1step 7.1step 7.2L7
9.1

Since d>0 we have d≠0 and ∣d∣=d, so every common divisor c satisfies c≤∣d∣=d by [L8].

step 5.1step 8.1L8L9
10.1

Therefore d is the greatest element of D(a,b), and greatest elements are unique, so d=gcd⁡(a,b) by [L6]; the hypothesis that a and b are not both 0 is what makes that clause of the definition apply.

step 8.1step 9.1L6given
11.1

Hence gcd⁡(a,b)=d is the least positive element of I by step 6.1, and gcd⁡(a,b)=ax0+by0 by step 5.1: the equation ax+by=gcd⁡(a,b) is solvable.

step 5.1step 6.1step 10.1∎

Remarks

CorollaryStatement: AI-adaptedProof: AI-generatedprecheck passverified 2026-08-02 (claude-opus-5)Open item page →

Every common divisor of a and b divides gcd⁡(a,b); consequently d=gcd⁡(a,b) exactly when d≥0, d∣a, d∣b, and every common divisor of a and b divides d — a characterisation that holds at (a,b)=(0,0) as well

Statement

Let a,b∈Z. Every common divisor of a and b divides gcd⁡(a,b) (Common divisor, and the greatest common divisor gcd⁡(a,b), with the convention gcd⁡(0,0):=0, Divisibility in Z: d∣a when a=dq for some integer q).

Consequently, for d∈Z the following are equivalent:

  1. d=gcd⁡(a,b);
  2. d≥0, d∣a, d∣b, and every common divisor of a and b divides d.

This characterisation holds for every pair (a,b), the pair (0,0) included, where it returns the value gcd⁡(0,0)=0 fixed by convention.

Facts & Assumptions

[L1]

For (a,b)≠(0,0), g is the greatest element of the set D(a,b) of common divisors, so in particular g∈D(a,b), and g≥1; at (a,b)=(0,0), g=0 by convention. In both cases g≥0 (Common divisor, and the greatest common divisor gcd⁡(a,b), with the convention gcd⁡(0,0):=0).

Proof

technique · direct
1.1

Suppose (a,b)≠(0,0) and let c be a common divisor of a and b. By [L2] fix x0,y0 with ax0+by0=g; then c∣g by [L4].

L2L4
1.2

Suppose instead (a,b)=(0,0). Then g=0, and every integer, in particular every common divisor c, divides 0=g.

L1L3
1.3

g itself is a common divisor of a and b: for (a,b)≠(0,0) this is g∈D(a,b), and for (a,b)=(0,0) it is 0∣0. And g≥0 in both cases.

L1L3
2.1

In both cases every common divisor of a and b divides g; since the two cases are exhaustive, this is the first assertion.

step 1.1step 1.2
3.1

Claim 1 implies claim 2: if d=g then d≥0, d∣a and d∣b by step 1.3, and every common divisor divides d by step 2.1.

step 2.1step 1.3
3.2

Claim 2 implies claim 1: suppose d≥0, d∣a, d∣b, and every common divisor of a and b divides d. Then d is a common divisor, so d∣g by step 2.1; and g is a common divisor by step 1.3, so g∣d by hypothesis. Hence ∣d∣=∣g∣ by [L5], and since d≥0 and g≥0 this reads d=∣d∣=∣g∣=g.

step 2.1step 1.3L1L5L6
4.1

The two claims are therefore equivalent, for every pair (a,b) including (0,0), where step 1.2 and step 1.3 were proved directly from the convention rather than from a maximum.

step 1.2step 1.3step 3.1step 3.2∎

Remarks

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-28Open item page →

If a=qb+r then a,b and b,r have exactly the same common divisors, so gcd⁡(a,b)=gcd⁡(b,r)

Statement

Let a,b,q,r∈Z satisfy

a  =  qb+r.

Then an integer d is a common divisor of a and b if and only if it is a common divisor of b and r (Divisibility in Z: d∣a when a=dq for some integer q); the two sets of common divisors are equal. Consequently

gcd⁡(a,b)  =  gcd⁡(b,r)

(Common divisor, and the greatest common divisor gcd⁡(a,b), with the convention gcd⁡(0,0):=0).

No inequality on r is assumed: the identity a=qb+r alone is what is used, so the lemma applies to any decomposition of a, not only to the one produced by division with remainder.

Facts & Assumptions

Given: Integers a,b,q,r with a=qb+r, and the sets D(a,b) and D(b,r) of common divisors (Common divisor, and the greatest common divisor gcd⁡(a,b), with the convention gcd⁡(0,0):=0).

[L1]

Z is a commutative ring: x⋅0=0, x+0=x, and every x has an additive inverse; we write u−v for u+(−v), and a=qb+r gives r=a−qb (The integers form a commutative ring, Arithmetic on the integers).

[L3]

For (u,v)≠(0,0), gcd⁡(u,v) is the greatest element of D(u,v), and gcd⁡(0,0)=0 by convention (Common divisor, and the greatest common divisor gcd⁡(a,b), with the convention gcd⁡(0,0):=0).

Proof

technique · direct
1.1

Suppose d∣b and d∣r. Then d∣bq+r⋅1=a by [L2], so d is a common divisor of a and b: D(b,r)⊆D(a,b).

givenL1L2
1.2

Suppose d∣a and d∣b. Then d∣a⋅1+b(−q)=a−qb=r by [L2], so d is a common divisor of b and r: D(a,b)⊆D(b,r).

givenL1L2
1.3

The pairs vanish together: if b=0 and r=0 then a=q⋅0+0=0, and if a=0 and b=0 then r=a−qb=0−0=0. So (a,b)=(0,0) exactly when (b,r)=(0,0).

givenL1
2.1

By steps 1.1 and 1.2 the two sets of common divisors are equal, D(a,b)=D(b,r).

step 1.1step 1.2
3.1

If (a,b)≠(0,0) then also (b,r)≠(0,0) by step 1.3, and both greatest common divisors are the greatest element of the one set D(a,b)=D(b,r), hence equal. If (a,b)=(0,0) then (b,r)=(0,0) and both values are 0. In either case gcd⁡(a,b)=gcd⁡(b,r).

step 1.3step 2.1L3∎

Remarks

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-28Open item page →

The Euclidean algorithm: for a∈Z and b>0 the remainder descent from (a,b) terminates, and the last nonzero remainder is gcd⁡(a,b)

Statement

Let a∈Z and b>0. Define Φ:Z×Z→Z×Z by

Φ(u,v)  =  {(v,  u−qv)if v>0,(u,v)if v≤0,

where in the first clause q is the unique quotient of u by v given by Division with remainder in Z: for a∈Z and b>0 there are unique q,r∈Z with a=qb+r and 0≤r<b, so that u−qv is the remainder and 0≤u−qv<v.

Let R:N→Z×Z be the unique function with R(0)=(a,b) and R(σ(k))=Φ(R(k)) supplied by the recursion theorem (The recursion theorem). Write R(k)=(ak,bk); the sequence b0,b1,b2,… is the remainder descent from (a,b).

Then:

  1. bk≥0 for every k, and bσ(k)<bk whenever bk>0;
  2. gcd⁡(ak,bk)=gcd⁡(a,b) for every k (Common divisor, and the greatest common divisor gcd⁡(a,b), with the convention gcd⁡(0,0):=0);
  3. there is a least N∈N with bN=0, and N≠0; writing N=σ(M), the value bM is the last nonzero remainder, and bM>0;
  4. aN=bM=gcd⁡(a,b).

So the descent terminates, and the last nonzero remainder is gcd⁡(a,b).

Facts & Assumptions

Given: a∈Z, b>0, the map Φ and the sequence R(k)=(ak,bk) described above, and the embedding ι:N→Z, ι(k)=[(k,0)], of The naturals embed in the integers.

[L1]

Z is a commutative ring; its order is total, antisymmetric and transitive, and is compatible with addition; x<y means x≤y together with x≠y (The integers form a commutative ring, Arithmetic on the integers, The integers form a totally ordered ring, Order on the integers, The integers as equivalence classes of pairs of naturals).

[L2]

For u∈Z and v>0 there is exactly one pair (q,r) of integers with u=qv+r and 0≤r<v (Division with remainder in Z: for a∈Z and b>0 there are unique q,r∈Z with a=qb+r and 0≤r<b).

[L3]

For a set A, an α∈A and a function f:A→A there is exactly one g:N→A with g(0)=α and g(σ(k))=f(g(k)) (The recursion theorem).

[L4]

Induction on N: a property holding at 0 and inherited by successors holds everywhere (The principle of mathematical induction).

[L6]

ι is injective, preserves addition, multiplication and order, and its image is exactly the nonnegative integers (The naturals embed in the integers).

[L7]

On N: exactly one of m<n, m=n, n<m holds (Trichotomy of the order on N); m<n if and only if σ(m)≤n (Discreteness: σ(n) is the immediate successor); and every n≠0 is a successor (Every nonzero natural number is a successor).

Proof

technique · induction
1.1

Φ is a well-defined function. For v>0 the pair (q,r) with u=qv+r and 0≤r<v is unique by [L2], so q and r=u−qv depend only on (u,v); for v≤0 the value is (u,v); and the two clauses are exhaustive and exclusive by totality. Hence [L3] applies with A=Z×Z, α=(a,b) and f=Φ, giving the sequence R.

L1L2L3construct
1.2

Base case of the induction, at k=0: b0=b>0, so b0≥0; and gcd⁡(a0,b0)=gcd⁡(a,b) because (a0,b0)=(a,b).

basegivenL1
1.3

Induction hypothesis: fix k and assume bk≥0 and gcd⁡(ak,bk)=gcd⁡(a,b).

ih
2.1

Inductive step. If bk>0, then by [L2] write ak=qbk+r with 0≤r<bk; by definition R(σ(k))=Φ(ak,bk)=(bk,r), so bσ(k)=r≥0 and bσ(k)=r<bk, while gcd⁡(aσ(k),bσ(k))=gcd⁡(bk,r)=gcd⁡(ak,bk)=gcd⁡(a,b) by [L8]. If instead bk=0, then bk≤0, so R(σ(k))=R(k) and both properties are inherited unchanged. Since bk≥0, these two cases are exhaustive.

step 1.3L1L2L8
3.1

By induction, bk≥0 and gcd⁡(ak,bk)=gcd⁡(a,b) for every k∈N; and step 2.1 also shows bσ(k)<bk whenever bk>0. This is claim 1 and claim 2.

step 1.2step 2.1L4
4.1

Let U:={ n∈N:ι(n)=bk for some k∈N }. Every bk is nonnegative, hence lies in the image of ι, so U is nonempty; let n0 be its least element and fix k0 with bk0=ι(n0).

step 3.1L5L6choose
5.1

bk0=0. Otherwise bk0>0, so 0≤bσ(k0)<bk0 by step 3.1; writing bσ(k0)=ι(n1) with n1∈U, we get ι(n1)<ι(n0), and hence n1<n0, since otherwise n0≤n1 by trichotomy and so ι(n0)≤ι(n1), contradicting antisymmetry. That contradicts the minimality of n0.

step 3.1step 4.1L1L6L7
6.1

So { k∈N:bk=0 } is nonempty; let N be its least element. N≠0, since b0=b>0. Hence N=σ(M) for some M∈N, and M<N because M<σ(M).

step 5.1givenL5L7
7.1

bM>0: indeed bM≥0 by step 3.1, and bM≠0 because M<N and N is the least index with vanishing b.

step 3.1step 6.1
8.1

Since bM>0, the definition gives R(N)=R(σ(M))=Φ(aM,bM)=(bM,  aM−qbM), so aN=bM and bN=aM−qbM; and bN=0 by the choice of N.

step 6.1step 7.1L2
9.1

Therefore gcd⁡(a,b)=gcd⁡(aN,bN)=gcd⁡(aN,0)=∣aN∣=aN=bM, the last equality because aN=bM>0. So the descent terminates at index N and the last nonzero remainder bM equals gcd⁡(a,b), which is claims 3 and 4.

step 3.1step 7.1step 8.1L9discharge-induction∎

Remarks

CorollaryStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-28Open item page →

The extended Euclidean algorithm: the same descent produces integers x,y with ax+by=gcd⁡(a,b), so Bézout coefficients are computed and not merely shown to exist

Statement

Let a∈Z and b>0, and let R(k)=(ak,bk) and N be the remainder descent and its terminating index from The Euclidean algorithm: for a∈Z and b>0 the remainder descent from (a,b) terminates, and the last nonzero remainder is gcd⁡(a,b). Define Ψ:Z6→Z6 by

Ψ(A,B,x,y,u,v)  =  {(B,  A−qB,  u,  v,  x−qu,  y−qv)if B>0,(A,B,x,y,u,v)if B≤0,

where in the first clause q is the unique quotient of A by B given by Division with remainder in Z: for a∈Z and b>0 there are unique q,r∈Z with a=qb+r and 0≤r<b. Let

S:N→Z6,S(0)=(a, b, 1, 0, 0, 1),S(σ(k))=Ψ(S(k))

be the function supplied by the recursion theorem (The recursion theorem), and write S(k)=(Ak,Bk,xk,yk,uk,vk). Then for every k∈N

(Ak,Bk)=(ak,bk),Ak=axk+byk,Bk=auk+bvk.

In particular, at the terminating index N,

axN+byN  =  AN  =  aN  =  gcd⁡(a,b),

so the descent that computes gcd⁡(a,b) computes a pair of Bézout coefficients alongside it.

Facts & Assumptions

Given: a∈Z, b>0, the descent R(k)=(ak,bk) and terminating index N of The Euclidean algorithm: for a∈Z and b>0 the remainder descent from (a,b) terminates, and the last nonzero remainder is gcd⁡(a,b), and the map Ψ and sequence S(k)=(Ak,Bk,xk,yk,uk,vk) described above.

[L1]

Z is a commutative ring: addition and multiplication are associative and commutative, x+0=x, x⋅1=x, x⋅0=0, multiplication distributes over addition, and every x has an additive inverse; we write u−v for u+(−v) (The integers form a commutative ring, Arithmetic on the integers, The integers as equivalence classes of pairs of naturals).

[L2]

For A′∈Z and B′>0 there is exactly one pair (q,r) of integers with A′=qB′+r and 0≤r<B′ (Division with remainder in Z: for a∈Z and b>0 there are unique q,r∈Z with a=qb+r and 0≤r<b).

[L3]

For a set X, an α∈X and f:X→X there is exactly one g:N→X with g(0)=α and g(σ(k))=f(g(k)) (The recursion theorem, The natural numbers N (von Neumann)).

[L5]

The descent satisfies R(0)=(a,b); bk≥0 for every k; R(σ(k))=(bk, ak−qbk) with q the quotient of ak by bk when bk>0, and R(σ(k))=R(k) when bk=0; N is the least index with bN=0; and aN=gcd⁡(a,b) (The Euclidean algorithm: for a∈Z and b>0 the remainder descent from (a,b) terminates, and the last nonzero remainder is gcd⁡(a,b), Common divisor, and the greatest common divisor gcd⁡(a,b), with the convention gcd⁡(0,0):=0).

[L6]

The order on Z is total and antisymmetric; x<y means x≤y together with x≠y (The integers form a totally ordered ring, Order on the integers).

Proof

technique · induction
1.1

Ψ is a well-defined function: for B>0 the quotient q of A by B is unique by [L2], so the first clause depends only on the argument; the second clause is the identity; and the two conditions B>0 and B≤0 are exhaustive and exclusive by totality. So [L3] applies with X=Z6 and produces S.

L1L2L3L6construct
1.2

Base case, k=0: (A0,B0)=(a,b)=(a0,b0); and A0=a=a⋅1+b⋅0=ax0+by0, B0=b=a⋅0+b⋅1=au0+bv0.

basegivenL1L5
1.3

Induction hypothesis: fix k and assume (Ak,Bk)=(ak,bk), Ak=axk+byk and Bk=auk+bvk.

ih
2.1

Inductive step, case bk>0. Then Bk=bk>0, so both recursions take their first clause with the same divisor and the same dividend, hence with the same quotient q by [L2]. Therefore (Aσ(k),Bσ(k))=(Bk, Ak−qBk)=(bk, ak−qbk)=(aσ(k),bσ(k)).

step 1.3L2L5
2.2

Inductive step, case bk=0. Then Bk=bk=0, so Bk≤0 and S(σ(k))=S(k), while R(σ(k))=R(k); all three equalities are inherited unchanged. Since bk≥0, the two cases are exhaustive.

step 1.3L5L6
3.1

Back in the case bk>0 of step 2.1, the coefficients transport: Aσ(k)=Bk=auk+bvk=axσ(k)+byσ(k), since (xσ(k),yσ(k))=(uk,vk); and Bσ(k)=Ak−qBk=(axk+byk)−q(auk+bvk)=a(xk−quk)+b(yk−qvk)=auσ(k)+bvσ(k) by distributivity.

step 1.3step 2.1L1
4.1

By induction the three equalities hold for every k∈N.

step 1.2step 2.1step 3.1step 2.2L4
5.1

At the terminating index N this reads axN+byN=AN=aN=gcd⁡(a,b), so (xN,yN) is a pair of Bézout coefficients for a and b, obtained from the descent itself.

step 4.1L5discharge-induction∎

Remarks

DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (z-ai/glm-5.2)audited 2026-07-28Open item page →

Coprime integers: gcd⁡(a,b)=1

Definition

Integers a and b are coprime, or relatively prime, when

gcd⁡(a,b)  =  1

(Common divisor, and the greatest common divisor gcd⁡(a,b), with the convention gcd⁡(0,0):=0). The relation is symmetric, since gcd⁡(a,b)=gcd⁡(b,a) (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)≥1 unless a=b=0), and unchanged by signs, since gcd⁡(a,b)=gcd⁡(∣a∣,∣b∣).

Boundary values. N contains 0 and Z contains 0 and 1, so the three degenerate pairs are recorded explicitly, each read off 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)≥1 unless a=b=0:

Remarks

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-28Open item page →

a and b are coprime if and only if ax+by=1 for some integers x,y; and in that case the only common divisors of a and b are 1 and −1

Statement

Let a,b∈Z. Then a and b are coprime (Coprime integers: gcd⁡(a,b)=1) if and only if

ax+by  =  1for some x,y∈Z.

When this holds, the set of common divisors of a and b is exactly {1,−1}.

Facts & Assumptions

Given: Integers a and b.

[L6]

Z is a commutative ring, with x⋅0=0, x+0=x, −(−x)=x and (−x)(−y)=xy (The integers form a commutative ring, Arithmetic on the integers); its order is total, antisymmetric and transitive and is compatible with addition, and positives are closed under multiplication (The integers form a totally ordered ring, Order on the integers).

Proof

technique · direct
1.1

1≠0 and 0≤1. If 1=0 then −1=−0=0=1, contradicting 1≠−1 in [L5]. By totality either 0≤1 or 1≤0; in the second case adding −1 gives 0≤−1, and −1≠0 since otherwise 1=0, so 0<−1 and hence 0<(−1)(−1)=1, which with 1≤0 contradicts antisymmetry.

L5L6
1.2

Conversely, suppose ax+by=1 for some x,y. Every common divisor c of a and b divides ax+by=1 by [L4], hence c=1 or c=−1 by [L5].

L4L5
2.1

Suppose a and b are coprime, so gcd⁡(a,b)=1. Then (a,b)≠(0,0), since gcd⁡(0,0)=0≠1; so [L2] supplies x0,y0 with ax0+by0=gcd⁡(a,b)=1.

step 1.1L1L2L7
2.2

The integer 1 then satisfies all four conditions of [L3]: 1≥0 by step 1.1, 1∣a and 1∣b by [L4], and every common divisor of a and b divides 1 by step 1.2. Hence gcd⁡(a,b)=1, that is, a and b are coprime.

step 1.1step 1.2L1L3L4
3.1

So coprimality and the solvability of ax+by=1 are equivalent, by step 2.1 and step 2.2.

step 2.1step 2.2
4.1

When they hold, step 1.2 shows every common divisor is 1 or −1; conversely 1 and −1 are common divisors of any pair, since 1∣a, 1∣b, −1∣a and −1∣b. So the set of common divisors is exactly {1,−1}, and it has two elements since 1≠−1.

step 1.2L4L5∎

Remarks

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-28Open item page →

If gcd⁡(a,b)=1 and a∣bc then a∣c; and if a∣c, b∣c and gcd⁡(a,b)=1 then ab∣c

Statement

Let a,b,c∈Z.

  1. If gcd⁡(a,b)=1 and a∣bc, then a∣c.
  2. If a∣c, b∣c and gcd⁡(a,b)=1, then ab∣c.

Facts & Assumptions

Given: Integers a,b,c.

[L3]

Divisibility is reflexive and transitive; if d∣u and d∣v then d∣ux+vy for all x,y; and d∣u implies d∣uw (Divisibility is reflexive and transitive on Z, and is linear: if d∣a and d∣b then d∣ax+by for all integers x,y; also d∣a implies d∣ac, −d∣a and d∣−a).

[L4]

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

[L5]

Z is a commutative ring: addition and multiplication are associative and commutative, x⋅1=x, and multiplication distributes over addition (The integers form a commutative ring, Arithmetic on the integers).

Proof

technique · direct
1.1

Claim 1. Assume gcd⁡(a,b)=1 and a∣bc, and fix x,y with ax+by=1.

L1choose
1.2

Claim 2. Assume a∣c, b∣c and gcd⁡(a,b)=1. Write c=as with s∈Z.

L4choose
2.1

Multiplying ax+by=1 by c gives a(xc)+(bc)y=c, using associativity, commutativity and distributivity.

step 1.1L5
3.1

Now a∣a, hence a∣a(xc) by [L3]; and a∣bc, hence a∣(bc)y by [L3]. Applying linearity to these two with coefficients 1 and 1 gives a∣a(xc)+(bc)y=c.

step 1.1step 2.1L3L5
4.1

Then b∣c=as, and gcd⁡(b,a)=gcd⁡(a,b)=1 by [L2], so claim 1 applied with b, a, s in place of a, b, c gives b∣s.

step 3.1step 1.2L2
5.1

Write s=bt; then c=as=a(bt)=(ab)t, so ab∣c.

step 1.2step 4.1L4L5∎

Remarks

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passverified 2026-08-02 (claude-opus-5)Open item page →

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

Statement

For all a,b,c∈Z,

gcd⁡(ca, cb)  =  ∣c∣ gcd⁡(a,b)

(Common divisor, and the greatest common divisor gcd⁡(a,b), with the convention gcd⁡(0,0):=0, The absolute value ∣a∣ of an integer). The identity is asserted for every triple, including c=0 and (a,b)=(0,0), where both sides are 0.

Facts & Assumptions

Given: Integers a,b,c, and g:=gcd⁡(a,b), h:=gcd⁡(ca,cb).

[L1]

Z is a commutative ring: addition and multiplication are associative and commutative, x⋅0=0, x⋅1=x, x⋅(−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, and positives are closed under multiplication; x<y means x≤y together with x≠y (The integers form a totally ordered ring, Order on the integers).

[L3]

gcd⁡(u,v)≥0 always, with gcd⁡(u,v)≥1 when (u,v)≠(0,0) and gcd⁡(0,0)=0 by convention; 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).

[L9]

A product of two nonzero integers is nonzero (The integers have no zero divisors; multiplicative cancellation).

Proof

technique · cases
1.1

If 0≤u and 0≤v then 0≤uv: for u=0 or v=0 the product is 0, and otherwise 0<u and 0<v, so 0<uv.

L1L2
1.2

Case c=0: then ca=cb=0, so the left side is gcd⁡(0,0)=0; and ∣c∣=∣0∣=0, so the right side is 0⋅g=0.

assume-case zeroL1L3L8
1.3

Case (a,b)=(0,0): then ca=cb=0, so the left side is gcd⁡(0,0)=0; and g=gcd⁡(0,0)=0, so the right side is ∣c∣⋅0=0.

assume-case originL1L3
1.4

Case c≠0 and (a,b)≠(0,0). Then g≥1, and one of a,b is nonzero, say a≠0; so ca≠0 by [L9] and hence (ca,cb)≠(0,0) and h≥1. Also ∣c∣≠0, and ∣c∣ g≠0 by [L9].

assume-case genericL3L8L9
2.1

In the case of step 1.4, ∣c∣ g is a common divisor of ca and cb. Indeed g∣a, say a=ga1; then ca=c g a1, and c is ∣c∣ or −∣c∣ by [L8], so ca=∣c∣ g a1 or ca=∣c∣ g (−a1), and in either case ∣c∣ g∣ca. The same argument with b gives ∣c∣ g∣cb.

step 1.4L1L3L7L8
2.2

Conversely, by [L5] fix x0,y0 with ax0+by0=g; multiplying by c gives (ca)x0+(cb)y0=cg. Since h∣ca and h∣cb, [L6] gives h∣cg; and ∣c∣ g is cg or −cg, because ∣c∣ is c or −c, so h∣∣c∣ g as well.

step 1.4L1L3L5L6L8
3.1

Hence ∣c∣ g∣h by [L4].

step 2.1L4
4.1

Both h and ∣c∣ g are nonzero by step 1.4, and both are nonnegative, h by [L3] and ∣c∣ g by step 1.1 and [L8]. From h∣∣c∣ g and ∣c∣ g≠0, [L7] gives ∣h∣≤∣∣c∣ g∣=∣c∣ g, that is h≤∣c∣ g; from ∣c∣ g∣h and h≠0, [L7] gives ∣c∣ g≤∣h∣=h.

step 1.1step 1.4step 3.1step 2.2L3L7L8
5.1

By antisymmetry h=∣c∣ g in the case of step 1.4.

step 4.1L2
6.1

The three cases of steps 1.2, 1.3 and 1.4 exhaust the possibilities, since either c=0, or (a,b)=(0,0), or neither; so gcd⁡(ca,cb)=∣c∣gcd⁡(a,b) for all a,b,c.

step 1.2step 1.3step 5.1cases-exhaustive∎

Remarks

CorollaryStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-28Open item page →

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

Statement

Let a,b∈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≠0, equivalently (a,b)≠(0,0). Since d∣a and d∣b, there are unique integers, written a/d and b/d, with

a  =  d⋅(a/d),b  =  d⋅(b/d),

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

[L1]

gcd⁡(u,v)≥1 when (u,v)≠(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).

[L3]

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

[L4]
[L6]

Z is a commutative ring with x⋅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)≠(0,0) we have d≥1, so d≠0 and d≥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=da′ and b=db′; each is unique, since da′=da′′ with d≠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⁡(da′,db′)=∣d∣gcd⁡(a′,b′)=d gcd⁡(a′,b′).

step 1.1step 2.1L2
4.1

Also d=d⋅1, so d⋅gcd⁡(a′,b′)=d⋅1 with d≠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≠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⋅x, and lives in Z throughout.

DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (z-ai/glm-5.2)audited 2026-07-28Open item page →

Common multiple, and the least common multiple lcm⁡(a,b), taken to be 0 when a=0 or b=0

Definition

Let a,b∈Z. An integer m is a common multiple of a and b when a∣m and b∣m (Divisibility in Z: d∣a when a=dq for some integer q).

Case a≠0 and b≠0: a least positive common multiple exists. The integer ∣ab∣ is a positive common multiple. It is a common multiple because a∣a gives a∣ab and hence a∣∣ab∣, the last step because ∣ab∣ is ab or −ab (Divisibility is reflexive and transitive on Z, and is linear: if d∣a and d∣b then d∣ax+by for all integers x,y; also d∣a implies d∣ac, −d∣a and d∣−a, The absolute value ∣a∣ of an integer), and symmetrically for b; and it is positive because ab≠0 (The integers have no zero divisors; multiplicative cancellation), so ∣ab∣≥0 and ∣ab∣≠0 (Absolute value in Z: ∣a∣≥0; ∣a∣=0 exactly when a=0; ∣−a∣=∣a∣; ∣ab∣=∣a∣ ∣b∣; −∣a∣≤a≤∣a∣; and ∣a∣≤c exactly when −c≤a≤c). Every positive common multiple is nonnegative, hence of the form ι(k) for a unique k∈N, where ι:N→Z is the embedding of The naturals embed in the integers; so the set

T  :=  { k∈N  :  ι(k) is a positive common multiple of a and b }

is a nonempty subset of N and has a least element k0 (The well-ordering principle). Since ι preserves the order, ι(k0) is then the least positive common multiple of a and b, and we define

lcm⁡(a,b)  :=  ι(k0),

the least positive common multiple. It is unique, greatest and least elements being unique by antisymmetry (The integers form a totally ordered ring, Order on the integers).

Case a=0 or b=0: the only common multiple is 0. Say a=0. Then a∣m reads 0∣m, which holds exactly for m=0 (Divisibility in Z: d∣a when a=dq for some integer q); and 0 is indeed a common multiple, since every integer divides 0. So there is no positive common multiple at all, and we set

lcm⁡(a,b)  :=  0.

This is not a free choice dressed as one: 0 is the only common multiple of the pair, so any other value would name an integer that is not a common multiple.

With both cases together lcm⁡(a,b) is defined for every pair, and lcm⁡(a,b)≥0 always.

Remarks

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-28Open item page →

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

Statement

Let a,b∈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:

  1. every common multiple of a and b is a multiple of ℓ, that is, ℓ∣m whenever a∣m and b∣m;
  2. d⋅ℓ=∣ab∣.

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⋅1=x, x⋅0=0, x⋅(−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≤y together with x≠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≥1 when (a,b)≠(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≠0 then a=da′ and b=db′ 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).

[L11]

A product of two nonzero integers is nonzero, and xz=yz with z≠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 ab=0, so ∣ab∣=0=d⋅0=dℓ: clause 2 holds.

assume-case degenerateL1L3L8L10
1.2

Case a≠0 and b≠0. Then (a,b)≠(0,0), so d≥1; in particular d≠0 and d≥0, so ∣d∣=d. Fix a′,b′ with a=da′, b=db′ 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=da′≠0 and b=db′≠0; hence a′b′≠0, so ∣a′b′∣≥0 and ∣a′b′∣≠0, and M≠0.

step 1.2L1L10L11
3.1

M is a common multiple of a and b. Indeed da′b′=(da′)b′=ab′ and da′b′=(db′)a′=ba′, so a∣da′b′ and b∣da′b′; and M=d∣a′b′∣ equals da′b′ or −(da′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≥1>0 and ∣a′b′∣≥0 with ∣a′b′∣≠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=as=da′s. From b∣m, that is db′∣da′s, we get da′s=db′t for some t, and cancelling d≠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=da′b′u, so da′b′∣m and hence M∣m, because M is da′b′ or −(da′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≠0, so ∣M∣≤∣p∣ by [L9], that is M≤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⋅d ∣a′b′∣=∣d∣ ∣d∣ ∣a′∣ ∣b′∣=∣da′∣ ∣db′∣=∣(da′)(db′)∣=∣ab∣, 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

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-28Open item page →

Every subgroup of (Z,+) is ⟨n⟩=nZ for exactly one natural number n

Statement

Write ι:N→Z for the embedding of The naturals embed in the integers, and for g∈Z put

gZ  :=  { gk  :  k∈Z }.

Then (Z,+,0) is an abelian group (Group and abelian group), gZ is the cyclic subgroup ⟨g⟩ generated by g (The subgroup ⟨S⟩ generated by a subset, the cyclic subgroup ⟨g⟩, and cyclic groups) for every g, and:

every subgroup H≤(Z,+) (Subgroup) equals ι(n)Z=⟨ι(n)⟩ for exactly one natural number n. When H={0} that natural number is 0; otherwise it is the natural number whose image is the least positive element of H.

In particular every subgroup of (Z,+) is cyclic.

Facts & Assumptions

Given: The set Z with the operations of Arithmetic on the integers, and ι(k)=[(k,0)] (The naturals embed in the integers).

[L1]

Z is a commutative ring: addition and multiplication are associative and commutative, x+0=x, x⋅1=x, x⋅0=0, multiplication distributes over addition, and every x has an additive inverse −x, with −(−x)=x and (−x)y=−(xy); we write u−v for u+(−v) (The integers form a commutative ring, Arithmetic on the integers, The integers as equivalence classes of pairs of naturals).

[L2]

The order on Z is total, antisymmetric and transitive, is compatible with addition, and positives are closed under multiplication; x<y means x≤y together with x≠y (The integers form a totally ordered ring, Order on the integers).

[L3]

ι is injective, preserves addition, multiplication and order, and its image is exactly the nonnegative integers; ι(0)=0, ι(1)=1 (The naturals embed in the integers).

[L4]

On N: m<n if and only if σ(m)≤n (Discreteness: σ(n) is the immediate successor); 1=σ(0) (The natural numbers N (von Neumann)); 0≤k for every k (Order on the natural numbers); and every nonempty subset has a least element (The well-ordering principle).

[L5]

A group is a monoid in which every element is invertible; a subgroup is a subset containing the identity and closed under the operation and under inverses, and is itself a group under the restricted operation (Group and abelian group, Subgroup, One-step subgroup test: a nonempty H⊆G is a subgroup iff gh−1∈H for all g,h∈H; the identity and the inverses of H are then those of G).

[L6]

For g in a group, ⟨g⟩ is the smallest subgroup containing g, and ⟨g⟩={ gx:x∈Z } (The subgroup ⟨S⟩ generated by a subset, the cyclic subgroup ⟨g⟩, and cyclic groups, ⟨g⟩={ gn:n∈Z }, and every cyclic group is abelian).

[L7]

Powers are defined by g0=e and gσ(k)=gk⋅g for k∈N, this being the unique function on N with those two properties, and gx=(gk)−1 when x<0 and −x=ι(k) (Powers gn: natural exponents in a monoid and integer exponents in a group, with g0=e, The recursion theorem).

[L8]

For a∈Z and b>0 there are q,r∈Z with a=qb+r and 0≤r<b (Division with remainder in Z: for a∈Z and b>0 there are unique q,r∈Z with a=qb+r and 0≤r<b).

Proof

technique · direct
1.1

(Z,+,0) is an abelian group: addition is an associative and commutative binary operation, 0 is a two-sided identity, and every x has the two-sided inverse −x.

L1L5
1.2

In this group the power gx is the ring product gx. For x=ι(k) with k∈N, the function k↦g ι(k) satisfies g ι(0)=g⋅0=0 and g ι(σ(k))=g(ι(k)+1)=g ι(k)+g, which are exactly the two defining equations of k↦gk written additively; by the uniqueness in [L7] the two functions agree. For x<0, writing −x=ι(k), we get gx=−(gk)=−(g ι(k))=g(−ι(k))=gx.

L1L3L7
1.3

Discreteness: if 0<x in Z then 1≤x. Indeed x≥0, so x=ι(k) with k≠0, hence 0<k and 1=σ(0)≤k in N; applying ι gives 1≤x.

L2L3L4
1.4

Existence, main case. Suppose H≠{0} and pick h∈H with h≠0. Then −h∈H as well, and by totality one of h, −h is positive; so the set P of positive elements of H is nonempty.

L1L2L5
2.1

Hence ⟨g⟩={ gx:x∈Z }={ gk:k∈Z }=gZ for every g∈Z; in particular gZ is a subgroup.

step 1.2L6
2.2

Every element of P is nonnegative, hence of the form ι(k); so T:={ k∈N:ι(k)∈P } is a nonempty subset of N. Let k0 be its least element and put n:=ι(k0)∈P.

step 1.4L3L4choose
2.3

For g>0, g is the least positive element of gZ. Indeed g=g⋅1∈gZ and g>0; and if gk>0 then k>0, since k=0 gives gk=0 and k<0 gives 0<−k, hence 0<g(−k)=−(gk) and so gk<0. Then 1≤k by step 1.3, so 0≤k−1 and 0≤g(k−1)=gk−g, that is g≤gk.

step 1.3L1L2
3.1

Existence, trivial case. If H={0} then H=0Z=⟨0⟩=⟨ι(0)⟩, since 0⋅k=0 for every k.

step 2.1L1L3
3.2

n is the least element of P: for p∈P write p=ι(k) with k∈T; then k0≤k, and applying ι, which preserves the order, gives n≤p.

step 2.2L3
3.3

⟨n⟩⊆H, since n∈H and ⟨n⟩ is the smallest subgroup containing n.

step 2.2L6
3.4

Uniqueness. Suppose ι(m)Z=ι(n)Z=H with m,n∈N. If ι(n)=0 then H={0}, so ι(m)∈H forces ι(m)=0 and hence m=0=n by injectivity. Otherwise ι(n)>0, so H≠{0} and likewise ι(m)>0; by step 2.3 both ι(m) and ι(n) are the least positive element of H, hence equal, and m=n by injectivity.

step 2.3L2L3
4.1

H⊆nZ. Let h∈H. Since n>0, [L8] gives h=qn+r with 0≤r<n. Now qn∈nZ=⟨n⟩⊆H by step 2.1 and step 3.3, so r=h−qn∈H because H is closed under inverses and under addition. If r were positive it would lie in P and satisfy r<n, contradicting step 3.2 together with antisymmetry; so r=0 and h=qn∈nZ.

step 2.1step 3.2step 3.3L1L2L5L8
5.1

Combining, H=nZ=⟨n⟩ with n=ι(k0), which with step 3.1 proves existence for every subgroup.

step 2.1step 3.1step 3.3step 4.1
6.1

Every subgroup of (Z,+) is therefore ⟨ι(n)⟩=ι(n)Z for exactly one n∈N, and in particular is cyclic.

step 5.1step 3.4∎

Remarks

The two are not quite the same statement, and the difference is the whole reason this one is worded as it is. The example asserts that every subgroup is nZ for some n≥0, and adds that n may be taken to be 0 or the least positive element of H; it does not assert that no other n≥0 names the same subgroup. The statement above asserts exactly one, which is strictly stronger. The extra content is small — if aZ=bZ with a,b≥0 then each of a,b divides the other, so a=b — but it is what the uses below actually need, and it is proved here rather than assumed to come with the example.

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passverified 2026-08-02 (claude-opus-5)Open item page →

aZ+bZ=gcd⁡(a,b) Z and aZ∩bZ=lcm⁡(a,b) Z; equivalently, in (Z,+) the subgroup generated by {a,b} is ⟨gcd⁡(a,b)⟩ and ⟨a⟩∩⟨b⟩=⟨lcm⁡(a,b)⟩

Statement

Let a,b∈Z, and put

gZ:={ gk:k∈Z },aZ+bZ:={ ax+by  :  x,y∈Z }.

Then aZ+bZ and aZ∩bZ are subgroups of (Z,+) (Subgroup), and

aZ+bZ  =  gcd⁡(a,b) Z,aZ∩bZ  =  lcm⁡(a,b) Z

(Common divisor, and the greatest common divisor gcd⁡(a,b), with the convention gcd⁡(0,0):=0, Common multiple, and the least common multiple lcm⁡(a,b), taken to be 0 when a=0 or b=0). Equivalently, in the group (Z,+),

⟨{a,b}⟩  =  ⟨gcd⁡(a,b)⟩,⟨a⟩∩⟨b⟩  =  ⟨lcm⁡(a,b)⟩

(The subgroup ⟨S⟩ generated by a subset, the cyclic subgroup ⟨g⟩, and cyclic groups). Since gcd⁡(a,b)≥0 and lcm⁡(a,b)≥0, and every subgroup of (Z,+) has exactly one nonnegative generator (Every subgroup of (Z,+) is ⟨n⟩=nZ for exactly one natural number n), these are identifications of subgroups by their canonical generator, not merely equalities of two sets that happen to coincide.

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+0=x, x⋅1=x, x⋅0=0, multiplication distributes over addition, and every x has an additive inverse; we write u−v for u+(−v) (The integers form a commutative ring, Arithmetic on the integers, The integers as equivalence classes of pairs of naturals).

[L2]

(Z,+,0) is an abelian group; gZ=⟨g⟩ is a subgroup for every g; and every subgroup equals ι(n)Z for exactly one n∈N (Every subgroup of (Z,+) is ⟨n⟩=nZ for exactly one natural number n, Group and abelian group).

[L3]

A subgroup contains the identity and is closed under the operation and under inverses; a nonempty S⊆Z with x−y∈S for all x,y∈S is a subgroup of (Z,+) (Subgroup, One-step subgroup test: a nonempty H⊆G is a subgroup iff gh−1∈H for all g,h∈H; the identity and the inverses of H are then those of G).

[L4]

⟨S⟩ is the smallest subgroup containing S: it contains S and is contained in every subgroup containing S (The subgroup ⟨S⟩ generated by a subset, the cyclic subgroup ⟨g⟩, and cyclic groups).

[L6]

u∣v means v=uk for some k∈Z; equivalently v∈uZ (Divisibility in Z: d∣a when a=dq for some integer q).

[L7]

gcd⁡(a,b)≥0 and is a common divisor of a and b; gcd⁡(0,0)=0 (Common divisor, and the greatest common divisor gcd⁡(a,b), with the convention gcd⁡(0,0):=0).

[L9]
[L11]

The image of ι:N→Z is exactly the set of nonnegative integers, so every x≥0 is ι(n) for a unique n∈N (The naturals embed in the integers).

Proof

technique · direct
1.1

I:=aZ+bZ is a subgroup of (Z,+): it contains 0=a⋅0+b⋅0, so is nonempty, and for ax+by and ax′+by′ in I the difference is a(x−x′)+b(y−y′)∈I by distributivity, so the one-step test applies.

L1L3
1.2

I⊆dZ. Since d is a common divisor, write a=da1 and b=db1; then ax+by=d(a1x+b1y)∈dZ for all x,y.

L1L6L7
1.3

d∈I. If (a,b)≠(0,0) this is [L8]. If (a,b)=(0,0) then d=0=a⋅0+b⋅0∈I. The two cases are exhaustive.

L1L7L8
1.4

aZ∩bZ is a subgroup by [L2] and [L5], and by [L6] it is exactly the set of common multiples of a and b: m∈aZ says a∣m, and m∈bZ says b∣m.

L2L5L6
2.1

I=⟨{a,b}⟩. It contains a=a⋅1+b⋅0 and b=a⋅0+b⋅1, so ⟨{a,b}⟩⊆I by [L4]. Conversely any subgroup H containing a and b contains ⟨a⟩=aZ and ⟨b⟩=bZ by [L2] and [L4], hence contains ax+by for all x,y by closure under the operation; taking H=⟨{a,b}⟩ gives I⊆⟨{a,b}⟩.

step 1.1L1L2L3L4
2.2

Hence dZ=⟨d⟩⊆I, because I is a subgroup containing d and ⟨d⟩ is the smallest such. With step 1.2, I=dZ.

step 1.1step 1.2step 1.3L2L4
2.3

ℓZ⊆aZ∩bZ: ℓ is a common multiple by [L9], so ℓ lies in the subgroup aZ∩bZ, and ℓZ=⟨ℓ⟩ is the smallest subgroup containing ℓ.

step 1.4L2L4L9
3.1

aZ∩bZ⊆ℓZ: every common multiple m satisfies ℓ∣m by [L10], that is m∈ℓZ. With step 2.3, aZ∩bZ=ℓZ.

step 1.4step 2.3L6L10
4.1

Both identities are proved, and in group-theoretic form they read ⟨{a,b}⟩=I=dZ=⟨d⟩ by step 2.1 and step 2.2, and ⟨a⟩∩⟨b⟩=aZ∩bZ=ℓZ=⟨ℓ⟩ by step 3.1 and [L2].

step 2.1step 2.2step 3.1L2
5.1

Finally d≥0 and ℓ≥0, so each is ι(n) for a natural n by [L11], and by [L2] a subgroup of (Z,+) has exactly one such generator; hence d and ℓ are the canonical generators of the two subgroups, and the identities identify the subgroups and not merely the underlying sets.

step 4.1L2L7L9L11∎

Remarks

  • This is the seam between the arithmetic and the group theory of this page, and it is the concrete shadow of the statement that Z is a principal ideal domain. Read from left to right, it says that the set of integer combinations of a and b is exactly the set of multiples of their greatest common divisor — which is Bézout's identity and the divisibility characterisation of gcd⁡ packed into one equation between subgroups.

  • The classification is used for one thing only. Both inclusions above come from Bézout and divisibility; Every subgroup of (Z,+) is ⟨n⟩=nZ for exactly one natural number n is invoked in step 5.1, for the uniqueness of the nonnegative generator, and nowhere else.

  • Boundary pairs. At (a,b)=(0,0) the theorem reads {0}+{0}=0Z={0} and {0}∩{0}=0Z, using gcd⁡(0,0)=0 and lcm⁡(0,0)=0; at a=0 and b≠0 it reads {0}+bZ=∣b∣Z and {0}∩bZ={0}. Both are true as stated, and neither needed a separate clause.

5 · Examples, counterexamples and false statements

None yet.

Sources