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

Theorem sumeq1d 13170
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 13158 . 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 1369   sum_csu 13155
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ral 2715  df-rex 2716  df-rab 2719  df-v 2969  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-br 4288  df-opab 4346  df-mpt 4347  df-cnv 4843  df-dm 4845  df-rn 4846  df-res 4847  df-ima 4848  df-iota 5376  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-ov 6089  df-oprab 6090  df-mpt2 6091  df-recs 6824  df-rdg 6858  df-seq 11799  df-sum 13156
This theorem is referenced by:  sumeq12dv  13175  sumeq12rdv  13176  fsumf1o  13192  sumss  13193  fsumcllem  13201  fsum1  13210  fzosump1  13213  fsump1  13215  fsum2d  13230  fsumcom2  13233  fsumshftm  13240  fsumrev2  13241  fsumtscopo  13257  fsumtscop  13259  fsumtscop2  13260  fsumparts  13261  fsumiun  13276  bcxmas  13290  incexclem  13291  incexc2  13293  isumsplit  13295  isum1p  13296  arisum  13314  arisum2  13315  geoser  13321  geolim  13322  geo2sum2  13326  mertenslem1  13336  mertenslem2  13337  mertens  13338  efcvgfsum  13363  eftlub  13385  effsumlt  13387  eirrlem  13478  bitsinv1  13630  bitsinvp1  13637  pcfac  13953  prmreclem4  13972  prmreclem6  13974  ovoliunlem1  20965  uniioombllem3  21045  itg11  21149  dvfsumlem1  21478  dvfsumlem4  21481  dvfsum2  21486  elplyr  21649  coeeu  21673  coeeq  21675  plyco  21689  0dgrb  21694  dvply2g  21731  vieta1lem2  21757  vieta1  21758  aaliou3lem5  21793  aaliou3lem6  21794  aaliou3lem7  21795  taylpfval  21810  pserdvlem2  21873  abelthlem6  21881  logfac  22029  advlogexp  22080  emcllem2  22370  emcllem3  22371  emcllem7  22375  harmonicbnd  22377  harmonicbnd2  22378  harmonicbnd3  22381  harmonicbnd4  22384  chtval  22428  chpval  22440  chtfl  22467  chpfl  22468  chtprm  22471  chtnprm  22472  chpp1  22473  chtdif  22476  prmorcht  22496  musum  22511  muinv  22513  logfaclbnd  22541  logfacbnd3  22542  logexprlim  22544  chtppilimlem1  22702  rplogsumlem2  22714  rpvmasumlem  22716  dchrisumlem1  22718  dchrisumlem2  22719  dchrisumlem3  22720  dchrisum  22721  dchrisum0fval  22734  dchrisum0ff  22736  dchrisum0flblem1  22737  dchrisum0lem2  22747  dchrisum0  22749  mulog2sumlem1  22763  2vmadivsumlem  22769  log2sumbnd  22773  logdivbnd  22785  selberg3lem1  22786  pntrsumbnd  22795  pntrsumbnd2  22796  pntrlog2bndlem1  22806  pntrlog2bndlem4  22809  pntpbnd1  22815  pntpbnd2  22816  pntlemf  22834  brcgr  23114  axlowdimlem16  23171  eengv  23193  eulerpartlemgs2  26732  signsvfn  26952  subfacval2  27044  subfaclim  27045  fprodefsum  27454  bpolydiflem  28166  mettrifi  28624  rrncmslem  28702  stoweidlem17  29783  stoweidlem20  29786  stirlinglem12  29851  altgsumbcALT  30719
  Copyright terms: Public domain W3C validator