Theorem addcomd 11160

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 10954	. . . . . . . 8 ⊢ (𝜑 → 1 ∈ ℂ)
2	1, 1	addcld 10978	. . . . . . 7 ⊢ (𝜑 → (1 + 1) ∈ ℂ)
3		muld.1	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ ℂ)
4		addcomd.2	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ ℂ)
5	2, 3, 4	adddid 10983	. . . . . 6 ⊢ (𝜑 → ((1 + 1) · (𝐴 + 𝐵)) = (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)))
6	3, 4	addcld 10978	. . . . . . 7 ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℂ)
7		1p1times 11129	. . . . . . 7 ⊢ ((𝐴 + 𝐵) ∈ ℂ → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
8	6, 7	syl 17	. . . . . 6 ⊢ (𝜑 → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
9		1p1times 11129	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
10	3, 9	syl 17	. . . . . . 7 ⊢ (𝜑 → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
11		1p1times 11129	. . . . . . . 8 ⊢ (𝐵 ∈ ℂ → ((1 + 1) · 𝐵) = (𝐵 + 𝐵))
12	4, 11	syl 17	. . . . . . 7 ⊢ (𝜑 → ((1 + 1) · 𝐵) = (𝐵 + 𝐵))
13	10, 12	oveq12d 7286	. . . . . 6 ⊢ (𝜑 → (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
14	5, 8, 13	3eqtr3rd 2788	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐴) + (𝐵 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
15	3, 3	addcld 10978	. . . . . 6 ⊢ (𝜑 → (𝐴 + 𝐴) ∈ ℂ)
16	15, 4, 4	addassd 10981	. . . . 5 ⊢ (𝜑 → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
17	6, 3, 4	addassd 10981	. . . . 5 ⊢ (𝜑 → (((𝐴 + 𝐵) + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
18	14, 16, 17	3eqtr4d 2789	. . . 4 ⊢ (𝜑 → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵))
19	15, 4	addcld 10978	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) ∈ ℂ)
20	6, 3	addcld 10978	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐴) ∈ ℂ)
21		addcan2 11143	. . . . 5 ⊢ ((((𝐴 + 𝐴) + 𝐵) ∈ ℂ ∧ ((𝐴 + 𝐵) + 𝐴) ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
22	19, 20, 4, 21	syl3anc 1369	. . . 4 ⊢ (𝜑 → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
23	18, 22	mpbid 231	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴))
24	3, 3, 4	addassd 10981	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) = (𝐴 + (𝐴 + 𝐵)))
25	3, 4, 3	addassd 10981	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐴) = (𝐴 + (𝐵 + 𝐴)))
26	23, 24, 25	3eqtr3d 2787	. 2 ⊢ (𝜑 → (𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)))
27	4, 3	addcld 10978	. . 3 ⊢ (𝜑 → (𝐵 + 𝐴) ∈ ℂ)
28		addcan 11142	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ (𝐴 + 𝐵) ∈ ℂ ∧ (𝐵 + 𝐴) ∈ ℂ) → ((𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴)))
29	3, 6, 27, 28	syl3anc 1369	. 2 ⊢ (𝜑 → ((𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴)))
30	26, 29	mpbid 231	1 ⊢ (𝜑 → (𝐴 + 𝐵) = (𝐵 + 𝐴))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541   ∈ wcel 2109  (class class class)co 7268  ℂcc 10853  1c1 10856   + caddc 10858   · cmul 10860

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-10 2140  ax-11 2157  ax-12 2174  ax-ext 2710  ax-sep 5226  ax-nul 5233  ax-pow 5291  ax-pr 5355  ax-un 7579  ax-resscn 10912  ax-1cn 10913  ax-icn 10914  ax-addcl 10915  ax-addrcl 10916  ax-mulcl 10917  ax-mulrcl 10918  ax-mulcom 10919  ax-addass 10920  ax-mulass 10921  ax-distr 10922  ax-i2m1 10923  ax-1ne0 10924  ax-1rid 10925  ax-rnegex 10926  ax-rrecex 10927  ax-cnre 10928  ax-pre-lttri 10929  ax-pre-lttrn 10930  ax-pre-ltadd 10931

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-nf 1790  df-sb 2071  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3432  df-sbc 3720  df-csb 3837  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-nul 4262  df-if 4465  df-pw 4540  df-sn 4567  df-pr 4569  df-op 4573  df-uni 4845  df-br 5079  df-opab 5141  df-mpt 5162  df-id 5488  df-po 5502  df-so 5503  df-xp 5594  df-rel 5595  df-cnv 5596  df-co 5597  df-dm 5598  df-rn 5599  df-res 5600  df-ima 5601  df-iota 6388  df-fun 6432  df-fn 6433  df-f 6434  df-f1 6435  df-fo 6436  df-f1o 6437  df-fv 6438  df-ov 7271  df-er 8472  df-en 8708  df-dom 8709  df-sdom 8710  df-pnf 10995  df-mnf 10996  df-ltxr 10998

