Theorem addcomd 10999

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 10793	. . . . . . . 8 ⊢ (𝜑 → 1 ∈ ℂ)
2	1, 1	addcld 10817	. . . . . . 7 ⊢ (𝜑 → (1 + 1) ∈ ℂ)
3		muld.1	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ ℂ)
4		addcomd.2	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ ℂ)
5	2, 3, 4	adddid 10822	. . . . . 6 ⊢ (𝜑 → ((1 + 1) · (𝐴 + 𝐵)) = (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)))
6	3, 4	addcld 10817	. . . . . . 7 ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℂ)
7		1p1times 10968	. . . . . . 7 ⊢ ((𝐴 + 𝐵) ∈ ℂ → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
8	6, 7	syl 17	. . . . . 6 ⊢ (𝜑 → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
9		1p1times 10968	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
10	3, 9	syl 17	. . . . . . 7 ⊢ (𝜑 → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
11		1p1times 10968	. . . . . . . 8 ⊢ (𝐵 ∈ ℂ → ((1 + 1) · 𝐵) = (𝐵 + 𝐵))
12	4, 11	syl 17	. . . . . . 7 ⊢ (𝜑 → ((1 + 1) · 𝐵) = (𝐵 + 𝐵))
13	10, 12	oveq12d 7209	. . . . . 6 ⊢ (𝜑 → (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
14	5, 8, 13	3eqtr3rd 2780	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐴) + (𝐵 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
15	3, 3	addcld 10817	. . . . . 6 ⊢ (𝜑 → (𝐴 + 𝐴) ∈ ℂ)
16	15, 4, 4	addassd 10820	. . . . 5 ⊢ (𝜑 → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
17	6, 3, 4	addassd 10820	. . . . 5 ⊢ (𝜑 → (((𝐴 + 𝐵) + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
18	14, 16, 17	3eqtr4d 2781	. . . 4 ⊢ (𝜑 → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵))
19	15, 4	addcld 10817	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) ∈ ℂ)
20	6, 3	addcld 10817	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐴) ∈ ℂ)
21		addcan2 10982	. . . . 5 ⊢ ((((𝐴 + 𝐴) + 𝐵) ∈ ℂ ∧ ((𝐴 + 𝐵) + 𝐴) ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
22	19, 20, 4, 21	syl3anc 1373	. . . 4 ⊢ (𝜑 → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
23	18, 22	mpbid 235	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴))
24	3, 3, 4	addassd 10820	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) = (𝐴 + (𝐴 + 𝐵)))
25	3, 4, 3	addassd 10820	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐴) = (𝐴 + (𝐵 + 𝐴)))
26	23, 24, 25	3eqtr3d 2779	. 2 ⊢ (𝜑 → (𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)))
27	4, 3	addcld 10817	. . 3 ⊢ (𝜑 → (𝐵 + 𝐴) ∈ ℂ)
28		addcan 10981	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ (𝐴 + 𝐵) ∈ ℂ ∧ (𝐵 + 𝐴) ∈ ℂ) → ((𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴)))
29	3, 6, 27, 28	syl3anc 1373	. 2 ⊢ (𝜑 → ((𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴)))
30	26, 29	mpbid 235	1 ⊢ (𝜑 → (𝐴 + 𝐵) = (𝐵 + 𝐴))

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1543   ∈ wcel 2112  (class class class)co 7191  ℂcc 10692  1c1 10695   + caddc 10697   · cmul 10699

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2708  ax-sep 5177  ax-nul 5184  ax-pow 5243  ax-pr 5307  ax-un 7501  ax-resscn 10751  ax-1cn 10752  ax-icn 10753  ax-addcl 10754  ax-addrcl 10755  ax-mulcl 10756  ax-mulrcl 10757  ax-mulcom 10758  ax-addass 10759  ax-mulass 10760  ax-distr 10761  ax-i2m1 10762  ax-1ne0 10763  ax-1rid 10764  ax-rnegex 10765  ax-rrecex 10766  ax-cnre 10767  ax-pre-lttri 10768  ax-pre-lttrn 10769  ax-pre-ltadd 10770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2728  df-clel 2809  df-nfc 2879  df-ne 2933  df-nel 3037  df-ral 3056  df-rex 3057  df-rab 3060  df-v 3400  df-sbc 3684  df-csb 3799  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4224  df-if 4426  df-pw 4501  df-sn 4528  df-pr 4530  df-op 4534  df-uni 4806  df-br 5040  df-opab 5102  df-mpt 5121  df-id 5440  df-po 5453  df-so 5454  df-xp 5542  df-rel 5543  df-cnv 5544  df-co 5545  df-dm 5546  df-rn 5547  df-res 5548  df-ima 5549  df-iota 6316  df-fun 6360  df-fn 6361  df-f 6362  df-f1 6363  df-fo 6364  df-f1o 6365  df-fv 6366  df-ov 7194  df-er 8369  df-en 8605  df-dom 8606  df-sdom 8607  df-pnf 10834  df-mnf 10835  df-ltxr 10837

