Theorem addcomd 11321

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 11113	. . . . . . . 8 ⊢ (𝜑 → 1 ∈ ℂ)
2	1, 1	addcld 11137	. . . . . . 7 ⊢ (𝜑 → (1 + 1) ∈ ℂ)
3		muld.1	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ ℂ)
4		addcomd.2	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ ℂ)
5	2, 3, 4	adddid 11142	. . . . . 6 ⊢ (𝜑 → ((1 + 1) · (𝐴 + 𝐵)) = (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)))
6	3, 4	addcld 11137	. . . . . . 7 ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℂ)
7		1p1times 11290	. . . . . . 7 ⊢ ((𝐴 + 𝐵) ∈ ℂ → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
8	6, 7	syl 17	. . . . . 6 ⊢ (𝜑 → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
9		1p1times 11290	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
10	3, 9	syl 17	. . . . . . 7 ⊢ (𝜑 → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
11		1p1times 11290	. . . . . . . 8 ⊢ (𝐵 ∈ ℂ → ((1 + 1) · 𝐵) = (𝐵 + 𝐵))
12	4, 11	syl 17	. . . . . . 7 ⊢ (𝜑 → ((1 + 1) · 𝐵) = (𝐵 + 𝐵))
13	10, 12	oveq12d 7370	. . . . . 6 ⊢ (𝜑 → (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
14	5, 8, 13	3eqtr3rd 2775	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐴) + (𝐵 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
15	3, 3	addcld 11137	. . . . . 6 ⊢ (𝜑 → (𝐴 + 𝐴) ∈ ℂ)
16	15, 4, 4	addassd 11140	. . . . 5 ⊢ (𝜑 → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
17	6, 3, 4	addassd 11140	. . . . 5 ⊢ (𝜑 → (((𝐴 + 𝐵) + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
18	14, 16, 17	3eqtr4d 2776	. . . 4 ⊢ (𝜑 → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵))
19	15, 4	addcld 11137	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) ∈ ℂ)
20	6, 3	addcld 11137	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐴) ∈ ℂ)
21		addcan2 11304	. . . . 5 ⊢ ((((𝐴 + 𝐴) + 𝐵) ∈ ℂ ∧ ((𝐴 + 𝐵) + 𝐴) ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
22	19, 20, 4, 21	syl3anc 1373	. . . 4 ⊢ (𝜑 → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
23	18, 22	mpbid 232	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴))
24	3, 3, 4	addassd 11140	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) = (𝐴 + (𝐴 + 𝐵)))
25	3, 4, 3	addassd 11140	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐴) = (𝐴 + (𝐵 + 𝐴)))
26	23, 24, 25	3eqtr3d 2774	. 2 ⊢ (𝜑 → (𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)))
27	4, 3	addcld 11137	. . 3 ⊢ (𝜑 → (𝐵 + 𝐴) ∈ ℂ)
28		addcan 11303	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ (𝐴 + 𝐵) ∈ ℂ ∧ (𝐵 + 𝐴) ∈ ℂ) → ((𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴)))
29	3, 6, 27, 28	syl3anc 1373	. 2 ⊢ (𝜑 → ((𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴)))
30	26, 29	mpbid 232	1 ⊢ (𝜑 → (𝐴 + 𝐵) = (𝐵 + 𝐴))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ∈ wcel 2111  (class class class)co 7352  ℂcc 11010  1c1 11013   + caddc 11015   · cmul 11017

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5236  ax-nul 5246  ax-pow 5305  ax-pr 5372  ax-un 7674  ax-resscn 11069  ax-1cn 11070  ax-icn 11071  ax-addcl 11072  ax-addrcl 11073  ax-mulcl 11074  ax-mulrcl 11075  ax-mulcom 11076  ax-addass 11077  ax-mulass 11078  ax-distr 11079  ax-i2m1 11080  ax-1ne0 11081  ax-1rid 11082  ax-rnegex 11083  ax-rrecex 11084  ax-cnre 11085  ax-pre-lttri 11086  ax-pre-lttrn 11087  ax-pre-ltadd 11088

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-nel 3033  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4283  df-if 4475  df-pw 4551  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-opab 5156  df-mpt 5175  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 6443  df-fun 6489  df-fn 6490  df-f 6491  df-f1 6492  df-fo 6493  df-f1o 6494  df-fv 6495  df-ov 7355  df-er 8628  df-en 8876  df-dom 8877  df-sdom 8878  df-pnf 11154  df-mnf 11155  df-ltxr 11157

