Theorem cnncvsaddassdemo

Description: Derive the associative law for complex number addition addass to demonstrate the use of the properties of a normed subcomplex vector space for the complex numbers. (Contributed by NM, 12-Jan-2008) (Revised by AV, 9-Oct-2021) (Proof modification is discouraged.)

	Ref	Expression
Assertion	cnncvsaddassdemo	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 + 𝐵 ) + 𝐶 ) = ( 𝐴 + ( 𝐵 + 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		cnring	⊢ ℂfld ∈ Ring
2		ringgrp	⊢ ( ℂfld ∈ Ring → ℂfld ∈ Grp )
3	1 2	ax-mp	⊢ ℂfld ∈ Grp
4		cnfldbas	⊢ ℂ = ( Base ‘ ℂfld )
5		cnfldadd	⊢ + = ( +g ‘ ℂfld )
6	4 5	grpass	⊢ ( ( ℂfld ∈ Grp ∧ ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ) → ( ( 𝐴 + 𝐵 ) + 𝐶 ) = ( 𝐴 + ( 𝐵 + 𝐶 ) ) )
7	3 6	mpan	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 + 𝐵 ) + 𝐶 ) = ( 𝐴 + ( 𝐵 + 𝐶 ) ) )