Theorem addcomd 11396

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 11186	. . . . . . . 8 ⊢ (𝜑 → 1 ∈ ℂ)
2	1, 1	addcld 11212	. . . . . . 7 ⊢ (𝜑 → (1 + 1) ∈ ℂ)
3		muld.1	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ ℂ)
4		addcomd.2	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ ℂ)
5	2, 3, 4	adddid 11217	. . . . . 6 ⊢ (𝜑 → ((1 + 1) · (𝐴 + 𝐵)) = (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)))
6	3, 4	addcld 11212	. . . . . . 7 ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℂ)
7		1p1times 11365	. . . . . . 7 ⊢ ((𝐴 + 𝐵) ∈ ℂ → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
8	6, 7	syl 17	. . . . . 6 ⊢ (𝜑 → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
9		1p1times 11365	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
10	3, 9	syl 17	. . . . . . 7 ⊢ (𝜑 → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
11		1p1times 11365	. . . . . . . 8 ⊢ (𝐵 ∈ ℂ → ((1 + 1) · 𝐵) = (𝐵 + 𝐵))
12	4, 11	syl 17	. . . . . . 7 ⊢ (𝜑 → ((1 + 1) · 𝐵) = (𝐵 + 𝐵))
13	10, 12	oveq12d 7414	. . . . . 6 ⊢ (𝜑 → (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
14	5, 8, 13	3eqtr3rd 2807	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐴) + (𝐵 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
15	3, 3	addcld 11212	. . . . . 6 ⊢ (𝜑 → (𝐴 + 𝐴) ∈ ℂ)
16	15, 4, 4	addassd 11215	. . . . 5 ⊢ (𝜑 → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
17	6, 3, 4	addassd 11215	. . . . 5 ⊢ (𝜑 → (((𝐴 + 𝐵) + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
18	14, 16, 17	3eqtr4d 2808	. . . 4 ⊢ (𝜑 → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵))
19	15, 4	addcld 11212	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) ∈ ℂ)
20	6, 3	addcld 11212	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐴) ∈ ℂ)
21		addcan2 11379	. . . . 5 ⊢ ((((𝐴 + 𝐴) + 𝐵) ∈ ℂ ∧ ((𝐴 + 𝐵) + 𝐴) ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
22	19, 20, 4, 21	syl3anc 1392	. . . 4 ⊢ (𝜑 → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
23	18, 22	mpbid 234	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴))
24	3, 3, 4	addassd 11215	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) = (𝐴 + (𝐴 + 𝐵)))
25	3, 4, 3	addassd 11215	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐴) = (𝐴 + (𝐵 + 𝐴)))
26	23, 24, 25	3eqtr3d 2806	. 2 ⊢ (𝜑 → (𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)))
27	4, 3	addcld 11212	. . 3 ⊢ (𝜑 → (𝐵 + 𝐴) ∈ ℂ)
28		addcan 11378	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ (𝐴 + 𝐵) ∈ ℂ ∧ (𝐵 + 𝐴) ∈ ℂ) → ((𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴)))
29	3, 6, 27, 28	syl3anc 1392	. 2 ⊢ (𝜑 → ((𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴)))
30	26, 29	mpbid 234	1 ⊢ (𝜑 → (𝐴 + 𝐵) = (𝐵 + 𝐴))

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1561   ∈ wcel 2143  (class class class)co 7396  ℂcc 11082  1c1 11085   + caddc 11087   · cmul 11089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5247  ax-nul 5257  ax-pow 5323  ax-pr 5391  ax-un 7718  ax-resscn 11141  ax-1cn 11142  ax-icn 11143  ax-addcl 11144  ax-addrcl 11145  ax-mulcl 11146  ax-mulrcl 11147  ax-mulcom 11148  ax-addass 11149  ax-mulass 11150  ax-distr 11151  ax-i2m1 11152  ax-1ne0 11153  ax-1rid 11154  ax-rnegex 11155  ax-rrecex 11156  ax-cnre 11157  ax-pre-lttri 11158  ax-pre-lttrn 11159  ax-pre-ltadd 11160

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1100  df-3an 1101  df-tru 1564  df-fal 1574  df-ex 1801  df-nf 1805  df-sb 2092  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3063  df-ral 3078  df-rex 3088  df-rab 3416  df-v 3457  df-sbc 3746  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5102  df-opab 5164  df-mpt 5183  df-id 5543  df-po 5556  df-so 5557  df-xp 5654  df-rel 5655  df-cnv 5656  df-co 5657  df-dm 5658  df-rn 5659  df-res 5660  df-ima 5661  df-iota 6477  df-fun 6523  df-fn 6524  df-f 6525  df-f1 6526  df-fo 6527  df-f1o 6528  df-fv 6529  df-ov 7399  df-er 8678  df-en 8928  df-dom 8929  df-sdom 8930  df-pnf 11229  df-mnf 11230  df-ltxr 11232

