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

Theorem cbvsumv 14220
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 2750 . 2 𝑘𝐴
3 nfcv 2750 . 2 𝑗𝐴
4 nfcv 2750 . 2 𝑘𝐵
5 nfcv 2750 . 2 𝑗𝐶
61, 2, 3, 4, 5cbvsum 14219 1 Σ𝑗𝐴 𝐵 = Σ𝑘𝐴 𝐶
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  Σcsu 14210
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2232  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ral 2900  df-rex 2901  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-br 4578  df-opab 4638  df-mpt 4639  df-xp 5034  df-cnv 5036  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-iota 5754  df-fv 5798  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-wrecs 7271  df-recs 7332  df-rdg 7370  df-seq 12619  df-sum 14211
This theorem is referenced by:  isumge0  14285  telfsumo  14321  fsumparts  14325  binomlem  14346  incexclem  14353  mertenslem1  14401  mertens  14403  binomfallfaclem2  14556  bpolyval  14565  efaddlem  14608  pwp1fsum  14898  bitsinv2  14949  prmreclem6  15409  ovolicc2lem4  23012  uniioombllem6  23079  plymullem1  23691  plyadd  23694  plymul  23695  coeeu  23702  coeid  23715  dvply1  23760  vieta1  23788  aaliou3  23827  abelthlem8  23914  abelthlem9  23915  abelth  23916  logtayl  24123  ftalem2  24517  ftalem6  24521  dchrsum2  24710  sumdchr2  24712  dchrisumlem1  24895  dchrisum  24898  dchrisum0fval  24911  dchrisum0ff  24913  rpvmasum  24932  mulog2sumlem1  24940  2vmadivsumlem  24946  logsqvma  24948  logsqvma2  24949  selberg  24954  chpdifbndlem1  24959  selberg3lem1  24963  selberg4lem1  24966  pntsval  24978  pntsval2  24982  pntpbnd1  24992  pntlemo  25013  axsegconlem9  25523  hashunif  28755  eulerpartlems  29555  eulerpartlemgs2  29575  fwddifnp1  31248  binomcxplemnotnn0  37380  mccl  38469  sumnnodd  38501  dvnprodlem1  38640  dvnprodlem3  38642  dvnprod  38643  fourierdlem73  38876  fourierdlem112  38915  fourierdlem113  38916  etransclem11  38942  etransclem32  38963  etransclem35  38966  etransc  38980  fsumlesge0  39074  meaiuninclem  39177  omeiunltfirp  39213  hoidmvlelem3  39291  pwdif  39844  altgsumbcALT  41926  nn0sumshdiglemA  42213  nn0sumshdiglemB  42214
  Copyright terms: Public domain W3C validator