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 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 ) ) )