Theorem addcomd 11307

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ∈ wcel 2110  (class class class)co 7341  ℂcc 10996  1c1 10999   + caddc 11001   · cmul 11003

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 2112  ax-9 2120  ax-10 2143  ax-11 2159  ax-12 2179  ax-ext 2702  ax-sep 5232  ax-nul 5242  ax-pow 5301  ax-pr 5368  ax-un 7663  ax-resscn 11055  ax-1cn 11056  ax-icn 11057  ax-addcl 11058  ax-addrcl 11059  ax-mulcl 11060  ax-mulrcl 11061  ax-mulcom 11062  ax-addass 11063  ax-mulass 11064  ax-distr 11065  ax-i2m1 11066  ax-1ne0 11067  ax-1rid 11068  ax-rnegex 11069  ax-rrecex 11070  ax-cnre 11071  ax-pre-lttri 11072  ax-pre-lttrn 11073  ax-pre-ltadd 11074

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 2067  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-rab 3394  df-v 3436  df-sbc 3740  df-csb 3849  df-dif 3903  df-un 3905  df-in 3907  df-ss 3917  df-nul 4282  df-if 4474  df-pw 4550  df-sn 4575  df-pr 4577  df-op 4581  df-uni 4858  df-br 5090  df-opab 5152  df-mpt 5171  df-id 5509  df-po 5522  df-so 5523  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-iota 6433  df-fun 6479  df-fn 6480  df-f 6481  df-f1 6482  df-fo 6483  df-f1o 6484  df-fv 6485  df-ov 7344  df-er 8617  df-en 8865  df-dom 8866  df-sdom 8867  df-pnf 11140  df-mnf 11141  df-ltxr 11143

