Theorem addcomd 11512

Description: Addition is commutative. 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 11302	. . . . . . . 8 ⊢ (𝜑 → 1 ∈ ℂ)
2	1, 1	addcld 11328	. . . . . . 7 ⊢ (𝜑 → (1 + 1) ∈ ℂ)
3		muld.1	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ ℂ)
4		addcomd.2	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ ℂ)
5	2, 3, 4	adddid 11333	. . . . . 6 ⊢ (𝜑 → ((1 + 1) · (𝐴 + 𝐵)) = (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)))
6	3, 4	addcld 11328	. . . . . . 7 ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℂ)
7		1p1times 11481	. . . . . . 7 ⊢ ((𝐴 + 𝐵) ∈ ℂ → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
8	6, 7	syl 18	. . . . . 6 ⊢ (𝜑 → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
9		1p1times 11481	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
10	3, 9	syl 18	. . . . . . 7 ⊢ (𝜑 → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
11		1p1times 11481	. . . . . . . 8 ⊢ (𝐵 ∈ ℂ → ((1 + 1) · 𝐵) = (𝐵 + 𝐵))
12	4, 11	syl 18	. . . . . . 7 ⊢ (𝜑 → ((1 + 1) · 𝐵) = (𝐵 + 𝐵))
13	10, 12	oveq12d 7438	. . . . . 6 ⊢ (𝜑 → (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
14	5, 8, 13	3eqtr3rd 2804	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐴) + (𝐵 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
15	3, 3	addcld 11328	. . . . . 6 ⊢ (𝜑 → (𝐴 + 𝐴) ∈ ℂ)
16	15, 4, 4	addassd 11331	. . . . 5 ⊢ (𝜑 → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
17	6, 3, 4	addassd 11331	. . . . 5 ⊢ (𝜑 → (((𝐴 + 𝐵) + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
18	14, 16, 17	3eqtr4d 2805	. . . 4 ⊢ (𝜑 → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵))
19	15, 4	addcld 11328	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) ∈ ℂ)
20	6, 3	addcld 11328	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐴) ∈ ℂ)
21		addcan2 11495	. . . . 5 ⊢ ((((𝐴 + 𝐴) + 𝐵) ∈ ℂ ∧ ((𝐴 + 𝐵) + 𝐴) ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
22	19, 20, 4, 21	syl3anc 1398	. . . 4 ⊢ (𝜑 → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
23	18, 22	mpbid 235	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴))
24	3, 3, 4	addassd 11331	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) = (𝐴 + (𝐴 + 𝐵)))
25	3, 4, 3	addassd 11331	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐴) = (𝐴 + (𝐵 + 𝐴)))
26	23, 24, 25	3eqtr3d 2803	. 2 ⊢ (𝜑 → (𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)))
27	4, 3	addcld 11328	. . 3 ⊢ (𝜑 → (𝐵 + 𝐴) ∈ ℂ)
28		addcan 11494	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ (𝐴 + 𝐵) ∈ ℂ ∧ (𝐵 + 𝐴) ∈ ℂ) → ((𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴)))
29	3, 6, 27, 28	syl3anc 1398	. 2 ⊢ (𝜑 → ((𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴)))
30	26, 29	mpbid 235	1 ⊢ (𝜑 → (𝐴 + 𝐵) = (𝐵 + 𝐴))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1569   ∈ wcel 2144  (class class class)co 7420  ℂcc 11198  1c1 11201   + caddc 11203   · cmul 11205

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7751  ax-resscn 11257  ax-1cn 11258  ax-icn 11259  ax-addcl 11260  ax-addrcl 11261  ax-mulcl 11262  ax-mulrcl 11263  ax-mulcom 11264  ax-addass 11265  ax-mulass 11266  ax-distr 11267  ax-i2m1 11268  ax-1ne0 11269  ax-1rid 11270  ax-rnegex 11271  ax-rrecex 11272  ax-cnre 11273  ax-pre-lttri 11274  ax-pre-lttrn 11275  ax-pre-ltadd 11276

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-po 5558  df-so 5559  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-ov 7423  df-er 8717  df-en 8974  df-dom 8975  df-sdom 8976  df-pnf 11345  df-mnf 11346  df-ltxr 11348

