Theorem addcomd 11371

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 11161	. . . . . . . 8 ⊢ (𝜑 → 1 ∈ ℂ)
2	1, 1	addcld 11187	. . . . . . 7 ⊢ (𝜑 → (1 + 1) ∈ ℂ)
3		muld.1	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ ℂ)
4		addcomd.2	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ ℂ)
5	2, 3, 4	adddid 11192	. . . . . 6 ⊢ (𝜑 → ((1 + 1) · (𝐴 + 𝐵)) = (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)))
6	3, 4	addcld 11187	. . . . . . 7 ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℂ)
7		1p1times 11340	. . . . . . 7 ⊢ ((𝐴 + 𝐵) ∈ ℂ → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
8	6, 7	syl 17	. . . . . 6 ⊢ (𝜑 → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
9		1p1times 11340	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
10	3, 9	syl 17	. . . . . . 7 ⊢ (𝜑 → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
11		1p1times 11340	. . . . . . . 8 ⊢ (𝐵 ∈ ℂ → ((1 + 1) · 𝐵) = (𝐵 + 𝐵))
12	4, 11	syl 17	. . . . . . 7 ⊢ (𝜑 → ((1 + 1) · 𝐵) = (𝐵 + 𝐵))
13	10, 12	oveq12d 7399	. . . . . 6 ⊢ (𝜑 → (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
14	5, 8, 13	3eqtr3rd 2796	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐴) + (𝐵 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
15	3, 3	addcld 11187	. . . . . 6 ⊢ (𝜑 → (𝐴 + 𝐴) ∈ ℂ)
16	15, 4, 4	addassd 11190	. . . . 5 ⊢ (𝜑 → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
17	6, 3, 4	addassd 11190	. . . . 5 ⊢ (𝜑 → (((𝐴 + 𝐵) + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
18	14, 16, 17	3eqtr4d 2797	. . . 4 ⊢ (𝜑 → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵))
19	15, 4	addcld 11187	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) ∈ ℂ)
20	6, 3	addcld 11187	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐴) ∈ ℂ)
21		addcan2 11354	. . . . 5 ⊢ ((((𝐴 + 𝐴) + 𝐵) ∈ ℂ ∧ ((𝐴 + 𝐵) + 𝐴) ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
22	19, 20, 4, 21	syl3anc 1382	. . . 4 ⊢ (𝜑 → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
23	18, 22	mpbid 234	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴))
24	3, 3, 4	addassd 11190	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) = (𝐴 + (𝐴 + 𝐵)))
25	3, 4, 3	addassd 11190	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐴) = (𝐴 + (𝐵 + 𝐴)))
26	23, 24, 25	3eqtr3d 2795	. 2 ⊢ (𝜑 → (𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)))
27	4, 3	addcld 11187	. . 3 ⊢ (𝜑 → (𝐵 + 𝐴) ∈ ℂ)
28		addcan 11353	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ (𝐴 + 𝐵) ∈ ℂ ∧ (𝐵 + 𝐴) ∈ ℂ) → ((𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴)))
29	3, 6, 27, 28	syl3anc 1382	. 2 ⊢ (𝜑 → ((𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴)))
30	26, 29	mpbid 234	1 ⊢ (𝜑 → (𝐴 + 𝐵) = (𝐵 + 𝐴))

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1550   ∈ wcel 2132  (class class class)co 7381  ℂcc 11057  1c1 11060   + caddc 11062   · cmul 11064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-10 2165  ax-11 2181  ax-12 2202  ax-ext 2724  ax-sep 5236  ax-nul 5246  ax-pow 5312  ax-pr 5380  ax-un 7703  ax-resscn 11116  ax-1cn 11117  ax-icn 11118  ax-addcl 11119  ax-addrcl 11120  ax-mulcl 11121  ax-mulrcl 11122  ax-mulcom 11123  ax-addass 11124  ax-mulass 11125  ax-distr 11126  ax-i2m1 11127  ax-1ne0 11128  ax-1rid 11129  ax-rnegex 11130  ax-rrecex 11131  ax-cnre 11132  ax-pre-lttri 11133  ax-pre-lttrn 11134  ax-pre-ltadd 11135

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3or 1096  df-3an 1097  df-tru 1553  df-fal 1563  df-ex 1790  df-nf 1794  df-sb 2081  df-mo 2556  df-eu 2586  df-clab 2731  df-cleq 2744  df-clel 2827  df-nfc 2901  df-ne 2948  df-nel 3052  df-ral 3067  df-rex 3077  df-rab 3405  df-v 3446  df-sbc 3736  df-csb 3844  df-dif 3898  df-un 3900  df-in 3902  df-ss 3912  df-nul 4277  df-if 4471  df-pw 4547  df-sn 4573  df-pr 4575  df-op 4579  df-uni 4856  df-br 5091  df-opab 5153  df-mpt 5172  df-id 5531  df-po 5544  df-so 5545  df-xp 5642  df-rel 5643  df-cnv 5644  df-co 5645  df-dm 5646  df-rn 5647  df-res 5648  df-ima 5649  df-iota 6462  df-fun 6508  df-fn 6509  df-f 6510  df-f1 6511  df-fo 6512  df-f1o 6513  df-fv 6514  df-ov 7384  df-er 8662  df-en 8913  df-dom 8914  df-sdom 8915  df-pnf 11204  df-mnf 11205  df-ltxr 11207

