Theorem addcomd 11448

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 11241	. . . . . . . 8 ⊢ (𝜑 → 1 ∈ ℂ)
2	1, 1	addcld 11265	. . . . . . 7 ⊢ (𝜑 → (1 + 1) ∈ ℂ)
3		muld.1	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ ℂ)
4		addcomd.2	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ ℂ)
5	2, 3, 4	adddid 11270	. . . . . 6 ⊢ (𝜑 → ((1 + 1) · (𝐴 + 𝐵)) = (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)))
6	3, 4	addcld 11265	. . . . . . 7 ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℂ)
7		1p1times 11417	. . . . . . 7 ⊢ ((𝐴 + 𝐵) ∈ ℂ → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
8	6, 7	syl 17	. . . . . 6 ⊢ (𝜑 → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
9		1p1times 11417	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
10	3, 9	syl 17	. . . . . . 7 ⊢ (𝜑 → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
11		1p1times 11417	. . . . . . . 8 ⊢ (𝐵 ∈ ℂ → ((1 + 1) · 𝐵) = (𝐵 + 𝐵))
12	4, 11	syl 17	. . . . . . 7 ⊢ (𝜑 → ((1 + 1) · 𝐵) = (𝐵 + 𝐵))
13	10, 12	oveq12d 7437	. . . . . 6 ⊢ (𝜑 → (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
14	5, 8, 13	3eqtr3rd 2774	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐴) + (𝐵 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
15	3, 3	addcld 11265	. . . . . 6 ⊢ (𝜑 → (𝐴 + 𝐴) ∈ ℂ)
16	15, 4, 4	addassd 11268	. . . . 5 ⊢ (𝜑 → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
17	6, 3, 4	addassd 11268	. . . . 5 ⊢ (𝜑 → (((𝐴 + 𝐵) + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
18	14, 16, 17	3eqtr4d 2775	. . . 4 ⊢ (𝜑 → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵))
19	15, 4	addcld 11265	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) ∈ ℂ)
20	6, 3	addcld 11265	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐴) ∈ ℂ)
21		addcan2 11431	. . . . 5 ⊢ ((((𝐴 + 𝐴) + 𝐵) ∈ ℂ ∧ ((𝐴 + 𝐵) + 𝐴) ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
22	19, 20, 4, 21	syl3anc 1368	. . . 4 ⊢ (𝜑 → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
23	18, 22	mpbid 231	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴))
24	3, 3, 4	addassd 11268	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) = (𝐴 + (𝐴 + 𝐵)))
25	3, 4, 3	addassd 11268	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐴) = (𝐴 + (𝐵 + 𝐴)))
26	23, 24, 25	3eqtr3d 2773	. 2 ⊢ (𝜑 → (𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)))
27	4, 3	addcld 11265	. . 3 ⊢ (𝜑 → (𝐵 + 𝐴) ∈ ℂ)
28		addcan 11430	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ (𝐴 + 𝐵) ∈ ℂ ∧ (𝐵 + 𝐴) ∈ ℂ) → ((𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴)))
29	3, 6, 27, 28	syl3anc 1368	. 2 ⊢ (𝜑 → ((𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴)))
30	26, 29	mpbid 231	1 ⊢ (𝜑 → (𝐴 + 𝐵) = (𝐵 + 𝐴))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1533   ∈ wcel 2098  (class class class)co 7419  ℂcc 11138  1c1 11141   + caddc 11143   · cmul 11145

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5300  ax-nul 5307  ax-pow 5365  ax-pr 5429  ax-un 7741  ax-resscn 11197  ax-1cn 11198  ax-icn 11199  ax-addcl 11200  ax-addrcl 11201  ax-mulcl 11202  ax-mulrcl 11203  ax-mulcom 11204  ax-addass 11205  ax-mulass 11206  ax-distr 11207  ax-i2m1 11208  ax-1ne0 11209  ax-1rid 11210  ax-rnegex 11211  ax-rrecex 11212  ax-cnre 11213  ax-pre-lttri 11214  ax-pre-lttrn 11215  ax-pre-ltadd 11216

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-nel 3036  df-ral 3051  df-rex 3060  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5576  df-po 5590  df-so 5591  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554  df-fo 6555  df-f1o 6556  df-fv 6557  df-ov 7422  df-er 8725  df-en 8965  df-dom 8966  df-sdom 8967  df-pnf 11282  df-mnf 11283  df-ltxr 11285

