Theorem addcomd 10533

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 10330	. . . . . . . 8 ⊢ (𝜑 → 1 ∈ ℂ)
2	1, 1	addcld 10354	. . . . . . 7 ⊢ (𝜑 → (1 + 1) ∈ ℂ)
3		muld.1	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ ℂ)
4		addcomd.2	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ ℂ)
5	2, 3, 4	adddid 10359	. . . . . 6 ⊢ (𝜑 → ((1 + 1) · (𝐴 + 𝐵)) = (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)))
6	3, 4	addcld 10354	. . . . . . 7 ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℂ)
7		1p1times 10502	. . . . . . 7 ⊢ ((𝐴 + 𝐵) ∈ ℂ → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
8	6, 7	syl 17	. . . . . 6 ⊢ (𝜑 → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
9		1p1times 10502	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
10	3, 9	syl 17	. . . . . . 7 ⊢ (𝜑 → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
11		1p1times 10502	. . . . . . . 8 ⊢ (𝐵 ∈ ℂ → ((1 + 1) · 𝐵) = (𝐵 + 𝐵))
12	4, 11	syl 17	. . . . . . 7 ⊢ (𝜑 → ((1 + 1) · 𝐵) = (𝐵 + 𝐵))
13	10, 12	oveq12d 6902	. . . . . 6 ⊢ (𝜑 → (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
14	5, 8, 13	3eqtr3rd 2860	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐴) + (𝐵 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
15	3, 3	addcld 10354	. . . . . 6 ⊢ (𝜑 → (𝐴 + 𝐴) ∈ ℂ)
16	15, 4, 4	addassd 10357	. . . . 5 ⊢ (𝜑 → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
17	6, 3, 4	addassd 10357	. . . . 5 ⊢ (𝜑 → (((𝐴 + 𝐵) + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
18	14, 16, 17	3eqtr4d 2861	. . . 4 ⊢ (𝜑 → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵))
19	15, 4	addcld 10354	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) ∈ ℂ)
20	6, 3	addcld 10354	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐴) ∈ ℂ)
21		addcan2 10516	. . . . 5 ⊢ ((((𝐴 + 𝐴) + 𝐵) ∈ ℂ ∧ ((𝐴 + 𝐵) + 𝐴) ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
22	19, 20, 4, 21	syl3anc 1483	. . . 4 ⊢ (𝜑 → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
23	18, 22	mpbid 223	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴))
24	3, 3, 4	addassd 10357	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) = (𝐴 + (𝐴 + 𝐵)))
25	3, 4, 3	addassd 10357	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐴) = (𝐴 + (𝐵 + 𝐴)))
26	23, 24, 25	3eqtr3d 2859	. 2 ⊢ (𝜑 → (𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)))
27	4, 3	addcld 10354	. . 3 ⊢ (𝜑 → (𝐵 + 𝐴) ∈ ℂ)
28		addcan 10515	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ (𝐴 + 𝐵) ∈ ℂ ∧ (𝐵 + 𝐴) ∈ ℂ) → ((𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴)))
29	3, 6, 27, 28	syl3anc 1483	. 2 ⊢ (𝜑 → ((𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴)))
30	26, 29	mpbid 223	1 ⊢ (𝜑 → (𝐴 + 𝐵) = (𝐵 + 𝐴))

Syntax hints:   → wi 4   ↔ wb 197   = wceq 1637   ∈ wcel 2157  (class class class)co 6884  ℂcc 10229  1c1 10232   + caddc 10234   · cmul 10236

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795  ax-sep 4988  ax-nul 4996  ax-pow 5048  ax-pr 5109  ax-un 7189  ax-resscn 10288  ax-1cn 10289  ax-icn 10290  ax-addcl 10291  ax-addrcl 10292  ax-mulcl 10293  ax-mulrcl 10294  ax-mulcom 10295  ax-addass 10296  ax-mulass 10297  ax-distr 10298  ax-i2m1 10299  ax-1ne0 10300  ax-1rid 10301  ax-rnegex 10302  ax-rrecex 10303  ax-cnre 10304  ax-pre-lttri 10305  ax-pre-lttrn 10306  ax-pre-ltadd 10307

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2642  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ne 2990  df-nel 3093  df-ral 3112  df-rex 3113  df-rab 3116  df-v 3404  df-sbc 3645  df-csb 3740  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-nul 4128  df-if 4291  df-pw 4364  df-sn 4382  df-pr 4384  df-op 4388  df-uni 4642  df-br 4856  df-opab 4918  df-mpt 4935  df-id 5232  df-po 5245  df-so 5246  df-xp 5330  df-rel 5331  df-cnv 5332  df-co 5333  df-dm 5334  df-rn 5335  df-res 5336  df-ima 5337  df-iota 6074  df-fun 6113  df-fn 6114  df-f 6115  df-f1 6116  df-fo 6117  df-f1o 6118  df-fv 6119  df-ov 6887  df-er 7989  df-en 8203  df-dom 8204  df-sdom 8205  df-pnf 10371  df-mnf 10372  df-ltxr 10374

