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.
Prime and composite integers: is prime when and its only positive divisors are and
Definition
Let (The integers as equivalence classes of pairs of naturals), ordered as in Order on the integers, with divisibility as in Divisibility in : when for some integer . Then is prime when
In words: exceeds , and its only positive divisors are and . An integer with that is not prime is composite; unfolding the definition, is composite exactly when and has a positive divisor with and .
Numerals. For the symbol inside means , the embedding of The naturals embed in the integers; in particular and are the ring constants of Arithmetic on the integers.
Boundary values, stated rather than assumed. contains (The natural numbers (von Neumann)) and contains , and the negatives, so the small cases are recorded explicitly. The clause decides all of them at once:
- is not prime, since is false, and not composite either, since composite also requires .
- is not prime, since is false. This is decided by the size clause alone and not by counting divisors: every integer divides (Divisibility in : when for some integer ), so the divisor condition is not what rules out.
- Every negative integer is neither prime nor composite, again because fails. So a prime is in particular positive, and , , are not primes in this library, though each is times one.
Thus "prime" and "composite" between them classify exactly the integers greater than , and nothing else.
The same condition read over all divisors. For the following are equivalent:
- the only positive divisors of are and ;
- the only divisors of are , , and .
That 2 implies 1 is immediate, since of those four only and are positive (, so and ). For the converse let . Since we have , so by If and then and ; hence the set of divisors of a nonzero integer is bounded above by ; and , because is or (The absolute value of an integer) and those two divide together (Divisibility is reflexive and transitive on , and is linear: if and then for all integers ; also implies , and ). Also and (Absolute value in : ; exactly when ; ; ; ; and exactly when ), so and clause 1 gives or . If then or , by the case split defining ; and if then for a unit (For integers and the following are equivalent: and ; for a unit ; . Being associates is an equivalence relation whose class of is , is a commutative monoid whose group of units is ; equivalently holds exactly for and ), that is or . Both readings are used below without further comment.
Why is excluded, and it is not a matter of taste. The exclusion is forced by the uniqueness half of 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 , proved on this page: if counted as a prime, a factorisation could be padded with any number of factors , so lists of different lengths would represent the same integer and no permutation could match them. Existence of a factorisation would survive the change; it is uniqueness alone that fixes the convention, and the explicit witness is recorded on the companion page.
Remarks
-
The witness for the exclusion of . The companion page carries it explicitly: If were admitted as a prime, uniqueness would fail: , lists of different lengths that no permutation matches ↗ displays , three lists of lengths , and that no permutation can match.
-
No ring vocabulary is used here, deliberately. In a general commutative ring one distinguishes a prime element from an irreducible element, and in the two notions coincide; that dictionary needs the definition of a ring, which this library develops far above this page, so it is not stated here and nothing below depends on it. What is proved here is the arithmetic content of the coincidence: For an integer : is prime if and only if, for all integers and , implies or shows that for the definition above is equivalent to the property that forces or .
-
Primality is about ; coprimality is about a pair. Coprime integers: is the condition on two integers and needs no primality at all — and are coprime and neither is prime. The bridge in the other direction is For a prime and any integer , is when and otherwise; so makes and coprime, the next item, and it is the only place on this page where primality is converted into coprimality.
Depends on
Divisibility in : when for some integer
Divisibility is reflexive and transitive on , and is linear: if and then for all integers ; also implies , and
If and then and ; hence the set of divisors of a nonzero integer is bounded above by
The absolute value of an integer
Absolute value in : ; exactly when ; ; ; ; and exactly when
For integers and the following are equivalent: and ; for a unit ; . Being associates is an equivalence relation whose class of is
is a commutative monoid whose group of units is ; equivalently holds exactly for and
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 (von Neumann)
The naturals embed in the integers