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

Theorem sumeq1d 13486
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 13474 . 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 1379   sum_csu 13471
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-br 4448  df-opab 4506  df-mpt 4507  df-cnv 5007  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5551  df-f 5592  df-f1 5593  df-fo 5594  df-f1o 5595  df-fv 5596  df-ov 6287  df-oprab 6288  df-mpt2 6289  df-recs 7042  df-rdg 7076  df-seq 12076  df-sum 13472
This theorem is referenced by:  sumeq12dv  13491  sumeq12rdv  13492  fsumf1o  13508  sumss  13509  fsumcllem  13517  fsum1  13527  fzosump1  13530  fsump1  13534  fsum2d  13549  fsumcom2  13552  fsumshftm  13559  fsumrev2  13560  telfsumo  13579  telfsum  13581  telfsum2  13582  fsumparts  13583  fsumiun  13598  bcxmas  13610  incexclem  13611  incexc2  13613  isumsplit  13615  isum1p  13616  arisum  13634  arisum2  13635  geoser  13641  geolim  13642  geo2sum2  13646  mertenslem1  13656  mertenslem2  13657  mertens  13658  efcvgfsum  13683  eftlub  13705  effsumlt  13707  eirrlem  13798  bitsinv1  13951  bitsinvp1  13958  pcfac  14277  prmreclem4  14296  prmreclem6  14298  ovoliunlem1  21676  uniioombllem3  21757  itg11  21861  dvfsumlem1  22190  dvfsumlem4  22193  dvfsum2  22198  elplyr  22361  coeeu  22385  coeeq  22387  plyco  22401  0dgrb  22406  dvply2g  22443  vieta1lem2  22469  vieta1  22470  aaliou3lem5  22505  aaliou3lem6  22506  aaliou3lem7  22507  taylpfval  22522  pserdvlem2  22585  abelthlem6  22593  logfac  22741  advlogexp  22792  emcllem2  23082  emcllem3  23083  emcllem7  23087  harmonicbnd  23089  harmonicbnd2  23090  harmonicbnd3  23093  harmonicbnd4  23096  chtval  23140  chpval  23152  chtfl  23179  chpfl  23180  chtprm  23183  chtnprm  23184  chpp1  23185  chtdif  23188  prmorcht  23208  musum  23223  muinv  23225  logfaclbnd  23253  logfacbnd3  23254  logexprlim  23256  chtppilimlem1  23414  rplogsumlem2  23426  rpvmasumlem  23428  dchrisumlem1  23430  dchrisumlem2  23431  dchrisumlem3  23432  dchrisum  23433  dchrisum0fval  23446  dchrisum0ff  23448  dchrisum0flblem1  23449  dchrisum0lem2  23459  dchrisum0  23461  mulog2sumlem1  23475  2vmadivsumlem  23481  log2sumbnd  23485  logdivbnd  23497  selberg3lem1  23498  pntrsumbnd  23507  pntrsumbnd2  23508  pntrlog2bndlem1  23518  pntrlog2bndlem4  23521  pntpbnd1  23527  pntpbnd2  23528  pntlemf  23546  brcgr  23907  axlowdimlem16  23964  eengv  23986  eulerpartlemgs2  27987  signsvfn  28207  subfacval2  28299  subfaclim  28300  fprodefsum  28709  bpolydiflem  29421  mettrifi  29881  rrncmslem  29959  sumnnodd  31200  itgspltprt  31325  stoweidlem17  31345  stoweidlem20  31348  stirlinglem12  31413  dirkertrigeqlem1  31426  dirkertrigeqlem3  31428  fourierdlem83  31518  fourierdlem112  31547  fourierdlem113  31548  altgsumbcALT  32038
  Copyright terms: Public domain W3C validator