LemmaStatement: AI-adaptedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passverified 2026-08-03 (gpt-5.6-sol-codex-subscription)

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.

Every integer $n > 1$ has a prime divisor; indeed the least divisor of $n$ that exceeds $1$ is prime

Statement

Let $n \in \mathbb{Z}$ with $n > 1$ , and put

$S \;:=\; \{\, d \in \mathbb{Z} \;:\; d \mid n \ \text{ and } \ d > 1 \,\}$

(Divisibility in $\mathbb{Z}$ : $d \mid a$ when $a = dq$ for some integer $q$ ). Then $S$ is nonempty and has a least element $q$ , and $q$ is prime (Prime and composite integers: $p$ is prime when $p > 1$ and its only positive divisors are $1$ and $p$ ). In particular every integer greater than $1$ has a prime divisor.

Facts & Assumptions

Given: An integer $n$ with $n > 1$ , and the set $S$ above.

[L2]

Divisibility is reflexive and transitive (Divisibility is reflexive and transitive on $\mathbb{Z}$ , and is linear: if $d \mid a$ and $d \mid b$ then $d \mid ax + by$ for all integers $x, y$ ; also $d \mid a$ implies $d \mid ac$ , $-d \mid a$ and $d \mid -a$ ).

[L3]

A nonempty set of integers with a lower bound has a unique least element (A nonempty set of integers bounded above has a greatest element, and a nonempty set of integers bounded below has a least element).

[L4]

If $d \mid u$ and $u \ne 0$ then $d \ne 0$ and $|d| \le |u|$ (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|$ ).

[L5]

$p$ is prime exactly when $p > 1$ and every positive divisor of $p$ is $1$ or $p$ (Prime and composite integers: $p$ is prime when $p > 1$ and its only positive divisors are $1$ and $p$ ).

[L6]

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

[L8]

The embedding $\iota : \mathbb{N} \to \mathbb{Z}$ is injective, preserves addition and order, and has as image exactly the nonnegative integers, with $\iota(0) = 0$ and $\iota(1) = 1$ (The naturals embed in the integers).

[L9]

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

[L10]

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

Proof

technique · direct

1.1

$0 < 1$ in $\mathbb{Z}$ : $1 = \iota(1)$ lies in the image of $\iota$ , so $1 \ge 0$ , and $1 \ne 0$ because $\iota$ is injective and $\iota(0) = 0$ .

1.2

Discreteness: if $x \in \mathbb{Z}$ and $0 < x$ then $1 \le x$ . Indeed $x \ge 0$ , so $x = \iota(k)$ for some $k \in \mathbb{N}$ ; $k \ne 0$ since $\iota(0) = 0 \ne x$ ; hence $0 < k$ in $\mathbb{N}$ , so $1 = \sigma(0) \le k$ , and applying the order-preserving $\iota$ gives $1 = \iota(1) \le \iota(k) = x$ .

L8L9

1.3

$n \in S$ , since $n \mid n$ and $n > 1$ ; so $S$ is nonempty.

1.4

$1$ is a lower bound for $S$ : every $d \in S$ satisfies $d > 1$ , hence $1 \le d$ .

2.1

By [L3] the set $S$ has a unique least element $q$ : that is, $q \mid n$ , $q > 1$ , and $q \le d$ for every $d \in S$ .

step 1.3step 1.4L3

3.1

$n > 1 > 0$ and $q > 1 > 0$ , so $n \ne 0$ and $q \ne 0$ , and $|q| = q$ .

step 1.1step 2.1L6L10

3.2

Let $e$ be a positive divisor of $q$ with $e \ne 1$ . Then $1 \le e$ by step 1.2, and $e \ne 1$ , so $e > 1$ .

step 1.2step 2.1L6

4.1

Also $e \mid q$ and $q \mid n$ , so $e \mid n$ by transitivity; with $e > 1$ this gives $e \in S$ , hence $q \le e$ .

step 2.1step 3.2L2

5.1

On the other hand $e \mid q$ with $q \ne 0$ gives $|e| \le |q| = q$ , and $|e| = e$ because $e > 0$ ; so $e \le q$ . With step 4.1 and antisymmetry, $e = q$ .

step 3.1step 3.2step 4.1L4L6L10

6.1

So every positive divisor of $q$ is $1$ or $q$ , and $q > 1$ : $q$ is prime. Since $q \mid n$ , the integer $n$ has a prime divisor.

step 2.1step 3.2step 5.1L5∎

Remarks

Well-ordering is used through the integer bridge, not directly. The well-ordering principle gives a least element of a nonempty subset of $\mathbb{N}$ , whereas $S$ is a set of integers. A nonempty set of integers bounded above has a greatest element, and a nonempty set of integers bounded below has a least element is the published lemma that crosses that gap, and its Statement covers the lower-bound case explicitly, so it is what this proof cites.
The bound $q$ is genuinely the least divisor above $1$ , not merely some prime divisor. That is what makes the argument work: minimality is the only reason $q$ has no proper divisor above $1$ , since any such divisor would divide $n$ as well and be smaller.
The hypothesis $n > 1$ cannot be dropped. At $n = 1$ the set $S$ is empty, since $d \mid 1$ forces $d = 1$ or $d = -1$ ( $(\mathbb{Z}, \cdot, 1)$ is a commutative monoid whose group of units is $\{1, -1\}$ ; equivalently $u \mid 1$ holds exactly for $u = 1$ and $u = -1$ ) and neither exceeds $1$ ; so $1$ has no prime divisor, which is exactly why the empty product is the right factorisation of $1$ in Every integer $n \ge 1$ is a finite product of primes: there are $r \in \mathbb{N}$ and a list $p : r \to \mathbb{Z}$ of primes with $n = \prod_{i<r} p_i$ , the case $n = 1$ being the empty product. At $n = 0$ every integer divides $0$ , so $S$ is the whole set of integers greater than $1$ ; it does have a least element, namely $2$ , but a statement about the divisors of $0$ is of no use below and the lemma is not claimed there.

Depends on

Used by

Dependency tree · next 3 levels

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

Fundamental theorem of arithmetic (Wikipedia) (standard reference, not scraped)
Janssen and Lindsey, Rings with Inquiry: Primes and Factorization (standard reference, not scraped)

Every integer n>1n > 1n>1 has a prime divisor; indeed the least divisor of nnn that exceeds 111 is prime