This theorem is referenced by:  muladd11r  11318  comraddd  11319  subadd2  11356  pncan  11358  npcan  11361  subcan  11408  mvlladdd  11520  subaddeqd  11524  addrsub  11526  mulsubaddmulsub  11573  ltadd1  11576  leadd2  11578  ltsubadd2  11580  lesubadd2  11582  lesub3d  11727  supadd  12082  ltaddrp2d  12960  lincmb01cmp  13387  iccf1o  13388  elfzoext  13614  modaddabs  13807  muladdmodid  13809  negmod  13815  modadd2mod  13820  modadd12d  13826  modaddmulmod  13837  addmodlteq  13845  expaddz  14005  bcn2m1  14223  bcn2p1  14224  lenrevpfxcctswrd  14611  spllen  14653  splfv2a  14655  relexpaddnn  14950  relexpaddg  14952  rtrclreclem3  14959  remullem  15027  sqreulem  15259  bhmafibid2  15368  climaddc2  15535  iseraltlem2  15582  fsumsplit1  15644  telfsumo  15701  fsumparts  15705  bcxmas  15734  bpoly4  15958  sinadd  16065  sincossq  16077  cos2t  16079  absefi  16097  dvdsaddre2b  16210  pwp1fsum  16294  sadadd2lem2  16353  bitsres  16376  bezoutlem2  16443  bezoutlem4  16445  pythagtrip  16738  pcadd2  16794  vdwapun  16878  vdwlem5  16889  vdwlem6  16890  vdwlem8  16892  gsumsgrpccat  18740  mulgnndir  19008  mulgdirlem  19010  cyccom  19108  efgcpbllemb  19660  ablfacrp  19973  omndmul2  20038  cncrng  21318  rzgrp  21553  icccvx  24868  cnlmod  25060  cphipval  25163  pjthlem1  25357  cmmbl  25455  voliunlem1  25471  dvle  25932  dvcvx  25945  dvfsumlem2  25953  dvfsumlem2OLD  25954  dvfsumlem4  25956  dvfsum2  25961  ply1divex  26062  plymullem1  26139  coeeulem  26149  aaliou3lem6  26276  dvtaylp  26298  ulmcn  26328  abelthlem7  26368  pilem3  26383  lawcos  26746  affineequiv  26753  affineequiv3  26755  heron  26768  dcubic1lem  26773  dcubic2  26774  dcubic  26776  mcubic  26777  quart1lem  26785  quart1  26786  asinlem2  26799  asinsin  26822  cosasin  26834  atanlogaddlem  26843  atanlogadd  26844  cvxcl  26915  lgamgulmlem2  26960  lgamcvg2  26985  lgam1  26994  bposlem9  27223  lgseisenlem1  27306  2sqlem3  27351  2sqblem  27362  2sqmod  27367  addsqn2reu  27372  2sqreulem1  27377  2sqreunnlem1  27380  dchrisumlem2  27421  selberg  27479  selberg2  27482  selberg4  27492  pntrlog2bndlem1  27508  pntlemb  27528  pntlemf  27536  padicabv  27561  colinearalglem2  28878  axsegconlem9  28896  axeuclidlem  28933  eupth2lem3lem3  30200  numclwwlk3lem1  30352  smcnlem  30667  ipval2  30677  hhph  31148  pjhthlem1  31361  golem1  32241  stcltrlem1  32246  pythagreim  32719  quad3d  32723  cycpmco2lem3  33087  cycpmco2lem4  33088  cycpmco2lem5  33089  cycpmco2lem6  33090  cycpmco2  33092  archirngz  33148  archiabllem1a  33150  archiabllem1  33152  archiabllem2c  33154  constrrtcc  33738  cos9thpiminplylem1  33785  cos9thpiminplylem2  33786  cos9thpiminplylem3  33787  cos9thpinconstrlem1  33792  ballotlemsdom  34515  fsum2dsub  34610  revwlk  35137  resconn  35258  iprodgam  35754  faclimlem1  35755  faclimlem3  35757  faclim  35758  iprodfac  35759  fwddifnp1  36178  dnibndlem7  36497  dnibndlem8  36498  knoppndvlem14  36538  bj-bary1  37325  dvtan  37689  itgaddnclem2  37698  itgmulc2nc  37707  ftc1anclem8  37719  dvasin  37723  areacirclem1  37727  lcmineqlem19  42059  aks4d1p1p2  42082  posbezout  42112  sticksstones7  42164  sticksstones12a  42169  sticksstones12  42170  bcle2d  42191  aks6d1c7lem1  42192  dffltz  42646  fltbccoprm  42653  flt4lem3  42660  flt4lem5c  42666  flt4lem5d  42667  flt4lem5e  42668  flt4lem7  42671  nna4b4nsq  42672  fltnltalem  42674  3cubeslem2  42697  3cubeslem3l  42698  3cubeslem3r  42699  pellexlem2  42842  pell14qrgt0  42871  rmxyadd  42933  rmxluc  42948  fzmaxdif  42993  acongeq  42995  jm2.19lem2  43002  jm2.26lem3  43013  areaquad  43228  sqrtcval  43653  int-addcomd  44185  int-leftdistd  44191  subadd4b  45303  sub31  45310  coseq0  45881  coskpi2  45883  cosknegpi  45886  fperdvper  45936  dvbdfbdioolem2  45946  dvnmul  45960  dvmptfprodlem  45961  itgsincmulx  45991  itgsbtaddcnst  45999  stoweidlem11  46028  stirlinglem5  46095  stirlinglem7  46097  dirkertrigeqlem1  46115  dirkertrigeqlem2  46116  dirkertrigeqlem3  46117  dirkertrigeq  46118  dirkercncflem2  46121  fourierdlem4  46128  fourierdlem26  46150  fourierdlem40  46164  fourierdlem42  46166  fourierdlem47  46170  fourierdlem63  46186  fourierdlem64  46187  fourierdlem65  46188  fourierdlem74  46197  fourierdlem75  46198  fourierdlem78  46201  fourierdlem79  46202  fourierdlem84  46207  fourierdlem93  46216  fourierdlem103  46226  fourierdlem111  46234  fourierswlem  46247  fouriersw  46248  etransclem32  46283  etransclem46  46297  sge0gtfsumgt  46460  hoidmv1lelem2  46609  hoidmvlelem2  46613  hspmbllem1  46643  smfmullem1  46808  sigarperm  46877  cjnpoly  46899  2elfz2melfz  47328  m1modmmod  47368  mod2addne  47374  fargshiftfo  47452  ichexmpl2  47480  fmtnorec3  47558  2zrngacmnd  48258  2zrngagrp  48259  ply1mulgsumlem1  48397  ackval1  48692  ackval2  48693  resum2sqorgt0  48720  eenglngeehlnmlem2  48749  rrx2linest2  48755  line2xlem  48764  itsclc0yqsollem1  48773  itsclc0yqsol  48775  itscnhlc0xyqsol  48776  itsclc0xyqsolr  48780  itsclinecirc0b  48785  itsclquadb  48787  2itscplem1  48789  2itscp  48792  onetansqsecsq  49772