Theorem addcomd 11340

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 11132	. . . . . . . 8 ⊢ (𝜑 → 1 ∈ ℂ)
2	1, 1	addcld 11156	. . . . . . 7 ⊢ (𝜑 → (1 + 1) ∈ ℂ)
3		muld.1	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ ℂ)
4		addcomd.2	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ ℂ)
5	2, 3, 4	adddid 11161	. . . . . 6 ⊢ (𝜑 → ((1 + 1) · (𝐴 + 𝐵)) = (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)))
6	3, 4	addcld 11156	. . . . . . 7 ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℂ)
7		1p1times 11309	. . . . . . 7 ⊢ ((𝐴 + 𝐵) ∈ ℂ → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
8	6, 7	syl 17	. . . . . 6 ⊢ (𝜑 → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
9		1p1times 11309	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
10	3, 9	syl 17	. . . . . . 7 ⊢ (𝜑 → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
11		1p1times 11309	. . . . . . . 8 ⊢ (𝐵 ∈ ℂ → ((1 + 1) · 𝐵) = (𝐵 + 𝐵))
12	4, 11	syl 17	. . . . . . 7 ⊢ (𝜑 → ((1 + 1) · 𝐵) = (𝐵 + 𝐵))
13	10, 12	oveq12d 7379	. . . . . 6 ⊢ (𝜑 → (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
14	5, 8, 13	3eqtr3rd 2781	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐴) + (𝐵 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
15	3, 3	addcld 11156	. . . . . 6 ⊢ (𝜑 → (𝐴 + 𝐴) ∈ ℂ)
16	15, 4, 4	addassd 11159	. . . . 5 ⊢ (𝜑 → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
17	6, 3, 4	addassd 11159	. . . . 5 ⊢ (𝜑 → (((𝐴 + 𝐵) + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
18	14, 16, 17	3eqtr4d 2782	. . . 4 ⊢ (𝜑 → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵))
19	15, 4	addcld 11156	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) ∈ ℂ)
20	6, 3	addcld 11156	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐴) ∈ ℂ)
21		addcan2 11323	. . . . 5 ⊢ ((((𝐴 + 𝐴) + 𝐵) ∈ ℂ ∧ ((𝐴 + 𝐵) + 𝐴) ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
22	19, 20, 4, 21	syl3anc 1374	. . . 4 ⊢ (𝜑 → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
23	18, 22	mpbid 232	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴))
24	3, 3, 4	addassd 11159	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) = (𝐴 + (𝐴 + 𝐵)))
25	3, 4, 3	addassd 11159	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐴) = (𝐴 + (𝐵 + 𝐴)))
26	23, 24, 25	3eqtr3d 2780	. 2 ⊢ (𝜑 → (𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)))
27	4, 3	addcld 11156	. . 3 ⊢ (𝜑 → (𝐵 + 𝐴) ∈ ℂ)
28		addcan 11322	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ (𝐴 + 𝐵) ∈ ℂ ∧ (𝐵 + 𝐴) ∈ ℂ) → ((𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴)))
29	3, 6, 27, 28	syl3anc 1374	. 2 ⊢ (𝜑 → ((𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴)))
30	26, 29	mpbid 232	1 ⊢ (𝜑 → (𝐴 + 𝐵) = (𝐵 + 𝐴))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114  (class class class)co 7361  ℂcc 11029  1c1 11032   + caddc 11034   · cmul 11036

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5242  ax-nul 5252  ax-pow 5311  ax-pr 5378  ax-un 7683  ax-resscn 11088  ax-1cn 11089  ax-icn 11090  ax-addcl 11091  ax-addrcl 11092  ax-mulcl 11093  ax-mulrcl 11094  ax-mulcom 11095  ax-addass 11096  ax-mulass 11097  ax-distr 11098  ax-i2m1 11099  ax-1ne0 11100  ax-1rid 11101  ax-rnegex 11102  ax-rrecex 11103  ax-cnre 11104  ax-pre-lttri 11105  ax-pre-lttrn 11106  ax-pre-ltadd 11107

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3062  df-rab 3401  df-v 3443  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4287  df-if 4481  df-pw 4557  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5520  df-po 5533  df-so 5534  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-ov 7364  df-er 8638  df-en 8889  df-dom 8890  df-sdom 8891  df-pnf 11173  df-mnf 11174  df-ltxr 11176

