Theorem addcomd 11382

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 11175	. . . . . . . 8 ⊢ (𝜑 → 1 ∈ ℂ)
2	1, 1	addcld 11199	. . . . . . 7 ⊢ (𝜑 → (1 + 1) ∈ ℂ)
3		muld.1	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ ℂ)
4		addcomd.2	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ ℂ)
5	2, 3, 4	adddid 11204	. . . . . 6 ⊢ (𝜑 → ((1 + 1) · (𝐴 + 𝐵)) = (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)))
6	3, 4	addcld 11199	. . . . . . 7 ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℂ)
7		1p1times 11351	. . . . . . 7 ⊢ ((𝐴 + 𝐵) ∈ ℂ → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
8	6, 7	syl 17	. . . . . 6 ⊢ (𝜑 → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
9		1p1times 11351	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
10	3, 9	syl 17	. . . . . . 7 ⊢ (𝜑 → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
11		1p1times 11351	. . . . . . . 8 ⊢ (𝐵 ∈ ℂ → ((1 + 1) · 𝐵) = (𝐵 + 𝐵))
12	4, 11	syl 17	. . . . . . 7 ⊢ (𝜑 → ((1 + 1) · 𝐵) = (𝐵 + 𝐵))
13	10, 12	oveq12d 7407	. . . . . 6 ⊢ (𝜑 → (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
14	5, 8, 13	3eqtr3rd 2774	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐴) + (𝐵 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
15	3, 3	addcld 11199	. . . . . 6 ⊢ (𝜑 → (𝐴 + 𝐴) ∈ ℂ)
16	15, 4, 4	addassd 11202	. . . . 5 ⊢ (𝜑 → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
17	6, 3, 4	addassd 11202	. . . . 5 ⊢ (𝜑 → (((𝐴 + 𝐵) + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
18	14, 16, 17	3eqtr4d 2775	. . . 4 ⊢ (𝜑 → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵))
19	15, 4	addcld 11199	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) ∈ ℂ)
20	6, 3	addcld 11199	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐴) ∈ ℂ)
21		addcan2 11365	. . . . 5 ⊢ ((((𝐴 + 𝐴) + 𝐵) ∈ ℂ ∧ ((𝐴 + 𝐵) + 𝐴) ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
22	19, 20, 4, 21	syl3anc 1373	. . . 4 ⊢ (𝜑 → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
23	18, 22	mpbid 232	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴))
24	3, 3, 4	addassd 11202	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) = (𝐴 + (𝐴 + 𝐵)))
25	3, 4, 3	addassd 11202	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐴) = (𝐴 + (𝐵 + 𝐴)))
26	23, 24, 25	3eqtr3d 2773	. 2 ⊢ (𝜑 → (𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)))
27	4, 3	addcld 11199	. . 3 ⊢ (𝜑 → (𝐵 + 𝐴) ∈ ℂ)
28		addcan 11364	. . 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 7389  ℂcc 11072  1c1 11075   + caddc 11077   · cmul 11079

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 2702  ax-sep 5253  ax-nul 5263  ax-pow 5322  ax-pr 5389  ax-un 7713  ax-resscn 11131  ax-1cn 11132  ax-icn 11133  ax-addcl 11134  ax-addrcl 11135  ax-mulcl 11136  ax-mulrcl 11137  ax-mulcom 11138  ax-addass 11139  ax-mulass 11140  ax-distr 11141  ax-i2m1 11142  ax-1ne0 11143  ax-1rid 11144  ax-rnegex 11145  ax-rrecex 11146  ax-cnre 11147  ax-pre-lttri 11148  ax-pre-lttrn 11149  ax-pre-ltadd 11150

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 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 3409  df-v 3452  df-sbc 3756  df-csb 3865  df-dif 3919  df-un 3921  df-in 3923  df-ss 3933  df-nul 4299  df-if 4491  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5110  df-opab 5172  df-mpt 5191  df-id 5535  df-po 5548  df-so 5549  df-xp 5646  df-rel 5647  df-cnv 5648  df-co 5649  df-dm 5650  df-rn 5651  df-res 5652  df-ima 5653  df-iota 6466  df-fun 6515  df-fn 6516  df-f 6517  df-f1 6518  df-fo 6519  df-f1o 6520  df-fv 6521  df-ov 7392  df-er 8673  df-en 8921  df-dom 8922  df-sdom 8923  df-pnf 11216  df-mnf 11217  df-ltxr 11219

