Theorem addcomd 11336

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 11128	. . . . . . . 8 ⊢ (𝜑 → 1 ∈ ℂ)
2	1, 1	addcld 11152	. . . . . . 7 ⊢ (𝜑 → (1 + 1) ∈ ℂ)
3		muld.1	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ ℂ)
4		addcomd.2	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ ℂ)
5	2, 3, 4	adddid 11157	. . . . . 6 ⊢ (𝜑 → ((1 + 1) · (𝐴 + 𝐵)) = (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)))
6	3, 4	addcld 11152	. . . . . . 7 ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℂ)
7		1p1times 11305	. . . . . . 7 ⊢ ((𝐴 + 𝐵) ∈ ℂ → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
8	6, 7	syl 17	. . . . . 6 ⊢ (𝜑 → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
9		1p1times 11305	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
10	3, 9	syl 17	. . . . . . 7 ⊢ (𝜑 → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
11		1p1times 11305	. . . . . . . 8 ⊢ (𝐵 ∈ ℂ → ((1 + 1) · 𝐵) = (𝐵 + 𝐵))
12	4, 11	syl 17	. . . . . . 7 ⊢ (𝜑 → ((1 + 1) · 𝐵) = (𝐵 + 𝐵))
13	10, 12	oveq12d 7376	. . . . . 6 ⊢ (𝜑 → (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
14	5, 8, 13	3eqtr3rd 2781	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐴) + (𝐵 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
15	3, 3	addcld 11152	. . . . . 6 ⊢ (𝜑 → (𝐴 + 𝐴) ∈ ℂ)
16	15, 4, 4	addassd 11155	. . . . 5 ⊢ (𝜑 → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
17	6, 3, 4	addassd 11155	. . . . 5 ⊢ (𝜑 → (((𝐴 + 𝐵) + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
18	14, 16, 17	3eqtr4d 2782	. . . 4 ⊢ (𝜑 → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵))
19	15, 4	addcld 11152	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) ∈ ℂ)
20	6, 3	addcld 11152	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐴) ∈ ℂ)
21		addcan2 11319	. . . . 5 ⊢ ((((𝐴 + 𝐴) + 𝐵) ∈ ℂ ∧ ((𝐴 + 𝐵) + 𝐴) ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
22	19, 20, 4, 21	syl3anc 1374	. . . 4 ⊢ (𝜑 → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
23	18, 22	mpbid 232	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴))
24	3, 3, 4	addassd 11155	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) = (𝐴 + (𝐴 + 𝐵)))
25	3, 4, 3	addassd 11155	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐴) = (𝐴 + (𝐵 + 𝐴)))
26	23, 24, 25	3eqtr3d 2780	. 2 ⊢ (𝜑 → (𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)))
27	4, 3	addcld 11152	. . 3 ⊢ (𝜑 → (𝐵 + 𝐴) ∈ ℂ)
28		addcan 11318	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ (𝐴 + 𝐵) ∈ ℂ ∧ (𝐵 + 𝐴) ∈ ℂ) → ((𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴)))
29	3, 6, 27, 28	syl3anc 1374	. 2 ⊢ (𝜑 → ((𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴)))
30	26, 29	mpbid 232	1 ⊢ (𝜑 → (𝐴 + 𝐵) = (𝐵 + 𝐴))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114  (class class class)co 7358  ℂcc 11025  1c1 11028   + caddc 11030   · cmul 11032

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pow 5300  ax-pr 5368  ax-un 7680  ax-resscn 11084  ax-1cn 11085  ax-icn 11086  ax-addcl 11087  ax-addrcl 11088  ax-mulcl 11089  ax-mulrcl 11090  ax-mulcom 11091  ax-addass 11092  ax-mulass 11093  ax-distr 11094  ax-i2m1 11095  ax-1ne0 11096  ax-1rid 11097  ax-rnegex 11098  ax-rrecex 11099  ax-cnre 11100  ax-pre-lttri 11101  ax-pre-lttrn 11102  ax-pre-ltadd 11103

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5517  df-po 5530  df-so 5531  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498  df-ov 7361  df-er 8634  df-en 8885  df-dom 8886  df-sdom 8887  df-pnf 11169  df-mnf 11170  df-ltxr 11172

