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

Theorem sumeq2dv 15051
Description: Equality deduction for sum. (Contributed by NM, 3-Jan-2006.) (Revised by Mario Carneiro, 31-Jan-2014.)
Hypothesis
Ref Expression
sumeq2dv.1 ((𝜑𝑘𝐴) → 𝐵 = 𝐶)
Assertion
Ref Expression
sumeq2dv (𝜑 → Σ𝑘𝐴 𝐵 = Σ𝑘𝐴 𝐶)
Distinct variable groups:   𝐴,𝑘   𝜑,𝑘
Allowed substitution hints:   𝐵(𝑘)   𝐶(𝑘)

Proof of Theorem sumeq2dv
StepHypRef Expression
1 sumeq2dv.1 . . 3 ((𝜑𝑘𝐴) → 𝐵 = 𝐶)
21ralrimiva 3174 . 2 (𝜑 → ∀𝑘𝐴 𝐵 = 𝐶)
32sumeq2d 15050 1 (𝜑 → Σ𝑘𝐴 𝐵 = Σ𝑘𝐴 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399   = wceq 1538  wcel 2114  Σcsu 15033
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794  ax-sep 5179  ax-nul 5186  ax-pow 5243  ax-pr 5307  ax-un 7446  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-ne 3012  df-nel 3116  df-ral 3135  df-rex 3136  df-reu 3137  df-rab 3139  df-v 3471  df-sbc 3748  df-csb 3856  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3927  df-nul 4266  df-if 4440  df-pw 4513  df-sn 4540  df-pr 4542  df-tp 4544  df-op 4546  df-uni 4814  df-iun 4896  df-br 5043  df-opab 5105  df-mpt 5123  df-tr 5149  df-id 5437  df-eprel 5442  df-po 5451  df-so 5452  df-fr 5491  df-we 5493  df-xp 5538  df-rel 5539  df-cnv 5540  df-co 5541  df-dm 5542  df-rn 5543  df-res 5544  df-ima 5545  df-pred 6126  df-ord 6172  df-on 6173  df-lim 6174  df-suc 6175  df-iota 6293  df-fun 6336  df-fn 6337  df-f 6338  df-f1 6339  df-fo 6340  df-f1o 6341  df-fv 6342  df-riota 7098  df-ov 7143  df-oprab 7144  df-mpo 7145  df-om 7566  df-1st 7675  df-2nd 7676  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-er 8276  df-en 8497  df-dom 8498  df-sdom 8499  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-nn 11626  df-n0 11886  df-z 11970  df-uz 12232  df-fz 12886  df-seq 13365  df-sum 15034
This theorem is referenced by:  2sumeq2dv  15053  sumeq12dv  15054  sumeq12rdv  15055  fsumf1o  15071  fsumss  15073  fsumsplit  15088  isummulc1  15109  isumdivc  15110  isumge0  15112  fsum2dlem  15116  fsumshftm  15127  fsum0diag2  15129  fsummulc1  15131  fsumdivc  15132  fsumneg  15133  fsumsub  15134  fsum2mul  15135  telfsumo2  15149  fsumparts  15152  hashiun  15168  hash2iun  15169  hash2iun1dif1  15170  ackbijnn  15174  binomlem  15175  binom1p  15177  incexclem  15182  incexc  15183  incexc2  15184  isum1p  15187  arisum  15206  trireciplem  15208  geoserg  15212  pwdif  15214  geo2sum  15220  mertenslem1  15231  mertenslem2  15232  mertens  15233  binomfallfaclem2  15385  binomrisefac  15387  bpolylem  15393  bpolydiflem  15399  fsumkthpow  15401  efaddlem  15437  rpnnen2lem10  15567  rpnnen2lem11  15568  fsumdvds  15649  pwp1fsum  15731  phisum  16116  pcfac  16224  ramcl  16354  lagsubg2  18332  sylow2a  18735  rrxcph  23994  trirn  24002  rrxmval  24007  rrxmet  24010  ovoliunnul  24109  ovolicc2lem4  24122  uniioombllem4  24188  vitalilem5  24214  itg1addlem4  24301  itg1addlem5  24302  itg1mulc  24306  itg10a  24312  itg1climres  24316  itgss  24413  itgeqa  24415  itgsplit  24437  elply2  24791  elplyd  24797  plyeq0lem  24805  plyaddlem1  24808  plymullem1  24809  coeeulem  24819  coeeq2  24837  coemullem  24845  coe1termlem  24853  plycjlem  24871  plyrecj  24874  dvply1  24878  elqaalem3  24915  aareccl  24920  aannenlem1  24922  taylpval  24960  dvtaylp  24963  pserdvlem2  25021  pserdv2  25023  abelthlem8  25032  abelthlem9  25033  abelth  25034  logtayl  25249  leibpi  25526  birthdaylem2  25536  amgmlem  25573  emcllem5  25583  fsumharmonic  25595  lgamcvg2  25638  ftalem5  25660  basellem3  25666  basellem8  25671  sgmval2  25726  fsumdvdscom  25768  dvdsflsumcom  25771  musum  25774  musumsum  25775  muinv  25776  fsumdvdsmul  25778  sgmppw  25779  1sgmprm  25781  chtlepsi  25788  pclogsum  25797  vmasum  25798  logfac2  25799  chpval2  25800  chpchtsum  25801  logexprlim  25807  logfacrlim2  25808  perfectlem2  25812  dchrsum2  25850  sumdchr2  25852  dchrhash  25853  dchr2sum  25855  sum2dchr  25856  pcbcctr  25858  bposlem2  25867  lgsquadlem1  25962  lgsquadlem2  25963  chebbnd1lem1  26051  rplogsumlem1  26066  rplogsumlem2  26067  rpvmasumlem  26069  dchrisumlem1  26071  dchrisumlem2  26072  dchrmusum2  26076  dchrvmasumlem1  26077  dchrvmasum2lem  26078  dchrvmasum2if  26079  dchrvmasumiflem1  26083  dchrvmasumiflem2  26084  dchrisum0flblem1  26090  dchrisum0fno1  26093  rpvmasum2  26094  dchrisum0lem2a  26099  dchrisum0lem2  26100  dchrisum0lem3  26101  dchrisum0  26102  rplogsum  26109  mudivsum  26112  mulogsumlem  26113  mulogsum  26114  mulog2sumlem1  26116  mulog2sumlem2  26117  mulog2sumlem3  26118  vmalogdivsum2  26120  vmalogdivsum  26121  2vmadivsumlem  26122  logsqvma  26124  logsqvma2  26125  selberglem1  26127  selberglem2  26128  selberg  26130  selberg2  26133  selberg3lem1  26139  selberg4lem1  26142  selberg4  26143  pntrsumo1  26147  selbergr  26150  selberg3r  26151  selberg4r  26152  selberg34r  26153  pntsval2  26158  pntrlog2bndlem4  26162  pntrlog2bndlem5  26163  pntpbnd1  26168  pntlemk  26188  pntlemo  26189  axcgrrflx  26706  axcgrid  26708  axsegconlem1  26709  axsegconlem9  26717  ax5seglem1  26720  ax5seglem2  26721  ax5seglem9  26729  axlowdimlem16  26749  axlowdimlem17  26750  ecgrtg  26775  finsumvtxdg2ssteplem3  27335  rusgrnumwwlks  27758  fusgrhashclwwlkn  27862  fusgreghash2wsp  28121  numclwwlk6  28173  indsum  31354  indsumin  31355  eulerpartlemsv1  31688  eulerpartlemsf  31691  eulerpartlemgs2  31712  eulerpartlemn  31713  plymulx0  31891  signsvfn  31926  fsum2dsub  31952  reprsuc  31960  hashreprin  31965  reprpmtf1o  31971  breprexplema  31975  breprexplemc  31977  breprexp  31978  breprexpnat  31979  vtsprod  31984  circlemeth  31985  circlemethnat  31986  circlevma  31987  circlemethhgt  31988  hgt750lemd  31993  hgt750lemb  32001  hgt750lema  32002  subfaclim  32509  fwddifnp1  33700  knoppndvlem6  33930  rrnmet  35225  3factsumint2  39271  3factsumint3  39272  lcmineqlem1  39278  lcmineqlem3  39280  lcmineqlem6  39283  fltnltalem  39548  jm2.22  39866  jm2.23  39867  flcidc  40048  binomcxplemnn0  40987  binomcxplemdvsum  40993  binomcxplemnotnn0  40994  mccllem  42178  isumneg  42183  sumnnodd  42211  dvnmul  42524  dvnprodlem2  42528  dvnprodlem3  42529  stoweidlem37  42618  dirkertrigeqlem2  42680  dirkertrigeqlem3  42681  fourierdlem81  42768  fourierdlem83  42770  fourierdlem93  42780  fourierdlem103  42790  fourierdlem104  42791  elaa2lem  42814  etransclem23  42838  etransclem24  42839  etransclem31  42846  etransclem32  42847  etransclem35  42850  etransclem46  42861  rrxtopnfi  42868  rrndistlt  42871  sge0z  42953  sge0fsummpt  42968  sge0sup  42969  sge0resplit  42984  sge0split  42987  sge0ltfirpmpt2  43004  omeiunltfirp  43097  carageniuncllem2  43100  hoidmvlelem2  43174  hoidmvlelem3  43175  perfectALTVlem2  44179  nnsum3primesprm  44247  nnsum3primesgbe  44249  nnsum4primeseven  44257  altgsumbc  44693  altgsumbcALT  44694  nn0sumshdiglemA  44972  nn0sumshdiglemB  44973  nn0sumshdig  44976  aacllem  45268  amgmwlem  45269
  Copyright terms: Public domain W3C validator