This theorem is referenced by:  muladd11r  11407  comraddd  11408  subadd2  11445  pncan  11447  npcan  11450  subcan  11497  mvlladdd  11609  subaddeqd  11613  addrsub  11615  mulsubaddmulsub  11662  ltadd1  11665  leadd2  11667  ltsubadd2  11669  lesubadd2  11671  lesub3d  11816  supadd  12170  ltaddrp2d  13081  lincmb01cmp  13509  iccf1o  13510  elfzoext  13738  modaddabs  13931  muladdmodid  13933  negmod  13939  modadd2mod  13944  modadd12d  13950  modaddmulmod  13961  addmodlteq  13969  expaddz  14129  bcn2m1  14347  bcn2p1  14348  lenrevpfxcctswrd  14735  spllen  14777  splfv2a  14779  relexpaddnn  15074  relexpaddg  15076  rtrclreclem3  15083  remullem  15165  sqreulem  15397  bhmafibid2  15506  climaddc2  15673  iseraltlem2  15720  fsumsplit1  15782  telfsumo  15840  fsumparts  15844  bcxmas  15875  bpoly4  16099  sinadd  16206  sincossq  16218  cos2t  16220  absefi  16238  dvdsaddre2b  16351  pwp1fsum  16435  sadadd2lem2  16494  bitsres  16517  bezoutlem2  16584  bezoutlem4  16586  pythagtrip  16880  pcadd2  16936  vdwapun  17020  vdwlem5  17031  vdwlem6  17032  vdwlem8  17034  gsumsgrpccat  18884  mulgnndir  19155  mulgdirlem  19157  cyccom  19254  efgcpbllemb  19805  ablfacrp  20118  omndmul2  20183  cncrng  21452  rzgrp  21682  icccvx  25019  cnlmod  25209  cphipval  25312  pjthlem1  25506  cmmbl  25603  voliunlem1  25619  dvle  26076  dvcvx  26089  dvfsumlem2  26096  dvfsumlem4  26098  dvfsum2  26103  ply1divex  26204  plymullem1  26281  coeeulem  26291  aaliou3lem6  26419  dvtaylp  26440  ulmcn  26469  abelthlem7  26508  pilem3  26523  lawcos  26888  affineequiv  26895  affineequiv3  26897  heron  26910  dcubic1lem  26915  dcubic2  26916  dcubic  26918  mcubic  26919  quart1lem  26927  quart1  26928  asinlem2  26941  asinsin  26964  cosasin  26976  atanlogaddlem  26985  atanlogadd  26986  cvxcl  27056  lgamgulmlem2  27101  lgamcvg2  27126  lgam1  27135  bposlem9  27363  lgseisenlem1  27446  2sqlem3  27491  2sqblem  27502  2sqmod  27507  addsqn2reu  27512  2sqreulem1  27517  2sqreunnlem1  27520  dchrisumlem2  27561  selberg  27619  selberg2  27622  selberg4  27632  pntrlog2bndlem1  27648  pntlemb  27668  pntlemf  27676  padicabv  27701  colinearalglem2  29115  axsegconlem9  29133  axeuclidlem  29170  eupth2lem3lem3  30439  numclwwlk3lem1  30591  smcnlem  30907  ipval2  30917  hhph  31388  pjhthlem1  31601  golem1  32481  stcltrlem1  32486  pythagreim  32953  quad3d  32957  cycpmco2lem3  33314  cycpmco2lem4  33315  cycpmco2lem5  33316  cycpmco2lem6  33317  cycpmco2  33319  archirngz  33375  archiabllem1a  33377  archiabllem1  33379  archiabllem2c  33381  constrrtcc  34034  cos9thpiminplylem1  34081  cos9thpiminplylem2  34082  cos9thpiminplylem3  34083  cos9thpinconstrlem1  34088  ballotlemsdom  34811  fsum2dsub  34903  revwlk  35480  resconn  35601  iprodgam  36097  faclimlem1  36098  faclimlem3  36100  faclim  36101  iprodfac  36102  fwddifnp1  36520  dnibndlem7  36927  dnibndlem8  36928  knoppndvlem14  36968  bj-bary1  37809  dvtan  38174  itgaddnclem2  38183  itgmulc2nc  38192  ftc1anclem8  38204  dvasin  38208  areacirclem1  38212  lcmineqlem19  42669  aks4d1p1p2  42692  posbezout  42722  sticksstones7  42774  sticksstones12a  42779  sticksstones12  42780  bcle2d  42801  aks6d1c7lem1  42802  dffltz  43221  fltbccoprm  43228  flt4lem3  43235  flt4lem5c  43241  flt4lem5d  43242  flt4lem5e  43243  flt4lem7  43246  nna4b4nsq  43247  fltnltalem  43249  3cubeslem2  43271  3cubeslem3l  43272  3cubeslem3r  43273  pellexlem2  43412  pell14qrgt0  43441  rmxyadd  43503  rmxluc  43518  fzmaxdif  43563  acongeq  43565  jm2.19lem2  43572  jm2.26lem3  43583  areaquad  43798  sqrtcval  44222  int-addcomd  44754  int-leftdistd  44760  subadd4b  45853  sub31  45860  coseq0  46429  coskpi2  46431  cosknegpi  46434  fperdvper  46484  dvbdfbdioolem2  46494  dvnmul  46508  dvmptfprodlem  46509  itgsincmulx  46539  itgsbtaddcnst  46547  stoweidlem11  46576  stirlinglem5  46643  stirlinglem7  46645  dirkertrigeqlem1  46663  dirkertrigeqlem2  46664  dirkertrigeqlem3  46665  dirkertrigeq  46666  dirkercncflem2  46669  fourierdlem4  46676  fourierdlem26  46698  fourierdlem40  46712  fourierdlem42  46714  fourierdlem47  46718  fourierdlem63  46734  fourierdlem64  46735  fourierdlem65  46736  fourierdlem74  46745  fourierdlem75  46746  fourierdlem78  46749  fourierdlem79  46750  fourierdlem84  46755  fourierdlem93  46764  fourierdlem103  46774  fourierdlem111  46782  fourierswlem  46795  fouriersw  46796  etransclem32  46831  etransclem46  46845  sge0gtfsumgt  47008  hoidmv1lelem2  47157  hoidmvlelem2  47161  hspmbllem1  47191  smfmullem1  47356  sigarperm  47425  sin5tlem1  47458  sin5tlem5  47462  cjnpoly  47474  2elfz2melfz  47903  m1modmmod  47949  mod2addne  47955  fargshiftfo  48039  ichexmpl2  48067  fmtnorec3  48148  2zrngacmnd  48861  2zrngagrp  48862  ply1mulgsumlem1  48999  ackval1  49294  ackval2  49295  resum2sqorgt0  49322  eenglngeehlnmlem2  49351  rrx2linest2  49357  line2xlem  49366  itsclc0yqsollem1  49375  itsclc0yqsol  49377  itscnhlc0xyqsol  49378  itsclc0xyqsolr  49382  itsclinecirc0b  49387  itsclquadb  49389  2itscplem1  49391  2itscp  49394  onetansqsecsq  50373