CorollaryStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (z-ai/glm-5.2)audited 2026-07-28

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Division with remainder for any nonzero divisor: for $a \in \mathbb{Z}$ and $b \ne 0$ there are unique $q, r \in \mathbb{Z}$ with $a = qb + r$ and $0 \le r < |b|$

Statement

Let $a, b \in \mathbb{Z}$ with $b \ne 0$ . Then there is exactly one pair $(q,r)$ of integers with

$a \;=\; qb + r, \qquad 0 \le r < |b|,$

the absolute value being that of The absolute value $|a|$ of an integer. Moreover $b \mid a$ (Divisibility in $\mathbb{Z}$ : $d \mid a$ when $a = dq$ for some integer $q$ ) holds exactly when $r = 0$ .

Facts & Assumptions

Given: Integers $a$ and $b$ with $b \ne 0$ .

[L1]

For $a \in \mathbb{Z}$ and $b' > 0$ there is exactly one pair $(Q,r)$ of integers with $a = Q b' + r$ and $0 \le r < b'$ (Division with remainder in $\mathbb{Z}$ : for $a \in \mathbb{Z}$ and $b > 0$ there are unique $q, r \in \mathbb{Z}$ with $a = qb + r$ and $0 \le r < b$ ).

[L2]

$\mathbb{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$ , with $-(-x) = x$ and $(-x)(-y) = xy$ (The integers form a commutative ring, Arithmetic on the integers).

[L3]

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

[L4]

$|x| = x$ when $x \ge 0$ and $|x| = -x$ when $x \le 0$ (The absolute value $|a|$ of an integer); $|x| \ge 0$ , and $|x| = 0$ exactly when $x = 0$ (Absolute value in $\mathbb{Z}$ : $|a| \ge 0$ ; $|a| = 0$ exactly when $a = 0$ ; $|-a| = |a|$ ; $|ab| = |a|\,|b|$ ; $-|a| \le a \le |a|$ ; and $|a| \le c$ exactly when $-c \le a \le c$ ).

[L5]

$b \mid a$ means $a = bs$ for some $s \in \mathbb{Z}$ (Divisibility in $\mathbb{Z}$ : $d \mid a$ when $a = dq$ for some integer $q$ ).

Proof

technique · cases

1.1

$0 < |b|$ : indeed $|b| \ge 0$ , and $|b| \ne 0$ because $b \ne 0$ .

L4given

1.2

Case $b > 0$ : put $\varepsilon := 1$ . Then $|b| = b$ , so $\varepsilon |b| = b$ , and $\varepsilon^{2} = 1$ .

assume-case posL2L4

1.3

Case $b < 0$ : put $\varepsilon := -1$ . Then $|b| = -b$ , so $\varepsilon |b| = -(-b) = b$ , and $\varepsilon^{2} = (-1)(-1) = 1$ .

assume-case negL2L4

2.1

Since $b \ne 0$ , totality gives $0 \le b$ or $b \le 0$ , hence $b > 0$ or $b < 0$ ; so in either case there is an integer $\varepsilon$ with $b = \varepsilon|b|$ and $\varepsilon^{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 \le r < |b|$ .

step 1.1L1

3.1

Existence. Put $q := \varepsilon Q$ . Then $qb = \varepsilon Q \cdot \varepsilon |b| = \varepsilon^{2} Q |b| = Q|b|$ , so $a = qb + r$ with $0 \le r < |b|$ .

step 2.1step 2.2L2

3.2

Uniqueness. Suppose $a = q_1 b + r_1 = q_2 b + r_2$ with $0 \le r_i < |b|$ for $i = 1, 2$ . Since $b = \varepsilon|b|$ , this reads $a = (\varepsilon q_1)|b| + r_1 = (\varepsilon q_2)|b| + r_2$ , two representations of the form required by [L1] for the divisor $|b|$ ; hence $\varepsilon q_1 = \varepsilon q_2$ and $r_1 = r_2$ . Multiplying the first equation by $\varepsilon$ and using $\varepsilon^{2} = 1$ gives $q_1 = q_2$ .

step 2.1step 2.2L1L2

4.1

The remainder test. If $r = 0$ then $a = qb$ , so $b \mid a$ . Conversely, if $b \mid a$ , say $a = bs$ , then $a = sb + 0$ and $0 \le 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 $\mathbb{Z}$ : for $a \in \mathbb{Z}$ and $b > 0$ there are unique $q, r \in \mathbb{Z}$ with $a = qb + r$ and $0 \le r < b$ is stated for a positive divisor, and its own Remarks record that "the version for $b \ne 0$ , with $0 \le r < |b|$ , follows once absolute values are in hand". Absolute values on $\mathbb{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 \cdot (-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 \le r$ excludes. The clause $0 \le r < |b|$ is the one every use below makes, and no other convention is introduced anywhere on this page.

Depends on

Used by

The integers are a Euclidean domain with Euclidean function δ(b)=|b| Example

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 43 results over 16 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

Euclidean division (Wikipedia) (standard reference, not scraped)

Division with remainder for any nonzero divisor: for a∈Za \in \mathbb{Z}a∈Z and b≠0b \ne 0b=0 there are unique q,r∈Zq, r \in \mathbb{Z}q,r∈Z with a=qb+ra = qb + ra=qb+r and 0≤r<∣b∣0 \le r < |b|0≤r<∣b∣