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 is reflexive and transitive on , and is linear: if and then for all integers ; also implies , and
Statement
Let and let be divisibility (Divisibility in : when for some integer ). Then
- reflexivity: ;
- transitivity: and imply ;
- linearity: and imply ; in particular and ;
- implies ;
- implies and .
Consequently the four statements , , and are equivalent.
Facts & Assumptions
Given: Integers .
means for some ; exhibits (Divisibility in : when for some integer ).
is a commutative ring: addition and multiplication are 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).
Proof
Reflexivity: , so .
Transitivity: suppose and . Then by associativity, so .
Linearity: suppose and . Then by associativity, commutativity and distributivity, so .
Clause 4: suppose . Then , so .
Clause 5: suppose . Then , so ; and , so .
The two special cases in clause 3: taking gives , and taking , gives .
The four equivalent forms: clause 5 gives and ; applying each to in place of , or to in place of , and using , gives the reverse implications, so all four statements are equivalent.
Clauses 1 to 5 and the two consequences are established.
Remarks
-
Linearity is the workhorse of the whole page. Every later argument that a common divisor of and divides some combination of them — Bézout's identity, the Euclidean step, the coprimality criterion — is clause 3 applied once.
-
Divisibility ignores signs, and that is why can be normalised. Clause 5 says the divisors of and of are the same set, so holds exactly when , whichever of the two values takes (The absolute value of an integer). That is the observation behind in is symmetric and unchanged by signs: ; moreover , , , and unless .