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

Metamath Proof Explorer

Theorem 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 ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A + B + C = A + B + C

Proof

Step Hyp Ref Expression
1 dfcnqs ⊢ ℂ = 𝑹 × 𝑹 / E -1
2 addcnsrec ⊢ x ∈ 𝑹 ∧ y ∈ 𝑹 ∧ z ∈ 𝑹 ∧ w ∈ 𝑹 → x y E -1 + z w E -1 = x + 𝑹 z y + 𝑹 w E -1
3 addcnsrec ⊢ z ∈ 𝑹 ∧ w ∈ 𝑹 ∧ v ∈ 𝑹 ∧ u ∈ 𝑹 → z w E -1 + v u E -1 = z + 𝑹 v w + 𝑹 u E -1
4 addcnsrec ⊢ x + 𝑹 z ∈ 𝑹 ∧ y + 𝑹 w ∈ 𝑹 ∧ v ∈ 𝑹 ∧ u ∈ 𝑹 → x + 𝑹 z y + 𝑹 w E -1 + v u E -1 = x + 𝑹 z + 𝑹 v y + 𝑹 w + 𝑹 u E -1
5 addcnsrec ⊢ x ∈ 𝑹 ∧ y ∈ 𝑹 ∧ z + 𝑹 v ∈ 𝑹 ∧ w + 𝑹 u ∈ 𝑹 → x y E -1 + z + 𝑹 v w + 𝑹 u E -1 = x + 𝑹 z + 𝑹 v y + 𝑹 w + 𝑹 u E -1
6 addclsr ⊢ x ∈ 𝑹 ∧ z ∈ 𝑹 → x + 𝑹 z ∈ 𝑹
7 addclsr ⊢ y ∈ 𝑹 ∧ w ∈ 𝑹 → y + 𝑹 w ∈ 𝑹
8 6 7 anim12i ⊢ x ∈ 𝑹 ∧ z ∈ 𝑹 ∧ y ∈ 𝑹 ∧ w ∈ 𝑹 → x + 𝑹 z ∈ 𝑹 ∧ y + 𝑹 w ∈ 𝑹
9 8 an4s ⊢ x ∈ 𝑹 ∧ y ∈ 𝑹 ∧ z ∈ 𝑹 ∧ w ∈ 𝑹 → x + 𝑹 z ∈ 𝑹 ∧ y + 𝑹 w ∈ 𝑹
10 addclsr ⊢ z ∈ 𝑹 ∧ v ∈ 𝑹 → z + 𝑹 v ∈ 𝑹
11 addclsr ⊢ w ∈ 𝑹 ∧ u ∈ 𝑹 → w + 𝑹 u ∈ 𝑹
12 10 11 anim12i ⊢ z ∈ 𝑹 ∧ v ∈ 𝑹 ∧ w ∈ 𝑹 ∧ u ∈ 𝑹 → z + 𝑹 v ∈ 𝑹 ∧ w + 𝑹 u ∈ 𝑹
13 12 an4s ⊢ z ∈ 𝑹 ∧ w ∈ 𝑹 ∧ v ∈ 𝑹 ∧ u ∈ 𝑹 → z + 𝑹 v ∈ 𝑹 ∧ w + 𝑹 u ∈ 𝑹
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 ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A + B + C = A + B + C