Theorem addcomd 11460

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 11253	. . . . . . . 8 ⊢ (𝜑 → 1 ∈ ℂ)
2	1, 1	addcld 11277	. . . . . . 7 ⊢ (𝜑 → (1 + 1) ∈ ℂ)
3		muld.1	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ ℂ)
4		addcomd.2	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ ℂ)
5	2, 3, 4	adddid 11282	. . . . . 6 ⊢ (𝜑 → ((1 + 1) · (𝐴 + 𝐵)) = (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)))
6	3, 4	addcld 11277	. . . . . . 7 ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℂ)
7		1p1times 11429	. . . . . . 7 ⊢ ((𝐴 + 𝐵) ∈ ℂ → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
8	6, 7	syl 17	. . . . . 6 ⊢ (𝜑 → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
9		1p1times 11429	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
10	3, 9	syl 17	. . . . . . 7 ⊢ (𝜑 → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
11		1p1times 11429	. . . . . . . 8 ⊢ (𝐵 ∈ ℂ → ((1 + 1) · 𝐵) = (𝐵 + 𝐵))
12	4, 11	syl 17	. . . . . . 7 ⊢ (𝜑 → ((1 + 1) · 𝐵) = (𝐵 + 𝐵))
13	10, 12	oveq12d 7448	. . . . . 6 ⊢ (𝜑 → (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
14	5, 8, 13	3eqtr3rd 2783	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐴) + (𝐵 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
15	3, 3	addcld 11277	. . . . . 6 ⊢ (𝜑 → (𝐴 + 𝐴) ∈ ℂ)
16	15, 4, 4	addassd 11280	. . . . 5 ⊢ (𝜑 → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
17	6, 3, 4	addassd 11280	. . . . 5 ⊢ (𝜑 → (((𝐴 + 𝐵) + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
18	14, 16, 17	3eqtr4d 2784	. . . 4 ⊢ (𝜑 → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵))
19	15, 4	addcld 11277	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) ∈ ℂ)
20	6, 3	addcld 11277	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐴) ∈ ℂ)
21		addcan2 11443	. . . . 5 ⊢ ((((𝐴 + 𝐴) + 𝐵) ∈ ℂ ∧ ((𝐴 + 𝐵) + 𝐴) ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
22	19, 20, 4, 21	syl3anc 1370	. . . 4 ⊢ (𝜑 → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
23	18, 22	mpbid 232	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴))
24	3, 3, 4	addassd 11280	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) = (𝐴 + (𝐴 + 𝐵)))
25	3, 4, 3	addassd 11280	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐴) = (𝐴 + (𝐵 + 𝐴)))
26	23, 24, 25	3eqtr3d 2782	. 2 ⊢ (𝜑 → (𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)))
27	4, 3	addcld 11277	. . 3 ⊢ (𝜑 → (𝐵 + 𝐴) ∈ ℂ)
28		addcan 11442	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ (𝐴 + 𝐵) ∈ ℂ ∧ (𝐵 + 𝐴) ∈ ℂ) → ((𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴)))
29	3, 6, 27, 28	syl3anc 1370	. 2 ⊢ (𝜑 → ((𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴)))
30	26, 29	mpbid 232	1 ⊢ (𝜑 → (𝐴 + 𝐵) = (𝐵 + 𝐴))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1536   ∈ wcel 2105  (class class class)co 7430  ℂcc 11150  1c1 11153   + caddc 11155   · cmul 11157

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-po 5596  df-so 5597  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-ov 7433  df-er 8743  df-en 8984  df-dom 8985  df-sdom 8986  df-pnf 11294  df-mnf 11295  df-ltxr 11297