This theorem is used by:  muladd11r  11523  comraddd  11524  subadd2  11561  pncan  11563  npcan  11566  subcan  11613  mvlladdd  11725  subaddeqd  11731  addrsub  11733  mulsubaddmulsub  11780  ltadd1  11783  leadd2  11785  ltsubadd2  11787  lesubadd2  11789  lesub3d  11934  supadd  12285  ltaddrp2d  13198  lincmb01cmp  13626  iccf1o  13627  elfzoext  13857  modaddabs  14051  muladdmodid  14053  negmod  14059  modadd2mod  14064  modadd12d  14070  modaddmulmod  14081  addmodlteq  14089  expaddz  14249  bcn2m1  14468  bcn2p1  14469  lenrevpfxcctswrd  14861  spllen  14903  splfv2a  14905  relexpaddnn  15204  relexpaddg  15206  rtrclreclem3  15213  remullem  15295  sqreulem  15527  bhmafibid2  15636  climaddc2  15803  iseraltlem2  15850  fsumsplit1  15911  telfsumo  15969  fsumparts  15973  bcxmas  16004  bpoly4  16225  sinadd  16332  sincossq  16344  cos2t  16346  absefi  16364  dvdsaddre2b  16477  pwp1fsum  16561  sadadd2lem2  16620  bitsres  16643  bezoutlem2  16713  bezoutlem4  16715  pythagtrip  17012  pcadd2  17068  vdwapun  17152  vdwlem5  17163  vdwlem6  17164  vdwlem8  17166  gsumsgrpccat  19036  mulgnndir  19313  mulgdirlem  19315  cyccom  19418  efgcpbllemb  19969  ablfacrp  20282  omndmul2  20347  cncrng  21699  rzgrp  21929  icccvx  25271  cnlmod  25461  cphipval  25564  pjthlem1  25758  cmmbl  25855  voliunlem1  25871  dvle  26327  dvcvx  26340  dvfsumlem2  26347  dvfsumlem4  26349  dvfsum2  26354  ply1divex  26455  plymullem1  26533  coeeulem  26543  aaliou3lem6  26675  dvtaylp  26697  ulmcn  26726  abelthlem7  26765  pilem3  26780  lawcos  27144  affineequiv  27151  affineequiv3  27153  heron  27166  dcubic1lem  27171  dcubic2  27172  dcubic  27174  mcubic  27175  quart1lem  27183  quart1  27184  asinlem2  27197  asinsin  27220  cosasin  27232  atanlogaddlem  27241  atanlogadd  27242  cvxcl  27312  lgamgulmlem2  27357  lgamcvg2  27382  lgam1  27391  bposlem9  27619  lgseisenlem1  27702  2sqlem3  27747  2sqblem  27758  2sqmod  27763  addsqn2reu  27768  2sqreulem1  27773  2sqreunnlem1  27776  dchrisumlem2  27817  selberg  27875  selberg2  27878  selberg4  27888  pntrlog2bndlem1  27904  pntlemb  27924  pntlemf  27932  padicabv  27957  fltbccoprm  27973  flt4lem3  27978  flt4lem5c  27984  flt4lem5d  27985  flt4lem5e  27986  flt4lem7  27989  nna4b4nsq  27990  colinearalglem2  29485  axsegconlem9  29503  axeuclidlem  29540  revwlk  30267  eupth2lem3lem3  30831  numclwwlk3lem1  30983  smcnlem  31299  ipval2  31309  hhph  31780  pjhthlem1  31993  golem1  32873  stcltrlem1  32878  pythagreim  33379  quad3d  33383  cycpmco2lem3  33731  cycpmco2lem4  33732  cycpmco2lem5  33733  cycpmco2lem6  33734  cycpmco2  33736  archirngz  33792  archiabllem1a  33794  archiabllem1  33796  archiabllem2c  33798  constrrtcc  34409  cos9thpiminplylem1  34456  cos9thpiminplylem2  34457  cos9thpiminplylem3  34458  cos9thpinconstrlem1  34463  ballotlemsdom  35186  fsum2dsub  35278  resconn  36053  iprodgam  36549  faclimlem1  36550  faclimlem3  36552  faclim  36553  iprodfac  36554  fwddifnp1  36972  dnibndlem7  37392  dnibndlem8  37393  knoppndvlem14  37433  bj-bary1  38276  dvtan  38631  itgaddnclem2  38640  itgmulc2nc  38649  ftc1anclem8  38661  dvasin  38665  areacirclem1  38669  lcmineqlem19  43140  aks4d1p1p2  43163  posbezout  43193  sticksstones7  43245  sticksstones12a  43250  sticksstones12  43251  bcle2d  43272  aks6d1c7lem1  43273  quadfac  43298  dffltz  43713  fltnltalem  43716  3cubeslem2  43738  3cubeslem3l  43739  3cubeslem3r  43740  pellexlem2  43880  pell14qrgt0  43909  rmxyadd  43971  rmxluc  43986  fzmaxdif  44031  acongeq  44033  jm2.19lem2  44040  jm2.26lem3  44051  areaquad  44261  sqrtcval  44684  int-addcomd  45216  int-leftdistd  45222  subadd4b  46342  sub31  46349  coseq0  46917  coskpi2  46919  cosknegpi  46922  fperdvper  46972  dvbdfbdioolem2  46982  dvnmul  46996  dvmptfprodlem  46997  itgsincmulx  47027  itgsbtaddcnst  47035  stoweidlem11  47064  stirlinglem5  47131  stirlinglem7  47133  dirkertrigeqlem1  47151  dirkertrigeqlem2  47152  dirkertrigeqlem3  47153  dirkertrigeq  47154  dirkercncflem2  47157  fourierdlem4  47164  fourierdlem26  47186  fourierdlem40  47200  fourierdlem42  47202  fourierdlem47  47206  fourierdlem63  47222  fourierdlem64  47223  fourierdlem65  47224  fourierdlem74  47233  fourierdlem75  47234  fourierdlem78  47237  fourierdlem79  47238  fourierdlem84  47243  fourierdlem93  47252  fourierdlem103  47262  fourierdlem111  47270  fourierswlem  47283  fouriersw  47284  etransclem32  47319  etransclem46  47333  sge0gtfsumgt  47496  hoidmv1lelem2  47645  hoidmvlelem2  47649  hspmbllem1  47679  smfmullem1  47844  sigarperm  47913  sin5tlem1  47962  sin5tlem5  47966  cjnpoly  47982  2elfz2melfz  48431  m1modmmod  48477  mod2addne  48483  fargshiftfo  48567  ichexmpl2  48595  fmtnorec3  48676  2zrngacmnd  49388  2zrngagrp  49389  ply1mulgsumlem1  49541  ackval1  49836  ackval2  49837  resum2sqorgt0  49864  eenglngeehlnmlem2  49893  rrx2linest2  49899  line2xlem  49908  itsclc0yqsollem1  49917  itsclc0yqsol  49919  itscnhlc0xyqsol  49920  itsclc0xyqsolr  49924  itsclinecirc0b  49929  itsclquadb  49931  2itscplem1  49933  2itscp  49936  onetansqsecsq  50897  crossp3d  51010