Theorem addcom 10222

Description: Addition commutes. This used to be one of our complex number axioms, until it was found to be dependent on the others. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013.)

Assertion

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

Proof of Theorem addcom

Step	Hyp	Ref	Expression
1		1cnd 10056	. . . . . . . 8 |- ( ( A e. CC /\ B e. CC ) -> 1 e. CC )
2	1, 1	addcld 10059	. . . . . . 7 |- ( ( A e. CC /\ B e. CC ) -> ( 1 + 1 ) e. CC )
3		simpl 473	. . . . . . 7 |- ( ( A e. CC /\ B e. CC ) -> A e. CC )
4		simpr 477	. . . . . . 7 |- ( ( A e. CC /\ B e. CC ) -> B e. CC )
5	2, 3, 4	adddid 10064	. . . . . 6 |- ( ( A e. CC /\ B e. CC ) -> ( ( 1 + 1 ) x. ( A + B ) ) = ( ( ( 1 + 1 ) x. A ) + ( ( 1 + 1 ) x. B ) ) )
6	3, 4	addcld 10059	. . . . . . 7 |- ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC )
7		1p1times 10207	. . . . . . 7 |- ( ( A + B ) e. CC -> ( ( 1 + 1 ) x. ( A + B ) ) = ( ( A + B ) + ( A + B ) ) )
8	6, 7	syl 17	. . . . . 6 |- ( ( A e. CC /\ B e. CC ) -> ( ( 1 + 1 ) x. ( A + B ) ) = ( ( A + B ) + ( A + B ) ) )
9		1p1times 10207	. . . . . . 7 |- ( A e. CC -> ( ( 1 + 1 ) x. A ) = ( A + A ) )
10		1p1times 10207	. . . . . . 7 |- ( B e. CC -> ( ( 1 + 1 ) x. B ) = ( B + B ) )
11	9, 10	oveqan12d 6669	. . . . . 6 |- ( ( A e. CC /\ B e. CC ) -> ( ( ( 1 + 1 ) x. A ) + ( ( 1 + 1 ) x. B ) ) = ( ( A + A ) + ( B + B ) ) )
12	5, 8, 11	3eqtr3rd 2665	. . . . 5 |- ( ( A e. CC /\ B e. CC ) -> ( ( A + A ) + ( B + B ) ) = ( ( A + B ) + ( A + B ) ) )
13	3, 3	addcld 10059	. . . . . 6 |- ( ( A e. CC /\ B e. CC ) -> ( A + A ) e. CC )
14	13, 4, 4	addassd 10062	. . . . 5 |- ( ( A e. CC /\ B e. CC ) -> ( ( ( A + A ) + B ) + B ) = ( ( A + A ) + ( B + B ) ) )
15	6, 3, 4	addassd 10062	. . . . 5 |- ( ( A e. CC /\ B e. CC ) -> ( ( ( A + B ) + A ) + B ) = ( ( A + B ) + ( A + B ) ) )
16	12, 14, 15	3eqtr4d 2666	. . . 4 |- ( ( A e. CC /\ B e. CC ) -> ( ( ( A + A ) + B ) + B ) = ( ( ( A + B ) + A ) + B ) )
17	13, 4	addcld 10059	. . . . 5 |- ( ( A e. CC /\ B e. CC ) -> ( ( A + A ) + B ) e. CC )
18	6, 3	addcld 10059	. . . . 5 |- ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) + A ) e. CC )
19		addcan2 10221	. . . . 5 |- ( ( ( ( A + A ) + B ) e. CC /\ ( ( A + B ) + A ) e. CC /\ B e. CC ) -> ( ( ( ( A + A ) + B ) + B ) = ( ( ( A + B ) + A ) + B ) <-> ( ( A + A ) + B ) = ( ( A + B ) + A ) ) )
20	17, 18, 4, 19	syl3anc 1326	. . . 4 |- ( ( A e. CC /\ B e. CC ) -> ( ( ( ( A + A ) + B ) + B ) = ( ( ( A + B ) + A ) + B ) <-> ( ( A + A ) + B ) = ( ( A + B ) + A ) ) )
21	16, 20	mpbid 222	. . 3 |- ( ( A e. CC /\ B e. CC ) -> ( ( A + A ) + B ) = ( ( A + B ) + A ) )
22	3, 3, 4	addassd 10062	. . 3 |- ( ( A e. CC /\ B e. CC ) -> ( ( A + A ) + B ) = ( A + ( A + B ) ) )
23	3, 4, 3	addassd 10062	. . 3 |- ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) + A ) = ( A + ( B + A ) ) )
24	21, 22, 23	3eqtr3d 2664	. 2 |- ( ( A e. CC /\ B e. CC ) -> ( A + ( A + B ) ) = ( A + ( B + A ) ) )
25	4, 3	addcld 10059	. . 3 |- ( ( A e. CC /\ B e. CC ) -> ( B + A ) e. CC )
26		addcan 10220	. . 3 |- ( ( A e. CC /\ ( A + B ) e. CC /\ ( B + A ) e. CC ) -> ( ( A + ( A + B ) ) = ( A + ( B + A ) ) <-> ( A + B ) = ( B + A ) ) )
27	3, 6, 25, 26	syl3anc 1326	. 2 |- ( ( A e. CC /\ B e. CC ) -> ( ( A + ( A + B ) ) = ( A + ( B + A ) ) <-> ( A + B ) = ( B + A ) ) )
28	24, 27	mpbid 222	1 |- ( ( A e. CC /\ B e. CC ) -> ( A + B ) = ( B + A ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   = wceq 1483   e. wcel 1990  (class class class)co 6650   CCcc 9934   1c1 9937   + caddc 9939   x. cmul 9941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-po 5035  df-so 5036  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-ov 6653  df-er 7742  df-en 7956  df-dom 7957  df-sdom 7958  df-pnf 10076  df-mnf 10077  df-ltxr 10079

This theorem is referenced by:  addcomi  10227  ltaddnegr  10252  add12  10253  add32  10254  add42  10257  subsub23  10286  pncan2  10288  addsub  10292  addsub12  10294  addsubeq4  10296  sub32  10315  pnpcan2  10321  ppncan  10323  sub4  10326  negsubdi2  10340  ltaddsub2  10503  leaddsub2  10505  leltadd  10512  ltaddpos2  10519  addge02  10539  conjmul  10742  recp1lt1  10921  recreclt  10922  avgle1  11272  avgle2  11273  avgle  11274  nn0nnaddcl  11324  xaddcom  12071  fzen  12358  fzshftral  12428  fzo0addelr  12522  elfzoext  12524  flzadd  12627  addmodidr  12719  modadd2mod  12720  nn0ennn  12778  seradd  12843  bernneq2  12991  hashfz  13214  ccatalpha  13375  revccat  13515  2cshwcom  13562  shftval2  13815  shftval4  13817  crim  13855  absmax  14069  climshft2  14313  summolem3  14445  binom1dif  14565  isumshft  14571  arisum  14592  mertenslem1  14616  bpolydiflem  14785  addcos  14904  demoivreALT  14931  dvdsaddr  15025  sumodd  15111  divalglem4  15119  divalgb  15127  gcdaddm  15246  hashdvds  15480  phiprmpw  15481  pythagtriplem2  15522  prmgaplem7  15761  mulgnndir  17569  mulgnndirOLD  17570  cnaddablx  18271  cnaddabl  18272  zaddablx  18275  cncrng  19767  ioo2bl  22596  icopnfcnv  22741  uniioombllem3  23353  fta1glem1  23925  plyremlem  24059  fta1lem  24062  vieta1lem1  24065  vieta1lem2  24066  aaliou3lem2  24098  dvradcnv  24175  pserdv2  24184  reeff1olem  24200  ptolemy  24248  logcnlem4  24391  cxpsqrt  24449  atandm2  24604  atandm4  24606  atanlogsublem  24642  2efiatan  24645  dvatan  24662  birthdaylem2  24679  emcllem2  24723  fsumharmonic  24738  wilthlem1  24794  wilthlem2  24795  basellem8  24814  1sgmprm  24924  perfectlem2  24955  pntibndlem1  25278  pntibndlem2  25280  pntlemd  25283  pntlemc  25284  eucrctshift  27103  cnaddabloOLD  27436  cdj3lem3b  29299  isarchi3  29741  archiabllem2c  29749  cos2h  33400  tan2h  33401  eldioph2lem1  37323  addcomgi  38660  fz0addcom  41327  epoo  41612  perfectALTVlem2  41631  sbgoldbaltlem2  41668