# Metamath Proof Explorer

Description: Addition of signed reals is commutative. (Contributed by NM, 31-Aug-1995) (Revised by Mario Carneiro, 28-Apr-2015) (New usage is discouraged.)

Ref Expression
Assertion addcomsr ${⊢}{A}{+}_{𝑹}{B}={B}{+}_{𝑹}{A}$

### Proof

Step Hyp Ref Expression
1 df-nr ${⊢}𝑹=\left(𝑷×𝑷\right)/{~}_{𝑹}$
2 addsrpr ${⊢}\left(\left({x}\in 𝑷\wedge {y}\in 𝑷\right)\wedge \left({z}\in 𝑷\wedge {w}\in 𝑷\right)\right)\to \left[⟨{x},{y}⟩\right]{~}_{𝑹}{+}_{𝑹}\left[⟨{z},{w}⟩\right]{~}_{𝑹}=\left[⟨{x}{+}_{𝑷}{z},{y}{+}_{𝑷}{w}⟩\right]{~}_{𝑹}$
3 addsrpr ${⊢}\left(\left({z}\in 𝑷\wedge {w}\in 𝑷\right)\wedge \left({x}\in 𝑷\wedge {y}\in 𝑷\right)\right)\to \left[⟨{z},{w}⟩\right]{~}_{𝑹}{+}_{𝑹}\left[⟨{x},{y}⟩\right]{~}_{𝑹}=\left[⟨{z}{+}_{𝑷}{x},{w}{+}_{𝑷}{y}⟩\right]{~}_{𝑹}$
4 addcompr ${⊢}{x}{+}_{𝑷}{z}={z}{+}_{𝑷}{x}$
5 addcompr ${⊢}{y}{+}_{𝑷}{w}={w}{+}_{𝑷}{y}$
6 1 2 3 4 5 ecovcom ${⊢}\left({A}\in 𝑹\wedge {B}\in 𝑹\right)\to {A}{+}_{𝑹}{B}={B}{+}_{𝑹}{A}$
7 dmaddsr ${⊢}\mathrm{dom}{+}_{𝑹}=𝑹×𝑹$
8 7 ndmovcom ${⊢}¬\left({A}\in 𝑹\wedge {B}\in 𝑹\right)\to {A}{+}_{𝑹}{B}={B}{+}_{𝑹}{A}$
9 6 8 pm2.61i ${⊢}{A}{+}_{𝑹}{B}={B}{+}_{𝑹}{A}$