LemmaStatement: 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.

A nonempty set of integers bounded above has a greatest element, and a nonempty set of integers bounded below has a least element

Statement

Let $S \subseteq Z$ be nonempty. Call $b \in Z$ an upper bound for $S$ when $s \leq b$ for every $s \in S$ , and a lower bound when $b \leq s$ for every $s \in S$ ; call $m$ a greatest element of $S$ when $m \in S$ and $s \leq m$ for every $s \in S$ , and a least element when $m \in S$ and $m \leq s$ for every $s \in S$ .

If $S$ has an upper bound, it has a greatest element. If $S$ has a lower bound, it has a least element. In each case the element is unique.

Facts & Assumptions

Given: A nonempty $S \subseteq Z$ , and the embedding $ι : N \to Z$ , $ι (k) = [(k, 0)]$ , of The naturals embed in the integers.

[L1]

$Z$ is a commutative ring: addition is associative and commutative, $x + 0 = x$ , and every $x$ has an additive inverse $- x$ , with $- (- x) = x$ ; we write $u - v$ for $u + (- v)$ (The integers form a commutative ring, Arithmetic on the integers, The integers as equivalence classes of pairs of naturals).

[L2]

The order on $Z$ is total, antisymmetric and transitive, and is compatible with addition: $x \leq y$ implies $x + z \leq y + z$ (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, so every $x \geq 0$ is $ι (k)$ for a unique $k \in N$ (The naturals embed in the integers, The natural numbers $N$ (von Neumann)).

[L4]

Every nonempty subset of $N$ has a least element (The well-ordering principle, Order on the natural numbers).

Proof

technique · direct

1.1

Suppose $b$ is an upper bound for $S$ . For every $s \in S$ we have $s \leq b$ , and adding $- s$ gives $0 \leq b - s$ ; so $b - s$ is nonnegative and therefore equals $ι (k)$ for a unique $k \in N$ .

givenL1L2L3

1.2

Now suppose instead that $c$ is a lower bound for $S$ , and put $S^{'} : = {- s : s \in S}$ , a nonempty subset of $Z$ . For $s \in S$ , adding $- s - c$ to $c \leq s$ gives $- s \leq - c$ , so $- c$ is an upper bound for $S^{'}$ .

givenL1L2

2.1

Put $T : = {k \in N : b - ι (k) \in S}$ . It is nonempty: choosing $s \in S$ and the $k$ of step 1.1 with $ι (k) = b - s$ , we get $b - ι (k) = b - (b - s) = s \in S$ , so $k \in T$ .

step 1.1L1given

3.1

By well-ordering let $k_{0}$ be the least element of $T$ , and put $m : = b - ι (k_{0})$ , so that $m \in S$ .

step 2.1L4choose

4.1

Let $s \in S$ . By step 1.1 there is $k \in N$ with $ι (k) = b - s$ , and then $b - ι (k) = s \in S$ , so $k \in T$ and hence $k_{0} \leq k$ .

step 1.1step 2.1step 3.1L1

5.1

Applying $ι$ , which preserves the order, gives $ι (k_{0}) \leq ι (k) = b - s$ ; adding $s - ι (k_{0})$ to this inequality gives $s \leq b - ι (k_{0}) = m$ .

step 3.1step 4.1L1L2L3

6.1

So $m \in S$ and $s \leq m$ for every $s \in S$ : $m$ is a greatest element of $S$ . If $m^{'}$ were another one, then $m \leq m^{'}$ and $m^{'} \leq m$ , so $m = m^{'}$ by antisymmetry.

step 3.1step 5.1L2

7.1

By the first part $S^{'}$ has a greatest element, which has the form $- ℓ$ with $ℓ \in S$ ; then for every $s \in S$ we have $- s \leq - ℓ$ , and adding $s + ℓ$ gives $ℓ \leq s$ . So $ℓ$ is a least element of $S$ , and it is unique by antisymmetry as in step 6.1.

step 6.1step 1.2L1L2∎

Remarks

Why this has to be proved rather than quoted. The well-ordering principle (The well-ordering principle) gives a least element of a nonempty set of naturals. What the greatest common divisor needs is a greatest element of a set of integers bounded above, and neither the direction nor the ambient set matches. The bridge is the reflection $k \mapsto b - ι (k)$ , which turns "large elements of $S$ below $b$ " into "small naturals".
Both hypotheses are needed. $Z$ itself is nonempty and has no greatest element, and $\emptyset$ is bounded above by every integer and has no greatest element because it has no element at all. The first of these is exactly what makes the common divisors of $(0, 0)$ have no greatest element (The common divisors of $(0, 0)$ are all of $Z$ and have no greatest element in the order of $Z$ , so $\gcd (0, 0)$ cannot be defined as a maximum and is fixed by convention ↗).

Depends on

Used by

Dependency tree · two levels

33 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

Well-ordering principle (Wikipedia) (standard reference, not scraped)
Sets of integers bounded above have a largest element (Millersville University number theory notes) (standard reference, not scraped)