Theorem addcomd 11336

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 11129	. . . . . . . 8 ⊢ (𝜑 → 1 ∈ ℂ)
2	1, 1	addcld 11153	. . . . . . 7 ⊢ (𝜑 → (1 + 1) ∈ ℂ)
3		muld.1	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ ℂ)
4		addcomd.2	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ ℂ)
5	2, 3, 4	adddid 11158	. . . . . 6 ⊢ (𝜑 → ((1 + 1) · (𝐴 + 𝐵)) = (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)))
6	3, 4	addcld 11153	. . . . . . 7 ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℂ)
7		1p1times 11305	. . . . . . 7 ⊢ ((𝐴 + 𝐵) ∈ ℂ → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
8	6, 7	syl 17	. . . . . 6 ⊢ (𝜑 → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
9		1p1times 11305	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
10	3, 9	syl 17	. . . . . . 7 ⊢ (𝜑 → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
11		1p1times 11305	. . . . . . . 8 ⊢ (𝐵 ∈ ℂ → ((1 + 1) · 𝐵) = (𝐵 + 𝐵))
12	4, 11	syl 17	. . . . . . 7 ⊢ (𝜑 → ((1 + 1) · 𝐵) = (𝐵 + 𝐵))
13	10, 12	oveq12d 7371	. . . . . 6 ⊢ (𝜑 → (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
14	5, 8, 13	3eqtr3rd 2773	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐴) + (𝐵 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
15	3, 3	addcld 11153	. . . . . 6 ⊢ (𝜑 → (𝐴 + 𝐴) ∈ ℂ)
16	15, 4, 4	addassd 11156	. . . . 5 ⊢ (𝜑 → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
17	6, 3, 4	addassd 11156	. . . . 5 ⊢ (𝜑 → (((𝐴 + 𝐵) + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
18	14, 16, 17	3eqtr4d 2774	. . . 4 ⊢ (𝜑 → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵))
19	15, 4	addcld 11153	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) ∈ ℂ)
20	6, 3	addcld 11153	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐴) ∈ ℂ)
21		addcan2 11319	. . . . 5 ⊢ ((((𝐴 + 𝐴) + 𝐵) ∈ ℂ ∧ ((𝐴 + 𝐵) + 𝐴) ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
22	19, 20, 4, 21	syl3anc 1373	. . . 4 ⊢ (𝜑 → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
23	18, 22	mpbid 232	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴))
24	3, 3, 4	addassd 11156	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) = (𝐴 + (𝐴 + 𝐵)))
25	3, 4, 3	addassd 11156	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐴) = (𝐴 + (𝐵 + 𝐴)))
26	23, 24, 25	3eqtr3d 2772	. 2 ⊢ (𝜑 → (𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)))
27	4, 3	addcld 11153	. . 3 ⊢ (𝜑 → (𝐵 + 𝐴) ∈ ℂ)
28		addcan 11318	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ (𝐴 + 𝐵) ∈ ℂ ∧ (𝐵 + 𝐴) ∈ ℂ) → ((𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴)))
29	3, 6, 27, 28	syl3anc 1373	. 2 ⊢ (𝜑 → ((𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴)))
30	26, 29	mpbid 232	1 ⊢ (𝜑 → (𝐴 + 𝐵) = (𝐵 + 𝐴))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2109  (class class class)co 7353  ℂcc 11026  1c1 11029   + caddc 11031   · cmul 11033

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7675  ax-resscn 11085  ax-1cn 11086  ax-icn 11087  ax-addcl 11088  ax-addrcl 11089  ax-mulcl 11090  ax-mulrcl 11091  ax-mulcom 11092  ax-addass 11093  ax-mulass 11094  ax-distr 11095  ax-i2m1 11096  ax-1ne0 11097  ax-1rid 11098  ax-rnegex 11099  ax-rrecex 11100  ax-cnre 11101  ax-pre-lttri 11102  ax-pre-lttrn 11103  ax-pre-ltadd 11104

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5518  df-po 5531  df-so 5532  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-ov 7356  df-er 8632  df-en 8880  df-dom 8881  df-sdom 8882  df-pnf 11170  df-mnf 11171  df-ltxr 11173

