Theorem addcomd 11107

Description: Addition commutes. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013.) (Revised by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
muld.1	⊢ (𝜑 → 𝐴 ∈ ℂ)
addcomd.2	⊢ (𝜑 → 𝐵 ∈ ℂ)

Assertion

Ref	Expression
addcomd	⊢ (𝜑 → (𝐴 + 𝐵) = (𝐵 + 𝐴))

Proof of Theorem addcomd

Step	Hyp	Ref	Expression
1		1cnd 10901	. . . . . . . 8 ⊢ (𝜑 → 1 ∈ ℂ)
2	1, 1	addcld 10925	. . . . . . 7 ⊢ (𝜑 → (1 + 1) ∈ ℂ)
3		muld.1	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ ℂ)
4		addcomd.2	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ ℂ)
5	2, 3, 4	adddid 10930	. . . . . 6 ⊢ (𝜑 → ((1 + 1) · (𝐴 + 𝐵)) = (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)))
6	3, 4	addcld 10925	. . . . . . 7 ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℂ)
7		1p1times 11076	. . . . . . 7 ⊢ ((𝐴 + 𝐵) ∈ ℂ → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
8	6, 7	syl 17	. . . . . 6 ⊢ (𝜑 → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
9		1p1times 11076	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
10	3, 9	syl 17	. . . . . . 7 ⊢ (𝜑 → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
11		1p1times 11076	. . . . . . . 8 ⊢ (𝐵 ∈ ℂ → ((1 + 1) · 𝐵) = (𝐵 + 𝐵))
12	4, 11	syl 17	. . . . . . 7 ⊢ (𝜑 → ((1 + 1) · 𝐵) = (𝐵 + 𝐵))
13	10, 12	oveq12d 7273	. . . . . 6 ⊢ (𝜑 → (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
14	5, 8, 13	3eqtr3rd 2787	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐴) + (𝐵 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
15	3, 3	addcld 10925	. . . . . 6 ⊢ (𝜑 → (𝐴 + 𝐴) ∈ ℂ)
16	15, 4, 4	addassd 10928	. . . . 5 ⊢ (𝜑 → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
17	6, 3, 4	addassd 10928	. . . . 5 ⊢ (𝜑 → (((𝐴 + 𝐵) + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
18	14, 16, 17	3eqtr4d 2788	. . . 4 ⊢ (𝜑 → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵))
19	15, 4	addcld 10925	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) ∈ ℂ)
20	6, 3	addcld 10925	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐴) ∈ ℂ)
21		addcan2 11090	. . . . 5 ⊢ ((((𝐴 + 𝐴) + 𝐵) ∈ ℂ ∧ ((𝐴 + 𝐵) + 𝐴) ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
22	19, 20, 4, 21	syl3anc 1369	. . . 4 ⊢ (𝜑 → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
23	18, 22	mpbid 231	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴))
24	3, 3, 4	addassd 10928	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) = (𝐴 + (𝐴 + 𝐵)))
25	3, 4, 3	addassd 10928	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐴) = (𝐴 + (𝐵 + 𝐴)))
26	23, 24, 25	3eqtr3d 2786	. 2 ⊢ (𝜑 → (𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)))
27	4, 3	addcld 10925	. . 3 ⊢ (𝜑 → (𝐵 + 𝐴) ∈ ℂ)
28		addcan 11089	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ (𝐴 + 𝐵) ∈ ℂ ∧ (𝐵 + 𝐴) ∈ ℂ) → ((𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴)))
29	3, 6, 27, 28	syl3anc 1369	. 2 ⊢ (𝜑 → ((𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴)))
30	26, 29	mpbid 231	1 ⊢ (𝜑 → (𝐴 + 𝐵) = (𝐵 + 𝐴))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539   ∈ wcel 2108  (class class class)co 7255  ℂcc 10800  1c1 10803   + caddc 10805   · cmul 10807

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-resscn 10859  ax-1cn 10860  ax-icn 10861  ax-addcl 10862  ax-addrcl 10863  ax-mulcl 10864  ax-mulrcl 10865  ax-mulcom 10866  ax-addass 10867  ax-mulass 10868  ax-distr 10869  ax-i2m1 10870  ax-1ne0 10871  ax-1rid 10872  ax-rnegex 10873  ax-rrecex 10874  ax-cnre 10875  ax-pre-lttri 10876  ax-pre-lttrn 10877  ax-pre-ltadd 10878

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-po 5494  df-so 5495  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-ov 7258  df-er 8456  df-en 8692  df-dom 8693  df-sdom 8694  df-pnf 10942  df-mnf 10943  df-ltxr 10945