This theorem is referenced by:  muladd11r  11171  comraddd  11172  subadd2  11208  pncan  11210  npcan  11213  subcan  11259  mvlladdd  11369  subaddeqd  11373  addrsub  11375  mulsubaddmulsub  11422  ltadd1  11425  leadd2  11427  ltsubadd2  11429  lesubadd2  11431  lesub3d  11576  supadd  11926  ltaddrp2d  12788  lincmb01cmp  13209  iccf1o  13210  modaddabs  13610  muladdmodid  13612  negmod  13617  modadd2mod  13622  modadd12d  13628  modaddmulmod  13639  addmodlteq  13647  expaddz  13808  bcn2m1  14019  bcn2p1  14020  spllen  14448  splfv2a  14450  relexpaddnn  14743  relexpaddg  14745  rtrclreclem3  14752  remullem  14820  sqreulem  15052  bhmafibid2  15159  climaddc2  15326  iseraltlem2  15375  fsumsplit1  15438  telfsumo  15495  fsumparts  15499  bcxmas  15528  bpoly4  15750  sinadd  15854  sincossq  15866  cos2t  15868  absefi  15886  dvdsaddre2b  15997  pwp1fsum  16081  sadadd2lem2  16138  bitsres  16161  bezoutlem2  16229  bezoutlem4  16231  pythagtrip  16516  pcadd2  16572  vdwapun  16656  vdwlem5  16667  vdwlem6  16668  vdwlem8  16670  gsumsgrpccat  18459  gsumccatOLD  18460  mulgnndir  18713  mulgdirlem  18715  cyccom  18803  efgcpbllemb  19342  cygablOLD  19473  ablfacrp  19650  rzgrp  20809  icccvx  24094  cnlmod  24284  cphipval  24388  pjthlem1  24582  cmmbl  24679  voliunlem1  24695  dvle  25152  dvcvx  25165  dvfsumlem2  25172  dvfsumlem4  25174  dvfsum2  25179  ply1divex  25282  plymullem1  25356  coeeulem  25366  aaliou3lem6  25489  dvtaylp  25510  ulmcn  25539  abelthlem7  25578  pilem3  25593  lawcos  25947  affineequiv  25954  affineequiv3  25956  heron  25969  dcubic1lem  25974  dcubic2  25975  dcubic  25977  mcubic  25978  quart1lem  25986  quart1  25987  asinlem2  26000  asinsin  26023  cosasin  26035  atanlogaddlem  26044  atanlogadd  26045  cvxcl  26115  lgamgulmlem2  26160  lgamcvg2  26185  lgam1  26194  bposlem9  26421  lgseisenlem1  26504  2sqlem3  26549  2sqblem  26560  2sqmod  26565  addsqn2reu  26570  2sqreulem1  26575  2sqreunnlem1  26578  dchrisumlem2  26619  selberg  26677  selberg2  26680  selberg4  26690  pntrlog2bndlem1  26706  pntlemb  26726  pntlemf  26734  padicabv  26759  colinearalglem2  27256  axsegconlem9  27274  axeuclidlem  27311  eupth2lem3lem3  28573  numclwwlk3lem1  28725  smcnlem  29038  ipval2  29048  hhph  29519  pjhthlem1  29732  golem1  30612  stcltrlem1  30617  omndmul2  31317  cycpmco2lem3  31374  cycpmco2lem4  31375  cycpmco2lem5  31376  cycpmco2lem6  31377  cycpmco2  31379  archirngz  31422  archiabllem1a  31424  archiabllem1  31426  archiabllem2c  31428  ballotlemsdom  32457  fsum2dsub  32566  revwlk  33065  resconn  33187  iprodgam  33687  faclimlem1  33688  faclimlem3  33690  faclim  33691  iprodfac  33692  fwddifnp1  34446  dnibndlem7  34643  dnibndlem8  34644  knoppndvlem14  34684  bj-bary1  35462  dvtan  35806  itgaddnclem2  35815  itgmulc2nc  35824  ftc1anclem8  35836  dvasin  35840  areacirclem1  35844  lcmineqlem19  40035  aks4d1p1p2  40058  sticksstones7  40088  sticksstones12a  40093  sticksstones12  40094  metakunt15  40119  metakunt16  40120  dffltz  40451  fltbccoprm  40458  flt4lem3  40465  flt4lem5c  40471  flt4lem5d  40472  flt4lem5e  40473  flt4lem7  40476  nna4b4nsq  40477  fltnltalem  40479  3cubeslem2  40487  3cubeslem3l  40488  3cubeslem3r  40489  pellexlem2  40632  pell14qrgt0  40661  rmxyadd  40723  rmxluc  40738  fzmaxdif  40783  acongeq  40785  jm2.19lem2  40792  jm2.26lem3  40803  areaquad  41027  sqrtcval  41202  int-addcomd  41737  int-leftdistd  41743  subadd4b  42774  sub31  42783  coseq0  43359  coskpi2  43361  cosknegpi  43364  fperdvper  43414  dvbdfbdioolem2  43424  dvnmul  43438  dvmptfprodlem  43439  itgsincmulx  43469  itgsbtaddcnst  43477  stoweidlem11  43506  stirlinglem5  43573  stirlinglem7  43575  dirkertrigeqlem1  43593  dirkertrigeqlem2  43594  dirkertrigeqlem3  43595  dirkertrigeq  43596  dirkercncflem2  43599  fourierdlem4  43606  fourierdlem26  43628  fourierdlem40  43642  fourierdlem42  43644  fourierdlem47  43648  fourierdlem63  43664  fourierdlem64  43665  fourierdlem65  43666  fourierdlem74  43675  fourierdlem75  43676  fourierdlem78  43679  fourierdlem79  43680  fourierdlem84  43685  fourierdlem93  43694  fourierdlem103  43704  fourierdlem111  43712  fourierswlem  43725  fouriersw  43726  etransclem32  43761  etransclem46  43775  sge0gtfsumgt  43935  hoidmv1lelem2  44084  hoidmvlelem2  44088  hspmbllem1  44118  smfmullem1  44276  sigarperm  44327  2elfz2melfz  44762  fargshiftfo  44846  ichexmpl2  44874  fmtnorec3  44952  2zrngacmnd  45452  2zrngagrp  45453  ply1mulgsumlem1  45679  m1modmmod  45819  ackval1  45979  ackval2  45980  resum2sqorgt0  46007  eenglngeehlnmlem2  46036  rrx2linest2  46042  line2xlem  46051  itsclc0yqsollem1  46060  itsclc0yqsol  46062  itscnhlc0xyqsol  46063  itsclc0xyqsolr  46067  itsclinecirc0b  46072  itsclquadb  46074  2itscplem1  46076  2itscp  46079  onetansqsecsq  46415