This theorem is referenced by:  muladd11r  11347  comraddd  11348  subadd2  11385  pncan  11387  npcan  11390  subcan  11437  mvlladdd  11549  subaddeqd  11553  addrsub  11555  mulsubaddmulsub  11602  ltadd1  11605  leadd2  11607  ltsubadd2  11609  lesubadd2  11611  lesub3d  11756  supadd  12111  ltaddrp2d  12984  lincmb01cmp  13412  iccf1o  13413  elfzoext  13639  modaddabs  13832  muladdmodid  13834  negmod  13840  modadd2mod  13845  modadd12d  13851  modaddmulmod  13862  addmodlteq  13870  expaddz  14030  bcn2m1  14248  bcn2p1  14249  lenrevpfxcctswrd  14636  spllen  14678  splfv2a  14680  relexpaddnn  14975  relexpaddg  14977  rtrclreclem3  14984  remullem  15052  sqreulem  15284  bhmafibid2  15393  climaddc2  15560  iseraltlem2  15607  fsumsplit1  15669  telfsumo  15726  fsumparts  15730  bcxmas  15759  bpoly4  15983  sinadd  16090  sincossq  16102  cos2t  16104  absefi  16122  dvdsaddre2b  16235  pwp1fsum  16319  sadadd2lem2  16378  bitsres  16401  bezoutlem2  16468  bezoutlem4  16470  pythagtrip  16763  pcadd2  16819  vdwapun  16903  vdwlem5  16914  vdwlem6  16915  vdwlem8  16917  gsumsgrpccat  18766  mulgnndir  19037  mulgdirlem  19039  cyccom  19136  efgcpbllemb  19688  ablfacrp  20001  omndmul2  20066  cncrng  21345  rzgrp  21580  icccvx  24895  cnlmod  25085  cphipval  25188  pjthlem1  25382  cmmbl  25479  voliunlem1  25495  dvle  25953  dvcvx  25966  dvfsumlem2  25974  dvfsumlem2OLD  25975  dvfsumlem4  25977  dvfsum2  25982  ply1divex  26083  plymullem1  26160  coeeulem  26170  aaliou3lem6  26296  dvtaylp  26318  ulmcn  26348  abelthlem7  26388  pilem3  26403  lawcos  26766  affineequiv  26773  affineequiv3  26775  heron  26788  dcubic1lem  26793  dcubic2  26794  dcubic  26796  mcubic  26797  quart1lem  26805  quart1  26806  asinlem2  26819  asinsin  26842  cosasin  26854  atanlogaddlem  26863  atanlogadd  26864  cvxcl  26935  lgamgulmlem2  26980  lgamcvg2  27005  lgam1  27014  bposlem9  27243  lgseisenlem1  27326  2sqlem3  27371  2sqblem  27382  2sqmod  27387  addsqn2reu  27392  2sqreulem1  27397  2sqreunnlem1  27400  dchrisumlem2  27441  selberg  27499  selberg2  27502  selberg4  27512  pntrlog2bndlem1  27528  pntlemb  27548  pntlemf  27556  padicabv  27581  colinearalglem2  28964  axsegconlem9  28982  axeuclidlem  29019  eupth2lem3lem3  30289  numclwwlk3lem1  30441  smcnlem  30757  ipval2  30767  hhph  31238  pjhthlem1  31451  golem1  32331  stcltrlem1  32336  pythagreim  32808  quad3d  32812  cycpmco2lem3  33194  cycpmco2lem4  33195  cycpmco2lem5  33196  cycpmco2lem6  33197  cycpmco2  33199  archirngz  33255  archiabllem1a  33257  archiabllem1  33259  archiabllem2c  33261  constrrtcc  33885  cos9thpiminplylem1  33932  cos9thpiminplylem2  33933  cos9thpiminplylem3  33934  cos9thpinconstrlem1  33939  ballotlemsdom  34662  fsum2dsub  34757  revwlk  35313  resconn  35434  iprodgam  35930  faclimlem1  35931  faclimlem3  35933  faclim  35934  iprodfac  35935  fwddifnp1  36353  dnibndlem7  36742  dnibndlem8  36743  knoppndvlem14  36783  bj-bary1  37624  dvtan  37982  itgaddnclem2  37991  itgmulc2nc  38000  ftc1anclem8  38012  dvasin  38016  areacirclem1  38020  lcmineqlem19  42478  aks4d1p1p2  42501  posbezout  42531  sticksstones7  42583  sticksstones12a  42588  sticksstones12  42589  bcle2d  42610  aks6d1c7lem1  42611  dffltz  43066  fltbccoprm  43073  flt4lem3  43080  flt4lem5c  43086  flt4lem5d  43087  flt4lem5e  43088  flt4lem7  43091  nna4b4nsq  43092  fltnltalem  43094  3cubeslem2  43116  3cubeslem3l  43117  3cubeslem3r  43118  pellexlem2  43261  pell14qrgt0  43290  rmxyadd  43352  rmxluc  43367  fzmaxdif  43412  acongeq  43414  jm2.19lem2  43421  jm2.26lem3  43432  areaquad  43647  sqrtcval  44071  int-addcomd  44603  int-leftdistd  44609  subadd4b  45719  sub31  45726  coseq0  46296  coskpi2  46298  cosknegpi  46301  fperdvper  46351  dvbdfbdioolem2  46361  dvnmul  46375  dvmptfprodlem  46376  itgsincmulx  46406  itgsbtaddcnst  46414  stoweidlem11  46443  stirlinglem5  46510  stirlinglem7  46512  dirkertrigeqlem1  46530  dirkertrigeqlem2  46531  dirkertrigeqlem3  46532  dirkertrigeq  46533  dirkercncflem2  46536  fourierdlem4  46543  fourierdlem26  46565  fourierdlem40  46579  fourierdlem42  46581  fourierdlem47  46585  fourierdlem63  46601  fourierdlem64  46602  fourierdlem65  46603  fourierdlem74  46612  fourierdlem75  46613  fourierdlem78  46616  fourierdlem79  46617  fourierdlem84  46622  fourierdlem93  46631  fourierdlem103  46641  fourierdlem111  46649  fourierswlem  46662  fouriersw  46663  etransclem32  46698  etransclem46  46712  sge0gtfsumgt  46875  hoidmv1lelem2  47024  hoidmvlelem2  47028  hspmbllem1  47058  smfmullem1  47223  sigarperm  47292  cjnpoly  47323  2elfz2melfz  47752  m1modmmod  47792  mod2addne  47798  fargshiftfo  47876  ichexmpl2  47904  fmtnorec3  47982  2zrngacmnd  48682  2zrngagrp  48683  ply1mulgsumlem1  48820  ackval1  49115  ackval2  49116  resum2sqorgt0  49143  eenglngeehlnmlem2  49172  rrx2linest2  49178  line2xlem  49187  itsclc0yqsollem1  49196  itsclc0yqsol  49198  itscnhlc0xyqsol  49199  itsclc0xyqsolr  49203  itsclinecirc0b  49208  itsclquadb  49210  2itscplem1  49212  2itscp  49215  onetansqsecsq  50194