This theorem is referenced by:  muladd11r  11351  comraddd  11352  subadd2  11389  pncan  11391  npcan  11394  subcan  11441  mvlladdd  11553  subaddeqd  11557  addrsub  11559  mulsubaddmulsub  11606  ltadd1  11609  leadd2  11611  ltsubadd2  11613  lesubadd2  11615  lesub3d  11760  supadd  12115  ltaddrp2d  12988  lincmb01cmp  13416  iccf1o  13417  elfzoext  13643  modaddabs  13836  muladdmodid  13838  negmod  13844  modadd2mod  13849  modadd12d  13855  modaddmulmod  13866  addmodlteq  13874  expaddz  14034  bcn2m1  14252  bcn2p1  14253  lenrevpfxcctswrd  14640  spllen  14682  splfv2a  14684  relexpaddnn  14979  relexpaddg  14981  rtrclreclem3  14988  remullem  15056  sqreulem  15288  bhmafibid2  15397  climaddc2  15564  iseraltlem2  15611  fsumsplit1  15673  telfsumo  15730  fsumparts  15734  bcxmas  15763  bpoly4  15987  sinadd  16094  sincossq  16106  cos2t  16108  absefi  16126  dvdsaddre2b  16239  pwp1fsum  16323  sadadd2lem2  16382  bitsres  16405  bezoutlem2  16472  bezoutlem4  16474  pythagtrip  16767  pcadd2  16823  vdwapun  16907  vdwlem5  16918  vdwlem6  16919  vdwlem8  16921  gsumsgrpccat  18770  mulgnndir  19038  mulgdirlem  19040  cyccom  19137  efgcpbllemb  19689  ablfacrp  20002  omndmul2  20067  cncrng  21348  rzgrp  21583  icccvx  24909  cnlmod  25101  cphipval  25204  pjthlem1  25398  cmmbl  25496  voliunlem1  25512  dvle  25973  dvcvx  25986  dvfsumlem2  25994  dvfsumlem2OLD  25995  dvfsumlem4  25997  dvfsum2  26002  ply1divex  26103  plymullem1  26180  coeeulem  26190  aaliou3lem6  26317  dvtaylp  26339  ulmcn  26369  abelthlem7  26409  pilem3  26424  lawcos  26787  affineequiv  26794  affineequiv3  26796  heron  26809  dcubic1lem  26814  dcubic2  26815  dcubic  26817  mcubic  26818  quart1lem  26826  quart1  26827  asinlem2  26840  asinsin  26863  cosasin  26875  atanlogaddlem  26884  atanlogadd  26885  cvxcl  26956  lgamgulmlem2  27001  lgamcvg2  27026  lgam1  27035  bposlem9  27264  lgseisenlem1  27347  2sqlem3  27392  2sqblem  27403  2sqmod  27408  addsqn2reu  27413  2sqreulem1  27418  2sqreunnlem1  27421  dchrisumlem2  27462  selberg  27520  selberg2  27523  selberg4  27533  pntrlog2bndlem1  27549  pntlemb  27569  pntlemf  27577  padicabv  27602  colinearalglem2  28985  axsegconlem9  29003  axeuclidlem  29040  eupth2lem3lem3  30310  numclwwlk3lem1  30462  smcnlem  30777  ipval2  30787  hhph  31258  pjhthlem1  31471  golem1  32351  stcltrlem1  32356  pythagreim  32828  quad3d  32832  cycpmco2lem3  33214  cycpmco2lem4  33215  cycpmco2lem5  33216  cycpmco2lem6  33217  cycpmco2  33219  archirngz  33275  archiabllem1a  33277  archiabllem1  33279  archiabllem2c  33281  constrrtcc  33905  cos9thpiminplylem1  33952  cos9thpiminplylem2  33953  cos9thpiminplylem3  33954  cos9thpinconstrlem1  33959  ballotlemsdom  34682  fsum2dsub  34777  revwlk  35332  resconn  35453  iprodgam  35949  faclimlem1  35950  faclimlem3  35952  faclim  35953  iprodfac  35954  fwddifnp1  36372  dnibndlem7  36697  dnibndlem8  36698  knoppndvlem14  36738  bj-bary1  37530  dvtan  37884  itgaddnclem2  37893  itgmulc2nc  37902  ftc1anclem8  37914  dvasin  37918  areacirclem1  37922  lcmineqlem19  42380  aks4d1p1p2  42403  posbezout  42433  sticksstones7  42485  sticksstones12a  42490  sticksstones12  42491  bcle2d  42512  aks6d1c7lem1  42513  dffltz  42955  fltbccoprm  42962  flt4lem3  42969  flt4lem5c  42975  flt4lem5d  42976  flt4lem5e  42977  flt4lem7  42980  nna4b4nsq  42981  fltnltalem  42983  3cubeslem2  43005  3cubeslem3l  43006  3cubeslem3r  43007  pellexlem2  43150  pell14qrgt0  43179  rmxyadd  43241  rmxluc  43256  fzmaxdif  43301  acongeq  43303  jm2.19lem2  43310  jm2.26lem3  43321  areaquad  43536  sqrtcval  43960  int-addcomd  44492  int-leftdistd  44498  subadd4b  45608  sub31  45615  coseq0  46185  coskpi2  46187  cosknegpi  46190  fperdvper  46240  dvbdfbdioolem2  46250  dvnmul  46264  dvmptfprodlem  46265  itgsincmulx  46295  itgsbtaddcnst  46303  stoweidlem11  46332  stirlinglem5  46399  stirlinglem7  46401  dirkertrigeqlem1  46419  dirkertrigeqlem2  46420  dirkertrigeqlem3  46421  dirkertrigeq  46422  dirkercncflem2  46425  fourierdlem4  46432  fourierdlem26  46454  fourierdlem40  46468  fourierdlem42  46470  fourierdlem47  46474  fourierdlem63  46490  fourierdlem64  46491  fourierdlem65  46492  fourierdlem74  46501  fourierdlem75  46502  fourierdlem78  46505  fourierdlem79  46506  fourierdlem84  46511  fourierdlem93  46520  fourierdlem103  46530  fourierdlem111  46538  fourierswlem  46551  fouriersw  46552  etransclem32  46587  etransclem46  46601  sge0gtfsumgt  46764  hoidmv1lelem2  46913  hoidmvlelem2  46917  hspmbllem1  46947  smfmullem1  47112  sigarperm  47181  cjnpoly  47212  2elfz2melfz  47641  m1modmmod  47681  mod2addne  47687  fargshiftfo  47765  ichexmpl2  47793  fmtnorec3  47871  2zrngacmnd  48571  2zrngagrp  48572  ply1mulgsumlem1  48709  ackval1  49004  ackval2  49005  resum2sqorgt0  49032  eenglngeehlnmlem2  49061  rrx2linest2  49067  line2xlem  49076  itsclc0yqsollem1  49085  itsclc0yqsol  49087  itscnhlc0xyqsol  49088  itsclc0xyqsolr  49092  itsclinecirc0b  49097  itsclquadb  49099  2itscplem1  49101  2itscp  49104  onetansqsecsq  50083