Skip to content
Axiomatic Wiki
Lemma·L19

Basic laws of divisibility

Reflexivity, transitivity, sums, differences, and a size bound.

For all , with from D030:(i) ;(ii) ;(iii) ;(iv) ;(v) ;(vi) ;(vii) .
In words
Every number divides itself; one divides everything; everything divides zero; divisibility chains compose; a common divisor of two numbers divides their sum; a divisor of a number and of a sum containing it divides the other summand; and a divisor of a non-zero number cannot exceed it.
Rests onF02F03F04F06F08F09F11F12F14A01A06A08
Never needed: F05 · F10 · F13 · A02 · A03 · A04 · A05 · A07 (computed from the citation graph, not asserted).

Proof

  1. 1
    (i) Witness : indeed by D028, D027 and Claim A of L09. So and .
  2. 2
    (ii) Witness : by commutativity and the computation of (i).
  3. 3
    (iii) Witness : by D028.
  4. 4
    (iv) Say and (D030). Then by associativity, so with witness .
  5. 5
    (v) Say , . Then by distributivity read right to left.
  6. 6
    (vi) Say and . If : then and (Claim A of L11), so by Claim A of L09, and by (iii). Now let . First, : otherwise by L18 (ii), while by L17 (i); chaining gives (L15 (ii), handling the case by substitutivity), contradicting irreflexivity (L15 (i)). So by L16, or . If : then , so by cancellation, and (iii) applies. If : L17 (ii) gives with ; then by distributivity, so by cancellation: .
  7. 7
    (vii) Say with . Then , else . By L15 (vii), ; so by D028 and commutativity, whence by L17 (i).
∎

Remarks

Part (vi) is subtraction-free subtraction: from and one recovers without ever forming , which does not offer. It is the pivot of Euclid's theorem: a prime dividing both and would divide . Part (vii) turns divisibility into a size statement and, with trichotomy, powers the descent in L20.
Wikipedia ↗Nat.dvd_add ↗

Used by

L20L21L40T11T19
Propose an edit2 published revisions