This theorem is referenced by:  muladd11r  10544  comraddd  10545  subadd2  10580  pncan  10582  npcan  10585  subcan  10631  subaddeqd  10741  addrsub  10743  ltadd1  10790  leadd2  10792  ltsubadd2  10794  lesubadd2  10796  lesub3d  10940  supadd  11286  ltaddrp2d  12140  lincmb01cmp  12558  iccf1o  12559  modaddabs  12952  muladdmodid  12954  negmod  12959  modadd2mod  12964  modadd12d  12970  modaddmulmod  12981  addmodlteq  12989  expaddz  13147  bcn2m1  13351  bcn2p1  13352  ccatrn  13606  addlenswrd  13682  spllen  13749  splfv2a  13751  relexpaddnn  14034  relexpaddg  14036  rtrclreclem3  14043  remullem  14111  sqreulem  14342  climaddc2  14609  iseraltlem2  14656  telfsumo  14776  fsumparts  14780  bcxmas  14809  bpoly4  15030  cosneg  15117  coshval  15125  sinadd  15134  sincossq  15146  cos2t  15148  absefi  15166  absefib  15168  dvdsaddre2b  15272  pwp1fsum  15354  sadadd2lem2  15411  bitsres  15434  bezoutlem2  15496  bezoutlem4  15498  pythagtrip  15776  pcadd2  15831  vdwapun  15915  vdwlem5  15926  vdwlem6  15927  vdwlem8  15929  gsumccat  17603  mulgnndir  17793  mulgdirlem  17795  mulgdir  17796  sylow1lem1  18234  efgcpbllemb  18389  cygabl  18513  ablfacrp  18687  rzgrp  20198  icccvx  22983  cnlmod  23173  cphipval  23275  pjthlem1  23443  ovolicc2lem4  23524  cmmbl  23538  voliunlem1  23554  itgmulc2  23837  dvle  24007  dvcvx  24020  dvfsumlem2  24027  dvfsumlem4  24029  dvfsum2  24034  ply1divex  24133  plymullem1  24207  coeeulem  24217  aaliou3lem6  24340  dvtaylp  24361  ulmcn  24390  abelthlem7  24429  pilem3  24444  pilem3OLD  24445  lawcos  24783  affineequiv  24790  heron  24802  quad2  24803  dcubic1lem  24807  dcubic2  24808  dcubic  24810  mcubic  24811  quart1lem  24819  quart1  24820  asinlem2  24833  asinsin  24856  cosasin  24868  atanlogaddlem  24877  atanlogadd  24878  cvxcl  24948  scvxcvx  24949  lgamgulmlem2  24993  lgamgulmlem3  24994  lgamcvg2  25018  lgam1  25027  bposlem9  25254  lgseisenlem1  25337  2sqlem3  25382  2sqblem  25393  dchrisumlem2  25416  selberg  25474  selberg2  25477  chpdifbndlem1  25479  selberg4  25487  pntrlog2bndlem1  25503  pntrlog2bndlem6  25509  pntibndlem2  25517  pntlemb  25523  pntlemf  25531  padicabv  25556  colinearalglem2  26024  axsegconlem9  26042  axeuclidlem  26079  eupth2lem3lem3  27426  numclwwlk3lem1  27593  smcnlem  27903  ipval2  27913  hhph  28386  pjhthlem1  28601  golem1  29481  stcltrlem1  29486  bhmafibid2  29993  2sqmod  29996  omndmul2  30060  archirngz  30091  archiabllem1a  30093  archiabllem1  30095  archiabllem2c  30097  ballotlemsdom  30921  signshf  31013  fsum2dsub  31033  resconn  31573  iprodgam  31972  faclimlem1  31973  faclimlem3  31975  faclim  31976  iprodfac  31977  fwddifnp1  32615  dnibndlem7  32813  dnibndlem8  32814  knoppndvlem14  32855  bj-bary1  33498  dvtan  33791  itg2addnclem3  33794  itgaddnclem2  33800  itgmulc2nc  33809  ftc1anclem8  33823  dvasin  33827  areacirclem1  33831  pellexlem2  37914  pell14qrgt0  37943  rmxyadd  38005  rmxluc  38020  fzmaxdif  38067  acongeq  38069  jm2.19lem2  38076  jm2.26lem3  38087  areaquad  38320  int-addcomd  38994  int-leftdistd  39000  subadd4b  39994  sub31  40003  fsumsplit1  40302  coseq0  40573  coskpi2  40575  cosknegpi  40578  fperdvper  40631  dvbdfbdioolem2  40642  dvnmul  40656  dvmptfprodlem  40657  itgsincmulx  40687  itgsbtaddcnst  40695  stoweidlem11  40725  stirlinglem5  40792  stirlinglem7  40794  dirkertrigeqlem1  40812  dirkertrigeqlem2  40813  dirkertrigeqlem3  40814  dirkertrigeq  40815  dirkercncflem2  40818  fourierdlem4  40825  fourierdlem26  40847  fourierdlem40  40861  fourierdlem42  40863  fourierdlem47  40867  fourierdlem63  40883  fourierdlem64  40884  fourierdlem65  40885  fourierdlem74  40894  fourierdlem75  40895  fourierdlem78  40898  fourierdlem79  40899  fourierdlem84  40904  fourierdlem93  40913  fourierdlem103  40923  fourierdlem111  40931  fourierswlem  40944  fouriersw  40945  etransclem32  40980  etransclem46  40994  sge0gtfsumgt  41157  hoidmv1lelem2  41306  hoidmvlelem2  41310  hspmbllem1  41340  smfmullem1  41498  sigarperm  41549  2elfz2melfz  41921  fargshiftfo  41971  fmtnorec3  42053  2zrngacmnd  42528  2zrngagrp  42529  ply1mulgsumlem1  42760  m1modmmod  42902  onetansqsecsq  43091  mvlladdd  43102