Theorem axaddass 6871

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 10 of 23 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-addass 6894.

Assertion

Ref	Expression
axaddass	|- ((A e. CC /\ B e. CC /\ C e. CC) -> ((A + B) + C) = (A + (B + C)))

Proof of Theorem axaddass

Step	Hyp	Ref	Expression
1		dfcnqs 6857	. 2 |- CC = ((R. X. R.)/.`' _E )
2		addcnsrec 6858	. 2 |- (((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 6858	. 2 |- (((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 6858	. 2 |- ((((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 6858	. 2 |- (((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 6787	. . . 4 |- ((x e. R. /\ z e. R.) -> (x +R z) e. R.)
7		addclsr 6787	. . . 4 |- ((y e. R. /\ w e. R.) -> (y +R w) e. R.)
8	6, 7	anim12i 632	. . 3 |- (((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 941	. 2 |- (((x e. R. /\ y e. R.) /\ (z e. R. /\ w e. R.)) -> ((x +R z) e. R. /\ (y +R w) e. R.))
10		addclsr 6787	. . . 4 |- ((z e. R. /\ v e. R.) -> (z +R v) e. R.)
11		addclsr 6787	. . . 4 |- ((w e. R. /\ u e. R.) -> (w +R u) e. R.)
12	10, 11	anim12i 632	. . 3 |- (((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 941	. 2 |- (((z e. R. /\ w e. R.) /\ (v e. R. /\ u e. R.)) -> ((z +R v) e. R. /\ (w +R u) e. R.))
14		visset 2572	. . 3 |- z e. _V
15		visset 2572	. . 3 |- v e. _V
16	14, 15	addasssr 6792	. 2 |- ((x +R z) +R v) = (x +R (z +R v))
17		visset 2572	. . 3 |- w e. _V
18		visset 2572	. . 3 |- u e. _V
19	17, 18	addasssr 6792	. 2 |- ((y +R w) +R u) = (y +R (w +R u))
20	1, 2, 3, 4, 5, 9, 13, 16, 19	ecoprass 5583	1 |- ((A e. CC /\ B e. CC /\ C e. CC) -> ((A + B) + C) = (A + (B + C)))

Syntax hints:   -> wi 3   /\ wa 433   /\ w3a 1130   = wceq 1615   e. wcel 1617   _E cep 3774  `'ccnv 4150  (class class class)co 5020  R.cnr 6588   +R cplr 6592  CCcc 6827   + caddc 6832

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1621  ax-gen 1622  ax-8 1623  ax-9 1624  ax-10 1625  ax-11 1626  ax-12 1627  ax-13 1628  ax-14 1629  ax-17 1634  ax-4 1637  ax-5o 1639  ax-6o 1642  ax-9o 1792  ax-10o 1810  ax-16 1883  ax-11o 1893  ax-ext 2152  ax-rep 3628  ax-sep 3638  ax-nul 3645  ax-pow 3681  ax-pr 3719  ax-un 3961  ax-inf2 6008

This theorem depends on definitions:  df-bi 232  df-or 434  df-an 435  df-3or 1131  df-3an 1132  df-ex 1645  df-sb 1845  df-eu 2070  df-mo 2071  df-clab 2158  df-cleq 2163  df-clel 2166  df-ne 2297  df-ral 2389  df-rex 2390  df-reu 2391  df-rab 2392  df-v 2571  df-sbc 2731  df-csb 2806  df-dif 2862  df-un 2864  df-in 2866  df-ss 2868  df-pss 2870  df-nul 3115  df-if 3213  df-pw 3261  df-sn 3274  df-pr 3275  df-tp 3277  df-op 3278  df-uni 3399  df-int 3433  df-iun 3470  df-br 3540  df-opab 3598  df-tr 3612  df-eprel 3776  df-id 3779  df-po 3784  df-so 3796  df-fr 3814  df-we 3830  df-ord 3846  df-on 3847  df-lim 3848  df-suc 3849  df-om 4118  df-xp 4165  df-rel 4166  df-cnv 4167  df-co 4168  df-dm 4169  df-rn 4170  df-res 4171  df-ima 4172  df-fun 4173  df-fn 4174  df-f 4175  df-fv 4179  df-opr 5022  df-oprab 5023  df-1st 5166  df-2nd 5167  df-rdg 5344  df-1o 5384  df-oadd 5386  df-omul 5387  df-er 5519  df-ec 5521  df-qs 5524  df-ni 6595  df-pli 6596  df-mi 6597  df-lti 6598  df-plpq 6630  df-mpq 6631  df-enq 6632  df-nq 6633  df-plq 6634  df-mq 6635  df-rq 6636  df-ltq 6637  df-1q 6638  df-np 6681  df-plp 6683  df-ltp 6685  df-plpr 6759  df-enr 6761  df-nr 6762  df-plr 6763  df-c 6835  df-plus 6840

Copyright terms: Public domain