Theorem addcomd 11318

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 11110	. . . . . . . 8 ⊢ (𝜑 → 1 ∈ ℂ)
2	1, 1	addcld 11134	. . . . . . 7 ⊢ (𝜑 → (1 + 1) ∈ ℂ)
3		muld.1	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ ℂ)
4		addcomd.2	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ ℂ)
5	2, 3, 4	adddid 11139	. . . . . 6 ⊢ (𝜑 → ((1 + 1) · (𝐴 + 𝐵)) = (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)))
6	3, 4	addcld 11134	. . . . . . 7 ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℂ)
7		1p1times 11287	. . . . . . 7 ⊢ ((𝐴 + 𝐵) ∈ ℂ → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
8	6, 7	syl 17	. . . . . 6 ⊢ (𝜑 → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
9		1p1times 11287	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
10	3, 9	syl 17	. . . . . . 7 ⊢ (𝜑 → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
11		1p1times 11287	. . . . . . . 8 ⊢ (𝐵 ∈ ℂ → ((1 + 1) · 𝐵) = (𝐵 + 𝐵))
12	4, 11	syl 17	. . . . . . 7 ⊢ (𝜑 → ((1 + 1) · 𝐵) = (𝐵 + 𝐵))
13	10, 12	oveq12d 7367	. . . . . 6 ⊢ (𝜑 → (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
14	5, 8, 13	3eqtr3rd 2773	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐴) + (𝐵 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
15	3, 3	addcld 11134	. . . . . 6 ⊢ (𝜑 → (𝐴 + 𝐴) ∈ ℂ)
16	15, 4, 4	addassd 11137	. . . . 5 ⊢ (𝜑 → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
17	6, 3, 4	addassd 11137	. . . . 5 ⊢ (𝜑 → (((𝐴 + 𝐵) + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
18	14, 16, 17	3eqtr4d 2774	. . . 4 ⊢ (𝜑 → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵))
19	15, 4	addcld 11134	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) ∈ ℂ)
20	6, 3	addcld 11134	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐴) ∈ ℂ)
21		addcan2 11301	. . . . 5 ⊢ ((((𝐴 + 𝐴) + 𝐵) ∈ ℂ ∧ ((𝐴 + 𝐵) + 𝐴) ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
22	19, 20, 4, 21	syl3anc 1373	. . . 4 ⊢ (𝜑 → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
23	18, 22	mpbid 232	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴))
24	3, 3, 4	addassd 11137	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) = (𝐴 + (𝐴 + 𝐵)))
25	3, 4, 3	addassd 11137	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐴) = (𝐴 + (𝐵 + 𝐴)))
26	23, 24, 25	3eqtr3d 2772	. 2 ⊢ (𝜑 → (𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)))
27	4, 3	addcld 11134	. . 3 ⊢ (𝜑 → (𝐵 + 𝐴) ∈ ℂ)
28		addcan 11300	. . 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 7349  ℂcc 11007  1c1 11010   + caddc 11012   · cmul 11014

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 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671  ax-resscn 11066  ax-1cn 11067  ax-icn 11068  ax-addcl 11069  ax-addrcl 11070  ax-mulcl 11071  ax-mulrcl 11072  ax-mulcom 11073  ax-addass 11074  ax-mulass 11075  ax-distr 11076  ax-i2m1 11077  ax-1ne0 11078  ax-1rid 11079  ax-rnegex 11080  ax-rrecex 11081  ax-cnre 11082  ax-pre-lttri 11083  ax-pre-lttrn 11084  ax-pre-ltadd 11085

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 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-mpt 5174  df-id 5514  df-po 5527  df-so 5528  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489  df-fv 6490  df-ov 7352  df-er 8625  df-en 8873  df-dom 8874  df-sdom 8875  df-pnf 11151  df-mnf 11152  df-ltxr 11154

