Skip to content
Axiomatic Wiki

WLThe division algorithm for the integers

Lemma·L77

Every integer leaves a natural remainder below n when divided by a positive n.

For and , there exist with with from D057.
In words
Any integer divided by a positive natural number n leaves an integer quotient q and a natural remainder r with a equal to q times n plus r and the remainder below n.
Rests onF02F03F04F05F06F08F09F11F12F13F14A01A02A06A08
Never needed: F10 · A03 · A04 · A05 · A07 · A09 (computed from the citation graph, not asserted).

Proof

  1. 1
    By L75, or for some (with in the second case). Divide by : T10 gives with and (valid since ).
  2. 2
    Case . Applying and L46, . Take and : then with .
  3. 3
    Case with . Then , so (L46, L45 (ii)). Take and : then , and .
  4. 4
    Case with . Then . Let be the gap with (L47); since , also (L17 (ii)). Set . Using and (L46) together with the ring laws of T23: the last equality because . This is (L46). So with .
∎

Remarks

Existence is all the residue count T60 needs. The pair is in fact unique, giving each integer a canonical remainder with , but that is not used here. This extends T10 from to ; the only new content is the negative case, where dividing the magnitude of and borrowing one multiple of (when the remainder is nonzero) keeps the remainder in range.
Wikipedia ↗Int.ediv_add_emod ↗

Used by

T60
Propose an edit1 published revision