TheoremStatement: AI-adaptedProof: AI-generatedprecheck 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.

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)$

Statement

Finite products are taken 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, and a list of primes of length $r$ is 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. Every $n \in Z$ with $n \geq 1$ is $\prod_{i < r} p_{i}$ for some $r \in N$ and some list $p$ of primes of length $r$ (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).
Uniqueness up to order. Let $p$ and $q$ be lists of primes, of lengths $r$ and $s$ . If

$\prod_{i < r} p_{i} = \prod_{j < s} q_{j},$

then $r = s$ , and there is a permutation $π \in Sym (r)$ (The symmetric group $Sym (X)$ : the bijections of a set $X$ under composition) with

$q_{i} = p_{π (i)} for every i < r .$

At $r = 0$ clause 2 says that the only list of primes whose product is $1$ is the empty list, and the permutation condition is vacuous.

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); and the property $U (r)$ : "for every $s \in N$ and all lists $p$ , $q$ of primes of lengths $r$ and $s$ with $\prod_{i < r} p_{i} = \prod_{j < s} q_{j}$ , one has $r = s$ and $q_{i} = p_{π (i)}$ for all $i < r$ , for some $π \in Sym (r)$ ".

[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}$ (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]

Commutative case of generalised associativity: for a commutative monoid, $n \in N$ , $π \in Sym (n)$ and $h$ with $h_{i} = g_{π (i)}$ for $i < n$ , one has $\prod_{i < n} h_{i} = \prod_{i < n} g_{i}$ (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).

[L3]

If a prime $u$ divides $\prod_{j < s} q_{j}$ then $u ∣ q_{k}$ for some $k < s$ (If a prime $p$ divides a finite product $\prod_{i < n} a_{i}$ of integers then $p ∣ a_{i}$ for some $i < n$ ; at $n = 0$ the product is $1$ and the hypothesis cannot hold, Euclid's lemma: if $p$ is prime and $p ∣ a b$ then $p ∣ a$ or $p ∣ b$ ).

[L4]

Every prime $u$ satisfies $u > 1$ , and every positive divisor of a prime $w$ is $1$ or $w$ (Prime and composite integers: $p$ is prime when $p > 1$ and its only positive divisors are $1$ and $p$ ).

[L5]

$u ∣ 1$ exactly when $u = 1$ or $u = - 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$ ); $d ∣ v$ means $v = d c$ for some $c$ (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$ ).

[L6]

If $x z = y z$ and $z \neq 0$ then $x = y$ (The integers have no zero divisors; multiplicative cancellation).

[L7]

$Sym (X)$ is the set of bijections $X \to X$ under composition, with identity ${i d}_{X}$ ; it is closed under composition, and for $a \neq b$ in $X$ the transposition $(a b)$ is a permutation of $X$ with $(a b) \circ (a b) = {i d}_{X}$ (The symmetric group $Sym (X)$ : the bijections of a set $X$ under composition, $Sym (X)$ is a group under composition, and it is non-abelian whenever $X$ has at least three distinct elements, Injection, surjection, bijection).

[L8]

Induction on $N$ (The principle of mathematical induction).

[L9]

On $N$ : $n = {m : m < n}$ , $σ (n) = n \cup {n}$ , $n < σ (n)$ , $m < σ (n)$ exactly when $m \leq n$ , and $n \notin n$ (On $N$ the order is membership: $m < n ⟺ m \in n$ , The natural numbers $N$ (von Neumann)).

[L10]

Every natural number other than $0$ is a successor (Every nonzero natural number is a successor).

[L11]

The order on $Z$ is total, antisymmetric and transitive and is compatible with addition; $Z$ is a commutative ring (The integers form a totally ordered ring, Order on the integers, The integers form a commutative ring, Arithmetic on the integers, The integers as equivalence classes of pairs of naturals).

[L12]

$ι : N \to Z$ is injective, preserves the order, and has as image the nonnegative integers, with $ι (0) = 0$ , $ι (1) = 1$ (The naturals embed in the integers).

Proof

technique · induction

1.1

$0 < 1$ : $1 = ι (1)$ is nonnegative and differs from $0 = ι (0)$ by injectivity of $ι$ . Hence every prime $u$ satisfies $u > 1 > 0$ , so $u \neq 0$ , $u \neq 1$ and, adding $- 1$ to $0 < 1$ , also $u \neq - 1$ .

