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 is a finite product of primes: there are and a list of primes with , the case being the empty product
Statement
Write finite products in the commutative monoid of is a commutative monoid whose group of units is ; equivalently holds exactly for and , as in The product of a finite list in a monoid, by recursion, with the empty product () equal to the identity; a list of primes of length means a function on the von Neumann natural with every prime (Prime and composite integers: is prime when and its only positive divisors are and ).
-
Existence. For every with there are and a list of primes with
At this holds with : the empty product is , so is a product of primes, of no primes at all, and needs no separate clause.
-
Every such product is at least . Conversely, for every and every list of primes, . So the integers of clause 1 are exactly the values of finite products of primes.
Facts & Assumptions
Given: The commutative monoid ( is a commutative monoid whose group of units is ; equivalently holds exactly for and , Semigroup and monoid); the embedding of The naturals embed in the integers; and the property : "if then for some and some list of primes".
and ; the value depends only on , so a list determines (The product of a finite list in a monoid, by recursion, with the empty product () equal to the identity).
Every integer has a prime divisor (Every integer has a prime divisor; indeed the least divisor of that exceeds is prime, Divisibility in : when for some integer ).
Strong induction: if for every the truth of below implies , then holds everywhere on (Strong (complete) induction).
Induction: a subset of containing and closed under is (The principle of mathematical induction).
is injective, preserves addition, multiplication and order, and its image is exactly the nonnegative integers, with and (The naturals embed in the integers, The integers as equivalence classes of pairs of naturals).
Every prime satisfies (Prime and composite integers: is prime when and its only positive divisors are and ).
The order on 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).
is a commutative ring: multiplication is associative and commutative, , , multiplication distributes over addition, and every has an additive inverse , with and ; we write for (The integers form a commutative ring, Arithmetic on the integers).
On : for every (Order on the natural numbers); exactly when (Discreteness: is the immediate successor); (The natural numbers (von Neumann)); and , with exactly when (On the order is membership: ).
Proof
in : lies in the image of , so , and because is injective and .
Discreteness: if and then . Indeed , so for some ; since ; so in , hence , and applying the order-preserving gives .
Let and assume for every .
Clause 2. Let be the set of such that for every list of primes. Then , the empty product being . If and is a list of primes, then , where the restriction of to is again a list of primes, so the first factor is ; and ; positives being closed under multiplication the product is , hence by step 1.2. So , and .
holds vacuously: and is false, since .
Suppose and write ; by totality either or . If , take : the empty list is a list of primes and , so holds.
Suppose instead . Fix a prime with and an integer with .
: would give , and would give , hence , that is and ; both contradict . So and therefore by step 1.2.
: since we have , and , so ; and , whence and .
As , write with . Then : otherwise , and preserving the order would give , contradicting step 5.1.
By step 1.3 applied to there are and a list of primes with .
Define by for and ; every value is prime, and , the middle equality because the product over depends only on , which agree with . So holds with .
Steps 2.3 and 8.1 cover the two possibilities for , so follows from the truth of below ; with step 2.2 as the case , strong induction gives for every .
Finally, any satisfies , so for some , and is clause 1 for that ; clause 2 is step 2.1.
Remarks
-
is a product of primes here, and this is not a dodge. The empty product is the identity of the monoid by The product of a finite list in a monoid, by recursion, with the empty product () equal to the identity, so gives the value exactly. Excluding and starting at would force a special case into every later statement, including The fundamental theorem of arithmetic: every integer is a product of primes, and the factorisation is unique up to order — if with every and prime, then and for some , whose uniqueness clause at is precisely the assertion that only the empty list represents .
-
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 of positive integers one more than a multiple of , the element has two genuinely different factorisations into irreducibles, and ↗ 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 of a finite list in a monoid, by recursion, with the empty product () equal to the identity multiplies on the right, so putting the new prime at position costs nothing, whereas putting it at position 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
- Every integer $n > 1$ has a prime divisor; indeed the least divisor of $n$ that exceeds $1$ is prime
- Prime and composite integers: $p$ is prime when $p > 1$ and its only positive divisors are $1$ and $p$
- Semigroup and monoid
- $(\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$
- The product $g_0 g_1 \cdots g_{n-1}$ of a finite list in a monoid, by recursion, with the empty product ($n = 0$) equal to the identity
- Strong (complete) induction
- The principle of mathematical induction
- On $\mathbb{N}$ the order is membership: $m < n \iff m \in n$
- Divisibility in $\mathbb{Z}$: $d \mid a$ when $a = dq$ for some integer $q$
- 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$
- The integers as equivalence classes of pairs of naturals
- Arithmetic on the integers
- Order on the integers
- The integers form a commutative ring
- The integers form a totally ordered ring
- The natural numbers $\mathbb{N}$ (von Neumann)
- Order on the natural numbers
- The naturals embed in the integers
- Discreteness: $\sigma(n)$ is the immediate successor
Used by
- Every nonzero integer n is u ∏_i<r pᵢ with u ∈ {1,-1} and every pᵢ prime; u and r are determined by n, and the list is determined up to a permutation Corollary
- If 1 were admitted as a prime, uniqueness would fail: 6 = 2 · 3 = 1 · 2 · 3 = 1 · 1 · 2 · 3, lists of different lengths that no permutation matches Counterexample
- In the multiplicative monoid H = {1, 4, 7, 10, …} of positive integers one more than a multiple of 3, the element 100 has two genuinely different factorisations into irreducibles, 4 · 25 and 10 · 10 Counterexample
- 360 = 2³ · 3² · 5 and 84 = 2² · 3 · 7, with gcd(360,84) = 12 and lcm(360,84) = 2520 read off the exponents Example
- Euclid's theorem: for every n ∈ ℕ and every list p : n → ℤ of primes there is a prime not among p₀, …, pₙ₋₁; consequently the set of primes is not finite Theorem
- The fundamental theorem of arithmetic: every integer n ≥ 1 is a product of primes, and the factorisation is unique up to order — if ∏_i<r pᵢ = ∏_j<s qⱼ with every pᵢ and qⱼ prime, then r = s and qᵢ = p_π(i) for some π ∈ Sym(r) Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 74 results over 25 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)
- Number Theory: In Context — Fundamental Theorem of Arithmetic (standard reference, not scraped)