This theorem is referenced by:  muladd11r  11471  comraddd  11472  subadd2  11509  pncan  11511  npcan  11514  subcan  11561  mvlladdd  11671  subaddeqd  11675  addrsub  11677  mulsubaddmulsub  11724  ltadd1  11727  leadd2  11729  ltsubadd2  11731  lesubadd2  11733  lesub3d  11878  supadd  12233  ltaddrp2d  13108  lincmb01cmp  13531  iccf1o  13532  elfzoext  13757  modaddabs  13945  muladdmodid  13947  negmod  13953  modadd2mod  13958  modadd12d  13964  modaddmulmod  13975  addmodlteq  13983  expaddz  14143  bcn2m1  14359  bcn2p1  14360  spllen  14788  splfv2a  14790  relexpaddnn  15086  relexpaddg  15088  rtrclreclem3  15095  remullem  15163  sqreulem  15394  bhmafibid2  15501  climaddc2  15668  iseraltlem2  15715  fsumsplit1  15777  telfsumo  15834  fsumparts  15838  bcxmas  15867  bpoly4  16091  sinadd  16196  sincossq  16208  cos2t  16210  absefi  16228  dvdsaddre2b  16340  pwp1fsum  16424  sadadd2lem2  16483  bitsres  16506  bezoutlem2  16573  bezoutlem4  16575  pythagtrip  16867  pcadd2  16923  vdwapun  17007  vdwlem5  17018  vdwlem6  17019  vdwlem8  17021  gsumsgrpccat  18865  mulgnndir  19133  mulgdirlem  19135  cyccom  19233  efgcpbllemb  19787  ablfacrp  20100  cncrng  21418  rzgrp  21658  icccvx  24994  cnlmod  25186  cphipval  25290  pjthlem1  25484  cmmbl  25582  voliunlem1  25598  dvle  26060  dvcvx  26073  dvfsumlem2  26081  dvfsumlem2OLD  26082  dvfsumlem4  26084  dvfsum2  26089  ply1divex  26190  plymullem1  26267  coeeulem  26277  aaliou3lem6  26404  dvtaylp  26426  ulmcn  26456  abelthlem7  26496  pilem3  26511  lawcos  26873  affineequiv  26880  affineequiv3  26882  heron  26895  dcubic1lem  26900  dcubic2  26901  dcubic  26903  mcubic  26904  quart1lem  26912  quart1  26913  asinlem2  26926  asinsin  26949  cosasin  26961  atanlogaddlem  26970  atanlogadd  26971  cvxcl  27042  lgamgulmlem2  27087  lgamcvg2  27112  lgam1  27121  bposlem9  27350  lgseisenlem1  27433  2sqlem3  27478  2sqblem  27489  2sqmod  27494  addsqn2reu  27499  2sqreulem1  27504  2sqreunnlem1  27507  dchrisumlem2  27548  selberg  27606  selberg2  27609  selberg4  27619  pntrlog2bndlem1  27635  pntlemb  27655  pntlemf  27663  padicabv  27688  colinearalglem2  28936  axsegconlem9  28954  axeuclidlem  28991  eupth2lem3lem3  30258  numclwwlk3lem1  30410  smcnlem  30725  ipval2  30735  hhph  31206  pjhthlem1  31419  golem1  32299  stcltrlem1  32304  quad3d  32760  omndmul2  33071  cycpmco2lem3  33130  cycpmco2lem4  33131  cycpmco2lem5  33132  cycpmco2lem6  33133  cycpmco2  33135  archirngz  33178  archiabllem1a  33180  archiabllem1  33182  archiabllem2c  33184  constrrtcc  33740  ballotlemsdom  34492  fsum2dsub  34600  revwlk  35108  resconn  35230  iprodgam  35721  faclimlem1  35722  faclimlem3  35724  faclim  35725  iprodfac  35726  fwddifnp1  36146  dnibndlem7  36466  dnibndlem8  36467  knoppndvlem14  36507  bj-bary1  37294  dvtan  37656  itgaddnclem2  37665  itgmulc2nc  37674  ftc1anclem8  37686  dvasin  37690  areacirclem1  37694  lcmineqlem19  42028  aks4d1p1p2  42051  posbezout  42081  sticksstones7  42133  sticksstones12a  42138  sticksstones12  42139  bcle2d  42160  aks6d1c7lem1  42161  metakunt15  42200  metakunt16  42201  dffltz  42620  fltbccoprm  42627  flt4lem3  42634  flt4lem5c  42640  flt4lem5d  42641  flt4lem5e  42642  flt4lem7  42645  nna4b4nsq  42646  fltnltalem  42648  3cubeslem2  42672  3cubeslem3l  42673  3cubeslem3r  42674  pellexlem2  42817  pell14qrgt0  42846  rmxyadd  42909  rmxluc  42924  fzmaxdif  42969  acongeq  42971  jm2.19lem2  42978  jm2.26lem3  42989  areaquad  43204  sqrtcval  43630  int-addcomd  44162  int-leftdistd  44168  subadd4b  45232  sub31  45240  coseq0  45819  coskpi2  45821  cosknegpi  45824  fperdvper  45874  dvbdfbdioolem2  45884  dvnmul  45898  dvmptfprodlem  45899  itgsincmulx  45929  itgsbtaddcnst  45937  stoweidlem11  45966  stirlinglem5  46033  stirlinglem7  46035  dirkertrigeqlem1  46053  dirkertrigeqlem2  46054  dirkertrigeqlem3  46055  dirkertrigeq  46056  dirkercncflem2  46059  fourierdlem4  46066  fourierdlem26  46088  fourierdlem40  46102  fourierdlem42  46104  fourierdlem47  46108  fourierdlem63  46124  fourierdlem64  46125  fourierdlem65  46126  fourierdlem74  46135  fourierdlem75  46136  fourierdlem78  46139  fourierdlem79  46140  fourierdlem84  46145  fourierdlem93  46154  fourierdlem103  46164  fourierdlem111  46172  fourierswlem  46185  fouriersw  46186  etransclem32  46221  etransclem46  46235  sge0gtfsumgt  46398  hoidmv1lelem2  46547  hoidmvlelem2  46551  hspmbllem1  46581  smfmullem1  46746  sigarperm  46815  2elfz2melfz  47267  fargshiftfo  47366  ichexmpl2  47394  fmtnorec3  47472  2zrngacmnd  48091  2zrngagrp  48092  ply1mulgsumlem1  48231  m1modmmod  48370  ackval1  48530  ackval2  48531  resum2sqorgt0  48558  eenglngeehlnmlem2  48587  rrx2linest2  48593  line2xlem  48602  itsclc0yqsollem1  48611  itsclc0yqsol  48613  itscnhlc0xyqsol  48614  itsclc0xyqsolr  48618  itsclinecirc0b  48623  itsclquadb  48625  2itscplem1  48627  2itscp  48630  onetansqsecsq  48991