Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-generatedprecheck 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∣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

Depends on

Used by

Dependency tree · two levels

36 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