Theorem addcomd 11337

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 11128	. . . . . . . 8 ⊢ (𝜑 → 1 ∈ ℂ)
2	1, 1	addcld 11153	. . . . . . 7 ⊢ (𝜑 → (1 + 1) ∈ ℂ)
3		muld.1	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ ℂ)
4		addcomd.2	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ ℂ)
5	2, 3, 4	adddid 11158	. . . . . 6 ⊢ (𝜑 → ((1 + 1) · (𝐴 + 𝐵)) = (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)))
6	3, 4	addcld 11153	. . . . . . 7 ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℂ)
7		1p1times 11306	. . . . . . 7 ⊢ ((𝐴 + 𝐵) ∈ ℂ → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
8	6, 7	syl 17	. . . . . 6 ⊢ (𝜑 → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
9		1p1times 11306	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
10	3, 9	syl 17	. . . . . . 7 ⊢ (𝜑 → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
11		1p1times 11306	. . . . . . . 8 ⊢ (𝐵 ∈ ℂ → ((1 + 1) · 𝐵) = (𝐵 + 𝐵))
12	4, 11	syl 17	. . . . . . 7 ⊢ (𝜑 → ((1 + 1) · 𝐵) = (𝐵 + 𝐵))
13	10, 12	oveq12d 7374	. . . . . 6 ⊢ (𝜑 → (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
14	5, 8, 13	3eqtr3rd 2779	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐴) + (𝐵 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
15	3, 3	addcld 11153	. . . . . 6 ⊢ (𝜑 → (𝐴 + 𝐴) ∈ ℂ)
16	15, 4, 4	addassd 11156	. . . . 5 ⊢ (𝜑 → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
17	6, 3, 4	addassd 11156	. . . . 5 ⊢ (𝜑 → (((𝐴 + 𝐵) + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
18	14, 16, 17	3eqtr4d 2780	. . . 4 ⊢ (𝜑 → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵))
19	15, 4	addcld 11153	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) ∈ ℂ)
20	6, 3	addcld 11153	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐴) ∈ ℂ)
21		addcan2 11320	. . . . 5 ⊢ ((((𝐴 + 𝐴) + 𝐵) ∈ ℂ ∧ ((𝐴 + 𝐵) + 𝐴) ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
22	19, 20, 4, 21	syl3anc 1374	. . . 4 ⊢ (𝜑 → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
23	18, 22	mpbid 232	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴))
24	3, 3, 4	addassd 11156	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) = (𝐴 + (𝐴 + 𝐵)))
25	3, 4, 3	addassd 11156	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐴) = (𝐴 + (𝐵 + 𝐴)))
26	23, 24, 25	3eqtr3d 2778	. 2 ⊢ (𝜑 → (𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)))
27	4, 3	addcld 11153	. . 3 ⊢ (𝜑 → (𝐵 + 𝐴) ∈ ℂ)
28		addcan 11319	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ (𝐴 + 𝐵) ∈ ℂ ∧ (𝐵 + 𝐴) ∈ ℂ) → ((𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴)))
29	3, 6, 27, 28	syl3anc 1374	. 2 ⊢ (𝜑 → ((𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴)))
30	26, 29	mpbid 232	1 ⊢ (𝜑 → (𝐴 + 𝐵) = (𝐵 + 𝐴))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114  (class class class)co 7356  ℂcc 11025  1c1 11028   + caddc 11030   · cmul 11032

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2184  ax-ext 2707  ax-sep 5220  ax-nul 5230  ax-pow 5296  ax-pr 5364  ax-un 7678  ax-resscn 11084  ax-1cn 11085  ax-icn 11086  ax-addcl 11087  ax-addrcl 11088  ax-mulcl 11089  ax-mulrcl 11090  ax-mulcom 11091  ax-addass 11092  ax-mulass 11093  ax-distr 11094  ax-i2m1 11095  ax-1ne0 11096  ax-1rid 11097  ax-rnegex 11098  ax-rrecex 11099  ax-cnre 11100  ax-pre-lttri 11101  ax-pre-lttrn 11102  ax-pre-ltadd 11103

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2538  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2810  df-nfc 2884  df-ne 2931  df-nel 3035  df-ral 3050  df-rex 3060  df-rab 3388  df-v 3429  df-sbc 3726  df-csb 3834  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4264  df-if 4457  df-pw 4533  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4841  df-br 5075  df-opab 5137  df-mpt 5156  df-id 5515  df-po 5528  df-so 5529  df-xp 5626  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-rn 5631  df-res 5632  df-ima 5633  df-iota 6443  df-fun 6489  df-fn 6490  df-f 6491  df-f1 6492  df-fo 6493  df-f1o 6494  df-fv 6495  df-ov 7359  df-er 8632  df-en 8883  df-dom 8884  df-sdom 8885  df-pnf 11170  df-mnf 11171  df-ltxr 11173

