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

Theorem addcomd 11364
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 11157 . . . . . . . 8 (๐œ‘ โ†’ 1 โˆˆ โ„‚)
21, 1addcld 11181 . . . . . . 7 (๐œ‘ โ†’ (1 + 1) โˆˆ โ„‚)
3 muld.1 . . . . . . 7 (๐œ‘ โ†’ ๐ด โˆˆ โ„‚)
4 addcomd.2 . . . . . . 7 (๐œ‘ โ†’ ๐ต โˆˆ โ„‚)
52, 3, 4adddid 11186 . . . . . 6 (๐œ‘ โ†’ ((1 + 1) ยท (๐ด + ๐ต)) = (((1 + 1) ยท ๐ด) + ((1 + 1) ยท ๐ต)))
63, 4addcld 11181 . . . . . . 7 (๐œ‘ โ†’ (๐ด + ๐ต) โˆˆ โ„‚)
7 1p1times 11333 . . . . . . 7 ((๐ด + ๐ต) โˆˆ โ„‚ โ†’ ((1 + 1) ยท (๐ด + ๐ต)) = ((๐ด + ๐ต) + (๐ด + ๐ต)))
86, 7syl 17 . . . . . 6 (๐œ‘ โ†’ ((1 + 1) ยท (๐ด + ๐ต)) = ((๐ด + ๐ต) + (๐ด + ๐ต)))
9 1p1times 11333 . . . . . . . 8 (๐ด โˆˆ โ„‚ โ†’ ((1 + 1) ยท ๐ด) = (๐ด + ๐ด))
103, 9syl 17 . . . . . . 7 (๐œ‘ โ†’ ((1 + 1) ยท ๐ด) = (๐ด + ๐ด))
11 1p1times 11333 . . . . . . . 8 (๐ต โˆˆ โ„‚ โ†’ ((1 + 1) ยท ๐ต) = (๐ต + ๐ต))
124, 11syl 17 . . . . . . 7 (๐œ‘ โ†’ ((1 + 1) ยท ๐ต) = (๐ต + ๐ต))
1310, 12oveq12d 7380 . . . . . 6 (๐œ‘ โ†’ (((1 + 1) ยท ๐ด) + ((1 + 1) ยท ๐ต)) = ((๐ด + ๐ด) + (๐ต + ๐ต)))
145, 8, 133eqtr3rd 2786 . . . . 5 (๐œ‘ โ†’ ((๐ด + ๐ด) + (๐ต + ๐ต)) = ((๐ด + ๐ต) + (๐ด + ๐ต)))
153, 3addcld 11181 . . . . . 6 (๐œ‘ โ†’ (๐ด + ๐ด) โˆˆ โ„‚)
1615, 4, 4addassd 11184 . . . . 5 (๐œ‘ โ†’ (((๐ด + ๐ด) + ๐ต) + ๐ต) = ((๐ด + ๐ด) + (๐ต + ๐ต)))
176, 3, 4addassd 11184 . . . . 5 (๐œ‘ โ†’ (((๐ด + ๐ต) + ๐ด) + ๐ต) = ((๐ด + ๐ต) + (๐ด + ๐ต)))
1814, 16, 173eqtr4d 2787 . . . 4 (๐œ‘ โ†’ (((๐ด + ๐ด) + ๐ต) + ๐ต) = (((๐ด + ๐ต) + ๐ด) + ๐ต))
1915, 4addcld 11181 . . . . 5 (๐œ‘ โ†’ ((๐ด + ๐ด) + ๐ต) โˆˆ โ„‚)
206, 3addcld 11181 . . . . 5 (๐œ‘ โ†’ ((๐ด + ๐ต) + ๐ด) โˆˆ โ„‚)
21 addcan2 11347 . . . . 5 ((((๐ด + ๐ด) + ๐ต) โˆˆ โ„‚ โˆง ((๐ด + ๐ต) + ๐ด) โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚) โ†’ ((((๐ด + ๐ด) + ๐ต) + ๐ต) = (((๐ด + ๐ต) + ๐ด) + ๐ต) โ†” ((๐ด + ๐ด) + ๐ต) = ((๐ด + ๐ต) + ๐ด)))
2219, 20, 4, 21syl3anc 1372 . . . 4 (๐œ‘ โ†’ ((((๐ด + ๐ด) + ๐ต) + ๐ต) = (((๐ด + ๐ต) + ๐ด) + ๐ต) โ†” ((๐ด + ๐ด) + ๐ต) = ((๐ด + ๐ต) + ๐ด)))
2318, 22mpbid 231 . . 3 (๐œ‘ โ†’ ((๐ด + ๐ด) + ๐ต) = ((๐ด + ๐ต) + ๐ด))
243, 3, 4addassd 11184 . . 3 (๐œ‘ โ†’ ((๐ด + ๐ด) + ๐ต) = (๐ด + (๐ด + ๐ต)))
253, 4, 3addassd 11184 . . 3 (๐œ‘ โ†’ ((๐ด + ๐ต) + ๐ด) = (๐ด + (๐ต + ๐ด)))
2623, 24, 253eqtr3d 2785 . 2 (๐œ‘ โ†’ (๐ด + (๐ด + ๐ต)) = (๐ด + (๐ต + ๐ด)))
274, 3addcld 11181 . . 3 (๐œ‘ โ†’ (๐ต + ๐ด) โˆˆ โ„‚)
28 addcan 11346 . . 3 ((๐ด โˆˆ โ„‚ โˆง (๐ด + ๐ต) โˆˆ โ„‚ โˆง (๐ต + ๐ด) โˆˆ โ„‚) โ†’ ((๐ด + (๐ด + ๐ต)) = (๐ด + (๐ต + ๐ด)) โ†” (๐ด + ๐ต) = (๐ต + ๐ด)))
293, 6, 27, 28syl3anc 1372 . 2 (๐œ‘ โ†’ ((๐ด + (๐ด + ๐ต)) = (๐ด + (๐ต + ๐ด)) โ†” (๐ด + ๐ต) = (๐ต + ๐ด)))
3026, 29mpbid 231 1 (๐œ‘ โ†’ (๐ด + ๐ต) = (๐ต + ๐ด))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โ†” wb 205   = wceq 1542   โˆˆ wcel 2107  (class class class)co 7362  โ„‚cc 11056  1c1 11059   + caddc 11061   ยท cmul 11063
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-resscn 11115  ax-1cn 11116  ax-icn 11117  ax-addcl 11118  ax-addrcl 11119  ax-mulcl 11120  ax-mulrcl 11121  ax-mulcom 11122  ax-addass 11123  ax-mulass 11124  ax-distr 11125  ax-i2m1 11126  ax-1ne0 11127  ax-1rid 11128  ax-rnegex 11129  ax-rrecex 11130  ax-cnre 11131  ax-pre-lttri 11132  ax-pre-lttrn 11133  ax-pre-ltadd 11134
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-mpt 5194  df-id 5536  df-po 5550  df-so 5551  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-ov 7365  df-er 8655  df-en 8891  df-dom 8892  df-sdom 8893  df-pnf 11198  df-mnf 11199  df-ltxr 11201
This theorem is referenced by:  muladd11r  11375  comraddd  11376  subadd2  11412  pncan  11414  npcan  11417  subcan  11463  mvlladdd  11573  subaddeqd  11577  addrsub  11579  mulsubaddmulsub  11626  ltadd1  11629  leadd2  11631  ltsubadd2  11633  lesubadd2  11635  lesub3d  11780  supadd  12130  ltaddrp2d  12998  lincmb01cmp  13419  iccf1o  13420  modaddabs  13821  muladdmodid  13823  negmod  13828  modadd2mod  13833  modadd12d  13839  modaddmulmod  13850  addmodlteq  13858  expaddz  14019  bcn2m1  14231  bcn2p1  14232  spllen  14649  splfv2a  14651  relexpaddnn  14943  relexpaddg  14945  rtrclreclem3  14952  remullem  15020  sqreulem  15251  bhmafibid2  15358  climaddc2  15525  iseraltlem2  15574  fsumsplit1  15637  telfsumo  15694  fsumparts  15698  bcxmas  15727  bpoly4  15949  sinadd  16053  sincossq  16065  cos2t  16067  absefi  16085  dvdsaddre2b  16196  pwp1fsum  16280  sadadd2lem2  16337  bitsres  16360  bezoutlem2  16428  bezoutlem4  16430  pythagtrip  16713  pcadd2  16769  vdwapun  16853  vdwlem5  16864  vdwlem6  16865  vdwlem8  16867  gsumsgrpccat  18657  mulgnndir  18912  mulgdirlem  18914  cyccom  19003  efgcpbllemb  19544  ablfacrp  19852  rzgrp  21043  icccvx  24329  cnlmod  24519  cphipval  24623  pjthlem1  24817  cmmbl  24914  voliunlem1  24930  dvle  25387  dvcvx  25400  dvfsumlem2  25407  dvfsumlem4  25409  dvfsum2  25414  ply1divex  25517  plymullem1  25591  coeeulem  25601  aaliou3lem6  25724  dvtaylp  25745  ulmcn  25774  abelthlem7  25813  pilem3  25828  lawcos  26182  affineequiv  26189  affineequiv3  26191  heron  26204  dcubic1lem  26209  dcubic2  26210  dcubic  26212  mcubic  26213  quart1lem  26221  quart1  26222  asinlem2  26235  asinsin  26258  cosasin  26270  atanlogaddlem  26279  atanlogadd  26280  cvxcl  26350  lgamgulmlem2  26395  lgamcvg2  26420  lgam1  26429  bposlem9  26656  lgseisenlem1  26739  2sqlem3  26784  2sqblem  26795  2sqmod  26800  addsqn2reu  26805  2sqreulem1  26810  2sqreunnlem1  26813  dchrisumlem2  26854  selberg  26912  selberg2  26915  selberg4  26925  pntrlog2bndlem1  26941  pntlemb  26961  pntlemf  26969  padicabv  26994  colinearalglem2  27898  axsegconlem9  27916  axeuclidlem  27953  eupth2lem3lem3  29216  numclwwlk3lem1  29368  smcnlem  29681  ipval2  29691  hhph  30162  pjhthlem1  30375  golem1  31255  stcltrlem1  31260  omndmul2  31962  cycpmco2lem3  32019  cycpmco2lem4  32020  cycpmco2lem5  32021  cycpmco2lem6  32022  cycpmco2  32024  archirngz  32067  archiabllem1a  32069  archiabllem1  32071  archiabllem2c  32073  ballotlemsdom  33151  fsum2dsub  33260  revwlk  33758  resconn  33880  iprodgam  34354  faclimlem1  34355  faclimlem3  34357  faclim  34358  iprodfac  34359  fwddifnp1  34779  dnibndlem7  34976  dnibndlem8  34977  knoppndvlem14  35017  bj-bary1  35812  dvtan  36157  itgaddnclem2  36166  itgmulc2nc  36175  ftc1anclem8  36187  dvasin  36191  areacirclem1  36195  lcmineqlem19  40533  aks4d1p1p2  40556  sticksstones7  40589  sticksstones12a  40594  sticksstones12  40595  metakunt15  40620  metakunt16  40621  dffltz  41001  fltbccoprm  41008  flt4lem3  41015  flt4lem5c  41021  flt4lem5d  41022  flt4lem5e  41023  flt4lem7  41026  nna4b4nsq  41027  fltnltalem  41029  3cubeslem2  41037  3cubeslem3l  41038  3cubeslem3r  41039  pellexlem2  41182  pell14qrgt0  41211  rmxyadd  41274  rmxluc  41289  fzmaxdif  41334  acongeq  41336  jm2.19lem2  41343  jm2.26lem3  41354  areaquad  41579  sqrtcval  41987  int-addcomd  42520  int-leftdistd  42526  subadd4b  43590  sub31  43598  coseq0  44179  coskpi2  44181  cosknegpi  44184  fperdvper  44234  dvbdfbdioolem2  44244  dvnmul  44258  dvmptfprodlem  44259  itgsincmulx  44289  itgsbtaddcnst  44297  stoweidlem11  44326  stirlinglem5  44393  stirlinglem7  44395  dirkertrigeqlem1  44413  dirkertrigeqlem2  44414  dirkertrigeqlem3  44415  dirkertrigeq  44416  dirkercncflem2  44419  fourierdlem4  44426  fourierdlem26  44448  fourierdlem40  44462  fourierdlem42  44464  fourierdlem47  44468  fourierdlem63  44484  fourierdlem64  44485  fourierdlem65  44486  fourierdlem74  44495  fourierdlem75  44496  fourierdlem78  44499  fourierdlem79  44500  fourierdlem84  44505  fourierdlem93  44514  fourierdlem103  44524  fourierdlem111  44532  fourierswlem  44545  fouriersw  44546  etransclem32  44581  etransclem46  44595  sge0gtfsumgt  44758  hoidmv1lelem2  44907  hoidmvlelem2  44911  hspmbllem1  44941  smfmullem1  45106  sigarperm  45175  2elfz2melfz  45624  fargshiftfo  45708  ichexmpl2  45736  fmtnorec3  45814  2zrngacmnd  46314  2zrngagrp  46315  ply1mulgsumlem1  46541  m1modmmod  46681  ackval1  46841  ackval2  46842  resum2sqorgt0  46869  eenglngeehlnmlem2  46898  rrx2linest2  46904  line2xlem  46913  itsclc0yqsollem1  46922  itsclc0yqsol  46924  itscnhlc0xyqsol  46925  itsclc0xyqsolr  46929  itsclinecirc0b  46934  itsclquadb  46936  2itscplem1  46938  2itscp  46941  onetansqsecsq  47280
  Copyright terms: Public domain W3C validator