This theorem is referenced by:  muladd11r  11347  comraddd  11348  subadd2  11385  pncan  11387  npcan  11390  subcan  11437  mvlladdd  11549  subaddeqd  11553  addrsub  11555  mulsubaddmulsub  11602  ltadd1  11605  leadd2  11607  ltsubadd2  11609  lesubadd2  11611  lesub3d  11756  supadd  12111  ltaddrp2d  12989  lincmb01cmp  13416  iccf1o  13417  elfzoext  13643  modaddabs  13833  muladdmodid  13835  negmod  13841  modadd2mod  13846  modadd12d  13852  modaddmulmod  13863  addmodlteq  13871  expaddz  14031  bcn2m1  14249  bcn2p1  14250  lenrevpfxcctswrd  14636  spllen  14678  splfv2a  14680  relexpaddnn  14976  relexpaddg  14978  rtrclreclem3  14985  remullem  15053  sqreulem  15285  bhmafibid2  15394  climaddc2  15561  iseraltlem2  15608  fsumsplit1  15670  telfsumo  15727  fsumparts  15731  bcxmas  15760  bpoly4  15984  sinadd  16091  sincossq  16103  cos2t  16105  absefi  16123  dvdsaddre2b  16236  pwp1fsum  16320  sadadd2lem2  16379  bitsres  16402  bezoutlem2  16469  bezoutlem4  16471  pythagtrip  16764  pcadd2  16820  vdwapun  16904  vdwlem5  16915  vdwlem6  16916  vdwlem8  16918  gsumsgrpccat  18732  mulgnndir  19000  mulgdirlem  19002  cyccom  19100  efgcpbllemb  19652  ablfacrp  19965  omndmul2  20030  cncrng  21313  rzgrp  21548  icccvx  24864  cnlmod  25056  cphipval  25159  pjthlem1  25353  cmmbl  25451  voliunlem1  25467  dvle  25928  dvcvx  25941  dvfsumlem2  25949  dvfsumlem2OLD  25950  dvfsumlem4  25952  dvfsum2  25957  ply1divex  26058  plymullem1  26135  coeeulem  26145  aaliou3lem6  26272  dvtaylp  26294  ulmcn  26324  abelthlem7  26364  pilem3  26379  lawcos  26742  affineequiv  26749  affineequiv3  26751  heron  26764  dcubic1lem  26769  dcubic2  26770  dcubic  26772  mcubic  26773  quart1lem  26781  quart1  26782  asinlem2  26795  asinsin  26818  cosasin  26830  atanlogaddlem  26839  atanlogadd  26840  cvxcl  26911  lgamgulmlem2  26956  lgamcvg2  26981  lgam1  26990  bposlem9  27219  lgseisenlem1  27302  2sqlem3  27347  2sqblem  27358  2sqmod  27363  addsqn2reu  27368  2sqreulem1  27373  2sqreunnlem1  27376  dchrisumlem2  27417  selberg  27475  selberg2  27478  selberg4  27488  pntrlog2bndlem1  27504  pntlemb  27524  pntlemf  27532  padicabv  27557  colinearalglem2  28870  axsegconlem9  28888  axeuclidlem  28925  eupth2lem3lem3  30192  numclwwlk3lem1  30344  smcnlem  30659  ipval2  30669  hhph  31140  pjhthlem1  31353  golem1  32233  stcltrlem1  32238  pythagreim  32702  quad3d  32706  cycpmco2lem3  33083  cycpmco2lem4  33084  cycpmco2lem5  33085  cycpmco2lem6  33086  cycpmco2  33088  archirngz  33141  archiabllem1a  33143  archiabllem1  33145  archiabllem2c  33147  constrrtcc  33701  cos9thpiminplylem1  33748  cos9thpiminplylem2  33749  cos9thpiminplylem3  33750  cos9thpinconstrlem1  33755  ballotlemsdom  34479  fsum2dsub  34574  revwlk  35097  resconn  35218  iprodgam  35714  faclimlem1  35715  faclimlem3  35717  faclim  35718  iprodfac  35719  fwddifnp1  36138  dnibndlem7  36457  dnibndlem8  36458  knoppndvlem14  36498  bj-bary1  37285  dvtan  37649  itgaddnclem2  37658  itgmulc2nc  37667  ftc1anclem8  37679  dvasin  37683  areacirclem1  37687  lcmineqlem19  42020  aks4d1p1p2  42043  posbezout  42073  sticksstones7  42125  sticksstones12a  42130  sticksstones12  42131  bcle2d  42152  aks6d1c7lem1  42153  dffltz  42607  fltbccoprm  42614  flt4lem3  42621  flt4lem5c  42627  flt4lem5d  42628  flt4lem5e  42629  flt4lem7  42632  nna4b4nsq  42633  fltnltalem  42635  3cubeslem2  42658  3cubeslem3l  42659  3cubeslem3r  42660  pellexlem2  42803  pell14qrgt0  42832  rmxyadd  42894  rmxluc  42909  fzmaxdif  42954  acongeq  42956  jm2.19lem2  42963  jm2.26lem3  42974  areaquad  43189  sqrtcval  43614  int-addcomd  44146  int-leftdistd  44152  subadd4b  45265  sub31  45272  coseq0  45846  coskpi2  45848  cosknegpi  45851  fperdvper  45901  dvbdfbdioolem2  45911  dvnmul  45925  dvmptfprodlem  45926  itgsincmulx  45956  itgsbtaddcnst  45964  stoweidlem11  45993  stirlinglem5  46060  stirlinglem7  46062  dirkertrigeqlem1  46080  dirkertrigeqlem2  46081  dirkertrigeqlem3  46082  dirkertrigeq  46083  dirkercncflem2  46086  fourierdlem4  46093  fourierdlem26  46115  fourierdlem40  46129  fourierdlem42  46131  fourierdlem47  46135  fourierdlem63  46151  fourierdlem64  46152  fourierdlem65  46153  fourierdlem74  46162  fourierdlem75  46163  fourierdlem78  46166  fourierdlem79  46167  fourierdlem84  46172  fourierdlem93  46181  fourierdlem103  46191  fourierdlem111  46199  fourierswlem  46212  fouriersw  46213  etransclem32  46248  etransclem46  46262  sge0gtfsumgt  46425  hoidmv1lelem2  46574  hoidmvlelem2  46578  hspmbllem1  46608  smfmullem1  46773  sigarperm  46842  cjnpoly  46874  2elfz2melfz  47303  m1modmmod  47343  mod2addne  47349  fargshiftfo  47427  ichexmpl2  47455  fmtnorec3  47533  2zrngacmnd  48220  2zrngagrp  48221  ply1mulgsumlem1  48359  ackval1  48654  ackval2  48655  resum2sqorgt0  48682  eenglngeehlnmlem2  48711  rrx2linest2  48717  line2xlem  48726  itsclc0yqsollem1  48735  itsclc0yqsol  48737  itscnhlc0xyqsol  48738  itsclc0xyqsolr  48742  itsclinecirc0b  48747  itsclquadb  48749  2itscplem1  48751  2itscp  48754  onetansqsecsq  49734