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

Theorem sumeq1d 13295
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 13283 . 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 setvar class
Syntax hints:    -> wi 4    = wceq 1370   sum_csu 13280
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ral 2803  df-rex 2804  df-rab 2807  df-v 3078  df-dif 3438  df-un 3440  df-in 3442  df-ss 3449  df-nul 3745  df-if 3899  df-sn 3985  df-pr 3987  df-op 3991  df-uni 4199  df-br 4400  df-opab 4458  df-mpt 4459  df-cnv 4955  df-dm 4957  df-rn 4958  df-res 4959  df-ima 4960  df-iota 5488  df-f 5529  df-f1 5530  df-fo 5531  df-f1o 5532  df-fv 5533  df-ov 6202  df-oprab 6203  df-mpt2 6204  df-recs 6941  df-rdg 6975  df-seq 11923  df-sum 13281
This theorem is referenced by:  sumeq12dv  13300  sumeq12rdv  13301  fsumf1o  13317  sumss  13318  fsumcllem  13326  fsum1  13335  fzosump1  13338  fsump1  13340  fsum2d  13355  fsumcom2  13358  fsumshftm  13365  fsumrev2  13366  fsumtscopo  13382  fsumtscop  13384  fsumtscop2  13385  fsumparts  13386  fsumiun  13401  bcxmas  13415  incexclem  13416  incexc2  13418  isumsplit  13420  isum1p  13421  arisum  13439  arisum2  13440  geoser  13446  geolim  13447  geo2sum2  13451  mertenslem1  13461  mertenslem2  13462  mertens  13463  efcvgfsum  13488  eftlub  13510  effsumlt  13512  eirrlem  13603  bitsinv1  13755  bitsinvp1  13762  pcfac  14078  prmreclem4  14097  prmreclem6  14099  ovoliunlem1  21116  uniioombllem3  21197  itg11  21301  dvfsumlem1  21630  dvfsumlem4  21633  dvfsum2  21638  elplyr  21801  coeeu  21825  coeeq  21827  plyco  21841  0dgrb  21846  dvply2g  21883  vieta1lem2  21909  vieta1  21910  aaliou3lem5  21945  aaliou3lem6  21946  aaliou3lem7  21947  taylpfval  21962  pserdvlem2  22025  abelthlem6  22033  logfac  22181  advlogexp  22232  emcllem2  22522  emcllem3  22523  emcllem7  22527  harmonicbnd  22529  harmonicbnd2  22530  harmonicbnd3  22533  harmonicbnd4  22536  chtval  22580  chpval  22592  chtfl  22619  chpfl  22620  chtprm  22623  chtnprm  22624  chpp1  22625  chtdif  22628  prmorcht  22648  musum  22663  muinv  22665  logfaclbnd  22693  logfacbnd3  22694  logexprlim  22696  chtppilimlem1  22854  rplogsumlem2  22866  rpvmasumlem  22868  dchrisumlem1  22870  dchrisumlem2  22871  dchrisumlem3  22872  dchrisum  22873  dchrisum0fval  22886  dchrisum0ff  22888  dchrisum0flblem1  22889  dchrisum0lem2  22899  dchrisum0  22901  mulog2sumlem1  22915  2vmadivsumlem  22921  log2sumbnd  22925  logdivbnd  22937  selberg3lem1  22938  pntrsumbnd  22947  pntrsumbnd2  22948  pntrlog2bndlem1  22958  pntrlog2bndlem4  22961  pntpbnd1  22967  pntpbnd2  22968  pntlemf  22986  brcgr  23297  axlowdimlem16  23354  eengv  23376  eulerpartlemgs2  26906  signsvfn  27126  subfacval2  27218  subfaclim  27219  fprodefsum  27628  bpolydiflem  28340  mettrifi  28800  rrncmslem  28878  stoweidlem17  29959  stoweidlem20  29962  stirlinglem12  30027  altgsumbcALT  30897
  Copyright terms: Public domain W3C validator