This theorem is referenced by:  muladd11r  11382  comraddd  11383  subadd2  11420  pncan  11422  npcan  11425  subcan  11472  mvlladdd  11584  subaddeqd  11588  addrsub  11590  mulsubaddmulsub  11637  ltadd1  11640  leadd2  11642  ltsubadd2  11644  lesubadd2  11646  lesub3d  11791  supadd  12146  ltaddrp2d  13057  lincmb01cmp  13485  iccf1o  13486  elfzoext  13714  modaddabs  13907  muladdmodid  13909  negmod  13915  modadd2mod  13920  modadd12d  13926  modaddmulmod  13937  addmodlteq  13945  expaddz  14105  bcn2m1  14323  bcn2p1  14324  lenrevpfxcctswrd  14711  spllen  14753  splfv2a  14755  relexpaddnn  15050  relexpaddg  15052  rtrclreclem3  15059  remullem  15127  sqreulem  15359  bhmafibid2  15468  climaddc2  15635  iseraltlem2  15682  fsumsplit1  15744  telfsumo  15802  fsumparts  15806  bcxmas  15837  bpoly4  16061  sinadd  16168  sincossq  16180  cos2t  16182  absefi  16200  dvdsaddre2b  16313  pwp1fsum  16397  sadadd2lem2  16456  bitsres  16479  bezoutlem2  16546  bezoutlem4  16548  pythagtrip  16842  pcadd2  16898  vdwapun  16982  vdwlem5  16993  vdwlem6  16994  vdwlem8  16996  gsumsgrpccat  18846  mulgnndir  19117  mulgdirlem  19119  cyccom  19216  efgcpbllemb  19767  ablfacrp  20080  omndmul2  20145  cncrng  21414  rzgrp  21644  icccvx  24981  cnlmod  25171  cphipval  25274  pjthlem1  25468  cmmbl  25565  voliunlem1  25581  dvle  26038  dvcvx  26051  dvfsumlem2  26058  dvfsumlem4  26060  dvfsum2  26065  ply1divex  26166  plymullem1  26243  coeeulem  26253  aaliou3lem6  26378  dvtaylp  26399  ulmcn  26428  abelthlem7  26467  pilem3  26482  lawcos  26847  affineequiv  26854  affineequiv3  26856  heron  26869  dcubic1lem  26874  dcubic2  26875  dcubic  26877  mcubic  26878  quart1lem  26886  quart1  26887  asinlem2  26900  asinsin  26923  cosasin  26935  atanlogaddlem  26944  atanlogadd  26945  cvxcl  27015  lgamgulmlem2  27060  lgamcvg2  27085  lgam1  27094  bposlem9  27322  lgseisenlem1  27405  2sqlem3  27450  2sqblem  27461  2sqmod  27466  addsqn2reu  27471  2sqreulem1  27476  2sqreunnlem1  27479  dchrisumlem2  27520  selberg  27578  selberg2  27581  selberg4  27591  pntrlog2bndlem1  27607  pntlemb  27627  pntlemf  27635  padicabv  27660  colinearalglem2  29043  axsegconlem9  29061  axeuclidlem  29098  eupth2lem3lem3  30367  numclwwlk3lem1  30519  smcnlem  30835  ipval2  30845  hhph  31316  pjhthlem1  31529  golem1  32409  stcltrlem1  32414  pythagreim  32886  quad3d  32890  cycpmco2lem3  33258  cycpmco2lem4  33259  cycpmco2lem5  33260  cycpmco2lem6  33261  cycpmco2  33263  archirngz  33319  archiabllem1a  33321  archiabllem1  33323  archiabllem2c  33325  constrrtcc  33976  cos9thpiminplylem1  34023  cos9thpiminplylem2  34024  cos9thpiminplylem3  34025  cos9thpinconstrlem1  34030  ballotlemsdom  34753  fsum2dsub  34848  revwlk  35413  resconn  35534  iprodgam  36030  faclimlem1  36031  faclimlem3  36033  faclim  36034  iprodfac  36035  fwddifnp1  36453  dnibndlem7  36860  dnibndlem8  36861  knoppndvlem14  36901  bj-bary1  37742  dvtan  38107  itgaddnclem2  38116  itgmulc2nc  38125  ftc1anclem8  38137  dvasin  38141  areacirclem1  38145  lcmineqlem19  42602  aks4d1p1p2  42625  posbezout  42655  sticksstones7  42707  sticksstones12a  42712  sticksstones12  42713  bcle2d  42734  aks6d1c7lem1  42735  dffltz  43154  fltbccoprm  43161  flt4lem3  43168  flt4lem5c  43174  flt4lem5d  43175  flt4lem5e  43176  flt4lem7  43179  nna4b4nsq  43180  fltnltalem  43182  3cubeslem2  43204  3cubeslem3l  43205  3cubeslem3r  43206  pellexlem2  43345  pell14qrgt0  43374  rmxyadd  43436  rmxluc  43451  fzmaxdif  43496  acongeq  43498  jm2.19lem2  43505  jm2.26lem3  43516  areaquad  43731  sqrtcval  44155  int-addcomd  44687  int-leftdistd  44693  subadd4b  45800  sub31  45807  coseq0  46376  coskpi2  46378  cosknegpi  46381  fperdvper  46431  dvbdfbdioolem2  46441  dvnmul  46455  dvmptfprodlem  46456  itgsincmulx  46486  itgsbtaddcnst  46494  stoweidlem11  46523  stirlinglem5  46590  stirlinglem7  46592  dirkertrigeqlem1  46610  dirkertrigeqlem2  46611  dirkertrigeqlem3  46612  dirkertrigeq  46613  dirkercncflem2  46616  fourierdlem4  46623  fourierdlem26  46645  fourierdlem40  46659  fourierdlem42  46661  fourierdlem47  46665  fourierdlem63  46681  fourierdlem64  46682  fourierdlem65  46683  fourierdlem74  46692  fourierdlem75  46693  fourierdlem78  46696  fourierdlem79  46697  fourierdlem84  46702  fourierdlem93  46711  fourierdlem103  46721  fourierdlem111  46729  fourierswlem  46742  fouriersw  46743  etransclem32  46778  etransclem46  46792  sge0gtfsumgt  46955  hoidmv1lelem2  47104  hoidmvlelem2  47108  hspmbllem1  47138  smfmullem1  47303  sigarperm  47372  sin5tlem1  47405  sin5tlem5  47409  cjnpoly  47421  2elfz2melfz  47850  m1modmmod  47896  mod2addne  47902  fargshiftfo  47986  ichexmpl2  48014  fmtnorec3  48095  2zrngacmnd  48808  2zrngagrp  48809  ply1mulgsumlem1  48946  ackval1  49241  ackval2  49242  resum2sqorgt0  49269  eenglngeehlnmlem2  49298  rrx2linest2  49304  line2xlem  49313  itsclc0yqsollem1  49322  itsclc0yqsol  49324  itscnhlc0xyqsol  49325  itsclc0xyqsolr  49329  itsclinecirc0b  49334  itsclquadb  49336  2itscplem1  49338  2itscp  49341  onetansqsecsq  50320