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

Theorem sumeq1d 13745
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 13733 . 2  |-  ( A  =  B  ->  sum_ k  e.  A  C  =  sum_ k  e.  B  C
)
31, 2syl 17 1  |-  ( ph  -> 
sum_ k  e.  A  C  =  sum_ k  e.  B  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437   sum_csu 13730
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ral 2787  df-rex 2788  df-rab 2791  df-v 3089  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-sn 4003  df-pr 4005  df-op 4009  df-uni 4223  df-br 4427  df-opab 4485  df-mpt 4486  df-xp 4860  df-cnv 4862  df-dm 4864  df-rn 4865  df-res 4866  df-ima 4867  df-pred 5399  df-iota 5565  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-ov 6308  df-oprab 6309  df-mpt2 6310  df-wrecs 7036  df-recs 7098  df-rdg 7136  df-seq 12211  df-sum 13731
This theorem is referenced by:  sumeq12dv  13750  sumeq12rdv  13751  fsumf1o  13767  sumss  13768  fsumcllem  13776  fsum1  13786  fzosump1  13791  fsump1  13795  fsum2d  13810  fsumcom2  13813  fsumshftm  13820  fsumrev2  13821  telfsumo  13840  telfsum  13842  telfsum2  13843  fsumparts  13844  fsumiun  13859  bcxmas  13871  incexclem  13872  incexc2  13874  isumsplit  13876  isum1p  13877  arisum  13896  arisum2  13897  geoser  13903  geolim  13904  geo2sum2  13908  mertenslem1  13918  mertenslem2  13919  mertens  13920  bpolydiflem  14085  efcvgfsum  14118  fprodefsum  14127  eftlub  14141  effsumlt  14143  eirrlem  14234  bitsinv1  14390  bitsinvp1  14397  pcfac  14807  prmreclem4  14826  prmreclem6  14828  ovoliunlem1  22333  uniioombllem3  22420  itg11  22526  dvfsumlem1  22855  dvfsumlem4  22858  dvfsum2  22863  elplyr  23023  coeeu  23047  coeeq  23049  plyco  23063  0dgrb  23068  dvply2g  23106  vieta1lem2  23132  vieta1  23133  aaliou3lem5  23168  aaliou3lem6  23169  aaliou3lem7  23170  taylpfval  23185  pserdvlem2  23248  abelthlem6  23256  logfac  23415  advlogexp  23465  emcllem2  23787  emcllem3  23788  emcllem7  23792  harmonicbnd  23794  harmonicbnd2  23795  harmonicbnd3  23798  harmonicbnd4  23801  chtval  23900  chpval  23912  chtfl  23939  chpfl  23940  chtprm  23943  chtnprm  23944  chpp1  23945  chtdif  23948  prmorcht  23968  musum  23983  muinv  23985  logfaclbnd  24013  logfacbnd3  24014  logexprlim  24016  chtppilimlem1  24174  rplogsumlem2  24186  rpvmasumlem  24188  dchrisumlem1  24190  dchrisumlem2  24191  dchrisumlem3  24192  dchrisum  24193  dchrisum0fval  24206  dchrisum0ff  24208  dchrisum0flblem1  24209  dchrisum0lem2  24219  dchrisum0  24221  mulog2sumlem1  24235  2vmadivsumlem  24241  log2sumbnd  24245  logdivbnd  24257  selberg3lem1  24258  pntrsumbnd  24267  pntrsumbnd2  24268  pntrlog2bndlem1  24278  pntrlog2bndlem4  24281  pntpbnd1  24287  pntpbnd2  24288  pntlemf  24306  brcgr  24776  axlowdimlem16  24833  eengv  24855  eulerpartlemgs2  29039  signsvfn  29259  subfacval2  29698  subfaclim  29699  bccolsum  30162  mettrifi  31790  rrncmslem  31868  binomcxplemnn0  36335  fsumnncl  37225  fsumsplit1  37226  fsumiunss  37229  sumnnodd  37282  dvnmul  37387  dvnprodlem3  37392  itgspltprt  37425  stoweidlem17  37446  stoweidlem20  37449  stirlinglem12  37516  dirkertrigeqlem1  37529  dirkertrigeqlem3  37531  fourierdlem83  37621  fourierdlem112  37650  fourierdlem113  37651  elaa2lem  37665  etransclem32  37698  sge00  37752  sge0iunmptlemre  37791  carageniuncllem1  37851  nnsum3primes4  38273  nnsum3primesprm  38275  nnsum3primesgbe  38277  nnsum4primesodd  38281  nnsum4primesoddALTV  38282  wtgoldbnnsum4prm  38287  bgoldbnnsum3prm  38289  altgsumbcALT  38894  nn0sumshdiglemA  39191  nn0sumshdiglemB  39192  nn0sumshdiglem1  39193  nn0sumshdiglem2  39194
  Copyright terms: Public domain W3C validator