Theorem addcomd 11539

Description: Addition is commutative. 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 11329	. . . . . . . 8 ⊢ (𝜑 → 1 ∈ ℂ)
2	1, 1	addcld 11355	. . . . . . 7 ⊢ (𝜑 → (1 + 1) ∈ ℂ)
3		muld.1	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ ℂ)
4		addcomd.2	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ ℂ)
5	2, 3, 4	adddid 11360	. . . . . 6 ⊢ (𝜑 → ((1 + 1) · (𝐴 + 𝐵)) = (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)))
6	3, 4	addcld 11355	. . . . . . 7 ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℂ)
7		1p1times 11508	. . . . . . 7 ⊢ ((𝐴 + 𝐵) ∈ ℂ → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
8	6, 7	syl 18	. . . . . 6 ⊢ (𝜑 → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
9		1p1times 11508	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
10	3, 9	syl 18	. . . . . . 7 ⊢ (𝜑 → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
11		1p1times 11508	. . . . . . . 8 ⊢ (𝐵 ∈ ℂ → ((1 + 1) · 𝐵) = (𝐵 + 𝐵))
12	4, 11	syl 18	. . . . . . 7 ⊢ (𝜑 → ((1 + 1) · 𝐵) = (𝐵 + 𝐵))
13	10, 12	oveq12d 7461	. . . . . 6 ⊢ (𝜑 → (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
14	5, 8, 13	3eqtr3rd 2807	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐴) + (𝐵 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
15	3, 3	addcld 11355	. . . . . 6 ⊢ (𝜑 → (𝐴 + 𝐴) ∈ ℂ)
16	15, 4, 4	addassd 11358	. . . . 5 ⊢ (𝜑 → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
17	6, 3, 4	addassd 11358	. . . . 5 ⊢ (𝜑 → (((𝐴 + 𝐵) + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
18	14, 16, 17	3eqtr4d 2808	. . . 4 ⊢ (𝜑 → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵))
19	15, 4	addcld 11355	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) ∈ ℂ)
20	6, 3	addcld 11355	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐴) ∈ ℂ)
21		addcan2 11522	. . . . 5 ⊢ ((((𝐴 + 𝐴) + 𝐵) ∈ ℂ ∧ ((𝐴 + 𝐵) + 𝐴) ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
22	19, 20, 4, 21	syl3anc 1399	. . . 4 ⊢ (𝜑 → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
23	18, 22	mpbid 235	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴))
24	3, 3, 4	addassd 11358	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) = (𝐴 + (𝐴 + 𝐵)))
25	3, 4, 3	addassd 11358	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐴) = (𝐴 + (𝐵 + 𝐴)))
26	23, 24, 25	3eqtr3d 2806	. 2 ⊢ (𝜑 → (𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)))
27	4, 3	addcld 11355	. . 3 ⊢ (𝜑 → (𝐵 + 𝐴) ∈ ℂ)
28		addcan 11521	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ (𝐴 + 𝐵) ∈ ℂ ∧ (𝐵 + 𝐴) ∈ ℂ) → ((𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴)))
29	3, 6, 27, 28	syl3anc 1399	. 2 ⊢ (𝜑 → ((𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴)))
30	26, 29	mpbid 235	1 ⊢ (𝜑 → (𝐴 + 𝐵) = (𝐵 + 𝐴))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2147  (class class class)co 7443  ℂcc 11225  1c1 11228   + caddc 11230   · cmul 11232

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7775  ax-resscn 11284  ax-1cn 11285  ax-icn 11286  ax-addcl 11287  ax-addrcl 11288  ax-mulcl 11289  ax-mulrcl 11290  ax-mulcom 11291  ax-addass 11292  ax-mulass 11293  ax-distr 11294  ax-i2m1 11295  ax-1ne0 11296  ax-1rid 11297  ax-rnegex 11298  ax-rrecex 11299  ax-cnre 11300  ax-pre-lttri 11301  ax-pre-lttrn 11302  ax-pre-ltadd 11303

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-mpt 5190  df-id 5550  df-po 5563  df-so 5564  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6512  df-fun 6560  df-fn 6561  df-f 6562  df-f1 6563  df-fo 6564  df-f1o 6565  df-fv 6566  df-ov 7446  df-er 8745  df-en 9002  df-dom 9003  df-sdom 9004  df-pnf 11372  df-mnf 11373  df-ltxr 11375

