Theorem addcomd 11416

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 11209	. . . . . . . 8 ⊢ (𝜑 → 1 ∈ ℂ)
2	1, 1	addcld 11233	. . . . . . 7 ⊢ (𝜑 → (1 + 1) ∈ ℂ)
3		muld.1	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ ℂ)
4		addcomd.2	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ ℂ)
5	2, 3, 4	adddid 11238	. . . . . 6 ⊢ (𝜑 → ((1 + 1) · (𝐴 + 𝐵)) = (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)))
6	3, 4	addcld 11233	. . . . . . 7 ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℂ)
7		1p1times 11385	. . . . . . 7 ⊢ ((𝐴 + 𝐵) ∈ ℂ → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
8	6, 7	syl 17	. . . . . 6 ⊢ (𝜑 → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
9		1p1times 11385	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
10	3, 9	syl 17	. . . . . . 7 ⊢ (𝜑 → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
11		1p1times 11385	. . . . . . . 8 ⊢ (𝐵 ∈ ℂ → ((1 + 1) · 𝐵) = (𝐵 + 𝐵))
12	4, 11	syl 17	. . . . . . 7 ⊢ (𝜑 → ((1 + 1) · 𝐵) = (𝐵 + 𝐵))
13	10, 12	oveq12d 7427	. . . . . 6 ⊢ (𝜑 → (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
14	5, 8, 13	3eqtr3rd 2782	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐴) + (𝐵 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
15	3, 3	addcld 11233	. . . . . 6 ⊢ (𝜑 → (𝐴 + 𝐴) ∈ ℂ)
16	15, 4, 4	addassd 11236	. . . . 5 ⊢ (𝜑 → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
17	6, 3, 4	addassd 11236	. . . . 5 ⊢ (𝜑 → (((𝐴 + 𝐵) + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
18	14, 16, 17	3eqtr4d 2783	. . . 4 ⊢ (𝜑 → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵))
19	15, 4	addcld 11233	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) ∈ ℂ)
20	6, 3	addcld 11233	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐴) ∈ ℂ)
21		addcan2 11399	. . . . 5 ⊢ ((((𝐴 + 𝐴) + 𝐵) ∈ ℂ ∧ ((𝐴 + 𝐵) + 𝐴) ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
22	19, 20, 4, 21	syl3anc 1372	. . . 4 ⊢ (𝜑 → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
23	18, 22	mpbid 231	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴))
24	3, 3, 4	addassd 11236	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) = (𝐴 + (𝐴 + 𝐵)))
25	3, 4, 3	addassd 11236	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐴) = (𝐴 + (𝐵 + 𝐴)))
26	23, 24, 25	3eqtr3d 2781	. 2 ⊢ (𝜑 → (𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)))
27	4, 3	addcld 11233	. . 3 ⊢ (𝜑 → (𝐵 + 𝐴) ∈ ℂ)
28		addcan 11398	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ (𝐴 + 𝐵) ∈ ℂ ∧ (𝐵 + 𝐴) ∈ ℂ) → ((𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴)))
29	3, 6, 27, 28	syl3anc 1372	. 2 ⊢ (𝜑 → ((𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴)))
30	26, 29	mpbid 231	1 ⊢ (𝜑 → (𝐴 + 𝐵) = (𝐵 + 𝐴))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1542   ∈ wcel 2107  (class class class)co 7409  ℂcc 11108  1c1 11111   + caddc 11113   · cmul 11115

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-i2m1 11178  ax-1ne0 11179  ax-1rid 11180  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183  ax-pre-lttri 11184  ax-pre-lttrn 11185  ax-pre-ltadd 11186

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-po 5589  df-so 5590  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-ov 7412  df-er 8703  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11250  df-mnf 11251  df-ltxr 11253

