Theorem addcomd 11376

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 11169	. . . . . . . 8 ⊢ (𝜑 → 1 ∈ ℂ)
2	1, 1	addcld 11193	. . . . . . 7 ⊢ (𝜑 → (1 + 1) ∈ ℂ)
3		muld.1	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ ℂ)
4		addcomd.2	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ ℂ)
5	2, 3, 4	adddid 11198	. . . . . 6 ⊢ (𝜑 → ((1 + 1) · (𝐴 + 𝐵)) = (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)))
6	3, 4	addcld 11193	. . . . . . 7 ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℂ)
7		1p1times 11345	. . . . . . 7 ⊢ ((𝐴 + 𝐵) ∈ ℂ → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
8	6, 7	syl 17	. . . . . 6 ⊢ (𝜑 → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
9		1p1times 11345	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
10	3, 9	syl 17	. . . . . . 7 ⊢ (𝜑 → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
11		1p1times 11345	. . . . . . . 8 ⊢ (𝐵 ∈ ℂ → ((1 + 1) · 𝐵) = (𝐵 + 𝐵))
12	4, 11	syl 17	. . . . . . 7 ⊢ (𝜑 → ((1 + 1) · 𝐵) = (𝐵 + 𝐵))
13	10, 12	oveq12d 7405	. . . . . 6 ⊢ (𝜑 → (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
14	5, 8, 13	3eqtr3rd 2773	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐴) + (𝐵 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
15	3, 3	addcld 11193	. . . . . 6 ⊢ (𝜑 → (𝐴 + 𝐴) ∈ ℂ)
16	15, 4, 4	addassd 11196	. . . . 5 ⊢ (𝜑 → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
17	6, 3, 4	addassd 11196	. . . . 5 ⊢ (𝜑 → (((𝐴 + 𝐵) + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
18	14, 16, 17	3eqtr4d 2774	. . . 4 ⊢ (𝜑 → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵))
19	15, 4	addcld 11193	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) ∈ ℂ)
20	6, 3	addcld 11193	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐴) ∈ ℂ)
21		addcan2 11359	. . . . 5 ⊢ ((((𝐴 + 𝐴) + 𝐵) ∈ ℂ ∧ ((𝐴 + 𝐵) + 𝐴) ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
22	19, 20, 4, 21	syl3anc 1373	. . . 4 ⊢ (𝜑 → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
23	18, 22	mpbid 232	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴))
24	3, 3, 4	addassd 11196	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) = (𝐴 + (𝐴 + 𝐵)))
25	3, 4, 3	addassd 11196	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐴) = (𝐴 + (𝐵 + 𝐴)))
26	23, 24, 25	3eqtr3d 2772	. 2 ⊢ (𝜑 → (𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)))
27	4, 3	addcld 11193	. . 3 ⊢ (𝜑 → (𝐵 + 𝐴) ∈ ℂ)
28		addcan 11358	. . 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 7387  ℂcc 11066  1c1 11069   + caddc 11071   · cmul 11073

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 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711  ax-resscn 11125  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-addrcl 11129  ax-mulcl 11130  ax-mulrcl 11131  ax-mulcom 11132  ax-addass 11133  ax-mulass 11134  ax-distr 11135  ax-i2m1 11136  ax-1ne0 11137  ax-1rid 11138  ax-rnegex 11139  ax-rrecex 11140  ax-cnre 11141  ax-pre-lttri 11142  ax-pre-lttrn 11143  ax-pre-ltadd 11144

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 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-po 5546  df-so 5547  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-ov 7390  df-er 8671  df-en 8919  df-dom 8920  df-sdom 8921  df-pnf 11210  df-mnf 11211  df-ltxr 11213

