MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cbvsumv Structured version   Visualization version   GIF version

Theorem cbvsumv 14625
Description: Change bound variable in a sum. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jul-2013.)
Hypothesis
Ref Expression
cbvsum.1 (𝑗 = 𝑘𝐵 = 𝐶)
Assertion
Ref Expression
cbvsumv Σ𝑗𝐴 𝐵 = Σ𝑘𝐴 𝐶
Distinct variable groups:   𝑗,𝑘,𝐴   𝐵,𝑘   𝐶,𝑗
Allowed substitution hints:   𝐵(𝑗)   𝐶(𝑘)

Proof of Theorem cbvsumv
StepHypRef Expression
1 cbvsum.1 . 2 (𝑗 = 𝑘𝐵 = 𝐶)
2 nfcv 2902 . 2 𝑘𝐴
3 nfcv 2902 . 2 𝑗𝐴
4 nfcv 2902 . 2 𝑘𝐵
5 nfcv 2902 . 2 𝑗𝐶
61, 2, 3, 4, 5cbvsum 14624 1 Σ𝑗𝐴 𝐵 = Σ𝑘𝐴 𝐶
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1632  Σcsu 14615
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-opab 4865  df-mpt 4882  df-xp 5272  df-cnv 5274  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-iota 6012  df-fv 6057  df-ov 6816  df-oprab 6817  df-mpt2 6818  df-wrecs 7576  df-recs 7637  df-rdg 7675  df-seq 12996  df-sum 14616
This theorem is referenced by:  isumge0  14696  telfsumo  14733  fsumparts  14737  binomlem  14760  incexclem  14767  mertenslem1  14815  mertens  14817  binomfallfaclem2  14970  bpolyval  14979  efaddlem  15022  pwp1fsum  15316  bitsinv2  15367  prmreclem6  15827  ovolicc2lem4  23488  uniioombllem6  23556  plymullem1  24169  plyadd  24172  plymul  24173  coeeu  24180  coeid  24193  dvply1  24238  vieta1  24266  aaliou3  24305  abelthlem8  24392  abelthlem9  24393  abelth  24394  logtayl  24605  ftalem2  24999  ftalem6  25003  dchrsum2  25192  sumdchr2  25194  dchrisumlem1  25377  dchrisum  25380  dchrisum0fval  25393  dchrisum0ff  25395  rpvmasum  25414  mulog2sumlem1  25422  2vmadivsumlem  25428  logsqvma  25430  logsqvma2  25431  selberg  25436  chpdifbndlem1  25441  selberg3lem1  25445  selberg4lem1  25448  pntsval  25460  pntsval2  25464  pntpbnd1  25474  pntlemo  25495  axsegconlem9  26004  hashunif  29871  eulerpartlems  30731  eulerpartlemgs2  30751  breprexplema  31017  breprexplemc  31019  breprexp  31020  hgt750lema  31044  fwddifnp1  32578  binomcxplemnotnn0  39057  mccl  40333  sumnnodd  40365  dvnprodlem1  40664  dvnprodlem3  40666  dvnprod  40667  fourierdlem73  40899  fourierdlem112  40938  fourierdlem113  40939  etransclem11  40965  etransclem32  40986  etransclem35  40989  etransc  41003  fsumlesge0  41097  meaiuninclem  41200  omeiunltfirp  41239  hoidmvlelem3  41317  pwdif  42011  altgsumbcALT  42641  nn0sumshdiglemA  42923  nn0sumshdiglemB  42924
  Copyright terms: Public domain W3C validator