This theorem is referenced by:  muladd11r  11348  comraddd  11349  subadd2  11386  pncan  11388  npcan  11391  subcan  11438  mvlladdd  11550  subaddeqd  11554  addrsub  11556  mulsubaddmulsub  11603  ltadd1  11606  leadd2  11608  ltsubadd2  11610  lesubadd2  11612  lesub3d  11757  supadd  12113  ltaddrp2d  13009  lincmb01cmp  13437  iccf1o  13438  elfzoext  13666  modaddabs  13859  muladdmodid  13861  negmod  13867  modadd2mod  13872  modadd12d  13878  modaddmulmod  13889  addmodlteq  13897  expaddz  14057  bcn2m1  14275  bcn2p1  14276  lenrevpfxcctswrd  14663  spllen  14705  splfv2a  14707  relexpaddnn  15002  relexpaddg  15004  rtrclreclem3  15011  remullem  15079  sqreulem  15311  bhmafibid2  15420  climaddc2  15587  iseraltlem2  15634  fsumsplit1  15696  telfsumo  15754  fsumparts  15758  bcxmas  15789  bpoly4  16013  sinadd  16120  sincossq  16132  cos2t  16134  absefi  16152  dvdsaddre2b  16265  pwp1fsum  16349  sadadd2lem2  16408  bitsres  16431  bezoutlem2  16498  bezoutlem4  16500  pythagtrip  16794  pcadd2  16850  vdwapun  16934  vdwlem5  16945  vdwlem6  16946  vdwlem8  16948  gsumsgrpccat  18797  mulgnndir  19068  mulgdirlem  19070  cyccom  19167  efgcpbllemb  19719  ablfacrp  20032  omndmul2  20097  cncrng  21362  rzgrp  21592  icccvx  24905  cnlmod  25095  cphipval  25198  pjthlem1  25392  cmmbl  25489  voliunlem1  25505  dvle  25962  dvcvx  25975  dvfsumlem2  25982  dvfsumlem4  25984  dvfsum2  25989  ply1divex  26090  plymullem1  26167  coeeulem  26177  aaliou3lem6  26302  dvtaylp  26323  ulmcn  26352  abelthlem7  26391  pilem3  26406  lawcos  26768  affineequiv  26775  affineequiv3  26777  heron  26790  dcubic1lem  26795  dcubic2  26796  dcubic  26798  mcubic  26799  quart1lem  26807  quart1  26808  asinlem2  26821  asinsin  26844  cosasin  26856  atanlogaddlem  26865  atanlogadd  26866  cvxcl  26936  lgamgulmlem2  26981  lgamcvg2  27006  lgam1  27015  bposlem9  27243  lgseisenlem1  27326  2sqlem3  27371  2sqblem  27382  2sqmod  27387  addsqn2reu  27392  2sqreulem1  27397  2sqreunnlem1  27400  dchrisumlem2  27441  selberg  27499  selberg2  27502  selberg4  27512  pntrlog2bndlem1  27528  pntlemb  27548  pntlemf  27556  padicabv  27581  colinearalglem2  28964  axsegconlem9  28982  axeuclidlem  29019  eupth2lem3lem3  30288  numclwwlk3lem1  30440  smcnlem  30756  ipval2  30766  hhph  31237  pjhthlem1  31450  golem1  32330  stcltrlem1  32335  pythagreim  32806  quad3d  32810  cycpmco2lem3  33177  cycpmco2lem4  33178  cycpmco2lem5  33179  cycpmco2lem6  33180  cycpmco2  33182  archirngz  33238  archiabllem1a  33240  archiabllem1  33242  archiabllem2c  33244  constrrtcc  33867  cos9thpiminplylem1  33914  cos9thpiminplylem2  33915  cos9thpiminplylem3  33916  cos9thpinconstrlem1  33921  ballotlemsdom  34644  fsum2dsub  34739  revwlk  35295  resconn  35416  iprodgam  35912  faclimlem1  35913  faclimlem3  35915  faclim  35916  iprodfac  35917  fwddifnp1  36335  dnibndlem7  36732  dnibndlem8  36733  knoppndvlem14  36773  bj-bary1  37614  dvtan  37979  itgaddnclem2  37988  itgmulc2nc  37997  ftc1anclem8  38009  dvasin  38013  areacirclem1  38017  lcmineqlem19  42474  aks4d1p1p2  42497  posbezout  42527  sticksstones7  42579  sticksstones12a  42584  sticksstones12  42585  bcle2d  42606  aks6d1c7lem1  42607  dffltz  43055  fltbccoprm  43062  flt4lem3  43069  flt4lem5c  43075  flt4lem5d  43076  flt4lem5e  43077  flt4lem7  43080  nna4b4nsq  43081  fltnltalem  43083  3cubeslem2  43105  3cubeslem3l  43106  3cubeslem3r  43107  pellexlem2  43246  pell14qrgt0  43275  rmxyadd  43337  rmxluc  43352  fzmaxdif  43397  acongeq  43399  jm2.19lem2  43406  jm2.26lem3  43417  areaquad  43632  sqrtcval  44056  int-addcomd  44588  int-leftdistd  44594  subadd4b  45704  sub31  45711  coseq0  46280  coskpi2  46282  cosknegpi  46285  fperdvper  46335  dvbdfbdioolem2  46345  dvnmul  46359  dvmptfprodlem  46360  itgsincmulx  46390  itgsbtaddcnst  46398  stoweidlem11  46427  stirlinglem5  46494  stirlinglem7  46496  dirkertrigeqlem1  46514  dirkertrigeqlem2  46515  dirkertrigeqlem3  46516  dirkertrigeq  46517  dirkercncflem2  46520  fourierdlem4  46527  fourierdlem26  46549  fourierdlem40  46563  fourierdlem42  46565  fourierdlem47  46569  fourierdlem63  46585  fourierdlem64  46586  fourierdlem65  46587  fourierdlem74  46596  fourierdlem75  46597  fourierdlem78  46600  fourierdlem79  46601  fourierdlem84  46606  fourierdlem93  46615  fourierdlem103  46625  fourierdlem111  46633  fourierswlem  46646  fouriersw  46647  etransclem32  46682  etransclem46  46696  sge0gtfsumgt  46859  hoidmv1lelem2  47008  hoidmvlelem2  47012  hspmbllem1  47042  smfmullem1  47207  sigarperm  47276  sin5tlem1  47309  sin5tlem5  47313  cjnpoly  47325  2elfz2melfz  47754  m1modmmod  47800  mod2addne  47806  fargshiftfo  47890  ichexmpl2  47918  fmtnorec3  47999  2zrngacmnd  48712  2zrngagrp  48713  ply1mulgsumlem1  48850  ackval1  49145  ackval2  49146  resum2sqorgt0  49173  eenglngeehlnmlem2  49202  rrx2linest2  49208  line2xlem  49217  itsclc0yqsollem1  49226  itsclc0yqsol  49228  itscnhlc0xyqsol  49229  itsclc0xyqsolr  49233  itsclinecirc0b  49238  itsclquadb  49240  2itscplem1  49242  2itscp  49245  onetansqsecsq  50224