Theorem addcomd 10845

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 10639	. . . . . . . 8 ⊢ (𝜑 → 1 ∈ ℂ)
2	1, 1	addcld 10663	. . . . . . 7 ⊢ (𝜑 → (1 + 1) ∈ ℂ)
3		muld.1	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ ℂ)
4		addcomd.2	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ ℂ)
5	2, 3, 4	adddid 10668	. . . . . 6 ⊢ (𝜑 → ((1 + 1) · (𝐴 + 𝐵)) = (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)))
6	3, 4	addcld 10663	. . . . . . 7 ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℂ)
7		1p1times 10814	. . . . . . 7 ⊢ ((𝐴 + 𝐵) ∈ ℂ → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
8	6, 7	syl 17	. . . . . 6 ⊢ (𝜑 → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
9		1p1times 10814	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
10	3, 9	syl 17	. . . . . . 7 ⊢ (𝜑 → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
11		1p1times 10814	. . . . . . . 8 ⊢ (𝐵 ∈ ℂ → ((1 + 1) · 𝐵) = (𝐵 + 𝐵))
12	4, 11	syl 17	. . . . . . 7 ⊢ (𝜑 → ((1 + 1) · 𝐵) = (𝐵 + 𝐵))
13	10, 12	oveq12d 7177	. . . . . 6 ⊢ (𝜑 → (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
14	5, 8, 13	3eqtr3rd 2868	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐴) + (𝐵 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
15	3, 3	addcld 10663	. . . . . 6 ⊢ (𝜑 → (𝐴 + 𝐴) ∈ ℂ)
16	15, 4, 4	addassd 10666	. . . . 5 ⊢ (𝜑 → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
17	6, 3, 4	addassd 10666	. . . . 5 ⊢ (𝜑 → (((𝐴 + 𝐵) + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
18	14, 16, 17	3eqtr4d 2869	. . . 4 ⊢ (𝜑 → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵))
19	15, 4	addcld 10663	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) ∈ ℂ)
20	6, 3	addcld 10663	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐴) ∈ ℂ)
21		addcan2 10828	. . . . 5 ⊢ ((((𝐴 + 𝐴) + 𝐵) ∈ ℂ ∧ ((𝐴 + 𝐵) + 𝐴) ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
22	19, 20, 4, 21	syl3anc 1367	. . . 4 ⊢ (𝜑 → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
23	18, 22	mpbid 234	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴))
24	3, 3, 4	addassd 10666	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) = (𝐴 + (𝐴 + 𝐵)))
25	3, 4, 3	addassd 10666	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐴) = (𝐴 + (𝐵 + 𝐴)))
26	23, 24, 25	3eqtr3d 2867	. 2 ⊢ (𝜑 → (𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)))
27	4, 3	addcld 10663	. . 3 ⊢ (𝜑 → (𝐵 + 𝐴) ∈ ℂ)
28		addcan 10827	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ (𝐴 + 𝐵) ∈ ℂ ∧ (𝐵 + 𝐴) ∈ ℂ) → ((𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴)))
29	3, 6, 27, 28	syl3anc 1367	. 2 ⊢ (𝜑 → ((𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴)))
30	26, 29	mpbid 234	1 ⊢ (𝜑 → (𝐴 + 𝐵) = (𝐵 + 𝐴))

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1536   ∈ wcel 2113  (class class class)co 7159  ℂcc 10538  1c1 10541   + caddc 10543   · cmul 10545

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 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796  ax-sep 5206  ax-nul 5213  ax-pow 5269  ax-pr 5333  ax-un 7464  ax-resscn 10597  ax-1cn 10598  ax-icn 10599  ax-addcl 10600  ax-addrcl 10601  ax-mulcl 10602  ax-mulrcl 10603  ax-mulcom 10604  ax-addass 10605  ax-mulass 10606  ax-distr 10607  ax-i2m1 10608  ax-1ne0 10609  ax-1rid 10610  ax-rnegex 10611  ax-rrecex 10612  ax-cnre 10613  ax-pre-lttri 10614  ax-pre-lttrn 10615  ax-pre-ltadd 10616

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-mo 2621  df-eu 2653  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-ne 3020  df-nel 3127  df-ral 3146  df-rex 3147  df-rab 3150  df-v 3499  df-sbc 3776  df-csb 3887  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4471  df-pw 4544  df-sn 4571  df-pr 4573  df-op 4577  df-uni 4842  df-br 5070  df-opab 5132  df-mpt 5150  df-id 5463  df-po 5477  df-so 5478  df-xp 5564  df-rel 5565  df-cnv 5566  df-co 5567  df-dm 5568  df-rn 5569  df-res 5570  df-ima 5571  df-iota 6317  df-fun 6360  df-fn 6361  df-f 6362  df-f1 6363  df-fo 6364  df-f1o 6365  df-fv 6366  df-ov 7162  df-er 8292  df-en 8513  df-dom 8514  df-sdom 8515  df-pnf 10680  df-mnf 10681  df-ltxr 10683

