Theorem addcomd 10841

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 10635	. . . . . . . 8 ⊢ (𝜑 → 1 ∈ ℂ)
2	1, 1	addcld 10659	. . . . . . 7 ⊢ (𝜑 → (1 + 1) ∈ ℂ)
3		muld.1	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ ℂ)
4		addcomd.2	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ ℂ)
5	2, 3, 4	adddid 10664	. . . . . 6 ⊢ (𝜑 → ((1 + 1) · (𝐴 + 𝐵)) = (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)))
6	3, 4	addcld 10659	. . . . . . 7 ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℂ)
7		1p1times 10810	. . . . . . 7 ⊢ ((𝐴 + 𝐵) ∈ ℂ → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
8	6, 7	syl 17	. . . . . 6 ⊢ (𝜑 → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
9		1p1times 10810	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
10	3, 9	syl 17	. . . . . . 7 ⊢ (𝜑 → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
11		1p1times 10810	. . . . . . . 8 ⊢ (𝐵 ∈ ℂ → ((1 + 1) · 𝐵) = (𝐵 + 𝐵))
12	4, 11	syl 17	. . . . . . 7 ⊢ (𝜑 → ((1 + 1) · 𝐵) = (𝐵 + 𝐵))
13	10, 12	oveq12d 7173	. . . . . 6 ⊢ (𝜑 → (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
14	5, 8, 13	3eqtr3rd 2865	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐴) + (𝐵 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
15	3, 3	addcld 10659	. . . . . 6 ⊢ (𝜑 → (𝐴 + 𝐴) ∈ ℂ)
16	15, 4, 4	addassd 10662	. . . . 5 ⊢ (𝜑 → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
17	6, 3, 4	addassd 10662	. . . . 5 ⊢ (𝜑 → (((𝐴 + 𝐵) + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
18	14, 16, 17	3eqtr4d 2866	. . . 4 ⊢ (𝜑 → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵))
19	15, 4	addcld 10659	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) ∈ ℂ)
20	6, 3	addcld 10659	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐴) ∈ ℂ)
21		addcan2 10824	. . . . 5 ⊢ ((((𝐴 + 𝐴) + 𝐵) ∈ ℂ ∧ ((𝐴 + 𝐵) + 𝐴) ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
22	19, 20, 4, 21	syl3anc 1367	. . . 4 ⊢ (𝜑 → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
23	18, 22	mpbid 234	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴))
24	3, 3, 4	addassd 10662	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) = (𝐴 + (𝐴 + 𝐵)))
25	3, 4, 3	addassd 10662	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐴) = (𝐴 + (𝐵 + 𝐴)))
26	23, 24, 25	3eqtr3d 2864	. 2 ⊢ (𝜑 → (𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)))
27	4, 3	addcld 10659	. . 3 ⊢ (𝜑 → (𝐵 + 𝐴) ∈ ℂ)
28		addcan 10823	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ (𝐴 + 𝐵) ∈ ℂ ∧ (𝐵 + 𝐴) ∈ ℂ) → ((𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴)))
29	3, 6, 27, 28	syl3anc 1367	. 2 ⊢ (𝜑 → ((𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴)))
30	26, 29	mpbid 234	1 ⊢ (𝜑 → (𝐴 + 𝐵) = (𝐵 + 𝐴))

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1533   ∈ wcel 2110  (class class class)co 7155  ℂcc 10534  1c1 10537   + caddc 10539   · cmul 10541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5202  ax-nul 5209  ax-pow 5265  ax-pr 5329  ax-un 7460  ax-resscn 10593  ax-1cn 10594  ax-icn 10595  ax-addcl 10596  ax-addrcl 10597  ax-mulcl 10598  ax-mulrcl 10599  ax-mulcom 10600  ax-addass 10601  ax-mulass 10602  ax-distr 10603  ax-i2m1 10604  ax-1ne0 10605  ax-1rid 10606  ax-rnegex 10607  ax-rrecex 10608  ax-cnre 10609  ax-pre-lttri 10610  ax-pre-lttrn 10611  ax-pre-ltadd 10612

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-pw 4540  df-sn 4567  df-pr 4569  df-op 4573  df-uni 4838  df-br 5066  df-opab 5128  df-mpt 5146  df-id 5459  df-po 5473  df-so 5474  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-iota 6313  df-fun 6356  df-fn 6357  df-f 6358  df-f1 6359  df-fo 6360  df-f1o 6361  df-fv 6362  df-ov 7158  df-er 8288  df-en 8509  df-dom 8510  df-sdom 8511  df-pnf 10676  df-mnf 10677  df-ltxr 10679

