TheoremStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27

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.

Division with remainder in $Z$ : for $a \in Z$ and $b > 0$ there are unique $q, r \in Z$ with $a = q b + r$ and $0 \leq r < b$

Statement

Let $a, b \in Z$ (The integers as equivalence classes of pairs of naturals) with $b > 0$ . Then there exist integers $q$ and $r$ with

$a = q b + r, 0 \leq r < b,$

and the pair $(q, r)$ with these two properties is unique.

We say $b$ divides $a$ , written $b ∣ a$ , when $a = q b$ for some $q \in Z$ ; by the above, for $b > 0$ this holds exactly when the remainder $r$ is $0$ .

Facts & Assumptions

Given: Integers $a$ and $b$ with $b > 0$ , and the embedding $ι : N \to 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 \cdot 1 = x$ , 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 ( $x \leq y$ implies $x + z \leq y + z$ ), and positives are closed under multiplication ( $0 < x$ and $0 < y$ imply $0 < 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, Arithmetic on the integers).

[L4]

Every nonempty subset of $N$ has a least element (The well-ordering principle).

[L5]

On $N$ : every $k \neq 0$ is a successor $σ (j)$ (Every nonzero natural number is a successor); $σ (j) = j + 1 = 1 + j$ (The natural numbers $N$ (von Neumann), Addition is commutative); $m \leq n$ means $m + t = n$ for some $t \in N$ (Order on the natural numbers); and exactly one of $m < n$ , $m = n$ , $n < m$ holds (Trichotomy of the order on $N$ ).

Proof

technique · direct

1.1

Sums and products of nonnegative integers are nonnegative: if $0 \leq u$ and $0 \leq v$ then $u \leq u + v$ by compatibility with addition, so $0 \leq u + v$ by transitivity; and if either factor is $0$ then $u v = 0$ , while if both are positive then $0 < u v$ .

L1L2

1.2

Discreteness: if $0 < x$ in $Z$ then $1 \leq x$ . Indeed $x$ is nonnegative, so $x = ι (k)$ for some $k \in N$ , and $k \neq 0$ because $ι (0) = 0 \neq x$ ; hence $k = σ (j) = 1 + j$ for some $j$ , so $1 \leq k$ in $N$ , and applying $ι$ , which preserves the order, gives $1 = ι (1) \leq ι (k) = x$ .

L3L5

1.3

$ι$ reflects the order: if $ι (m) < ι (n)$ then $m < n$ . For otherwise trichotomy on $N$ gives $n \leq m$ , whence $ι (n) \leq ι (m)$ because $ι$ preserves the order, and this together with $ι (m) < ι (n)$ contradicts antisymmetry.

L2L3L5

1.4

Write $a = ι (a_{1}) - ι (a_{2})$ with $a_{1}, a_{2} \in N$ , which is possible because $a = [(a_{1}, a_{2})]$ for some naturals and $[(a_{1}, a_{2})] = [(a_{1}, 0)] + [(0, a_{2})] = ι (a_{1}) - ι (a_{2})$ .

L1L3given

1.5

Uniqueness. Suppose $a = q_{1} b + r_{1} = q_{2} b + r_{2}$ with $0 \leq r_{i} < b$ for $i = 1, 2$ , and set $d : = q_{1} - q_{2}$ . Ring arithmetic gives $d b = r_{2} - r_{1}$ .

L1given

2.1

From $0 < b$ and step 1.2, $1 \leq b$ , so $0 \leq b - 1$ by compatibility with addition.

step 1.2L1L2

2.2

Put $q_{0} : = - ι (a_{2})$ . Then $a - q_{0} b = a + ι (a_{2}) b = (ι (a_{1}) - ι (a_{2})) + ι (a_{2}) b = ι (a_{1}) + ι (a_{2}) (b - 1)$ , by ring arithmetic.

step 1.4L1

2.3

If $0 < d$ then $1 \leq d$ by step 1.2, so $0 \leq d - 1$ and hence $0 \leq (d - 1) b$ by step 1.1, that is $b \leq d b$ ; but $r_{1} \geq 0$ gives $r_{2} - r_{1} \leq r_{2} < b$ , so $b \leq d b = r_{2} - r_{1} < b$ , contradicting antisymmetry.

step 1.1step 1.2step 1.5L1L2

2.4