This theorem is referenced by:  muladd11r  10856  comraddd  10857  subadd2  10893  pncan  10895  npcan  10898  subcan  10944  mvlladdd  11054  subaddeqd  11058  addrsub  11060  mulsubaddmulsub  11107  ltadd1  11110  leadd2  11112  ltsubadd2  11114  lesubadd2  11116  lesub3d  11261  supadd  11612  ltaddrp2d  12468  lincmb01cmp  12884  iccf1o  12885  modaddabs  13280  muladdmodid  13282  negmod  13287  modadd2mod  13292  modadd12d  13298  modaddmulmod  13309  addmodlteq  13317  expaddz  13476  bcn2m1  13687  bcn2p1  13688  spllen  14119  splfv2a  14121  relexpaddnn  14413  relexpaddg  14415  rtrclreclem3  14422  remullem  14490  sqreulem  14722  bhmafibid2  14829  climaddc2  14995  iseraltlem2  15042  telfsumo  15160  fsumparts  15164  bcxmas  15193  bpoly4  15416  sinadd  15520  sincossq  15532  cos2t  15534  absefi  15552  dvdsaddre2b  15660  pwp1fsum  15745  sadadd2lem2  15802  bitsres  15825  bezoutlem2  15891  bezoutlem4  15893  pythagtrip  16174  pcadd2  16229  vdwapun  16313  vdwlem5  16324  vdwlem6  16325  vdwlem8  16327  gsumsgrpccat  18007  gsumccatOLD  18008  mulgnndir  18259  mulgdirlem  18261  cyccom  18349  efgcpbllemb  18884  cygablOLD  19014  ablfacrp  19191  rzgrp  20770  icccvx  23557  cnlmod  23747  cphipval  23849  pjthlem1  24043  cmmbl  24138  voliunlem1  24154  dvle  24607  dvcvx  24620  dvfsumlem2  24627  dvfsumlem4  24629  dvfsum2  24634  ply1divex  24733  plymullem1  24807  coeeulem  24817  aaliou3lem6  24940  dvtaylp  24961  ulmcn  24990  abelthlem7  25029  pilem3  25044  lawcos  25397  affineequiv  25404  affineequiv3  25406  heron  25419  dcubic1lem  25424  dcubic2  25425  dcubic  25427  mcubic  25428  quart1lem  25436  quart1  25437  asinlem2  25450  asinsin  25473  cosasin  25485  atanlogaddlem  25494  atanlogadd  25495  cvxcl  25565  lgamgulmlem2  25610  lgamcvg2  25635  lgam1  25644  bposlem9  25871  lgseisenlem1  25954  2sqlem3  25999  2sqblem  26010  2sqmod  26015  addsqn2reu  26020  2sqreulem1  26025  2sqreunnlem1  26028  dchrisumlem2  26069  selberg  26127  selberg2  26130  selberg4  26140  pntrlog2bndlem1  26156  pntlemb  26176  pntlemf  26184  padicabv  26209  colinearalglem2  26696  axsegconlem9  26714  axeuclidlem  26751  eupth2lem3lem3  28012  numclwwlk3lem1  28164  smcnlem  28477  ipval2  28487  hhph  28958  pjhthlem1  29171  golem1  30051  stcltrlem1  30056  omndmul2  30717  cycpmco2lem3  30774  cycpmco2lem4  30775  cycpmco2lem5  30776  cycpmco2lem6  30777  cycpmco2  30779  archirngz  30822  archiabllem1a  30824  archiabllem1  30826  archiabllem2c  30828  ballotlemsdom  31773  fsum2dsub  31882  revwlk  32375  resconn  32497  iprodgam  32978  faclimlem1  32979  faclimlem3  32981  faclim  32982  iprodfac  32983  fwddifnp1  33630  dnibndlem7  33827  dnibndlem8  33828  knoppndvlem14  33868  bj-bary1  34597  dvtan  34946  itg2addnclem3  34949  itgaddnclem2  34955  itgmulc2nc  34964  ftc1anclem8  34978  dvasin  34982  areacirclem1  34986  dffltz  39277  fltnltalem  39280  3cubeslem2  39288  3cubeslem3l  39289  3cubeslem3r  39290  pellexlem2  39433  pell14qrgt0  39462  rmxyadd  39524  rmxluc  39539  fzmaxdif  39584  acongeq  39586  jm2.19lem2  39593  jm2.26lem3  39604  areaquad  39829  int-addcomd  40532  int-leftdistd  40538  subadd4b  41554  sub31  41563  fsumsplit1  41859  coseq0  42151  coskpi2  42153  cosknegpi  42156  fperdvper  42209  dvbdfbdioolem2  42220  dvnmul  42234  dvmptfprodlem  42235  itgsincmulx  42265  itgsbtaddcnst  42273  stoweidlem11  42303  stirlinglem5  42370  stirlinglem7  42372  dirkertrigeqlem1  42390  dirkertrigeqlem2  42391  dirkertrigeqlem3  42392  dirkertrigeq  42393  dirkercncflem2  42396  fourierdlem4  42403  fourierdlem26  42425  fourierdlem40  42439  fourierdlem42  42441  fourierdlem47  42445  fourierdlem63  42461  fourierdlem64  42462  fourierdlem65  42463  fourierdlem74  42472  fourierdlem75  42473  fourierdlem78  42476  fourierdlem79  42477  fourierdlem84  42482  fourierdlem93  42491  fourierdlem103  42501  fourierdlem111  42509  fourierswlem  42522  fouriersw  42523  etransclem32  42558  etransclem46  42572  sge0gtfsumgt  42732  hoidmv1lelem2  42881  hoidmvlelem2  42885  hspmbllem1  42915  smfmullem1  43073  sigarperm  43124  2elfz2melfz  43525  fargshiftfo  43609  ichexmpl2  43639  fmtnorec3  43717  2zrngacmnd  44220  2zrngagrp  44221  ply1mulgsumlem1  44447  m1modmmod  44588  resum2sqorgt0  44703  eenglngeehlnmlem2  44732  rrx2linest2  44738  line2xlem  44747  itsclc0yqsollem1  44756  itsclc0yqsol  44758  itscnhlc0xyqsol  44759  itsclc0xyqsolr  44763  itsclinecirc0b  44768  itsclquadb  44770  2itscplem1  44772  2itscp  44775  onetansqsecsq  44867