Definition·D058
Addition of integers
Add integers by adding representative pairs coordinatewise.
For
, write
and
with
(D026), and define
(coordinatewise, using addition of naturals). This does not depend on the choice of representatives, so
is a well-defined binary operation on
.
In words
To add two integers, pick representative pairs for each and add the pairs coordinatewise, taking the class of the result; the choice of representatives does not affect the answer.
Rests onA02
Never needed: F02 · F03 · F04 · F05 · F06 · F08 · F09 · F10 · F11 · F12 · F13 · F14 · A01 · A03 · A04 · A05 · A06 · A07 · A08 (computed from the citation graph, not asserted).
Remarks
As a set,
is carved out of
by Separation, collecting exactly the triples
; well-definedness (L43) is exactly what makes this a function rather than a mere relation. Under the embedding,
(L46), so this genuinely extends addition on
.