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

Theorem sumeq1d 12416
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 12404 . 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 1649   sum_csu 12400
This theorem is referenced by:  sumeq12dv  12421  sumeq12rdv  12422  fsumf1o  12438  sumss  12439  fsumcllem  12447  fsum1  12456  fzosump1  12459  fsump1  12461  fsum2d  12476  fsumcom2  12479  fsumshftm  12485  fsumrev2  12486  fsumtscopo  12502  fsumtscop  12504  fsumtscop2  12505  fsumparts  12506  fsumiun  12521  bcxmas  12536  incexclem  12537  incexc2  12539  isumsplit  12541  isum1p  12542  arisum  12560  arisum2  12561  geoser  12567  geolim  12568  geo2sum2  12572  mertenslem1  12582  mertenslem2  12583  mertens  12584  efcvgfsum  12609  eftlub  12631  effsumlt  12633  eirrlem  12724  bitsinv1  12875  bitsinvp1  12882  pcfac  13189  prmreclem4  13208  prmreclem6  13210  ovoliunlem1  19259  uniioombllem3  19338  itg11  19444  dvfsumlem1  19771  dvfsumlem4  19774  dvfsum2  19779  elplyr  19981  coeeu  20005  coeeq  20007  plyco  20021  0dgrb  20026  dvply2g  20063  vieta1lem2  20089  vieta1  20090  aaliou3lem5  20125  aaliou3lem6  20126  aaliou3lem7  20127  taylpfval  20142  pserdvlem2  20205  abelthlem6  20213  logfac  20356  advlogexp  20407  emcllem2  20696  emcllem3  20697  emcllem7  20701  harmonicbnd  20703  harmonicbnd2  20704  harmonicbnd3  20707  harmonicbnd4  20710  chtval  20754  chpval  20766  chtfl  20793  chpfl  20794  chtprm  20797  chtnprm  20798  chpp1  20799  chtdif  20802  prmorcht  20822  musum  20837  muinv  20839  logfaclbnd  20867  logfacbnd3  20868  logexprlim  20870  chtppilimlem1  21028  rplogsumlem2  21040  rpvmasumlem  21042  dchrisumlem1  21044  dchrisumlem2  21045  dchrisumlem3  21046  dchrisum  21047  dchrisum0fval  21060  dchrisum0ff  21062  dchrisum0flblem1  21063  dchrisum0lem2  21073  dchrisum0  21075  mulog2sumlem1  21089  2vmadivsumlem  21095  log2sumbnd  21099  logdivbnd  21111  selberg3lem1  21112  pntrsumbnd  21121  pntrsumbnd2  21122  pntrlog2bndlem1  21132  pntrlog2bndlem4  21135  pntpbnd1  21141  pntpbnd2  21142  pntlemf  21160  subfacval2  24646  subfaclim  24647  fprodefsum  25071  brcgr  25547  axlowdimlem16  25604  bpolydiflem  25808  mettrifi  26148  rrncmslem  26226  stoweidlem17  27428  stoweidlem20  27431  stirlinglem12  27496
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2362
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2506  df-ral 2648  df-rex 2649  df-rab 2652  df-v 2895  df-dif 3260  df-un 3262  df-in 3264  df-ss 3271  df-nul 3566  df-if 3677  df-sn 3757  df-pr 3758  df-op 3760  df-uni 3952  df-br 4148  df-opab 4202  df-mpt 4203  df-cnv 4820  df-dm 4822  df-rn 4823  df-res 4824  df-ima 4825  df-iota 5352  df-f 5392  df-f1 5393  df-fo 5394  df-f1o 5395  df-fv 5396  df-ov 6017  df-oprab 6018  df-mpt2 6019  df-recs 6563  df-rdg 6598  df-seq 11245  df-sum 12401
  Copyright terms: Public domain W3C validator