This theorem is referenced by:  muladd11r  11118  comraddd  11119  subadd2  11155  pncan  11157  npcan  11160  subcan  11206  mvlladdd  11316  subaddeqd  11320  addrsub  11322  mulsubaddmulsub  11369  ltadd1  11372  leadd2  11374  ltsubadd2  11376  lesubadd2  11378  lesub3d  11523  supadd  11873  ltaddrp2d  12735  lincmb01cmp  13156  iccf1o  13157  modaddabs  13557  muladdmodid  13559  negmod  13564  modadd2mod  13569  modadd12d  13575  modaddmulmod  13586  addmodlteq  13594  expaddz  13755  bcn2m1  13966  bcn2p1  13967  spllen  14395  splfv2a  14397  relexpaddnn  14690  relexpaddg  14692  rtrclreclem3  14699  remullem  14767  sqreulem  14999  bhmafibid2  15106  climaddc2  15273  iseraltlem2  15322  fsumsplit1  15385  telfsumo  15442  fsumparts  15446  bcxmas  15475  bpoly4  15697  sinadd  15801  sincossq  15813  cos2t  15815  absefi  15833  dvdsaddre2b  15944  pwp1fsum  16028  sadadd2lem2  16085  bitsres  16108  bezoutlem2  16176  bezoutlem4  16178  pythagtrip  16463  pcadd2  16519  vdwapun  16603  vdwlem5  16614  vdwlem6  16615  vdwlem8  16617  gsumsgrpccat  18393  gsumccatOLD  18394  mulgnndir  18647  mulgdirlem  18649  cyccom  18737  efgcpbllemb  19276  cygablOLD  19407  ablfacrp  19584  rzgrp  20740  icccvx  24019  cnlmod  24209  cphipval  24312  pjthlem1  24506  cmmbl  24603  voliunlem1  24619  dvle  25076  dvcvx  25089  dvfsumlem2  25096  dvfsumlem4  25098  dvfsum2  25103  ply1divex  25206  plymullem1  25280  coeeulem  25290  aaliou3lem6  25413  dvtaylp  25434  ulmcn  25463  abelthlem7  25502  pilem3  25517  lawcos  25871  affineequiv  25878  affineequiv3  25880  heron  25893  dcubic1lem  25898  dcubic2  25899  dcubic  25901  mcubic  25902  quart1lem  25910  quart1  25911  asinlem2  25924  asinsin  25947  cosasin  25959  atanlogaddlem  25968  atanlogadd  25969  cvxcl  26039  lgamgulmlem2  26084  lgamcvg2  26109  lgam1  26118  bposlem9  26345  lgseisenlem1  26428  2sqlem3  26473  2sqblem  26484  2sqmod  26489  addsqn2reu  26494  2sqreulem1  26499  2sqreunnlem1  26502  dchrisumlem2  26543  selberg  26601  selberg2  26604  selberg4  26614  pntrlog2bndlem1  26630  pntlemb  26650  pntlemf  26658  padicabv  26683  colinearalglem2  27178  axsegconlem9  27196  axeuclidlem  27233  eupth2lem3lem3  28495  numclwwlk3lem1  28647  smcnlem  28960  ipval2  28970  hhph  29441  pjhthlem1  29654  golem1  30534  stcltrlem1  30539  omndmul2  31240  cycpmco2lem3  31297  cycpmco2lem4  31298  cycpmco2lem5  31299  cycpmco2lem6  31300  cycpmco2  31302  archirngz  31345  archiabllem1a  31347  archiabllem1  31349  archiabllem2c  31351  ballotlemsdom  32378  fsum2dsub  32487  revwlk  32986  resconn  33108  iprodgam  33614  faclimlem1  33615  faclimlem3  33617  faclim  33618  iprodfac  33619  fwddifnp1  34394  dnibndlem7  34591  dnibndlem8  34592  knoppndvlem14  34632  bj-bary1  35410  dvtan  35754  itgaddnclem2  35763  itgmulc2nc  35772  ftc1anclem8  35784  dvasin  35788  areacirclem1  35792  lcmineqlem19  39983  aks4d1p1p2  40006  sticksstones7  40036  sticksstones12a  40041  sticksstones12  40042  metakunt15  40067  metakunt16  40068  dffltz  40387  fltbccoprm  40394  flt4lem3  40401  flt4lem5c  40407  flt4lem5d  40408  flt4lem5e  40409  flt4lem7  40412  nna4b4nsq  40413  fltnltalem  40415  3cubeslem2  40423  3cubeslem3l  40424  3cubeslem3r  40425  pellexlem2  40568  pell14qrgt0  40597  rmxyadd  40659  rmxluc  40674  fzmaxdif  40719  acongeq  40721  jm2.19lem2  40728  jm2.26lem3  40739  areaquad  40963  sqrtcval  41138  int-addcomd  41673  int-leftdistd  41679  subadd4b  42710  sub31  42719  coseq0  43295  coskpi2  43297  cosknegpi  43300  fperdvper  43350  dvbdfbdioolem2  43360  dvnmul  43374  dvmptfprodlem  43375  itgsincmulx  43405  itgsbtaddcnst  43413  stoweidlem11  43442  stirlinglem5  43509  stirlinglem7  43511  dirkertrigeqlem1  43529  dirkertrigeqlem2  43530  dirkertrigeqlem3  43531  dirkertrigeq  43532  dirkercncflem2  43535  fourierdlem4  43542  fourierdlem26  43564  fourierdlem40  43578  fourierdlem42  43580  fourierdlem47  43584  fourierdlem63  43600  fourierdlem64  43601  fourierdlem65  43602  fourierdlem74  43611  fourierdlem75  43612  fourierdlem78  43615  fourierdlem79  43616  fourierdlem84  43621  fourierdlem93  43630  fourierdlem103  43640  fourierdlem111  43648  fourierswlem  43661  fouriersw  43662  etransclem32  43697  etransclem46  43711  sge0gtfsumgt  43871  hoidmv1lelem2  44020  hoidmvlelem2  44024  hspmbllem1  44054  smfmullem1  44212  sigarperm  44263  2elfz2melfz  44698  fargshiftfo  44782  ichexmpl2  44810  fmtnorec3  44888  2zrngacmnd  45388  2zrngagrp  45389  ply1mulgsumlem1  45615  m1modmmod  45755  ackval1  45915  ackval2  45916  resum2sqorgt0  45943  eenglngeehlnmlem2  45972  rrx2linest2  45978  line2xlem  45987  itsclc0yqsollem1  45996  itsclc0yqsol  45998  itscnhlc0xyqsol  45999  itsclc0xyqsolr  46003  itsclinecirc0b  46008  itsclquadb  46010  2itscplem1  46012  2itscp  46015  onetansqsecsq  46349