Theorem axaddcom 5198

Description: Addition of complex numbers is commutative. Axiom 9 of 25 for real and complex numbers, derived from ZF set theory.

Assertion

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

Proof of Theorem axaddcom

Step	Hyp	Ref	Expression
1		dfcnqs 5185	. 2 |- CC = ((R. X. R.)/.`'E)
2		addcnsrec 5186	. 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 5186	. 2 |- (((z e. R. /\ w e. R.) /\ (x e. R. /\ y e. R.)) -> ([<.z, w>.]`'E + [<.x, y>.]`'E) = [<.(z +R x), (w +R y)>.]`'E)
4		visset 1788	. . 3 |- x e. V
5		visset 1788	. . 3 |- z e. V
6	4, 5	addcomsr 5119	. 2 |- (x +R z) = (z +R x)
7		visset 1788	. . 3 |- y e. V
8		visset 1788	. . 3 |- w e. V
9	7, 8	addcomsr 5119	. 2 |- (y +R w) = (w +R y)
10	1, 2, 3, 6, 9	ecoprcom 4257	1 |- ((A e. CC /\ B e. CC) -> (A + B) = (B + A))

Syntax hints:   -> wi 3   /\ wa 223   = wceq 1099   e. wcel 1105  Ecep 2792  `'ccnv 3132  (class class class)co 3902  R.cnr 4916   +R cplr 4920  CCcc 5155   + caddc 5160

This theorem is referenced by:  addcomt 5228  addcom 5245  addid2t 5252  add12t 5259  add23t 5260  add42t 5262  cnegextlem1 5268  cnegextlem3 5270  addcan 5274  addcan2t 5276  subsub23t 5299  addsubt 5307  addsub12t 5309  pncan2t 5321  negsubdi2t 5381  sub23t 5388  nnncan1t 5390  sub4t 5399  pnpcan2t 5402  ppncant 5404  ltadd2t 5549  leadd2t 5551  ltsubadd2t 5553  lesubadd2t 5555  ltaddsub2t 5557  leaddsub2t 5559  addgtge0t 5573  ltaddpos2t 5576  addge02t 5597  conjmult 5704  recp1lt1 5800  recrecltt 5801  nnleltp1t 5852  nn0nnaddclt 6024  zaddclt 6063  zneo 6098  zneoOLD 6099  shftval2t 6235  shftval4t 6237  fzshftralt 6405  seqzval2t 6436  subsqt 6524  bernneq2 6535  rimul 6626  imret 6661  fsumrev 6918  fsumshft 6920  bcxmas 6965  climshft2 6994  climaddc2 7006  efaddlem14 7244  ef1tllem 7274  cosnegt 7336  addcost 7352  sincossqt 7354  cos2tt 7356  absefit 7375  demoivre 7377  nn0ennn 7390  ioo2bl 7799  cnaddabl 8011  addinv 8013  ipval2 8226  truni1 8743  2wsms 8824  hhph 9194  golem1 10322  stcltrlem1 10327  cdj3lem3b 10486

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-7 954  ax-gen 955  ax-8 1101  ax-9 1102  ax-10 1103  ax-12 1104  ax-13 1107  ax-14 1108  ax-11 1180  ax-17 1190  ax-16 1194  ax-11o 1202  ax-ext 1436  ax-rep 2661  ax-sep 2671  ax-nul 2678  ax-pow 2710  ax-pr 2747  ax-un 2830  ax-inf2 4549

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 773  df-3an 774  df-ex 957  df-sb 1155  df-eu 1359  df-mo 1360  df-clab 1441  df-cleq 1446  df-clel 1449  df-ne 1563  df-ral 1625  df-rex 1626  df-reu 1627  df-rab 1628  df-v 1787  df-sbc 1913  df-csb 1973  df-dif 2020  df-un 2021  df-in 2022  df-ss 2024  df-pss 2026  df-nul 2252  df-if 2333  df-pw 2373  df-sn 2383  df-pr 2384  df-tp 2386  df-op 2387  df-uni 2472  df-int 2502  df-iun 2536  df-br 2588  df-opab 2635  df-tr 2649  df-eprel 2794  df-id 2797  df-po 2804  df-so 2814  df-fr 2880  df-we 2897  df-ord 2914  df-on 2915  df-lim 2916  df-suc 2917  df-om 3095  df-xp 3147  df-rel 3148  df-cnv 3149  df-co 3150  df-dm 3151  df-rn 3152  df-res 3153  df-ima 3154  df-fun 3155  df-fn 3156  df-f 3157  df-fv 3161  df-rdg 3871  df-opr 3904  df-oprab 3905  df-1st 4017  df-2nd 4018  df-1o 4071  df-oadd 4073  df-omul 4074  df-er 4199  df-ec 4201  df-qs 4204  df-ni 4923  df-pli 4924  df-mi 4925  df-lti 4926  df-plpq 4958  df-mpq 4959  df-enq 4960  df-nq 4961  df-plq 4962  df-mq 4963  df-rq 4964  df-ltq 4965  df-1q 4966  df-np 5009  df-plp 5011  df-ltp 5013  df-plpr 5087  df-enr 5089  df-nr 5090  df-plr 5091  df-c 5163  df-plus 5168

Copyright terms: Public domain