This theorem is referenced by:  muladd11r  11393  comraddd  11394  subadd2  11431  pncan  11433  npcan  11436  subcan  11483  mvlladdd  11595  subaddeqd  11599  addrsub  11601  mulsubaddmulsub  11648  ltadd1  11651  leadd2  11653  ltsubadd2  11655  lesubadd2  11657  lesub3d  11802  supadd  12157  ltaddrp2d  13035  lincmb01cmp  13462  iccf1o  13463  elfzoext  13689  modaddabs  13879  muladdmodid  13881  negmod  13887  modadd2mod  13892  modadd12d  13898  modaddmulmod  13909  addmodlteq  13917  expaddz  14077  bcn2m1  14295  bcn2p1  14296  spllen  14725  splfv2a  14727  relexpaddnn  15023  relexpaddg  15025  rtrclreclem3  15032  remullem  15100  sqreulem  15332  bhmafibid2  15441  climaddc2  15608  iseraltlem2  15655  fsumsplit1  15717  telfsumo  15774  fsumparts  15778  bcxmas  15807  bpoly4  16031  sinadd  16138  sincossq  16150  cos2t  16152  absefi  16170  dvdsaddre2b  16283  pwp1fsum  16367  sadadd2lem2  16426  bitsres  16449  bezoutlem2  16516  bezoutlem4  16518  pythagtrip  16811  pcadd2  16867  vdwapun  16951  vdwlem5  16962  vdwlem6  16963  vdwlem8  16965  gsumsgrpccat  18773  mulgnndir  19041  mulgdirlem  19043  cyccom  19141  efgcpbllemb  19691  ablfacrp  20004  cncrng  21306  rzgrp  21538  icccvx  24854  cnlmod  25046  cphipval  25149  pjthlem1  25343  cmmbl  25441  voliunlem1  25457  dvle  25918  dvcvx  25931  dvfsumlem2  25939  dvfsumlem2OLD  25940  dvfsumlem4  25942  dvfsum2  25947  ply1divex  26048  plymullem1  26125  coeeulem  26135  aaliou3lem6  26262  dvtaylp  26284  ulmcn  26314  abelthlem7  26354  pilem3  26369  lawcos  26732  affineequiv  26739  affineequiv3  26741  heron  26754  dcubic1lem  26759  dcubic2  26760  dcubic  26762  mcubic  26763  quart1lem  26771  quart1  26772  asinlem2  26785  asinsin  26808  cosasin  26820  atanlogaddlem  26829  atanlogadd  26830  cvxcl  26901  lgamgulmlem2  26946  lgamcvg2  26971  lgam1  26980  bposlem9  27209  lgseisenlem1  27292  2sqlem3  27337  2sqblem  27348  2sqmod  27353  addsqn2reu  27358  2sqreulem1  27363  2sqreunnlem1  27366  dchrisumlem2  27407  selberg  27465  selberg2  27468  selberg4  27478  pntrlog2bndlem1  27494  pntlemb  27514  pntlemf  27522  padicabv  27547  colinearalglem2  28840  axsegconlem9  28858  axeuclidlem  28895  eupth2lem3lem3  30165  numclwwlk3lem1  30317  smcnlem  30632  ipval2  30642  hhph  31113  pjhthlem1  31326  golem1  32206  stcltrlem1  32211  pythagreim  32675  quad3d  32679  omndmul2  33032  cycpmco2lem3  33091  cycpmco2lem4  33092  cycpmco2lem5  33093  cycpmco2lem6  33094  cycpmco2  33096  archirngz  33149  archiabllem1a  33151  archiabllem1  33153  archiabllem2c  33155  constrrtcc  33731  cos9thpiminplylem1  33778  cos9thpiminplylem2  33779  cos9thpiminplylem3  33780  cos9thpinconstrlem1  33785  ballotlemsdom  34509  fsum2dsub  34604  revwlk  35112  resconn  35233  iprodgam  35724  faclimlem1  35725  faclimlem3  35727  faclim  35728  iprodfac  35729  fwddifnp1  36148  dnibndlem7  36467  dnibndlem8  36468  knoppndvlem14  36508  bj-bary1  37295  dvtan  37659  itgaddnclem2  37668  itgmulc2nc  37677  ftc1anclem8  37689  dvasin  37693  areacirclem1  37697  lcmineqlem19  42030  aks4d1p1p2  42053  posbezout  42083  sticksstones7  42135  sticksstones12a  42140  sticksstones12  42141  bcle2d  42162  aks6d1c7lem1  42163  dffltz  42615  fltbccoprm  42622  flt4lem3  42629  flt4lem5c  42635  flt4lem5d  42636  flt4lem5e  42637  flt4lem7  42640  nna4b4nsq  42641  fltnltalem  42643  3cubeslem2  42666  3cubeslem3l  42667  3cubeslem3r  42668  pellexlem2  42811  pell14qrgt0  42840  rmxyadd  42903  rmxluc  42918  fzmaxdif  42963  acongeq  42965  jm2.19lem2  42972  jm2.26lem3  42983  areaquad  43198  sqrtcval  43623  int-addcomd  44155  int-leftdistd  44161  subadd4b  45274  sub31  45281  coseq0  45855  coskpi2  45857  cosknegpi  45860  fperdvper  45910  dvbdfbdioolem2  45920  dvnmul  45934  dvmptfprodlem  45935  itgsincmulx  45965  itgsbtaddcnst  45973  stoweidlem11  46002  stirlinglem5  46069  stirlinglem7  46071  dirkertrigeqlem1  46089  dirkertrigeqlem2  46090  dirkertrigeqlem3  46091  dirkertrigeq  46092  dirkercncflem2  46095  fourierdlem4  46102  fourierdlem26  46124  fourierdlem40  46138  fourierdlem42  46140  fourierdlem47  46144  fourierdlem63  46160  fourierdlem64  46161  fourierdlem65  46162  fourierdlem74  46171  fourierdlem75  46172  fourierdlem78  46175  fourierdlem79  46176  fourierdlem84  46181  fourierdlem93  46190  fourierdlem103  46200  fourierdlem111  46208  fourierswlem  46221  fouriersw  46222  etransclem32  46257  etransclem46  46271  sge0gtfsumgt  46434  hoidmv1lelem2  46583  hoidmvlelem2  46587  hspmbllem1  46617  smfmullem1  46782  sigarperm  46851  2elfz2melfz  47309  m1modmmod  47349  mod2addne  47355  fargshiftfo  47433  ichexmpl2  47461  fmtnorec3  47539  2zrngacmnd  48226  2zrngagrp  48227  ply1mulgsumlem1  48365  ackval1  48660  ackval2  48661  resum2sqorgt0  48688  eenglngeehlnmlem2  48717  rrx2linest2  48723  line2xlem  48732  itsclc0yqsollem1  48741  itsclc0yqsol  48743  itscnhlc0xyqsol  48744  itsclc0xyqsolr  48748  itsclinecirc0b  48753  itsclquadb  48755  2itscplem1  48757  2itscp  48760  onetansqsecsq  49740