This theorem is referenced by:  muladd11r  11427  comraddd  11428  subadd2  11464  pncan  11466  npcan  11469  subcan  11515  mvlladdd  11625  subaddeqd  11629  addrsub  11631  mulsubaddmulsub  11678  ltadd1  11681  leadd2  11683  ltsubadd2  11685  lesubadd2  11687  lesub3d  11832  supadd  12182  ltaddrp2d  13050  lincmb01cmp  13472  iccf1o  13473  modaddabs  13874  muladdmodid  13876  negmod  13881  modadd2mod  13886  modadd12d  13892  modaddmulmod  13903  addmodlteq  13911  expaddz  14072  bcn2m1  14284  bcn2p1  14285  spllen  14704  splfv2a  14706  relexpaddnn  14998  relexpaddg  15000  rtrclreclem3  15007  remullem  15075  sqreulem  15306  bhmafibid2  15413  climaddc2  15580  iseraltlem2  15629  fsumsplit1  15691  telfsumo  15748  fsumparts  15752  bcxmas  15781  bpoly4  16003  sinadd  16107  sincossq  16119  cos2t  16121  absefi  16139  dvdsaddre2b  16250  pwp1fsum  16334  sadadd2lem2  16391  bitsres  16414  bezoutlem2  16482  bezoutlem4  16484  pythagtrip  16767  pcadd2  16823  vdwapun  16907  vdwlem5  16918  vdwlem6  16919  vdwlem8  16921  gsumsgrpccat  18721  mulgnndir  18983  mulgdirlem  18985  cyccom  19080  efgcpbllemb  19623  ablfacrp  19936  rzgrp  21176  icccvx  24466  cnlmod  24656  cphipval  24760  pjthlem1  24954  cmmbl  25051  voliunlem1  25067  dvle  25524  dvcvx  25537  dvfsumlem2  25544  dvfsumlem4  25546  dvfsum2  25551  ply1divex  25654  plymullem1  25728  coeeulem  25738  aaliou3lem6  25861  dvtaylp  25882  ulmcn  25911  abelthlem7  25950  pilem3  25965  lawcos  26321  affineequiv  26328  affineequiv3  26330  heron  26343  dcubic1lem  26348  dcubic2  26349  dcubic  26351  mcubic  26352  quart1lem  26360  quart1  26361  asinlem2  26374  asinsin  26397  cosasin  26409  atanlogaddlem  26418  atanlogadd  26419  cvxcl  26489  lgamgulmlem2  26534  lgamcvg2  26559  lgam1  26568  bposlem9  26795  lgseisenlem1  26878  2sqlem3  26923  2sqblem  26934  2sqmod  26939  addsqn2reu  26944  2sqreulem1  26949  2sqreunnlem1  26952  dchrisumlem2  26993  selberg  27051  selberg2  27054  selberg4  27064  pntrlog2bndlem1  27080  pntlemb  27100  pntlemf  27108  padicabv  27133  colinearalglem2  28196  axsegconlem9  28214  axeuclidlem  28251  eupth2lem3lem3  29514  numclwwlk3lem1  29666  smcnlem  29981  ipval2  29991  hhph  30462  pjhthlem1  30675  golem1  31555  stcltrlem1  31560  omndmul2  32261  cycpmco2lem3  32318  cycpmco2lem4  32319  cycpmco2lem5  32320  cycpmco2lem6  32321  cycpmco2  32323  archirngz  32366  archiabllem1a  32368  archiabllem1  32370  archiabllem2c  32372  ballotlemsdom  33541  fsum2dsub  33650  revwlk  34146  resconn  34268  iprodgam  34743  faclimlem1  34744  faclimlem3  34746  faclim  34747  iprodfac  34748  fwddifnp1  35168  gg-dvfsumlem2  35214  dnibndlem7  35408  dnibndlem8  35409  knoppndvlem14  35449  bj-bary1  36241  dvtan  36586  itgaddnclem2  36595  itgmulc2nc  36604  ftc1anclem8  36616  dvasin  36620  areacirclem1  36624  lcmineqlem19  40960  aks4d1p1p2  40983  sticksstones7  41016  sticksstones12a  41021  sticksstones12  41022  metakunt15  41047  metakunt16  41048  dffltz  41424  fltbccoprm  41431  flt4lem3  41438  flt4lem5c  41444  flt4lem5d  41445  flt4lem5e  41446  flt4lem7  41449  nna4b4nsq  41450  fltnltalem  41452  3cubeslem2  41471  3cubeslem3l  41472  3cubeslem3r  41473  pellexlem2  41616  pell14qrgt0  41645  rmxyadd  41708  rmxluc  41723  fzmaxdif  41768  acongeq  41770  jm2.19lem2  41777  jm2.26lem3  41788  areaquad  42013  sqrtcval  42440  int-addcomd  42973  int-leftdistd  42979  subadd4b  44040  sub31  44048  coseq0  44628  coskpi2  44630  cosknegpi  44633  fperdvper  44683  dvbdfbdioolem2  44693  dvnmul  44707  dvmptfprodlem  44708  itgsincmulx  44738  itgsbtaddcnst  44746  stoweidlem11  44775  stirlinglem5  44842  stirlinglem7  44844  dirkertrigeqlem1  44862  dirkertrigeqlem2  44863  dirkertrigeqlem3  44864  dirkertrigeq  44865  dirkercncflem2  44868  fourierdlem4  44875  fourierdlem26  44897  fourierdlem40  44911  fourierdlem42  44913  fourierdlem47  44917  fourierdlem63  44933  fourierdlem64  44934  fourierdlem65  44935  fourierdlem74  44944  fourierdlem75  44945  fourierdlem78  44948  fourierdlem79  44949  fourierdlem84  44954  fourierdlem93  44963  fourierdlem103  44973  fourierdlem111  44981  fourierswlem  44994  fouriersw  44995  etransclem32  45030  etransclem46  45044  sge0gtfsumgt  45207  hoidmv1lelem2  45356  hoidmvlelem2  45360  hspmbllem1  45390  smfmullem1  45555  sigarperm  45624  2elfz2melfz  46074  fargshiftfo  46158  ichexmpl2  46186  fmtnorec3  46264  2zrngacmnd  46888  2zrngagrp  46889  ply1mulgsumlem1  47115  m1modmmod  47255  ackval1  47415  ackval2  47416  resum2sqorgt0  47443  eenglngeehlnmlem2  47472  rrx2linest2  47478  line2xlem  47487  itsclc0yqsollem1  47496  itsclc0yqsol  47498  itscnhlc0xyqsol  47499  itsclc0xyqsolr  47503  itsclinecirc0b  47508  itsclquadb  47510  2itscplem1  47512  2itscp  47515  onetansqsecsq  47854