Theorem addcomd 11446

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 11239	. . . . . . . 8 ⊢ (𝜑 → 1 ∈ ℂ)
2	1, 1	addcld 11263	. . . . . . 7 ⊢ (𝜑 → (1 + 1) ∈ ℂ)
3		muld.1	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ ℂ)
4		addcomd.2	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ ℂ)
5	2, 3, 4	adddid 11268	. . . . . 6 ⊢ (𝜑 → ((1 + 1) · (𝐴 + 𝐵)) = (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)))
6	3, 4	addcld 11263	. . . . . . 7 ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℂ)
7		1p1times 11415	. . . . . . 7 ⊢ ((𝐴 + 𝐵) ∈ ℂ → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
8	6, 7	syl 17	. . . . . 6 ⊢ (𝜑 → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
9		1p1times 11415	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
10	3, 9	syl 17	. . . . . . 7 ⊢ (𝜑 → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
11		1p1times 11415	. . . . . . . 8 ⊢ (𝐵 ∈ ℂ → ((1 + 1) · 𝐵) = (𝐵 + 𝐵))
12	4, 11	syl 17	. . . . . . 7 ⊢ (𝜑 → ((1 + 1) · 𝐵) = (𝐵 + 𝐵))
13	10, 12	oveq12d 7435	. . . . . 6 ⊢ (𝜑 → (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
14	5, 8, 13	3eqtr3rd 2774	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐴) + (𝐵 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
15	3, 3	addcld 11263	. . . . . 6 ⊢ (𝜑 → (𝐴 + 𝐴) ∈ ℂ)
16	15, 4, 4	addassd 11266	. . . . 5 ⊢ (𝜑 → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
17	6, 3, 4	addassd 11266	. . . . 5 ⊢ (𝜑 → (((𝐴 + 𝐵) + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
18	14, 16, 17	3eqtr4d 2775	. . . 4 ⊢ (𝜑 → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵))
19	15, 4	addcld 11263	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) ∈ ℂ)
20	6, 3	addcld 11263	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐴) ∈ ℂ)
21		addcan2 11429	. . . . 5 ⊢ ((((𝐴 + 𝐴) + 𝐵) ∈ ℂ ∧ ((𝐴 + 𝐵) + 𝐴) ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
22	19, 20, 4, 21	syl3anc 1368	. . . 4 ⊢ (𝜑 → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
23	18, 22	mpbid 231	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴))
24	3, 3, 4	addassd 11266	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) = (𝐴 + (𝐴 + 𝐵)))
25	3, 4, 3	addassd 11266	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐴) = (𝐴 + (𝐵 + 𝐴)))
26	23, 24, 25	3eqtr3d 2773	. 2 ⊢ (𝜑 → (𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)))
27	4, 3	addcld 11263	. . 3 ⊢ (𝜑 → (𝐵 + 𝐴) ∈ ℂ)
28		addcan 11428	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ (𝐴 + 𝐵) ∈ ℂ ∧ (𝐵 + 𝐴) ∈ ℂ) → ((𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴)))
29	3, 6, 27, 28	syl3anc 1368	. 2 ⊢ (𝜑 → ((𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴)))
30	26, 29	mpbid 231	1 ⊢ (𝜑 → (𝐴 + 𝐵) = (𝐵 + 𝐴))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1533   ∈ wcel 2098  (class class class)co 7417  ℂcc 11136  1c1 11139   + caddc 11141   · cmul 11143

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5299  ax-nul 5306  ax-pow 5364  ax-pr 5428  ax-un 7739  ax-resscn 11195  ax-1cn 11196  ax-icn 11197  ax-addcl 11198  ax-addrcl 11199  ax-mulcl 11200  ax-mulrcl 11201  ax-mulcom 11202  ax-addass 11203  ax-mulass 11204  ax-distr 11205  ax-i2m1 11206  ax-1ne0 11207  ax-1rid 11208  ax-rnegex 11209  ax-rrecex 11210  ax-cnre 11211  ax-pre-lttri 11212  ax-pre-lttrn 11213  ax-pre-ltadd 11214

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rab 3420  df-v 3465  df-sbc 3775  df-csb 3891  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5575  df-po 5589  df-so 5590  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-iota 6499  df-fun 6549  df-fn 6550  df-f 6551  df-f1 6552  df-fo 6553  df-f1o 6554  df-fv 6555  df-ov 7420  df-er 8723  df-en 8963  df-dom 8964  df-sdom 8965  df-pnf 11280  df-mnf 11281  df-ltxr 11283

