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

How statement and proof provenance work

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

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

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

Division with remainder for any nonzero divisor: for $a \in Z$ and $b \neq 0$ there are unique $q, r \in Z$ with $a = q b + r$ and $0 \leq r < ∣ b ∣$

Statement

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

$a = q b + r, 0 \leq 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 = d q$ for some integer $q$ ) holds exactly when $r = 0$ .

Facts & Assumptions

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

[L1]

For $a \in Z$ and $b^{'} > 0$ there is exactly one pair $(Q, r)$ of integers with $a = Q b^{'} + r$ and $0 \leq r < b^{'}$ (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$ ).

[L2]

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

[L3]

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

[L4]

$∣ x ∣ = x$ when $x \geq 0$ and $∣ x ∣ = - x$ when $x \leq 0$ (The absolute value $∣ a ∣$ of an integer); $∣ x ∣ \geq 0$ , and $∣ x ∣ = 0$ exactly when $x = 0$ (Absolute value in $Z$ : $∣ a ∣ \geq 0$ ; $∣ a ∣ = 0$ exactly when $a = 0$ ; $∣ - a ∣ = ∣ a ∣$ ; $∣ a b ∣ = ∣ a ∣ ∣ b ∣$ ; $- ∣ a ∣ \leq a \leq ∣ a ∣$ ; and $∣ a ∣ \leq c$ exactly when $- c \leq a \leq c$ ).

[L5]

$b ∣ a$ means $a = b s$ for some $s \in Z$ (Divisibility in $Z$ : $d ∣ a$ when $a = d q$ for some integer $q$ ).

Proof

technique · cases

1.1

$0 < ∣ b ∣$ : indeed $∣ b ∣ \geq 0$ , and $∣ b ∣ \neq 0$ because $b \neq 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 \neq 0$ , totality gives $0 \leq b$ or $b \leq 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 \leq r < ∣ b ∣$ .

step 1.1L1

3.1

Existence. Put $q : = ε Q$ . Then $q b = ε Q \cdot ε ∣ b ∣ = ε^{2} Q ∣ b ∣ = Q ∣ b ∣$ , so $a = q b + r$ with $0 \leq r < ∣ b ∣$ .

step 2.1step 2.2L2

3.2

Uniqueness. Suppose $a = q_{1} b + r_{1} = q_{2} b + r_{2}$ with $0 \leq r_{i} < ∣ b ∣$ for $i = 1, 2$ . Since $b = ε ∣ b ∣$ , this reads $a = (ε q_{1}) ∣ b ∣ + r_{1} = (ε q_{2}) ∣ b ∣ + r_{2}$ , two representations of the form required by [L1] for the divisor $∣ b ∣$ ; hence $ε q_{1} = ε q_{2}$ and $r_{1} = r_{2}$ . Multiplying the first equation by $ε$ and using $ε^{2} = 1$ gives $q_{1} = q_{2}$ .

step 2.1step 2.2L1L2

4.1

The remainder test. If $r = 0$ then $a = q b$ , so $b ∣ a$ . Conversely, if $b ∣ a$ , say $a = b s$ , then $a = s b + 0$ and $0 \leq 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 \in Z$ and $b > 0$ there are unique $q, r \in Z$ with $a = q b + r$ and $0 \leq r < b$ is stated for a positive divisor, and its own Remarks record that "the version for $b \neq 0$ , with $0 \leq 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 \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 \leq r$ excludes. The clause $0 \leq r < ∣ b ∣$ is the one every use below makes, and no other convention is introduced anywhere on this page.

Depends on

Used by

Dependency tree · two levels

29 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)

Division with remainder for any nonzero divisor: 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<∣b∣0≤r<∣b∣