Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  addcomd Structured version   Visualization version   GIF version

Theorem addcomd 10351
 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
StepHypRef Expression
1 1cnd 10169 . . . . . . . 8 (𝜑 → 1 ∈ ℂ)
21, 1addcld 10172 . . . . . . 7 (𝜑 → (1 + 1) ∈ ℂ)
3 muld.1 . . . . . . 7 (𝜑𝐴 ∈ ℂ)
4 addcomd.2 . . . . . . 7 (𝜑𝐵 ∈ ℂ)
52, 3, 4adddid 10177 . . . . . 6 (𝜑 → ((1 + 1) · (𝐴 + 𝐵)) = (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)))
63, 4addcld 10172 . . . . . . 7 (𝜑 → (𝐴 + 𝐵) ∈ ℂ)
7 1p1times 10320 . . . . . . 7 ((𝐴 + 𝐵) ∈ ℂ → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
86, 7syl 17 . . . . . 6 (𝜑 → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
9 1p1times 10320 . . . . . . . 8 (𝐴 ∈ ℂ → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
103, 9syl 17 . . . . . . 7 (𝜑 → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
11 1p1times 10320 . . . . . . . 8 (𝐵 ∈ ℂ → ((1 + 1) · 𝐵) = (𝐵 + 𝐵))
124, 11syl 17 . . . . . . 7 (𝜑 → ((1 + 1) · 𝐵) = (𝐵 + 𝐵))
1310, 12oveq12d 6783 . . . . . 6 (𝜑 → (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
145, 8, 133eqtr3rd 2767 . . . . 5 (𝜑 → ((𝐴 + 𝐴) + (𝐵 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
153, 3addcld 10172 . . . . . 6 (𝜑 → (𝐴 + 𝐴) ∈ ℂ)
1615, 4, 4addassd 10175 . . . . 5 (𝜑 → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
176, 3, 4addassd 10175 . . . . 5 (𝜑 → (((𝐴 + 𝐵) + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
1814, 16, 173eqtr4d 2768 . . . 4 (𝜑 → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵))
1915, 4addcld 10172 . . . . 5 (𝜑 → ((𝐴 + 𝐴) + 𝐵) ∈ ℂ)
206, 3addcld 10172 . . . . 5 (𝜑 → ((𝐴 + 𝐵) + 𝐴) ∈ ℂ)
21 addcan2 10334 . . . . 5 ((((𝐴 + 𝐴) + 𝐵) ∈ ℂ ∧ ((𝐴 + 𝐵) + 𝐴) ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
2219, 20, 4, 21syl3anc 1439 . . . 4 (𝜑 → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
2318, 22mpbid 222 . . 3 (𝜑 → ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴))
243, 3, 4addassd 10175 . . 3 (𝜑 → ((𝐴 + 𝐴) + 𝐵) = (𝐴 + (𝐴 + 𝐵)))
253, 4, 3addassd 10175 . . 3 (𝜑 → ((𝐴 + 𝐵) + 𝐴) = (𝐴 + (𝐵 + 𝐴)))
2623, 24, 253eqtr3d 2766 . 2 (𝜑 → (𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)))
274, 3addcld 10172 . . 3 (𝜑 → (𝐵 + 𝐴) ∈ ℂ)
28 addcan 10333 . . 3 ((𝐴 ∈ ℂ ∧ (𝐴 + 𝐵) ∈ ℂ ∧ (𝐵 + 𝐴) ∈ ℂ) → ((𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴)))
293, 6, 27, 28syl3anc 1439 . 2 (𝜑 → ((𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴)))
3026, 29mpbid 222 1 (𝜑 → (𝐴 + 𝐵) = (𝐵 + 𝐴))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   = wceq 1596   ∈ wcel 2103  (class class class)co 6765  ℂcc 10047  1c1 10050   + caddc 10052   · cmul 10054 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-8 2105  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704  ax-sep 4889  ax-nul 4897  ax-pow 4948  ax-pr 5011  ax-un 7066  ax-resscn 10106  ax-1cn 10107  ax-icn 10108  ax-addcl 10109  ax-addrcl 10110  ax-mulcl 10111  ax-mulrcl 10112  ax-mulcom 10113  ax-addass 10114  ax-mulass 10115  ax-distr 10116  ax-i2m1 10117  ax-1ne0 10118  ax-1rid 10119  ax-rnegex 10120  ax-rrecex 10121  ax-cnre 10122  ax-pre-lttri 10123  ax-pre-lttrn 10124  ax-pre-ltadd 10125 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-eu 2575  df-mo 2576  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-ne 2897  df-nel 3000  df-ral 3019  df-rex 3020  df-rab 3023  df-v 3306  df-sbc 3542  df-csb 3640  df-dif 3683  df-un 3685  df-in 3687  df-ss 3694  df-nul 4024  df-if 4195  df-pw 4268  df-sn 4286  df-pr 4288  df-op 4292  df-uni 4545  df-br 4761  df-opab 4821  df-mpt 4838  df-id 5128  df-po 5139  df-so 5140  df-xp 5224  df-rel 5225  df-cnv 5226  df-co 5227  df-dm 5228  df-rn 5229  df-res 5230  df-ima 5231  df-iota 5964  df-fun 6003  df-fn 6004  df-f 6005  df-f1 6006  df-fo 6007  df-f1o 6008  df-fv 6009  df-ov 6768  df-er 7862  df-en 8073  df-dom 8074  df-sdom 8075  df-pnf 10189  df-mnf 10190  df-ltxr 10192 This theorem is referenced by:  muladd11r  10362  comraddd  10363  subadd2  10398  pncan  10400  npcan  10403  subcan  10449  subaddeqd  10559  addrsub  10561  ltadd1  10608  leadd2  10610  ltsubadd2  10612  lesubadd2  10614  lesub3d  10758  supadd  11104  ltaddrp2d  12020  lincmb01cmp  12429  iccf1o  12430  modaddabs  12823  muladdmodid  12825  negmod  12830  modadd2mod  12835  modadd12d  12841  modaddmulmod  12852  addmodlteq  12860  expaddz  13019  bcn2m1  13226  bcn2p1  13227  ccatrn  13482  addlenswrd  13559  spllen  13626  splfv2a  13628  relexpaddnn  13911  relexpaddg  13913  rtrclreclem3  13920  remullem  13988  sqreulem  14219  climaddc2  14486  clim2ser2  14506  iseraltlem2  14533  telfsumo  14654  fsumparts  14658  bcxmas  14687  bpoly4  14910  cosneg  14997  coshval  15005  sinadd  15014  sincossq  15026  cos2t  15028  absefi  15046  absefib  15048  dvdsaddre2b  15152  pwp1fsum  15237  sadadd2lem2  15295  bitsres  15318  bezoutlem2  15380  bezoutlem4  15382  pythagtrip  15662  pcadd2  15717  vdwapun  15801  vdwlem5  15812  vdwlem6  15813  vdwlem8  15815  gsumccat  17500  mulgnndir  17691  mulgnndirOLD  17692  mulgdirlem  17694  mulgdir  17695  sylow1lem1  18134  efgcpbllemb  18289  cygabl  18413  ablfacrp  18586  icccvx  22871  cnlmod  23061  cphipval  23163  pjthlem1  23329  ovolicc2lem4  23409  cmmbl  23423  voliunlem1  23439  itgmulc2  23720  dvle  23890  dvcvx  23903  dvfsumlem2  23910  dvfsumlem4  23912  dvfsum2  23917  ply1divex  24016  plymullem1  24090  coeeulem  24100  aaliou3lem6  24223  dvtaylp  24244  ulmcn  24273  abelthlem7  24312  pilem3  24327  rzgrp  24420  lawcos  24666  affineequiv  24673  heron  24685  quad2  24686  dcubic1lem  24690  dcubic2  24691  dcubic  24693  mcubic  24694  quart1lem  24702  quart1  24703  asinlem2  24716  asinsin  24739  cosasin  24751  atanlogaddlem  24760  atanlogadd  24761  cvxcl  24831  scvxcvx  24832  lgamgulmlem2  24876  lgamgulmlem3  24877  lgamcvg2  24901  lgam1  24910  bposlem9  25137  lgseisenlem1  25220  2sqlem3  25265  2sqblem  25276  dchrisumlem2  25299  selberg  25357  selberg2  25360  chpdifbndlem1  25362  selberg4  25370  pntrlog2bndlem1  25386  pntrlog2bndlem6  25392  pntibndlem2  25400  pntlemb  25406  pntlemf  25414  padicabv  25439  colinearalglem2  25907  axsegconlem9  25925  axeuclidlem  25962  eupth2lem3lem3  27303  numclwlk3lem3  27417  smcnlem  27782  ipval2  27792  hhph  28265  pjhthlem1  28480  golem1  29360  stcltrlem1  29365  bhmafibid2  29875  2sqmod  29878  omndmul2  29942  archirngz  29973  archiabllem1a  29975  archiabllem1  29977  archiabllem2c  29979  ballotlemsdom  30803  signshf  30895  fsum2dsub  30915  resconn  31456  iprodgam  31856  faclimlem1  31857  faclimlem3  31859  faclim  31860  iprodfac  31861  fwddifnp1  32499  dnibndlem7  32701  dnibndlem8  32702  knoppndvlem14  32743  bj-bary1  33394  dvtan  33692  itg2addnclem3  33695  itgaddnclem2  33701  itgmulc2nc  33710  ftc1anclem8  33724  dvasin  33728  areacirclem1  33732  pellexlem2  37813  pell14qrgt0  37842  rmxyadd  37905  rmxluc  37920  fzmaxdif  37967  acongeq  37969  jm2.19lem2  37976  jm2.26lem3  37987  areaquad  38221  int-addcomd  38895  int-leftdistd  38901  subadd4b  39910  sub31  39919  fsumsplit1  40224  coseq0  40495  coskpi2  40497  cosknegpi  40500  fperdvper  40553  dvbdfbdioolem2  40564  dvnmul  40578  dvmptfprodlem  40579  itgsincmulx  40610  itgsbtaddcnst  40618  stoweidlem11  40648  stirlinglem5  40715  stirlinglem7  40717  dirkertrigeqlem1  40735  dirkertrigeqlem2  40736  dirkertrigeqlem3  40737  dirkertrigeq  40738  dirkercncflem2  40741  fourierdlem4  40748  fourierdlem26  40770  fourierdlem40  40784  fourierdlem42  40786  fourierdlem47  40790  fourierdlem63  40806  fourierdlem64  40807  fourierdlem65  40808  fourierdlem74  40817  fourierdlem75  40818  fourierdlem78  40821  fourierdlem79  40822  fourierdlem84  40827  fourierdlem93  40836  fourierdlem103  40846  fourierdlem111  40854  fourierswlem  40867  fouriersw  40868  etransclem32  40903  etransclem46  40917  sge0gtfsumgt  41080  hoidmv1lelem2  41229  hoidmvlelem2  41233  hspmbllem1  41263  smfmullem1  41421  sigarperm  41472  2elfz2melfz  41755  fargshiftfo  41805  fmtnorec3  41887  2zrngacmnd  42369  2zrngagrp  42370  ply1mulgsumlem1  42601  m1modmmod  42743  onetansqsecsq  42932  mvlladdd  42943
 Copyright terms: Public domain W3C validator