This theorem is referenced by:  muladd11r  11459  comraddd  11460  subadd2  11496  pncan  11498  npcan  11501  subcan  11547  mvlladdd  11657  subaddeqd  11661  addrsub  11663  mulsubaddmulsub  11710  ltadd1  11713  leadd2  11715  ltsubadd2  11717  lesubadd2  11719  lesub3d  11864  supadd  12215  ltaddrp2d  13085  lincmb01cmp  13507  iccf1o  13508  modaddabs  13910  muladdmodid  13912  negmod  13917  modadd2mod  13922  modadd12d  13928  modaddmulmod  13939  addmodlteq  13947  expaddz  14107  bcn2m1  14319  bcn2p1  14320  spllen  14740  splfv2a  14742  relexpaddnn  15034  relexpaddg  15036  rtrclreclem3  15043  remullem  15111  sqreulem  15342  bhmafibid2  15449  climaddc2  15616  iseraltlem2  15665  fsumsplit1  15727  telfsumo  15784  fsumparts  15788  bcxmas  15817  bpoly4  16039  sinadd  16144  sincossq  16156  cos2t  16158  absefi  16176  dvdsaddre2b  16287  pwp1fsum  16371  sadadd2lem2  16428  bitsres  16451  bezoutlem2  16519  bezoutlem4  16521  pythagtrip  16806  pcadd2  16862  vdwapun  16946  vdwlem5  16957  vdwlem6  16958  vdwlem8  16960  gsumsgrpccat  18800  mulgnndir  19066  mulgdirlem  19068  cyccom  19166  efgcpbllemb  19722  ablfacrp  20035  cncrng  21333  rzgrp  21572  icccvx  24919  cnlmod  25111  cphipval  25215  pjthlem1  25409  cmmbl  25507  voliunlem1  25523  dvle  25984  dvcvx  25997  dvfsumlem2  26005  dvfsumlem2OLD  26006  dvfsumlem4  26008  dvfsum2  26013  ply1divex  26117  plymullem1  26193  coeeulem  26203  aaliou3lem6  26328  dvtaylp  26350  ulmcn  26380  abelthlem7  26420  pilem3  26435  lawcos  26793  affineequiv  26800  affineequiv3  26802  heron  26815  dcubic1lem  26820  dcubic2  26821  dcubic  26823  mcubic  26824  quart1lem  26832  quart1  26833  asinlem2  26846  asinsin  26869  cosasin  26881  atanlogaddlem  26890  atanlogadd  26891  cvxcl  26962  lgamgulmlem2  27007  lgamcvg2  27032  lgam1  27041  bposlem9  27270  lgseisenlem1  27353  2sqlem3  27398  2sqblem  27409  2sqmod  27414  addsqn2reu  27419  2sqreulem1  27424  2sqreunnlem1  27427  dchrisumlem2  27468  selberg  27526  selberg2  27529  selberg4  27539  pntrlog2bndlem1  27555  pntlemb  27575  pntlemf  27583  padicabv  27608  colinearalglem2  28790  axsegconlem9  28808  axeuclidlem  28845  eupth2lem3lem3  30112  numclwwlk3lem1  30264  smcnlem  30579  ipval2  30589  hhph  31060  pjhthlem1  31273  golem1  32153  stcltrlem1  32158  omndmul2  32882  cycpmco2lem3  32941  cycpmco2lem4  32942  cycpmco2lem5  32943  cycpmco2lem6  32944  cycpmco2  32946  archirngz  32989  archiabllem1a  32991  archiabllem1  32993  archiabllem2c  32995  ballotlemsdom  34262  fsum2dsub  34370  revwlk  34865  resconn  34987  iprodgam  35467  faclimlem1  35468  faclimlem3  35470  faclim  35471  iprodfac  35472  fwddifnp1  35892  dnibndlem7  36090  dnibndlem8  36091  knoppndvlem14  36131  bj-bary1  36922  dvtan  37274  itgaddnclem2  37283  itgmulc2nc  37292  ftc1anclem8  37304  dvasin  37308  areacirclem1  37312  lcmineqlem19  41650  aks4d1p1p2  41673  posbezout  41703  sticksstones7  41755  sticksstones12a  41760  sticksstones12  41761  bcle2d  41782  aks6d1c7lem1  41783  metakunt15  41805  metakunt16  41806  dffltz  42193  fltbccoprm  42200  flt4lem3  42207  flt4lem5c  42213  flt4lem5d  42214  flt4lem5e  42215  flt4lem7  42218  nna4b4nsq  42219  fltnltalem  42221  3cubeslem2  42247  3cubeslem3l  42248  3cubeslem3r  42249  pellexlem2  42392  pell14qrgt0  42421  rmxyadd  42484  rmxluc  42499  fzmaxdif  42544  acongeq  42546  jm2.19lem2  42553  jm2.26lem3  42564  areaquad  42786  sqrtcval  43213  int-addcomd  43745  int-leftdistd  43751  subadd4b  44802  sub31  44810  coseq0  45390  coskpi2  45392  cosknegpi  45395  fperdvper  45445  dvbdfbdioolem2  45455  dvnmul  45469  dvmptfprodlem  45470  itgsincmulx  45500  itgsbtaddcnst  45508  stoweidlem11  45537  stirlinglem5  45604  stirlinglem7  45606  dirkertrigeqlem1  45624  dirkertrigeqlem2  45625  dirkertrigeqlem3  45626  dirkertrigeq  45627  dirkercncflem2  45630  fourierdlem4  45637  fourierdlem26  45659  fourierdlem40  45673  fourierdlem42  45675  fourierdlem47  45679  fourierdlem63  45695  fourierdlem64  45696  fourierdlem65  45697  fourierdlem74  45706  fourierdlem75  45707  fourierdlem78  45710  fourierdlem79  45711  fourierdlem84  45716  fourierdlem93  45725  fourierdlem103  45735  fourierdlem111  45743  fourierswlem  45756  fouriersw  45757  etransclem32  45792  etransclem46  45806  sge0gtfsumgt  45969  hoidmv1lelem2  46118  hoidmvlelem2  46122  hspmbllem1  46152  smfmullem1  46317  sigarperm  46386  2elfz2melfz  46836  fargshiftfo  46919  ichexmpl2  46947  fmtnorec3  47025  2zrngacmnd  47496  2zrngagrp  47497  ply1mulgsumlem1  47640  m1modmmod  47780  ackval1  47940  ackval2  47941  resum2sqorgt0  47968  eenglngeehlnmlem2  47997  rrx2linest2  48003  line2xlem  48012  itsclc0yqsollem1  48021  itsclc0yqsol  48023  itscnhlc0xyqsol  48024  itsclc0xyqsolr  48028  itsclinecirc0b  48033  itsclquadb  48035  2itscplem1  48037  2itscp  48040  onetansqsecsq  48378