If $d < 0$ then $0 < - d$ , and the same computation with the roles of the two pairs interchanged, using $(- d) b = r_{1} - r_{2}$ , gives $b \leq r_{1} - r_{2} < b$ , again a contradiction.

step 1.1step 1.2step 1.5L1L2

3.1

The integer $a - q_{0} b$ is nonnegative: $ι (a_{1}) \geq 0$ and $ι (a_{2}) \geq 0$ because both lie in the image of $ι$ , $b - 1 \geq 0$ by step 2.1, and sums and products of nonnegative integers are nonnegative.

step 1.1step 2.1step 2.2L3

3.2

Hence $d = 0$ by totality, so $q_{1} = q_{2}$ , and then $r_{1} = a - q_{1} b = a - q_{2} b = r_{2}$ .

step 1.5step 2.3step 2.4L1L2

4.1

Hence the set $T : = {k \in N : ι (k) = a - q b for some q \in Z}$ is nonempty, since $a - q_{0} b$ is a nonnegative integer and therefore equals $ι (k)$ for some $k \in N$ .

step 3.1L3

5.1

By well-ordering let $r_{0}$ be the least element of $T$ , choose $q \in Z$ with $ι (r_{0}) = a - q b$ , and set $r : = ι (r_{0})$ . Then $a = q b + r$ and $0 \leq r$ .

step 4.1L1L3L4choose

6.1

Suppose $b \leq r$ . Then $0 \leq r - b$ by compatibility with addition, and $r - b = (a - q b) - b = a - (q + 1) b$ by ring arithmetic, so $r - b = ι (k^{'})$ for some $k^{'} \in N$ with $k^{'} \in T$ . Also $- b < 0$ , since $0 < b$ , so $r - b < r$ , that is $ι (k^{'}) < ι (r_{0})$ , whence $k^{'} < r_{0}$ by step 1.3. This contradicts the minimality of $r_{0}$ .

step 1.3step 5.1L1L2L3given

7.1

Therefore $b \leq r$ fails, and by totality of the order $r < b$ ; with step 5.1 this establishes existence of a pair $(q, r)$ with $a = q b + r$ and $0 \leq r < b$ .

step 5.1step 6.1L2

8.1

Existence is step 7.1 and uniqueness is step 3.2, so for every $a \in Z$ and every $b > 0$ there is exactly one pair $(q, r)$ of integers with $a = q b + r$ and $0 \leq r < b$ .

step 7.1step 3.2∎

Remarks

Stated for a positive divisor only. Nothing here needs an absolute value on $Z$ , and none is available at this point in the reading order. The version for $b \neq 0$ , with $0 \leq r < ∣ b ∣$ , follows once absolute values are in hand and is not needed by anything on this page.
Why it is proved here. The characterisation of the order of an element, $g^{k} = e$ exactly when $ord (g)$ divides $k$ , and the count $∣ ⟨ g ⟩ ∣ = ord (g)$ , are both unprovable without division with remainder (If $ord (g) = n$ then $g^{k} = e$ iff $k$ is an integer multiple of $n$ , the powers $g^{0}, \dots, g^{n - 1}$ are distinct, and $⟨ g ⟩$ has exactly $n$ elements; if $g$ has infinite order then $g^{j} = g^{k}$ only for $j = k$ ). No earlier page in the library supplies it.
This is not a theory of divisibility. The relation $b ∣ a$ is defined here for use on this page and its companion; greatest common divisors, primes and unique factorisation are developed on a later page, and that page must record that its general divisibility in a ring restricts on $Z$ to the relation defined here, rather than introduce a second notion silently.
A published claim this theorem falsified. A published example on the metric spaces companion page used to record in its Remarks that this library had no divisibility theory at all in which to state or prove Euclid's lemma. That was true when it was written; the present item, which is earlier in the reading order, made it false, and the sentence has since been narrowed to say that the example itself neither establishes nor assumes that lemma. Nothing here depends on that example, and nothing here supplies Euclid's lemma either: what is proved above is division with remainder, and no more.

Depends on

Used by

Dependency tree · two levels

35 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Euclidean division (Wikipedia) (standard reference, not scraped)
T. Tao, Analysis I, 3rd ed., §4.1 (the integers) (standard reference, not scraped)

Division with remainder in ZZ: for a∈Za∈Z and b>0b>0 there are unique q,r∈Zq,r∈Z with a=qb+ra=qb+r and 0≤r<b0≤r<b