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 e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) + C ) = ( A + ( B + C ) ) )

Proof

Step	Hyp	Ref	Expression
1		dfcnqs	|- CC = ( ( R. X. R. ) /. `' _E )
2		addcnsrec	|- ( ( ( x e. R. /\ y e. R. ) /\ ( z e. R. /\ w e. R. ) ) -> ( [ <. x , y >. ] `' _E + [ <. z , w >. ] `' _E ) = [ <. ( x +R z ) , ( y +R w ) >. ] `' _E )
3		addcnsrec	|- ( ( ( z e. R. /\ w e. R. ) /\ ( v e. R. /\ u e. R. ) ) -> ( [ <. z , w >. ] `' _E + [ <. v , u >. ] `' _E ) = [ <. ( z +R v ) , ( w +R u ) >. ] `' _E )
4		addcnsrec	|- ( ( ( ( x +R z ) e. R. /\ ( y +R w ) e. R. ) /\ ( v e. R. /\ u e. R. ) ) -> ( [ <. ( x +R z ) , ( y +R w ) >. ] `' _E + [ <. v , u >. ] `' _E ) = [ <. ( ( x +R z ) +R v ) , ( ( y +R w ) +R u ) >. ] `' _E )
5		addcnsrec	|- ( ( ( x e. R. /\ y e. R. ) /\ ( ( z +R v ) e. R. /\ ( w +R u ) e. R. ) ) -> ( [ <. x , y >. ] `' _E + [ <. ( z +R v ) , ( w +R u ) >. ] `' _E ) = [ <. ( x +R ( z +R v ) ) , ( y +R ( w +R u ) ) >. ] `' _E )
6		addclsr	|- ( ( x e. R. /\ z e. R. ) -> ( x +R z ) e. R. )
7		addclsr	|- ( ( y e. R. /\ w e. R. ) -> ( y +R w ) e. R. )
8	6 7	anim12i	|- ( ( ( x e. R. /\ z e. R. ) /\ ( y e. R. /\ w e. R. ) ) -> ( ( x +R z ) e. R. /\ ( y +R w ) e. R. ) )
9	8	an4s	|- ( ( ( x e. R. /\ y e. R. ) /\ ( z e. R. /\ w e. R. ) ) -> ( ( x +R z ) e. R. /\ ( y +R w ) e. R. ) )
10		addclsr	|- ( ( z e. R. /\ v e. R. ) -> ( z +R v ) e. R. )
11		addclsr	|- ( ( w e. R. /\ u e. R. ) -> ( w +R u ) e. R. )
12	10 11	anim12i	|- ( ( ( z e. R. /\ v e. R. ) /\ ( w e. R. /\ u e. R. ) ) -> ( ( z +R v ) e. R. /\ ( w +R u ) e. R. ) )
13	12	an4s	|- ( ( ( z e. R. /\ w e. R. ) /\ ( v e. R. /\ u e. R. ) ) -> ( ( z +R v ) e. R. /\ ( w +R u ) e. R. ) )
14		addasssr	|- ( ( x +R z ) +R v ) = ( x +R ( z +R v ) )
15		addasssr	|- ( ( y +R w ) +R u ) = ( y +R ( w +R u ) )
16	1 2 3 4 5 9 13 14 15	ecovass	|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) + C ) = ( A + ( B + C ) ) )