DefinitionDefinition: AI-adaptedProof: Not applicableSession-authored (Fable 5 assisted)audited 2026-07-24
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.
Order on the integers
Definition
For integers and (The integers as equivalence classes of pairs of naturals) define
Write when and . An integer is positive when ; on representatives, exactly when .
Remarks
- The defining inequality is "" restated without subtraction.
- Well-definedness, totality, and compatibility with the arithmetic are proved in The integers form a totally ordered ring ↗.
Depends on
Used by
- A rational root of xᵏ = m is an integer: if k ≥ 1, m ∈ ℤ, x ∈ ℚ and xᵏ is the image of m, then x is the image of an integer Corollary
- Division with remainder for any nonzero divisor: for a ∈ ℤ and b ≠ 0 there are unique q, r ∈ ℤ with a = qb + r and 0 ≤ r < |b| Corollary
- 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
- For an integer p > 1: p is prime if and only if, for all integers a and b, p ∣ ab implies p ∣ a or p ∣ b Corollary
- If a prime p divides a finite product ∏_i<n aᵢ of integers then p ∣ aᵢ for some i < n; at n = 0 the product is 1 and the hypothesis cannot hold Corollary
- If d = gcd(a,b) is nonzero then a/d and b/d are coprime Corollary
- The extended Euclidean algorithm: the same descent produces integers x, y with ax + by = gcd(a,b), so Bézout coefficients are computed and not merely shown to exist Corollary
- 2ℤ is closed under addition, negation and multiplication and is not a subring of ℤ, because it does not contain 1 Counterexample
- 6 ∣ 4 · 9 while 6 ∤ 4 and 6 ∤ 9: dividing a product does not force dividing a factor, and the coprimality hypothesis is what fails Counterexample
- A nonempty subset of a group closed under the operation need not be a subgroup: the nonnegative integers inside (ℤ, +) Counterexample
- 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
- The common divisors of (0,0) are all of ℤ and have no greatest element in the order of ℤ, so gcd(0,0) cannot be defined as a maximum and is fixed by convention Counterexample
- Common divisor, and the greatest common divisor gcd(a,b), with the convention gcd(0,0) := 0 Definition
- Common multiple, and the least common multiple lcm(a,b), taken to be 0 when a = 0 or b = 0 Definition
- Order on the rationals Definition
- Ordered ring: a ring with a total order compatible with addition and with positives closed under multiplication Definition
- Powers gⁿ: natural exponents in a monoid and integer exponents in a group, with g⁰ = e Definition
- Prime and composite integers: p is prime when p > 1 and its only positive divisors are 1 and p Definition
- The absolute value |a| of an integer Definition
- The formal Laurent series ℝ((t⁻¹)): support bounded below, valuation, leading coefficient Definition
- The p-adic valuation vₚ(a) of a nonzero integer: the greatest k ∈ ℕ with pᵏ ∣ a Definition
- (ℤ, +) is an abelian group, (ℤ, ·) is a commutative monoid that is not a group, and its group of units is {1, -1} Example
- 2 is prime, and it is the only even prime: every even integer n > 2 is composite Example
- 360 = 2³ · 3² · 5 and 84 = 2² · 3 · 7, with gcd(360,84) = 12 and lcm(360,84) = 2520 read off the exponents Example
- ax + by = c has an integer solution exactly when gcd(a,b) ∣ c: 6x + 15y = 9 is solvable and 6x + 15y = 7 is not Example
- Consecutive Fibonacci numbers are coprime, and for every m ∈ ℕ the Euclidean algorithm on (Fₘ₊₃, Fₘ₊₂) takes exactly m+1 divisions, with quotient 1 in the first m of them and quotient 2 in the last Example
- For every n ∈ ℕ there are n consecutive composite integers: with N := ∏_j<n(j+2), each of N+2, …, N+n+1 is composite Example
- For n ≥ 1 the congruence classes modulo n form an abelian group (ℤ/n, +) of order n, generated by the class of 1 Example
- gcd(1071, 462) = 21 by the Euclidean algorithm, with the back-substitution giving 21 = 7 · 462 - 3 · 1071 Example
- No rational squares to 3 or to 6, and none cubes to 2: three instances of the rational-root corollary Example
- nℤ is a subgroup of (ℤ, +) for every n ∈ ℤ, and every subgroup of (ℤ, +) has this form Example
- ℤ is a commutative ring and an ordered ring, the published construction being an instance of the general definitions Example
- ℤ is an integral domain of characteristic 0 whose group of units is {1,-1}, so it is not a field: 2 is nonzero and not invertible Example
- ℤ sits inside ℚ as a subring that is not a subfield, so the inverse-closure clause of the subfield definition is doing work Example
- FALSE: every Fermat number 2^2ⁿ + 1 is prime False statement
- FALSE: For all integers a and b, gcd(a,b) · lcm(a,b) = ab False statement
- FALSE: for every finite list p₀, …, pₙ₋₁ of distinct primes, p₀ ⋯ pₙ₋₁ + 1 is prime False statement
- FALSE: In every commutative ring, each nonzero element is either a unit or a zero divisor False statement
- FALSE: n² + n + 41 is prime for every natural number n False statement
…and 41 more results.
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 10 results over 7 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
- T. Tao, Analysis I, 3rd ed., §4.1 (standard reference, not scraped)
- Integer — construction from pairs of naturals (Wikipedia) (standard reference, not scraped)