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	$$⊢\left(A\in ℂ\wedge B\in ℂ\wedge C\in ℂ\right)\to A+B+C=A+B+C$$

Proof

Step	Hyp	Ref	Expression
1		cnring	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}$$
2		ringgrp	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}\to {ℂ}_{\mathrm{fld}}\in \mathrm{Grp}$$
3	1 2	ax-mp	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Grp}$$
4		cnfldbas	$$⊢ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$$
5		cnfldadd	$$⊢+={+}_{{ℂ}_{\mathrm{fld}}}$$
6	4 5	grpass	$$⊢\left({ℂ}_{\mathrm{fld}}\in \mathrm{Grp}\wedge \left(A\in ℂ\wedge B\in ℂ\wedge C\in ℂ\right)\right)\to A+B+C=A+B+C$$
7	3 6	mpan	$$⊢\left(A\in ℂ\wedge B\in ℂ\wedge C\in ℂ\right)\to A+B+C=A+B+C$$