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

How statement and proof provenance work

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

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

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

If $d \mid a$ and $a \ne 0$ then $d \ne 0$ and $|d| \le |a|$ ; hence the set of divisors of a nonzero integer is bounded above by $|a|$

Statement

Let $a, d \in \mathbb{Z}$ with $d \mid a$ (Divisibility in $\mathbb{Z}$ : $d \mid a$ when $a = dq$ for some integer $q$ ) and $a \ne 0$ . Then $d \ne 0$ and

$|d| \;\le\; |a| .$

Consequently, for $a \ne 0$ the set $\{\, d \in \mathbb{Z} : d \mid a \,\}$ of divisors of $a$ is bounded above by $|a|$ : every divisor $d$ of $a$ satisfies $d \le |a|$ .

Facts & Assumptions

Given: Integers $a$ and $d$ with $a = dq$ for some $q \in \mathbb{Z}$ and $a \ne 0$ ; and the embedding $\iota : \mathbb{N} \to \mathbb{Z}$ , $\iota(k) = [(k,0)]$ , of The naturals embed in the integers.

[L1]

$\mathbb{Z}$ is a commutative ring: addition and multiplication are associative and commutative, $x + 0 = x$ , $x \cdot 1 = x$ , $x \cdot 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 $\mathbb{Z}$ is total, antisymmetric and transitive, is compatible with addition, and positives are closed under multiplication; $x < y$ means $x \le y$ together with $x \ne y$ (The integers form a totally ordered ring, Order on the integers).

[L3]

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

[L4]

On $\mathbb{N}$ : $m < n$ if and only if $\sigma(m) \le n$ (Discreteness: $\sigma(n)$ is the immediate successor); $1 = \sigma(0)$ (The natural numbers $\mathbb{N}$ (von Neumann)); and $0 \le k$ for every $k$ , since $0 + k = k$ (Order on the natural numbers).

[L5]

$|x| \ge 0$ ; $|x| = 0$ exactly when $x = 0$ ; $|xy| = |x|\,|y|$ ; and $x \le |x|$ (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$ , The absolute value $|a|$ of an integer).

[L6]

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

Proof

technique · direct

1.1

Write $a = dq$ . If $d = 0$ then $a = 0 \cdot q = 0$ , and if $q = 0$ then $a = d \cdot 0 = 0$ ; both contradict $a \ne 0$ , so $d \ne 0$ and $q \ne 0$ .

givenL1L6

1.2

If $0 \le u$ and $0 \le v$ then $0 \le 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 $\mathbb{Z}$ : if $0 < x$ then $1 \le x$ . Indeed $x \ge 0$ , so $x = \iota(k)$ for some $k \in \mathbb{N}$ ; $k \ne 0$ because $\iota(0) = 0 \ne x$ ; hence $0 < k$ in $\mathbb{N}$ , so $1 = \sigma(0) \le k$ , and applying $\iota$ , which preserves the order, gives $1 = \iota(1) \le \iota(k) = x$ .

L2L3L4

2.1

$|a| = |d|\,|q|$ , and $|q| > 0$ because $|q| \ge 0$ and $|q| \ne 0$ , the latter since $q \ne 0$ .

step 1.1L5

3.1

Hence $1 \le |q|$ , so $0 \le |q| - 1$ by compatibility of the order with addition.

step 1.3step 2.1L2

4.1

Since $|d| \ge 0$ and $0 \le |q| - 1$ , the product $|d|\,(|q| - 1)$ is nonnegative, and it equals $|d|\,|q| - |d| = |a| - |d|$ by distributivity; adding $|d|$ gives $|d| \le |a|$ .

step 1.2step 2.1step 3.1L1L2L5

5.1

Finally, every divisor $d$ of $a$ satisfies $d \le |d|$ and $|d| \le |a|$ , hence $d \le |a|$ by transitivity: $|a|$ is an upper bound for the set of divisors of $a$ .

step 4.1L2L5∎

Remarks

There is no excluded case at $d = 0$ . The hypothesis is $a \ne 0$ , and the conclusion derives $d \ne 0$ rather than assuming it: $0 \mid a$ forces $a = 0$ (Divisibility in $\mathbb{Z}$ : $d \mid a$ when $a = dq$ for some integer $q$ ), so a zero divisor simply cannot occur under this hypothesis. The statement is therefore not vacuous anywhere, and it is not silently excluding a case.
The hypothesis $a \ne 0$ cannot be dropped. Every integer divides $0$ , so the divisors of $0$ are all of $\mathbb{Z}$ and are bounded neither above nor below. This is exactly why the greatest common divisor of $(0,0)$ has to be fixed by a convention rather than by a maximum (Common divisor, and the greatest common divisor $\gcd(a,b)$ , with the convention $\gcd(0,0) := 0$ ).

Depends on

Used by

Dependency tree · next 3 levels

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

Divisor (Wikipedia) (standard reference, not scraped)

If d∣ad \mid ad∣a and a≠0a \ne 0a=0 then d≠0d \ne 0d=0 and ∣d∣≤∣a∣|d| \le |a|∣d∣≤∣a∣; hence the set of divisors of a nonzero integer is bounded above by ∣a∣|a|∣a∣