Skip to content
Axiomatic Wiki

WLThe embedding preserves and reflects divisibility

Lemma·L76

A natural number divides another exactly when its image is an integer multiple of the other's image.

For , with from D057: divisibility on the left in (D030); that is, divides exactly when is an integer multiple of .
In words
One natural number divides another exactly when the second's integer image is an integer multiple of the first's.
Rests onF02F03F04F05F06F08F09F11F12F13F14A01A02A06A08
Never needed: F10 · A03 · A04 · A05 · A07 · A09 (computed from the citation graph, not asserted).

Proof

  1. 1
    Forward. If in , say with (D030), then (L46); take .
  2. 2
    Backward. Suppose with . If , then , so (L45 (i)), giving (L42); and in (D030, witness ).
  3. 3
    Now let . Since in , L49 gives , so is not negative. By L75, either or for some (with in the latter case).
  4. 4
    In the case : (L45 (ii), L46). Since and , (L18 (i)), so ; then is positive (L49 with L42, as ), making negative (L52): this contradicts not negative.
  5. 5
    Hence , and (L46) gives (L42), that is (D030).
∎

Remarks

The divisibility companion to L46 (which preserves and ) and L49 (which preserves ): carries a faithful copy of the arithmetic of into , divisibility included. It lets a divisibility question about nonnegative integers be answered in with L19 and carried back. This is the bridge used to pull coprimality and unit facts back to in L78 and to count residues in T60.
Wikipedia ↗Int.natCast_dvd_natCast ↗

Used by

L78T60T63
Propose an edit1 published revision