Theorem addcomd 11463

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 11256	. . . . . . . 8 ⊢ (𝜑 → 1 ∈ ℂ)
2	1, 1	addcld 11280	. . . . . . 7 ⊢ (𝜑 → (1 + 1) ∈ ℂ)
3		muld.1	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ ℂ)
4		addcomd.2	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ ℂ)
5	2, 3, 4	adddid 11285	. . . . . 6 ⊢ (𝜑 → ((1 + 1) · (𝐴 + 𝐵)) = (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)))
6	3, 4	addcld 11280	. . . . . . 7 ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℂ)
7		1p1times 11432	. . . . . . 7 ⊢ ((𝐴 + 𝐵) ∈ ℂ → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
8	6, 7	syl 17	. . . . . 6 ⊢ (𝜑 → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
9		1p1times 11432	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
10	3, 9	syl 17	. . . . . . 7 ⊢ (𝜑 → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
11		1p1times 11432	. . . . . . . 8 ⊢ (𝐵 ∈ ℂ → ((1 + 1) · 𝐵) = (𝐵 + 𝐵))
12	4, 11	syl 17	. . . . . . 7 ⊢ (𝜑 → ((1 + 1) · 𝐵) = (𝐵 + 𝐵))
13	10, 12	oveq12d 7449	. . . . . 6 ⊢ (𝜑 → (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
14	5, 8, 13	3eqtr3rd 2786	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐴) + (𝐵 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
15	3, 3	addcld 11280	. . . . . 6 ⊢ (𝜑 → (𝐴 + 𝐴) ∈ ℂ)
16	15, 4, 4	addassd 11283	. . . . 5 ⊢ (𝜑 → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
17	6, 3, 4	addassd 11283	. . . . 5 ⊢ (𝜑 → (((𝐴 + 𝐵) + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
18	14, 16, 17	3eqtr4d 2787	. . . 4 ⊢ (𝜑 → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵))
19	15, 4	addcld 11280	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) ∈ ℂ)
20	6, 3	addcld 11280	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐴) ∈ ℂ)
21		addcan2 11446	. . . . 5 ⊢ ((((𝐴 + 𝐴) + 𝐵) ∈ ℂ ∧ ((𝐴 + 𝐵) + 𝐴) ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
22	19, 20, 4, 21	syl3anc 1373	. . . 4 ⊢ (𝜑 → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
23	18, 22	mpbid 232	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴))
24	3, 3, 4	addassd 11283	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) = (𝐴 + (𝐴 + 𝐵)))
25	3, 4, 3	addassd 11283	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐴) = (𝐴 + (𝐵 + 𝐴)))
26	23, 24, 25	3eqtr3d 2785	. 2 ⊢ (𝜑 → (𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)))
27	4, 3	addcld 11280	. . 3 ⊢ (𝜑 → (𝐵 + 𝐴) ∈ ℂ)
28		addcan 11445	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ (𝐴 + 𝐵) ∈ ℂ ∧ (𝐵 + 𝐴) ∈ ℂ) → ((𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴)))
29	3, 6, 27, 28	syl3anc 1373	. 2 ⊢ (𝜑 → ((𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴)))
30	26, 29	mpbid 232	1 ⊢ (𝜑 → (𝐴 + 𝐵) = (𝐵 + 𝐴))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2108  (class class class)co 7431  ℂcc 11153  1c1 11156   + caddc 11158   · cmul 11160

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-po 5592  df-so 5593  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-ov 7434  df-er 8745  df-en 8986  df-dom 8987  df-sdom 8988  df-pnf 11297  df-mnf 11298  df-ltxr 11300