This theorem is referenced by:  muladd11r  11457  comraddd  11458  subadd2  11494  pncan  11496  npcan  11499  subcan  11545  mvlladdd  11655  subaddeqd  11659  addrsub  11661  mulsubaddmulsub  11708  ltadd1  11711  leadd2  11713  ltsubadd2  11715  lesubadd2  11717  lesub3d  11862  supadd  12212  ltaddrp2d  13082  lincmb01cmp  13504  iccf1o  13505  modaddabs  13907  muladdmodid  13909  negmod  13914  modadd2mod  13919  modadd12d  13925  modaddmulmod  13936  addmodlteq  13944  expaddz  14104  bcn2m1  14316  bcn2p1  14317  spllen  14737  splfv2a  14739  relexpaddnn  15031  relexpaddg  15033  rtrclreclem3  15040  remullem  15108  sqreulem  15339  bhmafibid2  15446  climaddc2  15613  iseraltlem2  15662  fsumsplit1  15724  telfsumo  15781  fsumparts  15785  bcxmas  15814  bpoly4  16036  sinadd  16141  sincossq  16153  cos2t  16155  absefi  16173  dvdsaddre2b  16284  pwp1fsum  16368  sadadd2lem2  16425  bitsres  16448  bezoutlem2  16516  bezoutlem4  16518  pythagtrip  16803  pcadd2  16859  vdwapun  16943  vdwlem5  16954  vdwlem6  16955  vdwlem8  16957  gsumsgrpccat  18797  mulgnndir  19063  mulgdirlem  19065  cyccom  19163  efgcpbllemb  19715  ablfacrp  20028  cncrng  21321  rzgrp  21560  icccvx  24906  cnlmod  25098  cphipval  25202  pjthlem1  25396  cmmbl  25494  voliunlem1  25510  dvle  25971  dvcvx  25984  dvfsumlem2  25992  dvfsumlem2OLD  25993  dvfsumlem4  25995  dvfsum2  26000  ply1divex  26103  plymullem1  26179  coeeulem  26189  aaliou3lem6  26314  dvtaylp  26336  ulmcn  26366  abelthlem7  26406  pilem3  26421  lawcos  26779  affineequiv  26786  affineequiv3  26788  heron  26801  dcubic1lem  26806  dcubic2  26807  dcubic  26809  mcubic  26810  quart1lem  26818  quart1  26819  asinlem2  26832  asinsin  26855  cosasin  26867  atanlogaddlem  26876  atanlogadd  26877  cvxcl  26948  lgamgulmlem2  26993  lgamcvg2  27018  lgam1  27027  bposlem9  27256  lgseisenlem1  27339  2sqlem3  27384  2sqblem  27395  2sqmod  27400  addsqn2reu  27405  2sqreulem1  27410  2sqreunnlem1  27413  dchrisumlem2  27454  selberg  27512  selberg2  27515  selberg4  27525  pntrlog2bndlem1  27541  pntlemb  27561  pntlemf  27569  padicabv  27594  colinearalglem2  28775  axsegconlem9  28793  axeuclidlem  28830  eupth2lem3lem3  30097  numclwwlk3lem1  30249  smcnlem  30564  ipval2  30574  hhph  31045  pjhthlem1  31258  golem1  32138  stcltrlem1  32143  omndmul2  32858  cycpmco2lem3  32917  cycpmco2lem4  32918  cycpmco2lem5  32919  cycpmco2lem6  32920  cycpmco2  32922  archirngz  32965  archiabllem1a  32967  archiabllem1  32969  archiabllem2c  32971  ballotlemsdom  34218  fsum2dsub  34326  revwlk  34821  resconn  34943  iprodgam  35423  faclimlem1  35424  faclimlem3  35426  faclim  35427  iprodfac  35428  fwddifnp1  35848  dnibndlem7  36046  dnibndlem8  36047  knoppndvlem14  36087  bj-bary1  36878  dvtan  37230  itgaddnclem2  37239  itgmulc2nc  37248  ftc1anclem8  37260  dvasin  37264  areacirclem1  37268  lcmineqlem19  41604  aks4d1p1p2  41627  posbezout  41657  sticksstones7  41710  sticksstones12a  41715  sticksstones12  41716  bcle2d  41737  aks6d1c7lem1  41738  metakunt15  41757  metakunt16  41758  dffltz  42140  fltbccoprm  42147  flt4lem3  42154  flt4lem5c  42160  flt4lem5d  42161  flt4lem5e  42162  flt4lem7  42165  nna4b4nsq  42166  fltnltalem  42168  3cubeslem2  42187  3cubeslem3l  42188  3cubeslem3r  42189  pellexlem2  42332  pell14qrgt0  42361  rmxyadd  42424  rmxluc  42439  fzmaxdif  42484  acongeq  42486  jm2.19lem2  42493  jm2.26lem3  42504  areaquad  42726  sqrtcval  43153  int-addcomd  43685  int-leftdistd  43691  subadd4b  44744  sub31  44752  coseq0  45332  coskpi2  45334  cosknegpi  45337  fperdvper  45387  dvbdfbdioolem2  45397  dvnmul  45411  dvmptfprodlem  45412  itgsincmulx  45442  itgsbtaddcnst  45450  stoweidlem11  45479  stirlinglem5  45546  stirlinglem7  45548  dirkertrigeqlem1  45566  dirkertrigeqlem2  45567  dirkertrigeqlem3  45568  dirkertrigeq  45569  dirkercncflem2  45572  fourierdlem4  45579  fourierdlem26  45601  fourierdlem40  45615  fourierdlem42  45617  fourierdlem47  45621  fourierdlem63  45637  fourierdlem64  45638  fourierdlem65  45639  fourierdlem74  45648  fourierdlem75  45649  fourierdlem78  45652  fourierdlem79  45653  fourierdlem84  45658  fourierdlem93  45667  fourierdlem103  45677  fourierdlem111  45685  fourierswlem  45698  fouriersw  45699  etransclem32  45734  etransclem46  45748  sge0gtfsumgt  45911  hoidmv1lelem2  46060  hoidmvlelem2  46064  hspmbllem1  46094  smfmullem1  46259  sigarperm  46328  2elfz2melfz  46778  fargshiftfo  46861  ichexmpl2  46889  fmtnorec3  46967  2zrngacmnd  47438  2zrngagrp  47439  ply1mulgsumlem1  47582  m1modmmod  47722  ackval1  47882  ackval2  47883  resum2sqorgt0  47910  eenglngeehlnmlem2  47939  rrx2linest2  47945  line2xlem  47954  itsclc0yqsollem1  47963  itsclc0yqsol  47965  itscnhlc0xyqsol  47966  itsclc0xyqsolr  47970  itsclinecirc0b  47975  itsclquadb  47977  2itscplem1  47979  2itscp  47982  onetansqsecsq  48320