Theorem addcomsr

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(𝑷\times 𝑷\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}{+}_{𝑹}=𝑹\times 𝑹$$
8	7	ndmovcom	$$⊢\neg \left(A\in 𝑹\wedge B\in 𝑹\right)\to A{+}_{𝑹}B=B{+}_{𝑹}A$$
9	6 8	pm2.61i	$$⊢A{+}_{𝑹}B=B{+}_{𝑹}A$$