Skip to content
Axiomatic Wiki

WLThe multiples of n form a subgroup of the integers

Lemma·L72

The integer multiples of n form a subgroup, and congruence mod n is membership of the difference in it.

Fix and let the set of integer multiples of (D057, Separation). Then (i) is a subgroup of the additive group (T22), and (ii) for all .
In words
The multiples of n are the integers of the form n times an integer. They form a subgroup of the integers under addition, and a is congruent to b modulo n exactly when their difference is a multiple of n.
Rests onF02F03F04F05F06F08F09F11F12F13F14A01A02A06A08
Never needed: F10 · A03 · A04 · A05 · A07 · A09 (computed from the citation graph, not asserted).

Proof

  1. 1
    is a set by Separation. The additive group has identity and the inverse of is (T22, D059); we check the three subgroup clauses.
  2. 2
    Identity. by L45 (i) (in the ring , T23), so (witness ).
  3. 3
    Closed under . Let , say and with . By distributivity (T23, (R2)), .
  4. 4
    Closed under inverses. With , the sign rule L45 (ii) gives . All three clauses hold, so (D039).
  5. 5
    (ii). By D113, means for some , which is exactly .
∎

Remarks

Because is abelian, the coset relation of , namely , coincides with : the two differ by a sign, and is closed under negation by clause (i). This identification is what powers L73. Special values: (congruence mod is equality) and (everything is congruent mod ). In fact every subgroup of is an , though that classification is not needed here.
Wikipedia ↗Int.instSubgroup ↗

Used by

L73
Propose an edit1 published revision