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 ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 + 𝐵 ) + 𝐶 ) = ( 𝐴 + ( 𝐵 + 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 dfcnqs ⊢ ℂ = ( ( R × R ) / ◡ E )
2 addcnsrec ⊢ ( ( ( 𝑥 ∈ R ∧ 𝑦 ∈ R ) ∧ ( 𝑧 ∈ R ∧ 𝑤 ∈ R ) ) → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ◡ E + [ ⟨ 𝑧 , 𝑤 ⟩ ] ◡ E ) = [ ⟨ ( 𝑥 +R 𝑧 ) , ( 𝑦 +R 𝑤 ) ⟩ ] ◡ E )
3 addcnsrec ⊢ ( ( ( 𝑧 ∈ R ∧ 𝑤 ∈ R ) ∧ ( 𝑣 ∈ R ∧ 𝑢 ∈ R ) ) → ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ◡ E + [ ⟨ 𝑣 , 𝑢 ⟩ ] ◡ E ) = [ ⟨ ( 𝑧 +R 𝑣 ) , ( 𝑤 +R 𝑢 ) ⟩ ] ◡ E )
4 addcnsrec ⊢ ( ( ( ( 𝑥 +R 𝑧 ) ∈ R ∧ ( 𝑦 +R 𝑤 ) ∈ R ) ∧ ( 𝑣 ∈ R ∧ 𝑢 ∈ R ) ) → ( [ ⟨ ( 𝑥 +R 𝑧 ) , ( 𝑦 +R 𝑤 ) ⟩ ] ◡ E + [ ⟨ 𝑣 , 𝑢 ⟩ ] ◡ E ) = [ ⟨ ( ( 𝑥 +R 𝑧 ) +R 𝑣 ) , ( ( 𝑦 +R 𝑤 ) +R 𝑢 ) ⟩ ] ◡ E )
5 addcnsrec ⊢ ( ( ( 𝑥 ∈ R ∧ 𝑦 ∈ R ) ∧ ( ( 𝑧 +R 𝑣 ) ∈ R ∧ ( 𝑤 +R 𝑢 ) ∈ R ) ) → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ◡ E + [ ⟨ ( 𝑧 +R 𝑣 ) , ( 𝑤 +R 𝑢 ) ⟩ ] ◡ E ) = [ ⟨ ( 𝑥 +R ( 𝑧 +R 𝑣 ) ) , ( 𝑦 +R ( 𝑤 +R 𝑢 ) ) ⟩ ] ◡ E )
6 addclsr ⊢ ( ( 𝑥 ∈ R ∧ 𝑧 ∈ R ) → ( 𝑥 +R 𝑧 ) ∈ R )
7 addclsr ⊢ ( ( 𝑦 ∈ R ∧ 𝑤 ∈ R ) → ( 𝑦 +R 𝑤 ) ∈ R )
8 6 7 anim12i ⊢ ( ( ( 𝑥 ∈ R ∧ 𝑧 ∈ R ) ∧ ( 𝑦 ∈ R ∧ 𝑤 ∈ R ) ) → ( ( 𝑥 +R 𝑧 ) ∈ R ∧ ( 𝑦 +R 𝑤 ) ∈ R ) )
9 8 an4s ⊢ ( ( ( 𝑥 ∈ R ∧ 𝑦 ∈ R ) ∧ ( 𝑧 ∈ R ∧ 𝑤 ∈ R ) ) → ( ( 𝑥 +R 𝑧 ) ∈ R ∧ ( 𝑦 +R 𝑤 ) ∈ R ) )
10 addclsr ⊢ ( ( 𝑧 ∈ R ∧ 𝑣 ∈ R ) → ( 𝑧 +R 𝑣 ) ∈ R )
11 addclsr ⊢ ( ( 𝑤 ∈ R ∧ 𝑢 ∈ R ) → ( 𝑤 +R 𝑢 ) ∈ R )
12 10 11 anim12i ⊢ ( ( ( 𝑧 ∈ R ∧ 𝑣 ∈ R ) ∧ ( 𝑤 ∈ R ∧ 𝑢 ∈ R ) ) → ( ( 𝑧 +R 𝑣 ) ∈ R ∧ ( 𝑤 +R 𝑢 ) ∈ R ) )
13 12 an4s ⊢ ( ( ( 𝑧 ∈ R ∧ 𝑤 ∈ R ) ∧ ( 𝑣 ∈ R ∧ 𝑢 ∈ R ) ) → ( ( 𝑧 +R 𝑣 ) ∈ R ∧ ( 𝑤 +R 𝑢 ) ∈ R ) )
14 addasssr ⊢ ( ( 𝑥 +R 𝑧 ) +R 𝑣 ) = ( 𝑥 +R ( 𝑧 +R 𝑣 ) )
15 addasssr ⊢ ( ( 𝑦 +R 𝑤 ) +R 𝑢 ) = ( 𝑦 +R ( 𝑤 +R 𝑢 ) )
16 1 2 3 4 5 9 13 14 15 ecovass ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 + 𝐵 ) + 𝐶 ) = ( 𝐴 + ( 𝐵 + 𝐶 ) ) )