Skip to content
Axiomatic Wiki
Theorem·T22

The integers form an abelian group under addition

Addition of integers is associative and commutative, has an identity, and every integer has an additive inverse.

(D058) is a group, and is commutative: it is abelian.
In words
Adding integers is associative and commutative, has an identity, and every integer has an additive inverse: the integers, with addition, form an abelian group.
Rests onF02F03F04F06F08F09F11F12F14A01A02A06A08
Never needed: F05 · F10 · F13 · A03 · A04 · A05 · A07 (computed from the citation graph, not asserted).

Proof

  1. 1
    Closure. For , directly by D058 (the result is again a class ).
  2. 2
    Associativity. Let . Two applications of D058 each give These agree by associativity of addition on in each coordinate.
  3. 3
    Commutativity. With as above, and are equal since and by commutativity of addition on .
  4. 4
    Identity. ( from D057) using D027 in each coordinate; by commutativity (part 3), too.
  5. 5
    Inverses. For , let . By D058, . Since by commutativity, and both and by D027 and commutativity, we get , i.e. (L41). So by T04. By commutativity, too.
  6. 6
    All clauses (G1)-(G3) of D038 hold for , plus commutativity: is an abelian group.
∎

Remarks

This is exactly the repair noted as missing from : the naturals have an identity but no inverses, and the integers were built precisely to fix that. Uniqueness of the identity and of inverses now follows for free from L28; the inverse of is written , constructed explicitly in D059.
Wikipedia ↗Int.instAddGroup ↗

Used by

L54L65L66T23T25T26
Propose an edit1 published revision