This theorem is used by:  muladd11r  11550  comraddd  11551  subadd2  11588  pncan  11590  npcan  11593  subcan  11640  mvlladdd  11752  subaddeqd  11758  addrsub  11760  mulsubaddmulsub  11807  ltadd1  11810  leadd2  11812  ltsubadd2  11814  lesubadd2  11816  lesub3d  11961  supadd  12312  ltaddrp2d  13225  lincmb01cmp  13653  iccf1o  13654  elfzoext  13884  modaddabs  14078  muladdmodid  14080  negmod  14086  modadd2mod  14091  modadd12d  14097  modaddmulmod  14108  addmodlteq  14116  expaddz  14276  bcn2m1  14495  bcn2p1  14496  lenrevpfxcctswrd  14889  spllen  14931  splfv2a  14933  relexpaddnn  15233  relexpaddg  15235  rtrclreclem3  15242  remullem  15324  sqreulem  15556  bhmafibid2  15665  climaddc2  15832  iseraltlem2  15879  fsumsplit1  15940  telfsumo  15998  fsumparts  16002  bcxmas  16033  bpoly4  16254  sinadd  16361  sincossq  16373  cos2t  16375  absefi  16393  dvdsaddre2b  16506  pwp1fsum  16590  sadadd2lem2  16649  bitsres  16672  bezoutlem2  16742  bezoutlem4  16744  pythagtrip  17041  pcadd2  17097  vdwapun  17181  vdwlem5  17192  vdwlem6  17193  vdwlem8  17195  gsumsgrpccat  19065  mulgnndir  19342  mulgdirlem  19344  cyccom  19447  efgcpbllemb  19999  ablfacrp  20312  omndmul2  20377  cncrng  21729  rzgrp  21959  icccvx  25301  cnlmod  25491  cphipval  25594  pjthlem1  25788  cmmbl  25885  voliunlem1  25901  dvle  26357  dvcvx  26370  dvfsumlem2  26377  dvfsumlem4  26379  dvfsum2  26384  ply1divex  26485  plymullem1  26563  coeeulem  26573  aaliou3lem6  26705  dvtaylp  26727  ulmcn  26756  abelthlem7  26795  pilem3  26810  lawcos  27174  affineequiv  27181  affineequiv3  27183  heron  27196  dcubic1lem  27201  dcubic2  27202  dcubic  27204  mcubic  27205  quart1lem  27213  quart1  27214  asinlem2  27227  asinsin  27250  cosasin  27262  atanlogaddlem  27271  atanlogadd  27272  cvxcl  27342  lgamgulmlem2  27387  lgamcvg2  27412  lgam1  27421  bposlem9  27649  lgseisenlem1  27732  2sqlem3  27777  2sqblem  27788  2sqmod  27793  addsqn2reu  27798  2sqreulem1  27803  2sqreunnlem1  27806  dchrisumlem2  27847  selberg  27905  selberg2  27908  selberg4  27918  pntrlog2bndlem1  27934  pntlemb  27954  pntlemf  27962  padicabv  27987  fltbccoprm  28003  flt4lem3  28008  flt4lem5c  28014  flt4lem5d  28015  flt4lem5e  28016  flt4lem7  28019  nna4b4nsq  28020  colinearalglem2  29515  axsegconlem9  29533  axeuclidlem  29570  revwlk  30297  eupth2lem3lem3  30861  numclwwlk3lem1  31013  smcnlem  31329  ipval2  31339  hhph  31810  pjhthlem1  32023  golem1  32903  stcltrlem1  32908  pythagreim  33407  quad3d  33411  cycpmco2lem3  33759  cycpmco2lem4  33760  cycpmco2lem5  33761  cycpmco2lem6  33762  cycpmco2  33764  archirngz  33820  archiabllem1a  33822  archiabllem1  33824  archiabllem2c  33826  constrrtcc  34437  cos9thpiminplylem1  34484  cos9thpiminplylem2  34485  cos9thpiminplylem3  34486  cos9thpinconstrlem1  34491  ballotlemsdom  35214  fsum2dsub  35306  resconn  36178  iprodgam  36685  faclimlem1  36686  faclimlem3  36688  faclim  36689  iprodfac  36690  fwddifnp1  37108  dnibndlem7  37528  dnibndlem8  37529  knoppndvlem14  37569  bj-bary1  38425  dvtan  38780  itgaddnclem2  38789  itgmulc2nc  38798  ftc1anclem8  38810  dvasin  38814  areacirclem1  38818  lcmineqlem19  43289  aks4d1p1p2  43312  posbezout  43342  sticksstones7  43394  sticksstones12a  43399  sticksstones12  43400  bcle2d  43421  aks6d1c7lem1  43422  quadfac  43447  dffltz  43863  fltnltalem  43866  3cubeslem2  43888  3cubeslem3l  43889  3cubeslem3r  43890  pellexlem2  44030  pell14qrgt0  44059  rmxyadd  44121  rmxluc  44136  fzmaxdif  44181  acongeq  44183  jm2.19lem2  44190  jm2.26lem3  44201  areaquad  44410  sqrtcval  44833  int-addcomd  45365  int-leftdistd  45371  subadd4b  46504  sub31  46511  coseq0  47079  coskpi2  47081  cosknegpi  47084  fperdvper  47134  dvbdfbdioolem2  47144  dvnmul  47158  dvmptfprodlem  47159  itgsincmulx  47189  itgsbtaddcnst  47197  stoweidlem11  47226  stirlinglem5  47293  stirlinglem7  47295  dirkertrigeqlem1  47313  dirkertrigeqlem2  47314  dirkertrigeqlem3  47315  dirkertrigeq  47316  dirkercncflem2  47319  fourierdlem4  47326  fourierdlem26  47348  fourierdlem40  47362  fourierdlem42  47364  fourierdlem47  47368  fourierdlem63  47384  fourierdlem64  47385  fourierdlem65  47386  fourierdlem74  47395  fourierdlem75  47396  fourierdlem78  47399  fourierdlem79  47400  fourierdlem84  47405  fourierdlem93  47414  fourierdlem103  47424  fourierdlem111  47432  fourierswlem  47445  fouriersw  47446  etransclem32  47481  etransclem46  47495  sge0gtfsumgt  47658  hoidmv1lelem2  47807  hoidmvlelem2  47811  hspmbllem1  47841  smfmullem1  48006  sigarperm  48075  sin5tlem1  48124  sin5tlem5  48128  cjnpoly  48144  2elfz2melfz  48593  m1modmmod  48639  mod2addne  48645  fargshiftfo  48729  ichexmpl2  48757  fmtnorec3  48838  2zrngacmnd  49550  2zrngagrp  49551  ply1mulgsumlem1  49703  ackval1  49998  ackval2  49999  resum2sqorgt0  50026  eenglngeehlnmlem2  50056  rrx2linest2  50061  line2xlem  50070  itsclc0yqsollem1  50079  itsclc0yqsol  50081  itscnhlc0xyqsol  50082  itsclc0xyqsolr  50086  itsclinecirc0b  50091  itsclquadb  50093  2itscplem1  50095  2itscp  50098  onetansqsecsq  51134  crossp3d  51247