Theorem addcomd 11412

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 11205	. . . . . . . 8 ⊢ (𝜑 → 1 ∈ ℂ)
2	1, 1	addcld 11229	. . . . . . 7 ⊢ (𝜑 → (1 + 1) ∈ ℂ)
3		muld.1	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ ℂ)
4		addcomd.2	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ ℂ)
5	2, 3, 4	adddid 11234	. . . . . 6 ⊢ (𝜑 → ((1 + 1) · (𝐴 + 𝐵)) = (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)))
6	3, 4	addcld 11229	. . . . . . 7 ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℂ)
7		1p1times 11381	. . . . . . 7 ⊢ ((𝐴 + 𝐵) ∈ ℂ → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
8	6, 7	syl 17	. . . . . 6 ⊢ (𝜑 → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
9		1p1times 11381	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
10	3, 9	syl 17	. . . . . . 7 ⊢ (𝜑 → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
11		1p1times 11381	. . . . . . . 8 ⊢ (𝐵 ∈ ℂ → ((1 + 1) · 𝐵) = (𝐵 + 𝐵))
12	4, 11	syl 17	. . . . . . 7 ⊢ (𝜑 → ((1 + 1) · 𝐵) = (𝐵 + 𝐵))
13	10, 12	oveq12d 7423	. . . . . 6 ⊢ (𝜑 → (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
14	5, 8, 13	3eqtr3rd 2781	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐴) + (𝐵 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
15	3, 3	addcld 11229	. . . . . 6 ⊢ (𝜑 → (𝐴 + 𝐴) ∈ ℂ)
16	15, 4, 4	addassd 11232	. . . . 5 ⊢ (𝜑 → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
17	6, 3, 4	addassd 11232	. . . . 5 ⊢ (𝜑 → (((𝐴 + 𝐵) + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
18	14, 16, 17	3eqtr4d 2782	. . . 4 ⊢ (𝜑 → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵))
19	15, 4	addcld 11229	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) ∈ ℂ)
20	6, 3	addcld 11229	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐴) ∈ ℂ)
21		addcan2 11395	. . . . 5 ⊢ ((((𝐴 + 𝐴) + 𝐵) ∈ ℂ ∧ ((𝐴 + 𝐵) + 𝐴) ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
22	19, 20, 4, 21	syl3anc 1371	. . . 4 ⊢ (𝜑 → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
23	18, 22	mpbid 231	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴))
24	3, 3, 4	addassd 11232	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) = (𝐴 + (𝐴 + 𝐵)))
25	3, 4, 3	addassd 11232	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐴) = (𝐴 + (𝐵 + 𝐴)))
26	23, 24, 25	3eqtr3d 2780	. 2 ⊢ (𝜑 → (𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)))
27	4, 3	addcld 11229	. . 3 ⊢ (𝜑 → (𝐵 + 𝐴) ∈ ℂ)
28		addcan 11394	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ (𝐴 + 𝐵) ∈ ℂ ∧ (𝐵 + 𝐴) ∈ ℂ) → ((𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴)))
29	3, 6, 27, 28	syl3anc 1371	. 2 ⊢ (𝜑 → ((𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴)))
30	26, 29	mpbid 231	1 ⊢ (𝜑 → (𝐴 + 𝐵) = (𝐵 + 𝐴))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541   ∈ wcel 2106  (class class class)co 7405  ℂcc 11104  1c1 11107   + caddc 11109   · cmul 11111

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-po 5587  df-so 5588  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-ov 7408  df-er 8699  df-en 8936  df-dom 8937  df-sdom 8938  df-pnf 11246  df-mnf 11247  df-ltxr 11249