L4L11L12

1.2

If $q$ is a list of primes of length $s \neq 0$ then $q_{t} ∣ \prod_{j < s} q_{j}$ , where $s = σ (t)$ : indeed the product equals $(\prod_{j < t} q_{j}) q_{t}$ .

L1L5L10

1.3

Let $r \in N$ and assume $U (r)$ .

1.4

Let $p$ be a list of primes of length $σ (r)$ and $q$ one of length $s$ , with $N : = \prod_{i < σ (r)} p_{i} = \prod_{j < s} q_{j}$ . Then $N = (\prod_{i < r} p_{i}) p_{r}$ , so $p_{r} ∣ N$ .

L1L5

2.1

A prime never divides $1$ : $u ∣ 1$ would force $u = 1$ or $u = - 1$ , both excluded by step 1.1.

step 1.1L5

2.2

By [L3] there is $k < s$ with $p_{r} ∣ q_{k}$ . Since $p_{r} > 1 > 0$ , $p_{r}$ is a positive divisor of the prime $q_{k}$ other than $1$ , so $p_{r} = q_{k}$ .

step 1.1step 1.4L3L4

3.1

$U (0)$ holds. Let $q$ be a list of primes of length $s$ with $\prod_{i < 0} p_{i} = \prod_{j < s} q_{j}$ , so $\prod_{j < s} q_{j} = 1$ . If $s \neq 0$ , then $s = σ (t)$ and step 1.2 gives $q_{t} ∣ 1$ , contradicting step 2.1; so $s = 0$ . Then $r = s = 0$ , ${i d}_{\emptyset} \in Sym (0)$ since $0 = \emptyset$ , and the condition " $q_{i} = p_{π (i)}$ for all $i < 0$ " is vacuous.

basestep 2.1step 1.2L1L7L9

3.2

$s \neq 0$ : otherwise $N = 1$ and $p_{r} ∣ 1$ , contradicting step 2.1. Write $s = σ (t)$ .

step 2.1step 1.4L1L10

4.1

Define $τ \in Sym (s)$ by $τ : = {i d}_{s}$ if $k = t$ and $τ : = (k t)$ otherwise; in both cases $τ$ is a permutation of $s$ with $τ \circ τ = {i d}_{s}$ and $τ (t) = k$ . Note $t < s$ and $k < s$ , so both lie in $s$ .

step 3.2step 2.2L7L9construct

5.1

