Lemma·L09
Commutativity of addition
Order does not matter when adding.
for all
; in particular
and
.
In words
The sum of m and n equals the sum of n and m, for all natural numbers m and n. Along the way: adding n to zero from the left gives back n, and a successor on the left can be pulled out of the sum.
Never needed: F03 · F04 · F05 · F06 · F08 · F10 · F11 · F12 · F13 · A02 · A03 · A04 · A05 · A07 · A08 (computed from the citation graph, not asserted).
Proof
- 1Claim A: . Induction on (T05, sets by Separation here and below). Base: by D027. Step: by D027 and the hypothesis.
- 2Claim B: . Fix , induct on . Base: by D027. Step: assuming , by D027 on the outside and the hypothesis inside (substitutivity).
- 3
- 4T05 closes each of the three inductions; universal quantifiers are discharged by generalization.
∎
Remarks
The proof is the standard double induction: the definitional equations of addition recurse on the right argument only, so the two auxiliary claims manufacture the mirrored equations for the left argument, after which the main induction is mechanical. Together with associativity this makes
a commutative monoid.