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.
Divisibility in : when for some integer
Definition
Let (The integers as equivalence classes of pairs of naturals). We say divides , and write , when
the product being that of Arithmetic on the integers. We write when this fails. In this situation is called a divisor, or a factor, of , and is called a multiple of .
This is the relation the library already has, not a second one. The published Division with remainder in : for and there are unique with and introduces it in its own Statement, in these words: "We say divides , written , when for some ." Since multiplication on is commutative (The integers form a commutative ring), and are the same condition, so the definition above is that relation verbatim and the two usages agree everywhere. The theorem defined it for use on its own page and left the systematic theory to a later page; this is that page, and this item records the agreement rather than introducing a rival notion.
The remainder test. For the same Statement records that holds exactly when the remainder in , , is .
Boundary values. Each is one line from the ring axioms, and each is used below, so all three are recorded here rather than assumed:
- for every integer , including , since ;
- only for , since forces ;
- and for every , since and .
Remarks
-
The remainder test for a negative divisor is Division with remainder for any nonzero divisor: for and there are unique with and , proved next: for every , holds exactly when the remainder in , , is .
-
says a quotient exists; it says nothing on its own about the size or the sign of . Signs are irrelevant to it — , and all hold — and that is Divisibility is reflexive and transitive on , and is linear: if and then for all integers ; also implies , and . The one place where divisibility does constrain size is If and then and ; hence the set of divisors of a nonzero integer is bounded above by , and it needs the hypothesis : without it holds for arbitrarily large .
-
Notation. The bar in is a relation symbol read from left to right: the divisor is on the left. The reversed reading is a common slip, and the two directions are genuinely different, since holds while (by If and then and ; hence the set of divisors of a nonzero integer is bounded above by , with would force ).
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
- Converse of Lagrange for finite abelian groups: every divisor occurs as a subgroup order 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 common divisor of a and b divides gcd(a,b); consequently d = gcd(a,b) exactly when d ≥ 0, d ∣ a, d ∣ b, and every common divisor of a and b divides d — a characterisation that holds at (a,b) = (0,0) as well 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 order of every element of a finite group divides the order of the group 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
- 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
- Associates in ℤ: integers each of which divides the other Definition
- 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
- Congruence modulo an integer: a≡ bpmod n when n∣(a-b), including the moduli 0 and 1 Definition
- Prime and composite integers: p is prime when p > 1 and its only positive divisors are 1 and p Definition
- The divisibility poset of positive integers Definition
- The p-adic valuation vₚ(a) of a nonzero integer: the greatest k ∈ ℕ with pᵏ ∣ a Definition
- 12ℤ + 18ℤ = 6ℤ and 12ℤ ∩ 18ℤ = 36ℤ, the arithmetic of gcd and lcm read off the subgroups of (ℤ,+) 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
- Bézout coefficients are not unique: 1071 · (-3) + 462 · 7 = 21 and 1071 · 19 + 462 · (-44) = 21, and for nonzero a, b every solution has the form (x₀ + t b/d, y₀ - t a/d) Example
- Every positive divisor of the order of a finite cyclic group occurs as the order of a subgroup 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
- gcd at the boundary: gcd(a,0) = |a|, gcd(0,0) = 0, and the convention gcd(0,0) = 0 is exactly what makes gcd(ca,cb) = |c|gcd(a,b) true at c = 0 Example
- gcd(1071, 462) = 21 by the Euclidean algorithm, with the back-substitution giving 21 = 7 · 462 - 3 · 1071 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: n² + n + 41 is prime for every natural number n False statement
- (ℤ, ·, 1) is a commutative monoid whose group of units is {1, -1}; equivalently u ∣ 1 holds exactly for u = 1 and u = -1 Lemma
- a and b are coprime if and only if ax + by = 1 for some integers x, y; and in that case the only common divisors of a and b are 1 and -1 Lemma
- Divisibility is reflexive and transitive on ℤ, and is linear: if d ∣ a and d ∣ b then d ∣ ax + by for all integers x, y; also d ∣ a implies d ∣ ac, -d ∣ a and d ∣ -a Lemma
- Every integer n > 1 has a prime divisor; indeed the least divisor of n that exceeds 1 is prime Lemma
- For a prime p and a nonzero integer a: p^vₚ(a) ∣ a and p^vₚ(a)+1 ∤ a; pᵏ ∣ a holds exactly for k ≤ vₚ(a); vₚ(a) ≥ 1 exactly when p ∣ a; vₚ(1) = vₚ(-1) = 0; and vₚ(p) = 1 Lemma
- For a prime p and any integer a, gcd(p,a) is p when p ∣ a and 1 otherwise; so p ∤ a makes p and a coprime Lemma
- For integers a and b the following are equivalent: a ∣ b and b ∣ a; b = ua for a unit u; |a| = |b|. Being associates is an equivalence relation whose class of a is {a, -a} Lemma
…and 21 more results.
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 39 results over 15 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
- Divisor (Wikipedia) (standard reference, not scraped)