This theorem is referenced by:  muladd11r  11423  comraddd  11424  subadd2  11460  pncan  11462  npcan  11465  subcan  11511  mvlladdd  11621  subaddeqd  11625  addrsub  11627  mulsubaddmulsub  11674  ltadd1  11677  leadd2  11679  ltsubadd2  11681  lesubadd2  11683  lesub3d  11828  supadd  12178  ltaddrp2d  13046  lincmb01cmp  13468  iccf1o  13469  modaddabs  13870  muladdmodid  13872  negmod  13877  modadd2mod  13882  modadd12d  13888  modaddmulmod  13899  addmodlteq  13907  expaddz  14068  bcn2m1  14280  bcn2p1  14281  spllen  14700  splfv2a  14702  relexpaddnn  14994  relexpaddg  14996  rtrclreclem3  15003  remullem  15071  sqreulem  15302  bhmafibid2  15409  climaddc2  15576  iseraltlem2  15625  fsumsplit1  15687  telfsumo  15744  fsumparts  15748  bcxmas  15777  bpoly4  15999  sinadd  16103  sincossq  16115  cos2t  16117  absefi  16135  dvdsaddre2b  16246  pwp1fsum  16330  sadadd2lem2  16387  bitsres  16410  bezoutlem2  16478  bezoutlem4  16480  pythagtrip  16763  pcadd2  16819  vdwapun  16903  vdwlem5  16914  vdwlem6  16915  vdwlem8  16917  gsumsgrpccat  18717  mulgnndir  18977  mulgdirlem  18979  cyccom  19074  efgcpbllemb  19617  ablfacrp  19930  rzgrp  21167  icccvx  24457  cnlmod  24647  cphipval  24751  pjthlem1  24945  cmmbl  25042  voliunlem1  25058  dvle  25515  dvcvx  25528  dvfsumlem2  25535  dvfsumlem4  25537  dvfsum2  25542  ply1divex  25645  plymullem1  25719  coeeulem  25729  aaliou3lem6  25852  dvtaylp  25873  ulmcn  25902  abelthlem7  25941  pilem3  25956  lawcos  26310  affineequiv  26317  affineequiv3  26319  heron  26332  dcubic1lem  26337  dcubic2  26338  dcubic  26340  mcubic  26341  quart1lem  26349  quart1  26350  asinlem2  26363  asinsin  26386  cosasin  26398  atanlogaddlem  26407  atanlogadd  26408  cvxcl  26478  lgamgulmlem2  26523  lgamcvg2  26548  lgam1  26557  bposlem9  26784  lgseisenlem1  26867  2sqlem3  26912  2sqblem  26923  2sqmod  26928  addsqn2reu  26933  2sqreulem1  26938  2sqreunnlem1  26941  dchrisumlem2  26982  selberg  27040  selberg2  27043  selberg4  27053  pntrlog2bndlem1  27069  pntlemb  27089  pntlemf  27097  padicabv  27122  colinearalglem2  28154  axsegconlem9  28172  axeuclidlem  28209  eupth2lem3lem3  29472  numclwwlk3lem1  29624  smcnlem  29937  ipval2  29947  hhph  30418  pjhthlem1  30631  golem1  31511  stcltrlem1  31516  omndmul2  32217  cycpmco2lem3  32274  cycpmco2lem4  32275  cycpmco2lem5  32276  cycpmco2lem6  32277  cycpmco2  32279  archirngz  32322  archiabllem1a  32324  archiabllem1  32326  archiabllem2c  32328  ballotlemsdom  33498  fsum2dsub  33607  revwlk  34103  resconn  34225  iprodgam  34700  faclimlem1  34701  faclimlem3  34703  faclim  34704  iprodfac  34705  fwddifnp1  35125  gg-dvfsumlem2  35171  dnibndlem7  35348  dnibndlem8  35349  knoppndvlem14  35389  bj-bary1  36181  dvtan  36526  itgaddnclem2  36535  itgmulc2nc  36544  ftc1anclem8  36556  dvasin  36560  areacirclem1  36564  lcmineqlem19  40900  aks4d1p1p2  40923  sticksstones7  40956  sticksstones12a  40961  sticksstones12  40962  metakunt15  40987  metakunt16  40988  dffltz  41372  fltbccoprm  41379  flt4lem3  41386  flt4lem5c  41392  flt4lem5d  41393  flt4lem5e  41394  flt4lem7  41397  nna4b4nsq  41398  fltnltalem  41400  3cubeslem2  41408  3cubeslem3l  41409  3cubeslem3r  41410  pellexlem2  41553  pell14qrgt0  41582  rmxyadd  41645  rmxluc  41660  fzmaxdif  41705  acongeq  41707  jm2.19lem2  41714  jm2.26lem3  41725  areaquad  41950  sqrtcval  42377  int-addcomd  42910  int-leftdistd  42916  subadd4b  43978  sub31  43986  coseq0  44566  coskpi2  44568  cosknegpi  44571  fperdvper  44621  dvbdfbdioolem2  44631  dvnmul  44645  dvmptfprodlem  44646  itgsincmulx  44676  itgsbtaddcnst  44684  stoweidlem11  44713  stirlinglem5  44780  stirlinglem7  44782  dirkertrigeqlem1  44800  dirkertrigeqlem2  44801  dirkertrigeqlem3  44802  dirkertrigeq  44803  dirkercncflem2  44806  fourierdlem4  44813  fourierdlem26  44835  fourierdlem40  44849  fourierdlem42  44851  fourierdlem47  44855  fourierdlem63  44871  fourierdlem64  44872  fourierdlem65  44873  fourierdlem74  44882  fourierdlem75  44883  fourierdlem78  44886  fourierdlem79  44887  fourierdlem84  44892  fourierdlem93  44901  fourierdlem103  44911  fourierdlem111  44919  fourierswlem  44932  fouriersw  44933  etransclem32  44968  etransclem46  44982  sge0gtfsumgt  45145  hoidmv1lelem2  45294  hoidmvlelem2  45298  hspmbllem1  45328  smfmullem1  45493  sigarperm  45562  2elfz2melfz  46012  fargshiftfo  46096  ichexmpl2  46124  fmtnorec3  46202  2zrngacmnd  46793  2zrngagrp  46794  ply1mulgsumlem1  47020  m1modmmod  47160  ackval1  47320  ackval2  47321  resum2sqorgt0  47348  eenglngeehlnmlem2  47377  rrx2linest2  47383  line2xlem  47392  itsclc0yqsollem1  47401  itsclc0yqsol  47403  itscnhlc0xyqsol  47404  itsclc0xyqsolr  47408  itsclinecirc0b  47413  itsclquadb  47415  2itscplem1  47417  2itscp  47420  onetansqsecsq  47759