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	⊢ ( 𝐴 +R 𝐵 ) = ( 𝐵 +R 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		df-nr	⊢ R = ( ( P × P ) / ~R )
2		addsrpr	⊢ ( ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ∧ ( 𝑧 ∈ P ∧ 𝑤 ∈ P ) ) → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R +R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ) = [ ⟨ ( 𝑥 +P 𝑧 ) , ( 𝑦 +P 𝑤 ) ⟩ ] ~R )
3		addsrpr	⊢ ( ( ( 𝑧 ∈ P ∧ 𝑤 ∈ P ) ∧ ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ) → ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R +R [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R ) = [ ⟨ ( 𝑧 +P 𝑥 ) , ( 𝑤 +P 𝑦 ) ⟩ ] ~R )
4		addcompr	⊢ ( 𝑥 +P 𝑧 ) = ( 𝑧 +P 𝑥 )
5		addcompr	⊢ ( 𝑦 +P 𝑤 ) = ( 𝑤 +P 𝑦 )
6	1 2 3 4 5	ecovcom	⊢ ( ( 𝐴 ∈ R ∧ 𝐵 ∈ R ) → ( 𝐴 +R 𝐵 ) = ( 𝐵 +R 𝐴 ) )
7		dmaddsr	⊢ dom +R = ( R × R )
8	7	ndmovcom	⊢ ( ¬ ( 𝐴 ∈ R ∧ 𝐵 ∈ R ) → ( 𝐴 +R 𝐵 ) = ( 𝐵 +R 𝐴 ) )
9	6 8	pm2.61i	⊢ ( 𝐴 +R 𝐵 ) = ( 𝐵 +R 𝐴 )