Theorem·T26
The rationals form an abelian group under addition
Addition of rationals is associative and commutative, has an identity, and every rational has an additive inverse.
In words
Adding rationals is associative and commutative, has an identity, and every rational has an additive inverse: the rationals, with addition, form an abelian group.
Never needed: F10 · A03 · A04 · A05 · A07 (computed from the citation graph, not asserted).
Proof
- 1Closure. For , directly by D065.
- 2Associativity. Let . Two applications of D065 give Both first coordinates expand, via distributivity, commutativity and associativity of , to ; both second coordinates equal . So the two representative pairs are equal outright.
- 3Commutativity. With as above, and are the same pair, using commutativity of and on .
- 4Identity. ( from D064) , using zero times anything is zero, the unity and additive-identity laws of T23 and T22; by commutativity, too.
- 5Inverses. For , let (D066). By D065, . By the sign rule and the inverse law of T22, . So exactly when , i.e. , i.e. (zero times anything is zero applied on both sides), which holds. So by T04. By commutativity, too.
- 6All clauses of D038 hold for , plus commutativity: an abelian group.
∎