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

Every integer $n \geq 1$ is a finite product of primes: there are $r \in N$ and a list $p : r \to Z$ of primes with $n = \prod_{i < r} p_{i}$ , the case $n = 1$ being the empty product

Statement

Write finite products in the commutative monoid $(Z, \cdot, 1)$ of $(Z, \cdot, 1)$ is a commutative monoid whose group of units is ${1, - 1}$ ; equivalently $u ∣ 1$ holds exactly for $u = 1$ and $u = - 1$ , as in The product $g_{0} g_{1} \dots g_{n - 1}$ of a finite list in a monoid, by recursion, with the empty product ( $n = 0$ ) equal to the identity; a list of primes of length $r$ means a function $p : r \to Z$ on the von Neumann natural $r = {0, \dots, r - 1}$ with every $p_{i}$ prime (Prime and composite integers: $p$ is prime when $p > 1$ and its only positive divisors are $1$ and $p$ ).

Existence. For every $n \in Z$ with $n \geq 1$ there are $r \in N$ and a list $p : r \to Z$ of primes with

$n = \prod_{i < r} p_{i} .$

At $n = 1$ this holds with $r = 0$ : the empty product is $1$ , so $1$ is a product of primes, of no primes at all, and needs no separate clause.
Every such product is at least $1$ . Conversely, for every $r \in N$ and every list $p : r \to Z$ of primes, $\prod_{i < r} p_{i} \geq 1$ . So the integers of clause 1 are exactly the values of finite products of primes.

Facts & Assumptions

Given: The commutative monoid $(Z, \cdot, 1)$ ( $(Z, \cdot, 1)$ is a commutative monoid whose group of units is ${1, - 1}$ ; equivalently $u ∣ 1$ holds exactly for $u = 1$ and $u = - 1$ , Semigroup and monoid); the embedding $ι : N \to Z$ of The naturals embed in the integers; and the property $P (k)$ : "if $ι (k) \geq 1$ then $ι (k) = \prod_{i < r} p_{i}$ for some $r \in N$ and some list $p : r \to Z$ of primes".

[L1]

$\prod_{i < 0} g_{i} = e$ and $\prod_{i < σ (r)} g_{i} = (\prod_{i < r} g_{i}) \cdot g_{r}$ ; the value depends only on $g_{0}, \dots, g_{r - 1}$ , so a list $u : r \to M$ determines $\prod_{i < r} u_{i}$ (The product $g_{0} g_{1} \dots g_{n - 1}$ of a finite list in a monoid, by recursion, with the empty product ( $n = 0$ ) equal to the identity).

[L2]

Every integer $n > 1$ has a prime divisor (Every integer $n > 1$ has a prime divisor; indeed the least divisor of $n$ that exceeds $1$ is prime, Divisibility in $Z$ : $d ∣ a$ when $a = d q$ for some integer $q$ ).

[L3]

Strong induction: if for every $k$ the truth of $P$ below $k$ implies $P (k)$ , then $P$ holds everywhere on $N$ (Strong (complete) induction).

[L4]

Induction: a subset of $N$ containing $0$ and closed under $σ$ is $N$ (The principle of mathematical induction).

[L5]

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

[L6]

Every prime satisfies $p > 1$ (Prime and composite integers: $p$ is prime when $p > 1$ and its only positive divisors are $1$ and $p$ ).

[L7]

The order on $Z$ is total, antisymmetric and transitive, is compatible with addition, and positives are closed under multiplication (The integers form a totally ordered ring, Order on the integers).

[L8]

$Z$ is a commutative ring: multiplication is associative and commutative, $x \cdot 1 = x$ , $x \cdot 0 = 0$ , multiplication distributes over addition, and every $x$ has an additive inverse $- x$ , with $- (- x) = x$ and $(- x) y = - (x y)$ ; we write $u - v$ for $u + (- v)$ (The integers form a commutative ring, Arithmetic on the integers).

[L9]