This theorem is referenced by:  muladd11r  11332  comraddd  11333  subadd2  11370  pncan  11372  npcan  11375  subcan  11422  mvlladdd  11534  subaddeqd  11538  addrsub  11540  mulsubaddmulsub  11587  ltadd1  11590  leadd2  11592  ltsubadd2  11594  lesubadd2  11596  lesub3d  11741  supadd  12096  ltaddrp2d  12974  lincmb01cmp  13401  iccf1o  13402  elfzoext  13628  modaddabs  13821  muladdmodid  13823  negmod  13829  modadd2mod  13834  modadd12d  13840  modaddmulmod  13851  addmodlteq  13859  expaddz  14019  bcn2m1  14237  bcn2p1  14238  lenrevpfxcctswrd  14625  spllen  14667  splfv2a  14669  relexpaddnn  14964  relexpaddg  14966  rtrclreclem3  14973  remullem  15041  sqreulem  15273  bhmafibid2  15382  climaddc2  15549  iseraltlem2  15596  fsumsplit1  15658  telfsumo  15715  fsumparts  15719  bcxmas  15748  bpoly4  15972  sinadd  16079  sincossq  16091  cos2t  16093  absefi  16111  dvdsaddre2b  16224  pwp1fsum  16308  sadadd2lem2  16367  bitsres  16390  bezoutlem2  16457  bezoutlem4  16459  pythagtrip  16752  pcadd2  16808  vdwapun  16892  vdwlem5  16903  vdwlem6  16904  vdwlem8  16906  gsumsgrpccat  18754  mulgnndir  19022  mulgdirlem  19024  cyccom  19121  efgcpbllemb  19673  ablfacrp  19986  omndmul2  20051  cncrng  21331  rzgrp  21566  icccvx  24881  cnlmod  25073  cphipval  25176  pjthlem1  25370  cmmbl  25468  voliunlem1  25484  dvle  25945  dvcvx  25958  dvfsumlem2  25966  dvfsumlem2OLD  25967  dvfsumlem4  25969  dvfsum2  25974  ply1divex  26075  plymullem1  26152  coeeulem  26162  aaliou3lem6  26289  dvtaylp  26311  ulmcn  26341  abelthlem7  26381  pilem3  26396  lawcos  26759  affineequiv  26766  affineequiv3  26768  heron  26781  dcubic1lem  26786  dcubic2  26787  dcubic  26789  mcubic  26790  quart1lem  26798  quart1  26799  asinlem2  26812  asinsin  26835  cosasin  26847  atanlogaddlem  26856  atanlogadd  26857  cvxcl  26928  lgamgulmlem2  26973  lgamcvg2  26998  lgam1  27007  bposlem9  27236  lgseisenlem1  27319  2sqlem3  27364  2sqblem  27375  2sqmod  27380  addsqn2reu  27385  2sqreulem1  27390  2sqreunnlem1  27393  dchrisumlem2  27434  selberg  27492  selberg2  27495  selberg4  27505  pntrlog2bndlem1  27521  pntlemb  27541  pntlemf  27549  padicabv  27574  colinearalglem2  28892  axsegconlem9  28910  axeuclidlem  28947  eupth2lem3lem3  30217  numclwwlk3lem1  30369  smcnlem  30684  ipval2  30694  hhph  31165  pjhthlem1  31378  golem1  32258  stcltrlem1  32263  pythagreim  32736  quad3d  32740  cycpmco2lem3  33104  cycpmco2lem4  33105  cycpmco2lem5  33106  cycpmco2lem6  33107  cycpmco2  33109  archirngz  33165  archiabllem1a  33167  archiabllem1  33169  archiabllem2c  33171  constrrtcc  33755  cos9thpiminplylem1  33802  cos9thpiminplylem2  33803  cos9thpiminplylem3  33804  cos9thpinconstrlem1  33809  ballotlemsdom  34532  fsum2dsub  34627  revwlk  35176  resconn  35297  iprodgam  35793  faclimlem1  35794  faclimlem3  35796  faclim  35797  iprodfac  35798  fwddifnp1  36216  dnibndlem7  36535  dnibndlem8  36536  knoppndvlem14  36576  bj-bary1  37363  dvtan  37716  itgaddnclem2  37725  itgmulc2nc  37734  ftc1anclem8  37746  dvasin  37750  areacirclem1  37754  lcmineqlem19  42146  aks4d1p1p2  42169  posbezout  42199  sticksstones7  42251  sticksstones12a  42256  sticksstones12  42257  bcle2d  42278  aks6d1c7lem1  42279  dffltz  42733  fltbccoprm  42740  flt4lem3  42747  flt4lem5c  42753  flt4lem5d  42754  flt4lem5e  42755  flt4lem7  42758  nna4b4nsq  42759  fltnltalem  42761  3cubeslem2  42783  3cubeslem3l  42784  3cubeslem3r  42785  pellexlem2  42928  pell14qrgt0  42957  rmxyadd  43019  rmxluc  43034  fzmaxdif  43079  acongeq  43081  jm2.19lem2  43088  jm2.26lem3  43099  areaquad  43314  sqrtcval  43739  int-addcomd  44271  int-leftdistd  44277  subadd4b  45389  sub31  45396  coseq0  45967  coskpi2  45969  cosknegpi  45972  fperdvper  46022  dvbdfbdioolem2  46032  dvnmul  46046  dvmptfprodlem  46047  itgsincmulx  46077  itgsbtaddcnst  46085  stoweidlem11  46114  stirlinglem5  46181  stirlinglem7  46183  dirkertrigeqlem1  46201  dirkertrigeqlem2  46202  dirkertrigeqlem3  46203  dirkertrigeq  46204  dirkercncflem2  46207  fourierdlem4  46214  fourierdlem26  46236  fourierdlem40  46250  fourierdlem42  46252  fourierdlem47  46256  fourierdlem63  46272  fourierdlem64  46273  fourierdlem65  46274  fourierdlem74  46283  fourierdlem75  46284  fourierdlem78  46287  fourierdlem79  46288  fourierdlem84  46293  fourierdlem93  46302  fourierdlem103  46312  fourierdlem111  46320  fourierswlem  46333  fouriersw  46334  etransclem32  46369  etransclem46  46383  sge0gtfsumgt  46546  hoidmv1lelem2  46695  hoidmvlelem2  46699  hspmbllem1  46729  smfmullem1  46894  sigarperm  46963  cjnpoly  46994  2elfz2melfz  47423  m1modmmod  47463  mod2addne  47469  fargshiftfo  47547  ichexmpl2  47575  fmtnorec3  47653  2zrngacmnd  48353  2zrngagrp  48354  ply1mulgsumlem1  48492  ackval1  48787  ackval2  48788  resum2sqorgt0  48815  eenglngeehlnmlem2  48844  rrx2linest2  48850  line2xlem  48859  itsclc0yqsollem1  48868  itsclc0yqsol  48870  itscnhlc0xyqsol  48871  itsclc0xyqsolr  48875  itsclinecirc0b  48880  itsclquadb  48882  2itscplem1  48884  2itscp  48887  onetansqsecsq  49867