axaddass

Description: Addition of complex numbers is associative. This theorem transfers the associative laws for the real and imaginary signed real components of complex number pairs, to complex number addition itself. Axiom 9 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-addass be used later. Instead, use addass . (Contributed by NM, 2-Sep-1995) (New usage is discouraged.)

		Ref	Expression
	Assertion	axaddass	$⊢ (A \in ℂ \land B \in ℂ \land C \in ℂ) \to A + B + C = A + B + C$

Proof

Step	Hyp	Ref	Expression
1		dfcnqs	$⊢ ℂ = (𝑹 \times 𝑹) / E^{-1}$
2		addcnsrec	$⊢ ((x \in 𝑹 \land y \in 𝑹) \land (z \in 𝑹 \land w \in 𝑹)) \to [⟨x, y⟩] E^{-1} + [⟨z, w⟩] E^{-1} = [⟨x +_{𝑹} z, y +_{𝑹} w⟩] E^{-1}$
3		addcnsrec	$⊢ ((z \in 𝑹 \land w \in 𝑹) \land (v \in 𝑹 \land u \in 𝑹)) \to [⟨z, w⟩] E^{-1} + [⟨v, u⟩] E^{-1} = [⟨z +_{𝑹} v, w +_{𝑹} u⟩] E^{-1}$
4		addcnsrec	$⊢ ((x +_{𝑹} z \in 𝑹 \land y +_{𝑹} w \in 𝑹) \land (v \in 𝑹 \land u \in 𝑹)) \to [⟨x +_{𝑹} z, y +_{𝑹} w⟩] E^{-1} + [⟨v, u⟩] E^{-1} = [⟨(x +_{𝑹} z) +_{𝑹} v, (y +_{𝑹} w) +_{𝑹} u⟩] E^{-1}$
5		addcnsrec	$⊢ ((x \in 𝑹 \land y \in 𝑹) \land (z +_{𝑹} v \in 𝑹 \land w +_{𝑹} u \in 𝑹)) \to [⟨x, y⟩] E^{-1} + [⟨z +_{𝑹} v, w +_{𝑹} u⟩] E^{-1} = [⟨x +_{𝑹} (z +_{𝑹} v), y +_{𝑹} (w +_{𝑹} u)⟩] E^{-1}$
6		addclsr	$⊢ (x \in 𝑹 \land z \in 𝑹) \to x +_{𝑹} z \in 𝑹$
7		addclsr	$⊢ (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		addclsr	$⊢ (z \in 𝑹 \land v \in 𝑹) \to z +_{𝑹} v \in 𝑹$
11		addclsr	$⊢ (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		addasssr	$⊢ (x +_{𝑹} z) +_{𝑹} v = x +_{𝑹} (z +_{𝑹} v)$
15		addasssr	$⊢ (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$

Metamath Proof Explorer

Theorem axaddass

Proof