Put $q_{j}^{'} : = q_{τ (j)}$ for $j < s$ ; every $q_{j}^{'}$ is prime, and $\prod_{j < s} q_{j}^{'} = \prod_{j < s} q_{j} = N$ by the commutative clause [L2], the monoid $(Z, \cdot, 1)$ being commutative.

step 4.1L2

6.1

Also $q_{t}^{'} = q_{τ (t)} = q_{k} = p_{r}$ , so $N = \prod_{j < σ (t)} q_{j}^{'} = (\prod_{j < t} q_{j}^{'}) q_{t}^{'} = (\prod_{j < t} q_{j}^{'}) p_{r}$ .

step 2.2step 4.1step 5.1L1

7.1

Comparing with step 1.4, $(\prod_{i < r} p_{i}) p_{r} = (\prod_{j < t} q_{j}^{'}) p_{r}$ , and $p_{r} \neq 0$ by step 1.1, so cancellation gives $\prod_{i < r} p_{i} = \prod_{j < t} q_{j}^{'}$ .

step 1.1step 1.4step 6.1L6

8.1

The restrictions of $p$ to $r$ and of $q^{'}$ to $t$ are lists of primes of lengths $r$ and $t$ , and their products are the two sides of step 7.1, since a finite product depends only on the entries it names. So $U (r)$ applies: $r = t$ , hence $s = σ (t) = σ (r)$ , and there is $ρ \in Sym (r)$ with $q_{i}^{'} = p_{ρ (i)}$ for every $i < r$ .

step 1.3step 7.1L1

9.1

Define $\hat{ρ} : σ (r) \to σ (r)$ by $\hat{ρ} (i) : = ρ (i)$ for $i < r$ and $\hat{ρ} (r) : = r$ . Since $σ (r) = r \cup {r}$ with $r \notin r$ , and $ρ$ is a bijection of $r$ , the map $\hat{ρ}$ is a bijection of $σ (r)$ , that is $\hat{ρ} \in Sym (σ (r))$ .

step 8.1L7L9construct

10.1

Put $π : = \hat{ρ} \circ τ$ , a permutation of $s = σ (r)$ because $Sym (σ (r))$ is closed under composition.

step 4.1step 8.1step 9.1L7

11.1

For $i < σ (r)$ we get $q_{i} = q_{τ (τ (i))} = q_{τ (i)}^{'}$ . If $τ (i) < r$ then $q_{τ (i)}^{'} = p_{ρ (τ (i))} = p_{\hat{ρ} (τ (i))} = p_{π (i)}$ ; and if $τ (i) = r = t$ then $q_{τ (i)}^{'} = q_{t}^{'} = p_{r} = p_{\hat{ρ} (r)} = p_{π (i)}$ . Since $τ (i) < σ (r)$ these two possibilities are exhaustive, so $q_{i} = p_{π (i)}$ throughout.

step 4.1step 6.1step 8.1step 9.1step 10.1L9

12.1

Steps 8.1 and 11.1 give $s = σ (r)$ and a permutation $π \in Sym (σ (r))$ with $q_{i} = p_{π (i)}$ for all $i < σ (r)$ , so $U (σ (r))$ holds; with step 3.1 as base, induction gives $U (r)$ for every $r \in N$ , which is clause 2. Clause 1 is 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.

step 3.1step 8.1step 11.1L8discharge-induction∎

Remarks

"Unique up to order" is spelt out, not gestured at. The symmetric group $Sym (X)$ : the bijections of a set $X$ under composition is available at this point in the library, so the uniqueness clause names a permutation $π$ of the von Neumann natural $r$ and asserts an equality for every index, rather than saying the two factorisations "agree up to rearrangement". The letter $π$ is used because $σ$ is already the successor function on $N$ throughout this library.
The theorem is stated for $n \geq 1$ . It is not stated for $n \geq 2$ , which would exclude the empty product and gain nothing, and it is not stated for all nonzero $n$ , which is false as it stands because a negative integer is not a product of primes. The signed form is Every nonzero integer $n$ is $u \prod_{i < r} p_{i}$ with $u \in {1, - 1}$ and every $p_{i}$ prime; $u$ and $r$ are determined by $n$ , and the list is determined up to a permutation, where the sign is carried by a unit.
Where each hypothesis is used. Primality of $p_{r}$ lets If a prime $p$ divides a finite product $\prod_{i < n} a_{i}$ of integers then $p ∣ a_{i}$ for some $i < n$ ; at $n = 0$ the product is $1$ and the hypothesis cannot hold supply the index $k$ , and also makes $p_{r}$ a nonzero factor different from $1$ . Primality of the selected $q_{k}$ is then used separately in step 2.2: the positive divisor $p_{r} ∣ q_{k}$ , being different from $1$ , must equal $q_{k}$ . Drop Euclid's lemma and the argument collapses before that comparison — 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$ ↗ is the witness.
Reading the theorem by exponents. Collecting equal primes turns clause 2 into For $n \geq 1$ and any injective list $p : r \to Z$ of primes containing every prime divisor of $n$ , one has $n = \prod_{i < r} p_{i}^{v_{p_{i}} (n)}$ ; the exponents are determined by $n$ , and $v_{q} (n) = 0$ for every prime $q$ outside the list, which records the multiplicity of each prime as its $p$ -adic valuation. That is the same theorem in different notation, not a further result.

Depends on

Used by

Dependency tree · two levels

69 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)
Inquiry into Advanced Algebra: Division, primes, and factorisation (standard reference, not scraped)

The fundamental theorem of arithmetic: every integer n≥1n≥1 is a product of primes, and the factorisation is unique up to order — if ∏i<rpi=∏j<sqj∏i<r​pi​=∏j<s​qj​ with every pipi​ and qjqj​ prime, then r=sr=s and qi=pπ(i)qi​=pπ(i)​ for some π∈Sym⁡(r)π∈Sym(r)