This theorem is referenced by:  muladd11r  11329  comraddd  11330  subadd2  11367  pncan  11369  npcan  11372  subcan  11419  mvlladdd  11531  subaddeqd  11535  addrsub  11537  mulsubaddmulsub  11584  ltadd1  11587  leadd2  11589  ltsubadd2  11591  lesubadd2  11593  lesub3d  11738  supadd  12093  ltaddrp2d  12971  lincmb01cmp  13398  iccf1o  13399  elfzoext  13625  modaddabs  13815  muladdmodid  13817  negmod  13823  modadd2mod  13828  modadd12d  13834  modaddmulmod  13845  addmodlteq  13853  expaddz  14013  bcn2m1  14231  bcn2p1  14232  lenrevpfxcctswrd  14618  spllen  14660  splfv2a  14662  relexpaddnn  14958  relexpaddg  14960  rtrclreclem3  14967  remullem  15035  sqreulem  15267  bhmafibid2  15376  climaddc2  15543  iseraltlem2  15590  fsumsplit1  15652  telfsumo  15709  fsumparts  15713  bcxmas  15742  bpoly4  15966  sinadd  16073  sincossq  16085  cos2t  16087  absefi  16105  dvdsaddre2b  16218  pwp1fsum  16302  sadadd2lem2  16361  bitsres  16384  bezoutlem2  16451  bezoutlem4  16453  pythagtrip  16746  pcadd2  16802  vdwapun  16886  vdwlem5  16897  vdwlem6  16898  vdwlem8  16900  gsumsgrpccat  18714  mulgnndir  18982  mulgdirlem  18984  cyccom  19082  efgcpbllemb  19634  ablfacrp  19947  omndmul2  20012  cncrng  21295  rzgrp  21530  icccvx  24846  cnlmod  25038  cphipval  25141  pjthlem1  25335  cmmbl  25433  voliunlem1  25449  dvle  25910  dvcvx  25923  dvfsumlem2  25931  dvfsumlem2OLD  25932  dvfsumlem4  25934  dvfsum2  25939  ply1divex  26040  plymullem1  26117  coeeulem  26127  aaliou3lem6  26254  dvtaylp  26276  ulmcn  26306  abelthlem7  26346  pilem3  26361  lawcos  26724  affineequiv  26731  affineequiv3  26733  heron  26746  dcubic1lem  26751  dcubic2  26752  dcubic  26754  mcubic  26755  quart1lem  26763  quart1  26764  asinlem2  26777  asinsin  26800  cosasin  26812  atanlogaddlem  26821  atanlogadd  26822  cvxcl  26893  lgamgulmlem2  26938  lgamcvg2  26963  lgam1  26972  bposlem9  27201  lgseisenlem1  27284  2sqlem3  27329  2sqblem  27340  2sqmod  27345  addsqn2reu  27350  2sqreulem1  27355  2sqreunnlem1  27358  dchrisumlem2  27399  selberg  27457  selberg2  27460  selberg4  27470  pntrlog2bndlem1  27486  pntlemb  27506  pntlemf  27514  padicabv  27539  colinearalglem2  28852  axsegconlem9  28870  axeuclidlem  28907  eupth2lem3lem3  30174  numclwwlk3lem1  30326  smcnlem  30641  ipval2  30651  hhph  31122  pjhthlem1  31335  golem1  32215  stcltrlem1  32220  pythagreim  32689  quad3d  32693  cycpmco2lem3  33070  cycpmco2lem4  33071  cycpmco2lem5  33072  cycpmco2lem6  33073  cycpmco2  33075  archirngz  33131  archiabllem1a  33133  archiabllem1  33135  archiabllem2c  33137  constrrtcc  33702  cos9thpiminplylem1  33749  cos9thpiminplylem2  33750  cos9thpiminplylem3  33751  cos9thpinconstrlem1  33756  ballotlemsdom  34480  fsum2dsub  34575  revwlk  35102  resconn  35223  iprodgam  35719  faclimlem1  35720  faclimlem3  35722  faclim  35723  iprodfac  35724  fwddifnp1  36143  dnibndlem7  36462  dnibndlem8  36463  knoppndvlem14  36503  bj-bary1  37290  dvtan  37654  itgaddnclem2  37663  itgmulc2nc  37672  ftc1anclem8  37684  dvasin  37688  areacirclem1  37692  lcmineqlem19  42024  aks4d1p1p2  42047  posbezout  42077  sticksstones7  42129  sticksstones12a  42134  sticksstones12  42135  bcle2d  42156  aks6d1c7lem1  42157  dffltz  42611  fltbccoprm  42618  flt4lem3  42625  flt4lem5c  42631  flt4lem5d  42632  flt4lem5e  42633  flt4lem7  42636  nna4b4nsq  42637  fltnltalem  42639  3cubeslem2  42662  3cubeslem3l  42663  3cubeslem3r  42664  pellexlem2  42807  pell14qrgt0  42836  rmxyadd  42898  rmxluc  42913  fzmaxdif  42958  acongeq  42960  jm2.19lem2  42967  jm2.26lem3  42978  areaquad  43193  sqrtcval  43618  int-addcomd  44150  int-leftdistd  44156  subadd4b  45269  sub31  45276  coseq0  45849  coskpi2  45851  cosknegpi  45854  fperdvper  45904  dvbdfbdioolem2  45914  dvnmul  45928  dvmptfprodlem  45929  itgsincmulx  45959  itgsbtaddcnst  45967  stoweidlem11  45996  stirlinglem5  46063  stirlinglem7  46065  dirkertrigeqlem1  46083  dirkertrigeqlem2  46084  dirkertrigeqlem3  46085  dirkertrigeq  46086  dirkercncflem2  46089  fourierdlem4  46096  fourierdlem26  46118  fourierdlem40  46132  fourierdlem42  46134  fourierdlem47  46138  fourierdlem63  46154  fourierdlem64  46155  fourierdlem65  46156  fourierdlem74  46165  fourierdlem75  46166  fourierdlem78  46169  fourierdlem79  46170  fourierdlem84  46175  fourierdlem93  46184  fourierdlem103  46194  fourierdlem111  46202  fourierswlem  46215  fouriersw  46216  etransclem32  46251  etransclem46  46265  sge0gtfsumgt  46428  hoidmv1lelem2  46577  hoidmvlelem2  46581  hspmbllem1  46611  smfmullem1  46776  sigarperm  46845  cjnpoly  46877  2elfz2melfz  47306  m1modmmod  47346  mod2addne  47352  fargshiftfo  47430  ichexmpl2  47458  fmtnorec3  47536  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