This theorem is referenced by:  muladd11r  11010  comraddd  11011  subadd2  11047  pncan  11049  npcan  11052  subcan  11098  mvlladdd  11208  subaddeqd  11212  addrsub  11214  mulsubaddmulsub  11261  ltadd1  11264  leadd2  11266  ltsubadd2  11268  lesubadd2  11270  lesub3d  11415  supadd  11765  ltaddrp2d  12627  lincmb01cmp  13048  iccf1o  13049  modaddabs  13447  muladdmodid  13449  negmod  13454  modadd2mod  13459  modadd12d  13465  modaddmulmod  13476  addmodlteq  13484  expaddz  13644  bcn2m1  13855  bcn2p1  13856  spllen  14284  splfv2a  14286  relexpaddnn  14579  relexpaddg  14581  rtrclreclem3  14588  remullem  14656  sqreulem  14888  bhmafibid2  14995  climaddc2  15162  iseraltlem2  15211  telfsumo  15329  fsumparts  15333  bcxmas  15362  bpoly4  15584  sinadd  15688  sincossq  15700  cos2t  15702  absefi  15720  dvdsaddre2b  15831  pwp1fsum  15915  sadadd2lem2  15972  bitsres  15995  bezoutlem2  16063  bezoutlem4  16065  pythagtrip  16350  pcadd2  16406  vdwapun  16490  vdwlem5  16501  vdwlem6  16502  vdwlem8  16504  gsumsgrpccat  18220  gsumccatOLD  18221  mulgnndir  18474  mulgdirlem  18476  cyccom  18564  efgcpbllemb  19099  cygablOLD  19230  ablfacrp  19407  rzgrp  20539  icccvx  23801  cnlmod  23991  cphipval  24094  pjthlem1  24288  cmmbl  24385  voliunlem1  24401  dvle  24858  dvcvx  24871  dvfsumlem2  24878  dvfsumlem4  24880  dvfsum2  24885  ply1divex  24988  plymullem1  25062  coeeulem  25072  aaliou3lem6  25195  dvtaylp  25216  ulmcn  25245  abelthlem7  25284  pilem3  25299  lawcos  25653  affineequiv  25660  affineequiv3  25662  heron  25675  dcubic1lem  25680  dcubic2  25681  dcubic  25683  mcubic  25684  quart1lem  25692  quart1  25693  asinlem2  25706  asinsin  25729  cosasin  25741  atanlogaddlem  25750  atanlogadd  25751  cvxcl  25821  lgamgulmlem2  25866  lgamcvg2  25891  lgam1  25900  bposlem9  26127  lgseisenlem1  26210  2sqlem3  26255  2sqblem  26266  2sqmod  26271  addsqn2reu  26276  2sqreulem1  26281  2sqreunnlem1  26284  dchrisumlem2  26325  selberg  26383  selberg2  26386  selberg4  26396  pntrlog2bndlem1  26412  pntlemb  26432  pntlemf  26440  padicabv  26465  colinearalglem2  26952  axsegconlem9  26970  axeuclidlem  27007  eupth2lem3lem3  28267  numclwwlk3lem1  28419  smcnlem  28732  ipval2  28742  hhph  29213  pjhthlem1  29426  golem1  30306  stcltrlem1  30311  omndmul2  31011  cycpmco2lem3  31068  cycpmco2lem4  31069  cycpmco2lem5  31070  cycpmco2lem6  31071  cycpmco2  31073  archirngz  31116  archiabllem1a  31118  archiabllem1  31120  archiabllem2c  31122  ballotlemsdom  32144  fsum2dsub  32253  revwlk  32753  resconn  32875  iprodgam  33377  faclimlem1  33378  faclimlem3  33380  faclim  33381  iprodfac  33382  fwddifnp1  34153  dnibndlem7  34350  dnibndlem8  34351  knoppndvlem14  34391  bj-bary1  35166  dvtan  35513  itgaddnclem2  35522  itgmulc2nc  35531  ftc1anclem8  35543  dvasin  35547  areacirclem1  35551  lcmineqlem19  39738  aks4d1p1p2  39760  sticksstones7  39777  sticksstones12a  39782  sticksstones12  39783  metakunt15  39802  metakunt16  39803  dffltz  40115  fltbccoprm  40122  flt4lem3  40129  flt4lem5c  40135  flt4lem5d  40136  flt4lem5e  40137  flt4lem7  40140  nna4b4nsq  40141  fltnltalem  40143  3cubeslem2  40151  3cubeslem3l  40152  3cubeslem3r  40153  pellexlem2  40296  pell14qrgt0  40325  rmxyadd  40387  rmxluc  40402  fzmaxdif  40447  acongeq  40449  jm2.19lem2  40456  jm2.26lem3  40467  areaquad  40691  sqrtcval  40866  int-addcomd  41403  int-leftdistd  41409  subadd4b  42434  sub31  42443  fsumsplit1  42731  coseq0  43023  coskpi2  43025  cosknegpi  43028  fperdvper  43078  dvbdfbdioolem2  43088  dvnmul  43102  dvmptfprodlem  43103  itgsincmulx  43133  itgsbtaddcnst  43141  stoweidlem11  43170  stirlinglem5  43237  stirlinglem7  43239  dirkertrigeqlem1  43257  dirkertrigeqlem2  43258  dirkertrigeqlem3  43259  dirkertrigeq  43260  dirkercncflem2  43263  fourierdlem4  43270  fourierdlem26  43292  fourierdlem40  43306  fourierdlem42  43308  fourierdlem47  43312  fourierdlem63  43328  fourierdlem64  43329  fourierdlem65  43330  fourierdlem74  43339  fourierdlem75  43340  fourierdlem78  43343  fourierdlem79  43344  fourierdlem84  43349  fourierdlem93  43358  fourierdlem103  43368  fourierdlem111  43376  fourierswlem  43389  fouriersw  43390  etransclem32  43425  etransclem46  43439  sge0gtfsumgt  43599  hoidmv1lelem2  43748  hoidmvlelem2  43752  hspmbllem1  43782  smfmullem1  43940  sigarperm  43991  2elfz2melfz  44426  fargshiftfo  44510  ichexmpl2  44538  fmtnorec3  44616  2zrngacmnd  45116  2zrngagrp  45117  ply1mulgsumlem1  45343  m1modmmod  45483  ackval1  45643  ackval2  45644  resum2sqorgt0  45671  eenglngeehlnmlem2  45700  rrx2linest2  45706  line2xlem  45715  itsclc0yqsollem1  45724  itsclc0yqsol  45726  itscnhlc0xyqsol  45727  itsclc0xyqsolr  45731  itsclinecirc0b  45736  itsclquadb  45738  2itscplem1  45740  2itscp  45743  onetansqsecsq  46077