On $N$ : $0 \leq k$ for every $k$ (Order on the natural numbers); $m < k$ exactly when $σ (m) \leq k$ (Discreteness: $σ (n)$ is the immediate successor); $1 = σ (0)$ (The natural numbers $N$ (von Neumann)); and $r < σ (r)$ , with $i < σ (r)$ exactly when $i \leq r$ (On $N$ the order is membership: $m < n ⟺ m \in n$ ).

[L10]

$d ∣ u$ means $u = d q$ for some $q \in Z$ (Divisibility in $Z$ : $d ∣ a$ when $a = d q$ for some integer $q$ , Divisibility is reflexive and transitive on $Z$ , and is linear: if $d ∣ a$ and $d ∣ b$ then $d ∣ a x + b y$ for all integers $x, y$ ; also $d ∣ a$ implies $d ∣ a c$ , $- d ∣ a$ and $d ∣ - a$ ).

Proof

technique · induction

1.1

$0 < 1$ in $Z$ : $1 = ι (1)$ lies in the image of $ι$ , so $1 \geq 0$ , and $1 \neq 0$ because $ι$ is injective and $ι (0) = 0$ .

1.2

Discreteness: if $x \in Z$ and $0 < x$ then $1 \leq x$ . Indeed $x \geq 0$ , so $x = ι (k)$ for some $k$ ; $k \neq 0$ since $ι (0) = 0 \neq x$ ; so $0 < k$ in $N$ , hence $1 = σ (0) \leq k$ , and applying the order-preserving $ι$ gives $1 \leq x$ .

L5L9

1.3

Let $k \in N$ and assume $P (j)$ for every $j < k$ .

2.1

Clause 2. Let $T$ be the set of $r \in N$ such that $\prod_{i < r} p_{i} \geq 1$ for every list $p : r \to Z$ of primes. Then $0 \in T$ , the empty product being $1$ . If $r \in T$ and $p : σ (r) \to Z$ is a list of primes, then $\prod_{i < σ (r)} p_{i} = (\prod_{i < r} p_{i}) p_{r}$ , where the restriction of $p$ to $r$ is again a list of primes, so the first factor is $\geq 1 > 0$ ; and $p_{r} > 1 > 0$ ; positives being closed under multiplication the product is $> 0$ , hence $\geq 1$ by step 1.2. So $σ (r) \in T$ , and $T = N$ .

step 1.1step 1.2L1L4L6L7

2.2

$P (0)$ holds vacuously: $ι (0) = 0$ and $0 \geq 1$ is false, since $0 < 1$ .

basestep 1.1L5

2.3

Suppose $ι (k) \geq 1$ and write $n : = ι (k)$ ; by totality either $n = 1$ or $n > 1$ . If $n = 1$ , take $r : = 0$ : the empty list is a list of primes and $\prod_{i < 0} p_{i} = 1 = n$ , so $P (k)$ holds.

step 1.1L1L7

3.1

Suppose instead $n > 1$ . Fix a prime $q$ with $q ∣ n$ and an integer $m$ with $n = q m$ .

step 2.3L2L10choose

4.1

$m > 0$ : $m = 0$ would give $n = q \cdot 0 = 0 < 1$ , and $m < 0$ would give $- m > 0$ , hence $q (- m) > 0$ , that is $- n > 0$ and $n < 0 < 1$ ; both contradict $n \geq 1$ . So $m > 0$ and therefore $m \geq 1$ by step 1.2.

step 1.1step 1.2step 3.1L7L8

5.1

$m < n$ : since $q > 1$ we have $q - 1 > 0$ , and $m > 0$ , so $(q - 1) m > 0$ ; and $(q - 1) m = q m - m = n - m$ , whence $n - m > 0$ and $m < n$ .

step 3.1step 4.1L6L7L8

6.1

As $m \geq 1 > 0$ , write $m = ι (j)$ with $j \in N$ . Then $j < k$ : otherwise $k \leq j$ , and $ι$ preserving the order would give $n = ι (k) \leq ι (j) = m$ , contradicting step 5.1.