This theorem is referenced by:  muladd11r  10852  comraddd  10853  subadd2  10889  pncan  10891  npcan  10894  subcan  10940  mvlladdd  11050  subaddeqd  11054  addrsub  11056  mulsubaddmulsub  11103  ltadd1  11106  leadd2  11108  ltsubadd2  11110  lesubadd2  11112  lesub3d  11257  supadd  11608  ltaddrp2d  12464  lincmb01cmp  12880  iccf1o  12881  modaddabs  13276  muladdmodid  13278  negmod  13283  modadd2mod  13288  modadd12d  13294  modaddmulmod  13305  addmodlteq  13313  expaddz  13472  bcn2m1  13683  bcn2p1  13684  spllen  14115  splfv2a  14117  relexpaddnn  14409  relexpaddg  14411  rtrclreclem3  14418  remullem  14486  sqreulem  14718  bhmafibid2  14825  climaddc2  14991  iseraltlem2  15038  telfsumo  15156  fsumparts  15160  bcxmas  15189  bpoly4  15412  sinadd  15516  sincossq  15528  cos2t  15530  absefi  15548  dvdsaddre2b  15656  pwp1fsum  15741  sadadd2lem2  15798  bitsres  15821  bezoutlem2  15887  bezoutlem4  15889  pythagtrip  16170  pcadd2  16225  vdwapun  16309  vdwlem5  16320  vdwlem6  16321  vdwlem8  16323  gsumsgrpccat  18003  gsumccatOLD  18004  mulgnndir  18255  mulgdirlem  18257  cyccom  18345  efgcpbllemb  18880  cygablOLD  19010  ablfacrp  19187  rzgrp  20766  icccvx  23553  cnlmod  23743  cphipval  23845  pjthlem1  24039  cmmbl  24134  voliunlem1  24150  dvle  24603  dvcvx  24616  dvfsumlem2  24623  dvfsumlem4  24625  dvfsum2  24630  ply1divex  24729  plymullem1  24803  coeeulem  24813  aaliou3lem6  24936  dvtaylp  24957  ulmcn  24986  abelthlem7  25025  pilem3  25040  lawcos  25393  affineequiv  25400  affineequiv3  25402  heron  25415  dcubic1lem  25420  dcubic2  25421  dcubic  25423  mcubic  25424  quart1lem  25432  quart1  25433  asinlem2  25446  asinsin  25469  cosasin  25481  atanlogaddlem  25490  atanlogadd  25491  cvxcl  25561  lgamgulmlem2  25606  lgamcvg2  25631  lgam1  25640  bposlem9  25867  lgseisenlem1  25950  2sqlem3  25995  2sqblem  26006  2sqmod  26011  addsqn2reu  26016  2sqreulem1  26021  2sqreunnlem1  26024  dchrisumlem2  26065  selberg  26123  selberg2  26126  selberg4  26136  pntrlog2bndlem1  26152  pntlemb  26172  pntlemf  26180  padicabv  26205  colinearalglem2  26692  axsegconlem9  26710  axeuclidlem  26747  eupth2lem3lem3  28008  numclwwlk3lem1  28160  smcnlem  28473  ipval2  28483  hhph  28954  pjhthlem1  29167  golem1  30047  stcltrlem1  30052  omndmul2  30713  cycpmco2lem3  30770  cycpmco2lem4  30771  cycpmco2lem5  30772  cycpmco2lem6  30773  cycpmco2  30775  archirngz  30818  archiabllem1a  30820  archiabllem1  30822  archiabllem2c  30824  ballotlemsdom  31769  fsum2dsub  31878  revwlk  32371  resconn  32493  iprodgam  32974  faclimlem1  32975  faclimlem3  32977  faclim  32978  iprodfac  32979  fwddifnp1  33626  dnibndlem7  33823  dnibndlem8  33824  knoppndvlem14  33864  bj-bary1  34592  dvtan  34941  itg2addnclem3  34944  itgaddnclem2  34950  itgmulc2nc  34959  ftc1anclem8  34973  dvasin  34977  areacirclem1  34981  dffltz  39269  fltnltalem  39272  3cubeslem2  39280  3cubeslem3l  39281  3cubeslem3r  39282  pellexlem2  39425  pell14qrgt0  39454  rmxyadd  39516  rmxluc  39531  fzmaxdif  39576  acongeq  39578  jm2.19lem2  39585  jm2.26lem3  39596  areaquad  39821  int-addcomd  40524  int-leftdistd  40530  subadd4b  41546  sub31  41555  fsumsplit1  41851  coseq0  42143  coskpi2  42145  cosknegpi  42148  fperdvper  42201  dvbdfbdioolem2  42212  dvnmul  42226  dvmptfprodlem  42227  itgsincmulx  42257  itgsbtaddcnst  42265  stoweidlem11  42295  stirlinglem5  42362  stirlinglem7  42364  dirkertrigeqlem1  42382  dirkertrigeqlem2  42383  dirkertrigeqlem3  42384  dirkertrigeq  42385  dirkercncflem2  42388  fourierdlem4  42395  fourierdlem26  42417  fourierdlem40  42431  fourierdlem42  42433  fourierdlem47  42437  fourierdlem63  42453  fourierdlem64  42454  fourierdlem65  42455  fourierdlem74  42464  fourierdlem75  42465  fourierdlem78  42468  fourierdlem79  42469  fourierdlem84  42474  fourierdlem93  42483  fourierdlem103  42493  fourierdlem111  42501  fourierswlem  42514  fouriersw  42515  etransclem32  42550  etransclem46  42564  sge0gtfsumgt  42724  hoidmv1lelem2  42873  hoidmvlelem2  42877  hspmbllem1  42907  smfmullem1  43065  sigarperm  43116  2elfz2melfz  43517  fargshiftfo  43601  ichexmpl2  43631  fmtnorec3  43709  2zrngacmnd  44212  2zrngagrp  44213  ply1mulgsumlem1  44439  m1modmmod  44580  resum2sqorgt0  44695  eenglngeehlnmlem2  44724  rrx2linest2  44730  line2xlem  44739  itsclc0yqsollem1  44748  itsclc0yqsol  44750  itscnhlc0xyqsol  44751  itsclc0xyqsolr  44755  itsclinecirc0b  44760  itsclquadb  44762  2itscplem1  44764  2itscp  44767  onetansqsecsq  44859