addasssr

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

		Ref	Expression
	Assertion	addasssr	$⊢ (A +_{𝑹} B) +_{𝑹} C = A +_{𝑹} (B +_{𝑹} C)$

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 (v \in 𝑷 \land u \in 𝑷)) \to [⟨z, w⟩] ~_{𝑹} +_{𝑹} [⟨v, u⟩] ~_{𝑹} = [⟨z +_{𝑷} v, w +_{𝑷} u⟩] ~_{𝑹}$
4		addsrpr	$⊢ ((x +_{𝑷} z \in 𝑷 \land y +_{𝑷} w \in 𝑷) \land (v \in 𝑷 \land u \in 𝑷)) \to [⟨x +_{𝑷} z, y +_{𝑷} w⟩] ~_{𝑹} +_{𝑹} [⟨v, u⟩] ~_{𝑹} = [⟨(x +_{𝑷} z) +_{𝑷} v, (y +_{𝑷} w) +_{𝑷} u⟩] ~_{𝑹}$
5		addsrpr	$⊢ ((x \in 𝑷 \land y \in 𝑷) \land (z +_{𝑷} v \in 𝑷 \land w +_{𝑷} u \in 𝑷)) \to [⟨x, y⟩] ~_{𝑹} +_{𝑹} [⟨z +_{𝑷} v, w +_{𝑷} u⟩] ~_{𝑹} = [⟨x +_{𝑷} (z +_{𝑷} v), y +_{𝑷} (w +_{𝑷} u)⟩] ~_{𝑹}$
6		addclpr	$⊢ (x \in 𝑷 \land z \in 𝑷) \to x +_{𝑷} z \in 𝑷$
7		addclpr	$⊢ (y \in 𝑷 \land w \in 𝑷) \to y +_{𝑷} w \in 𝑷$
8	6 7	anim12i	$⊢ ((x \in 𝑷 \land z \in 𝑷) \land (y \in 𝑷 \land w \in 𝑷)) \to (x +_{𝑷} z \in 𝑷 \land y +_{𝑷} w \in 𝑷)$
9	8	an4s	$⊢ ((x \in 𝑷 \land y \in 𝑷) \land (z \in 𝑷 \land w \in 𝑷)) \to (x +_{𝑷} z \in 𝑷 \land y +_{𝑷} w \in 𝑷)$
10		addclpr	$⊢ (z \in 𝑷 \land v \in 𝑷) \to z +_{𝑷} v \in 𝑷$
11		addclpr	$⊢ (w \in 𝑷 \land u \in 𝑷) \to w +_{𝑷} u \in 𝑷$
12	10 11	anim12i	$⊢ ((z \in 𝑷 \land v \in 𝑷) \land (w \in 𝑷 \land u \in 𝑷)) \to (z +_{𝑷} v \in 𝑷 \land w +_{𝑷} u \in 𝑷)$
13	12	an4s	$⊢ ((z \in 𝑷 \land w \in 𝑷) \land (v \in 𝑷 \land u \in 𝑷)) \to (z +_{𝑷} v \in 𝑷 \land w +_{𝑷} u \in 𝑷)$
14		addasspr	$⊢ (x +_{𝑷} z) +_{𝑷} v = x +_{𝑷} (z +_{𝑷} v)$
15		addasspr	$⊢ (y +_{𝑷} w) +_{𝑷} u = y +_{𝑷} (w +_{𝑷} u)$
16	1 2 3 4 5 9 13 14 15	ecovass	$⊢ (A \in 𝑹 \land B \in 𝑹 \land C \in 𝑹) \to (A +_{𝑹} B) +_{𝑹} C = A +_{𝑹} (B +_{𝑹} C)$
17		dmaddsr	$⊢ dom +_{𝑹} = 𝑹 \times 𝑹$
18		0nsr	$⊢ \neg \emptyset \in 𝑹$
19	17 18	ndmovass	$⊢ \neg (A \in 𝑹 \land B \in 𝑹 \land C \in 𝑹) \to (A +_{𝑹} B) +_{𝑹} C = A +_{𝑹} (B +_{𝑹} C)$
20	16 19	pm2.61i	$⊢ (A +_{𝑹} B) +_{𝑹} C = A +_{𝑹} (B +_{𝑹} C)$

Metamath Proof Explorer

Theorem addasssr

Proof