step 4.1step 5.1L5L7

7.1

By step 1.3 applied to $j$ there are $s \in N$ and a list $p : s \to Z$ of primes with $m = \prod_{i < s} p_{i}$ .

step 1.3step 4.1step 6.1

8.1

Define $p^{'} : σ (s) \to Z$ by $p_{i}^{'} : = p_{i}$ for $i < s$ and $p_{s}^{'} : = q$ ; every value is prime, and $\prod_{i < σ (s)} p_{i}^{'} = (\prod_{i < s} p_{i}^{'}) \cdot p_{s}^{'} = m q = q m = n$ , the middle equality because the product over $i < s$ depends only on $p_{0}^{'}, \dots, p_{s - 1}^{'}$ , which agree with $p$ . So $P (k)$ holds with $r : = σ (s)$ .

step 3.1step 7.1L1L8L9

9.1

Steps 2.3 and 8.1 cover the two possibilities for $n$ , so $P (k)$ follows from the truth of $P$ below $k$ ; with step 2.2 as the case $k = 0$ , strong induction gives $P (k)$ for every $k \in N$ .

step 2.2step 2.3step 8.1L3

10.1

Finally, any $n \geq 1$ satisfies $n > 0$ , so $n = ι (k)$ for some $k \in N$ , and $P (k)$ is clause 1 for that $n$ ; clause 2 is step 2.1.

step 1.1step 2.1step 9.1L5L7discharge-induction∎

Remarks

$1$ is a product of primes here, and this is not a dodge. The empty product is the identity of the monoid by The product $g_{0} g_{1} \dots g_{n - 1}$ of a finite list in a monoid, by recursion, with the empty product ( $n = 0$ ) equal to the identity, so $r = 0$ gives the value $1$ exactly. Excluding $n = 1$ and starting at $n \geq 2$ would force a special case into every later statement, including The fundamental theorem of arithmetic: every integer $n \geq 1$ is a product of primes, and the factorisation is unique up to order — if $\prod_{i < r} p_{i} = \prod_{j < s} q_{j}$ with every $p_{i}$ and $q_{j}$ prime, then $r = s$ and $q_{i} = p_{π (i)}$ for some $π \in Sym (r)$ , whose uniqueness clause at $r = 0$ is precisely the assertion that only the empty list represents $1$ .
Uniqueness is a separate theorem and is not proved here. Existence needs only a least prime divisor and a descent; uniqueness needs Euclid's lemma. In the multiplicative monoid $H = {1, 4, 7, 10, \dots}$ of positive integers one more than a multiple of $3$ , the element $100$ has two genuinely different factorisations into irreducibles, $4 \cdot 25$ and $10 \cdot 10$ ↗ on the companion page exhibits a setting where the existence half holds and the uniqueness half fails, which is what shows the two halves are genuinely independent.
The list is appended to, not prepended to. The successor clause of The product $g_{0} g_{1} \dots g_{n - 1}$ of a finite list in a monoid, by recursion, with the empty product ( $n = 0$ ) equal to the identity multiplies on the right, so putting the new prime $q$ at position $s$ costs nothing, whereas putting it at position $0$ would need the splitting law of Generalised associativity: in a monoid the product of a finite list does not depend on the bracketing, and in a commutative monoid it does not depend on the order of the factors either. Order is irrelevant to the value, by the commutative clause of that theorem, so nothing is lost.

Depends on

Used by

Dependency tree · two levels

59 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

Fundamental theorem of arithmetic (Wikipedia) (standard reference, not scraped)
Number Theory: In Context — Fundamental Theorem of Arithmetic (standard reference, not scraped)

Every integer n≥1n≥1 is a finite product of primes: there are r∈Nr∈N and a list p:r→Zp:r→Z of primes with n=∏i<rpin=∏i<r​pi​, the case n=1n=1 being the empty product