This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ 𝑹 = (𝑷 \times 𝑷) / ~_{𝑹}$
2		addsrpr	$⊢ ((x \in 𝑷 \land y \in 𝑷) \land (z \in 𝑷 \land w \in 𝑷)) \to [⟨x, y⟩] ~_{𝑹} +_{𝑹} [⟨z, w⟩] ~_{𝑹} = [⟨x +_{𝑷} z, y +_{𝑷} w⟩] ~_{𝑹}$
3		addsrpr	$⊢ ((z \in 𝑷 \land w \in 𝑷) \land (x \in 𝑷 \land y \in 𝑷)) \to [⟨z, w⟩] ~_{𝑹} +_{𝑹} [⟨x, y⟩] ~_{𝑹} = [⟨z +_{𝑷} x, w +_{𝑷} y⟩] ~_{𝑹}$
4		addcompr	$⊢ x +_{𝑷} z = z +_{𝑷} x$
5		addcompr	$⊢ y +_{𝑷} w = w +_{𝑷} y$
6	1 2 3 4 5	ecovcom	$⊢ (A \in 𝑹 \land B \in 𝑹) \to A +_{𝑹} B = B +_{𝑹} A$
7		dmaddsr	$⊢ dom +_{𝑹} = 𝑹 \times 𝑹$
8	7	ndmovcom	$⊢ \neg (A \in 𝑹 \land B \in 𝑹) \to A +_{𝑹} B = B +_{𝑹} A$
9	6 8	pm2.61i	$⊢ A +_{𝑹} B = B +_{𝑹} A$