This theorem is referenced by:  muladd11r  11387  comraddd  11388  subadd2  11425  pncan  11427  npcan  11430  subcan  11477  mvlladdd  11589  subaddeqd  11593  addrsub  11595  mulsubaddmulsub  11642  ltadd1  11645  leadd2  11647  ltsubadd2  11649  lesubadd2  11651  lesub3d  11796  supadd  12151  ltaddrp2d  13029  lincmb01cmp  13456  iccf1o  13457  elfzoext  13683  modaddabs  13873  muladdmodid  13875  negmod  13881  modadd2mod  13886  modadd12d  13892  modaddmulmod  13903  addmodlteq  13911  expaddz  14071  bcn2m1  14289  bcn2p1  14290  spllen  14719  splfv2a  14721  relexpaddnn  15017  relexpaddg  15019  rtrclreclem3  15026  remullem  15094  sqreulem  15326  bhmafibid2  15435  climaddc2  15602  iseraltlem2  15649  fsumsplit1  15711  telfsumo  15768  fsumparts  15772  bcxmas  15801  bpoly4  16025  sinadd  16132  sincossq  16144  cos2t  16146  absefi  16164  dvdsaddre2b  16277  pwp1fsum  16361  sadadd2lem2  16420  bitsres  16443  bezoutlem2  16510  bezoutlem4  16512  pythagtrip  16805  pcadd2  16861  vdwapun  16945  vdwlem5  16956  vdwlem6  16957  vdwlem8  16959  gsumsgrpccat  18767  mulgnndir  19035  mulgdirlem  19037  cyccom  19135  efgcpbllemb  19685  ablfacrp  19998  cncrng  21300  rzgrp  21532  icccvx  24848  cnlmod  25040  cphipval  25143  pjthlem1  25337  cmmbl  25435  voliunlem1  25451  dvle  25912  dvcvx  25925  dvfsumlem2  25933  dvfsumlem2OLD  25934  dvfsumlem4  25936  dvfsum2  25941  ply1divex  26042  plymullem1  26119  coeeulem  26129  aaliou3lem6  26256  dvtaylp  26278  ulmcn  26308  abelthlem7  26348  pilem3  26363  lawcos  26726  affineequiv  26733  affineequiv3  26735  heron  26748  dcubic1lem  26753  dcubic2  26754  dcubic  26756  mcubic  26757  quart1lem  26765  quart1  26766  asinlem2  26779  asinsin  26802  cosasin  26814  atanlogaddlem  26823  atanlogadd  26824  cvxcl  26895  lgamgulmlem2  26940  lgamcvg2  26965  lgam1  26974  bposlem9  27203  lgseisenlem1  27286  2sqlem3  27331  2sqblem  27342  2sqmod  27347  addsqn2reu  27352  2sqreulem1  27357  2sqreunnlem1  27360  dchrisumlem2  27401  selberg  27459  selberg2  27462  selberg4  27472  pntrlog2bndlem1  27488  pntlemb  27508  pntlemf  27516  padicabv  27541  colinearalglem2  28834  axsegconlem9  28852  axeuclidlem  28889  eupth2lem3lem3  30159  numclwwlk3lem1  30311  smcnlem  30626  ipval2  30636  hhph  31107  pjhthlem1  31320  golem1  32200  stcltrlem1  32205  pythagreim  32669  quad3d  32673  omndmul2  33026  cycpmco2lem3  33085  cycpmco2lem4  33086  cycpmco2lem5  33087  cycpmco2lem6  33088  cycpmco2  33090  archirngz  33143  archiabllem1a  33145  archiabllem1  33147  archiabllem2c  33149  constrrtcc  33725  cos9thpiminplylem1  33772  cos9thpiminplylem2  33773  cos9thpiminplylem3  33774  cos9thpinconstrlem1  33779  ballotlemsdom  34503  fsum2dsub  34598  revwlk  35112  resconn  35233  iprodgam  35729  faclimlem1  35730  faclimlem3  35732  faclim  35733  iprodfac  35734  fwddifnp1  36153  dnibndlem7  36472  dnibndlem8  36473  knoppndvlem14  36513  bj-bary1  37300  dvtan  37664  itgaddnclem2  37673  itgmulc2nc  37682  ftc1anclem8  37694  dvasin  37698  areacirclem1  37702  lcmineqlem19  42035  aks4d1p1p2  42058  posbezout  42088  sticksstones7  42140  sticksstones12a  42145  sticksstones12  42146  bcle2d  42167  aks6d1c7lem1  42168  dffltz  42622  fltbccoprm  42629  flt4lem3  42636  flt4lem5c  42642  flt4lem5d  42643  flt4lem5e  42644  flt4lem7  42647  nna4b4nsq  42648  fltnltalem  42650  3cubeslem2  42673  3cubeslem3l  42674  3cubeslem3r  42675  pellexlem2  42818  pell14qrgt0  42847  rmxyadd  42910  rmxluc  42925  fzmaxdif  42970  acongeq  42972  jm2.19lem2  42979  jm2.26lem3  42990  areaquad  43205  sqrtcval  43630  int-addcomd  44162  int-leftdistd  44168  subadd4b  45281  sub31  45288  coseq0  45862  coskpi2  45864  cosknegpi  45867  fperdvper  45917  dvbdfbdioolem2  45927  dvnmul  45941  dvmptfprodlem  45942  itgsincmulx  45972  itgsbtaddcnst  45980  stoweidlem11  46009  stirlinglem5  46076  stirlinglem7  46078  dirkertrigeqlem1  46096  dirkertrigeqlem2  46097  dirkertrigeqlem3  46098  dirkertrigeq  46099  dirkercncflem2  46102  fourierdlem4  46109  fourierdlem26  46131  fourierdlem40  46145  fourierdlem42  46147  fourierdlem47  46151  fourierdlem63  46167  fourierdlem64  46168  fourierdlem65  46169  fourierdlem74  46178  fourierdlem75  46179  fourierdlem78  46182  fourierdlem79  46183  fourierdlem84  46188  fourierdlem93  46197  fourierdlem103  46207  fourierdlem111  46215  fourierswlem  46228  fouriersw  46229  etransclem32  46264  etransclem46  46278  sge0gtfsumgt  46441  hoidmv1lelem2  46590  hoidmvlelem2  46594  hspmbllem1  46624  smfmullem1  46789  sigarperm  46858  cjnpoly  46890  2elfz2melfz  47319  m1modmmod  47359  mod2addne  47365  fargshiftfo  47443  ichexmpl2  47471  fmtnorec3  47549  2zrngacmnd  48236  2zrngagrp  48237  ply1mulgsumlem1  48375  ackval1  48670  ackval2  48671  resum2sqorgt0  48698  eenglngeehlnmlem2  48727  rrx2linest2  48733  line2xlem  48742  itsclc0yqsollem1  48751  itsclc0yqsol  48753  itscnhlc0xyqsol  48754  itsclc0xyqsolr  48758  itsclinecirc0b  48763  itsclquadb  48765  2itscplem1  48767  2itscp  48770  onetansqsecsq  49750