This theorem is referenced by:  muladd11r  11474  comraddd  11475  subadd2  11512  pncan  11514  npcan  11517  subcan  11564  mvlladdd  11674  subaddeqd  11678  addrsub  11680  mulsubaddmulsub  11727  ltadd1  11730  leadd2  11732  ltsubadd2  11734  lesubadd2  11736  lesub3d  11881  supadd  12236  ltaddrp2d  13111  lincmb01cmp  13535  iccf1o  13536  elfzoext  13761  modaddabs  13949  muladdmodid  13951  negmod  13957  modadd2mod  13962  modadd12d  13968  modaddmulmod  13979  addmodlteq  13987  expaddz  14147  bcn2m1  14363  bcn2p1  14364  spllen  14792  splfv2a  14794  relexpaddnn  15090  relexpaddg  15092  rtrclreclem3  15099  remullem  15167  sqreulem  15398  bhmafibid2  15505  climaddc2  15672  iseraltlem2  15719  fsumsplit1  15781  telfsumo  15838  fsumparts  15842  bcxmas  15871  bpoly4  16095  sinadd  16200  sincossq  16212  cos2t  16214  absefi  16232  dvdsaddre2b  16344  pwp1fsum  16428  sadadd2lem2  16487  bitsres  16510  bezoutlem2  16577  bezoutlem4  16579  pythagtrip  16872  pcadd2  16928  vdwapun  17012  vdwlem5  17023  vdwlem6  17024  vdwlem8  17026  gsumsgrpccat  18853  mulgnndir  19121  mulgdirlem  19123  cyccom  19221  efgcpbllemb  19773  ablfacrp  20086  cncrng  21401  rzgrp  21641  icccvx  24981  cnlmod  25173  cphipval  25277  pjthlem1  25471  cmmbl  25569  voliunlem1  25585  dvle  26046  dvcvx  26059  dvfsumlem2  26067  dvfsumlem2OLD  26068  dvfsumlem4  26070  dvfsum2  26075  ply1divex  26176  plymullem1  26253  coeeulem  26263  aaliou3lem6  26390  dvtaylp  26412  ulmcn  26442  abelthlem7  26482  pilem3  26497  lawcos  26859  affineequiv  26866  affineequiv3  26868  heron  26881  dcubic1lem  26886  dcubic2  26887  dcubic  26889  mcubic  26890  quart1lem  26898  quart1  26899  asinlem2  26912  asinsin  26935  cosasin  26947  atanlogaddlem  26956  atanlogadd  26957  cvxcl  27028  lgamgulmlem2  27073  lgamcvg2  27098  lgam1  27107  bposlem9  27336  lgseisenlem1  27419  2sqlem3  27464  2sqblem  27475  2sqmod  27480  addsqn2reu  27485  2sqreulem1  27490  2sqreunnlem1  27493  dchrisumlem2  27534  selberg  27592  selberg2  27595  selberg4  27605  pntrlog2bndlem1  27621  pntlemb  27641  pntlemf  27649  padicabv  27674  colinearalglem2  28922  axsegconlem9  28940  axeuclidlem  28977  eupth2lem3lem3  30249  numclwwlk3lem1  30401  smcnlem  30716  ipval2  30726  hhph  31197  pjhthlem1  31410  golem1  32290  stcltrlem1  32295  quad3d  32754  omndmul2  33089  cycpmco2lem3  33148  cycpmco2lem4  33149  cycpmco2lem5  33150  cycpmco2lem6  33151  cycpmco2  33153  archirngz  33196  archiabllem1a  33198  archiabllem1  33200  archiabllem2c  33202  constrrtcc  33776  ballotlemsdom  34514  fsum2dsub  34622  revwlk  35130  resconn  35251  iprodgam  35742  faclimlem1  35743  faclimlem3  35745  faclim  35746  iprodfac  35747  fwddifnp1  36166  dnibndlem7  36485  dnibndlem8  36486  knoppndvlem14  36526  bj-bary1  37313  dvtan  37677  itgaddnclem2  37686  itgmulc2nc  37695  ftc1anclem8  37707  dvasin  37711  areacirclem1  37715  lcmineqlem19  42048  aks4d1p1p2  42071  posbezout  42101  sticksstones7  42153  sticksstones12a  42158  sticksstones12  42159  bcle2d  42180  aks6d1c7lem1  42181  metakunt15  42220  metakunt16  42221  dffltz  42644  fltbccoprm  42651  flt4lem3  42658  flt4lem5c  42664  flt4lem5d  42665  flt4lem5e  42666  flt4lem7  42669  nna4b4nsq  42670  fltnltalem  42672  3cubeslem2  42696  3cubeslem3l  42697  3cubeslem3r  42698  pellexlem2  42841  pell14qrgt0  42870  rmxyadd  42933  rmxluc  42948  fzmaxdif  42993  acongeq  42995  jm2.19lem2  43002  jm2.26lem3  43013  areaquad  43228  sqrtcval  43654  int-addcomd  44186  int-leftdistd  44192  subadd4b  45294  sub31  45302  coseq0  45879  coskpi2  45881  cosknegpi  45884  fperdvper  45934  dvbdfbdioolem2  45944  dvnmul  45958  dvmptfprodlem  45959  itgsincmulx  45989  itgsbtaddcnst  45997  stoweidlem11  46026  stirlinglem5  46093  stirlinglem7  46095  dirkertrigeqlem1  46113  dirkertrigeqlem2  46114  dirkertrigeqlem3  46115  dirkertrigeq  46116  dirkercncflem2  46119  fourierdlem4  46126  fourierdlem26  46148  fourierdlem40  46162  fourierdlem42  46164  fourierdlem47  46168  fourierdlem63  46184  fourierdlem64  46185  fourierdlem65  46186  fourierdlem74  46195  fourierdlem75  46196  fourierdlem78  46199  fourierdlem79  46200  fourierdlem84  46205  fourierdlem93  46214  fourierdlem103  46224  fourierdlem111  46232  fourierswlem  46245  fouriersw  46246  etransclem32  46281  etransclem46  46295  sge0gtfsumgt  46458  hoidmv1lelem2  46607  hoidmvlelem2  46611  hspmbllem1  46641  smfmullem1  46806  sigarperm  46875  2elfz2melfz  47330  fargshiftfo  47429  ichexmpl2  47457  fmtnorec3  47535  2zrngacmnd  48164  2zrngagrp  48165  ply1mulgsumlem1  48303  m1modmmod  48442  ackval1  48602  ackval2  48603  resum2sqorgt0  48630  eenglngeehlnmlem2  48659  rrx2linest2  48665  line2xlem  48674  itsclc0yqsollem1  48683  itsclc0yqsol  48685  itscnhlc0xyqsol  48686  itsclc0xyqsolr  48690  itsclinecirc0b  48695  itsclquadb  48697  2itscplem1  48699  2itscp  48702  onetansqsecsq  49280