MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sumeq1d Structured version   Unicode version

Theorem sumeq1d 12487
Description: Equality deduction for sum. (Contributed by NM, 1-Nov-2005.)
Hypothesis
Ref Expression
sumeq1d.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
sumeq1d  |-  ( ph  -> 
sum_ k  e.  A  C  =  sum_ k  e.  B  C )
Distinct variable groups:    A, k    B, k
Allowed substitution hints:    ph( k)    C( k)

Proof of Theorem sumeq1d
StepHypRef Expression
1 sumeq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 sumeq1 12475 . 2  |-  ( A  =  B  ->  sum_ k  e.  A  C  =  sum_ k  e.  B  C
)
31, 2syl 16 1  |-  ( ph  -> 
sum_ k  e.  A  C  =  sum_ k  e.  B  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652   sum_csu 12471
This theorem is referenced by:  sumeq12dv  12492  sumeq12rdv  12493  fsumf1o  12509  sumss  12510  fsumcllem  12518  fsum1  12527  fzosump1  12530  fsump1  12532  fsum2d  12547  fsumcom2  12550  fsumshftm  12556  fsumrev2  12557  fsumtscopo  12573  fsumtscop  12575  fsumtscop2  12576  fsumparts  12577  fsumiun  12592  bcxmas  12607  incexclem  12608  incexc2  12610  isumsplit  12612  isum1p  12613  arisum  12631  arisum2  12632  geoser  12638  geolim  12639  geo2sum2  12643  mertenslem1  12653  mertenslem2  12654  mertens  12655  efcvgfsum  12680  eftlub  12702  effsumlt  12704  eirrlem  12795  bitsinv1  12946  bitsinvp1  12953  pcfac  13260  prmreclem4  13279  prmreclem6  13281  ovoliunlem1  19390  uniioombllem3  19469  itg11  19575  dvfsumlem1  19902  dvfsumlem4  19905  dvfsum2  19910  elplyr  20112  coeeu  20136  coeeq  20138  plyco  20152  0dgrb  20157  dvply2g  20194  vieta1lem2  20220  vieta1  20221  aaliou3lem5  20256  aaliou3lem6  20257  aaliou3lem7  20258  taylpfval  20273  pserdvlem2  20336  abelthlem6  20344  logfac  20487  advlogexp  20538  emcllem2  20827  emcllem3  20828  emcllem7  20832  harmonicbnd  20834  harmonicbnd2  20835  harmonicbnd3  20838  harmonicbnd4  20841  chtval  20885  chpval  20897  chtfl  20924  chpfl  20925  chtprm  20928  chtnprm  20929  chpp1  20930  chtdif  20933  prmorcht  20953  musum  20968  muinv  20970  logfaclbnd  20998  logfacbnd3  20999  logexprlim  21001  chtppilimlem1  21159  rplogsumlem2  21171  rpvmasumlem  21173  dchrisumlem1  21175  dchrisumlem2  21176  dchrisumlem3  21177  dchrisum  21178  dchrisum0fval  21191  dchrisum0ff  21193  dchrisum0flblem1  21194  dchrisum0lem2  21204  dchrisum0  21206  mulog2sumlem1  21220  2vmadivsumlem  21226  log2sumbnd  21230  logdivbnd  21242  selberg3lem1  21243  pntrsumbnd  21252  pntrsumbnd2  21253  pntrlog2bndlem1  21263  pntrlog2bndlem4  21266  pntpbnd1  21272  pntpbnd2  21273  pntlemf  21291  subfacval2  24865  subfaclim  24866  fprodefsum  25290  brcgr  25831  axlowdimlem16  25888  bpolydiflem  26092  mettrifi  26454  rrncmslem  26532  stoweidlem17  27733  stoweidlem20  27736  stirlinglem12  27801
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ral 2702  df-rex 2703  df-rab 2706  df-v 2950  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815  df-uni 4008  df-br 4205  df-opab 4259  df-mpt 4260  df-cnv 4878  df-dm 4880  df-rn 4881  df-res 4882  df-ima 4883  df-iota 5410  df-f 5450  df-f1 5451  df-fo 5452  df-f1o 5453  df-fv 5454  df-ov 6076  df-oprab 6077  df-mpt2 6078  df-recs 6625  df-rdg 6660  df-seq 11316  df-sum 12472
  Copyright terms: Public domain W3C validator