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

Theorem sumeq2dv 14659
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 3161 . 2 (𝜑 → ∀𝑘𝐴 𝐵 = 𝐶)
32sumeq2d 14658 1 (𝜑 → Σ𝑘𝐴 𝐵 = Σ𝑘𝐴 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1637  wcel 2157  Σcsu 14642
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2791  ax-sep 4982  ax-nul 4990  ax-pow 5042  ax-pr 5103  ax-un 7182  ax-cnex 10280  ax-resscn 10281  ax-1cn 10282  ax-icn 10283  ax-addcl 10284  ax-addrcl 10285  ax-mulcl 10286  ax-mulrcl 10287  ax-mulcom 10288  ax-addass 10289  ax-mulass 10290  ax-distr 10291  ax-i2m1 10292  ax-1ne0 10293  ax-1rid 10294  ax-rnegex 10295  ax-rrecex 10296  ax-cnre 10297  ax-pre-lttri 10298  ax-pre-lttrn 10299  ax-pre-ltadd 10300  ax-pre-mulgt0 10301
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-fal 1651  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2638  df-clab 2800  df-cleq 2806  df-clel 2809  df-nfc 2944  df-ne 2986  df-nel 3089  df-ral 3108  df-rex 3109  df-reu 3110  df-rab 3112  df-v 3400  df-sbc 3641  df-csb 3736  df-dif 3779  df-un 3781  df-in 3783  df-ss 3790  df-pss 3792  df-nul 4124  df-if 4287  df-pw 4360  df-sn 4378  df-pr 4380  df-tp 4382  df-op 4384  df-uni 4638  df-iun 4721  df-br 4852  df-opab 4914  df-mpt 4931  df-tr 4954  df-id 5226  df-eprel 5231  df-po 5239  df-so 5240  df-fr 5277  df-we 5279  df-xp 5324  df-rel 5325  df-cnv 5326  df-co 5327  df-dm 5328  df-rn 5329  df-res 5330  df-ima 5331  df-pred 5900  df-ord 5946  df-on 5947  df-lim 5948  df-suc 5949  df-iota 6067  df-fun 6106  df-fn 6107  df-f 6108  df-f1 6109  df-fo 6110  df-f1o 6111  df-fv 6112  df-riota 6838  df-ov 6880  df-oprab 6881  df-mpt2 6882  df-om 7299  df-1st 7401  df-2nd 7402  df-wrecs 7645  df-recs 7707  df-rdg 7745  df-er 7982  df-en 8196  df-dom 8197  df-sdom 8198  df-pnf 10364  df-mnf 10365  df-xr 10366  df-ltxr 10367  df-le 10368  df-sub 10556  df-neg 10557  df-nn 11309  df-n0 11563  df-z 11647  df-uz 11908  df-fz 12553  df-seq 13028  df-sum 14643
This theorem is referenced by:  sumeq2sdv  14661  2sumeq2dv  14662  sumeq12dv  14663  sumeq12rdv  14664  fsumf1o  14680  fsumss  14682  fsumsplit  14697  isummulc1  14720  isumdivc  14721  isumge0  14723  fsum2dlem  14727  fsumshftm  14738  fsum0diag2  14740  fsummulc1  14742  fsumdivc  14743  fsumneg  14744  fsumsub  14745  fsum2mul  14746  telfsumo2  14760  fsumparts  14763  hashiun  14779  hash2iun  14780  hash2iun1dif1  14781  ackbijnn  14785  binomlem  14786  binom1p  14788  incexclem  14793  incexc  14794  incexc2  14795  isum1p  14798  arisum  14817  trireciplem  14819  geoserg  14823  geo2sum  14829  mertenslem1  14840  mertenslem2  14841  mertens  14842  binomfallfaclem2  14994  binomrisefac  14996  bpolylem  15002  bpolydiflem  15008  fsumkthpow  15010  efaddlem  15046  rpnnen2lem10  15175  rpnnen2lem11  15176  fsumdvds  15256  pwp1fsum  15337  phisum  15715  pcfac  15823  ramcl  15953  lagsubg2  17860  sylow2a  18238  rrxcph  23398  trirn  23401  rrxmval  23406  rrxmet  23409  ovoliunnul  23494  ovolicc2lem4  23507  uniioombllem4  23573  vitalilem5  23599  itg1addlem4  23686  itg1addlem5  23687  itg1mulc  23691  itg10a  23697  itg1climres  23701  itgss  23798  itgeqa  23800  itgsplit  23822  elply2  24172  elplyd  24178  plyeq0lem  24186  plyaddlem1  24189  plymullem1  24190  coeeulem  24200  coeeq2  24218  coemullem  24226  coe1termlem  24234  plycjlem  24252  plyrecj  24255  dvply1  24259  elqaalem3  24296  aareccl  24301  aannenlem1  24303  taylpval  24341  dvtaylp  24344  pserdvlem2  24402  pserdv2  24404  abelthlem8  24413  abelthlem9  24414  abelth  24415  logtayl  24626  leibpi  24889  birthdaylem2  24899  amgmlem  24936  emcllem5  24946  fsumharmonic  24958  lgamcvg2  25001  ftalem5  25023  basellem3  25029  basellem8  25034  sgmval2  25089  fsumdvdscom  25131  dvdsflsumcom  25134  musum  25137  musumsum  25138  muinv  25139  fsumdvdsmul  25141  sgmppw  25142  1sgmprm  25144  chtlepsi  25151  pclogsum  25160  vmasum  25161  logfac2  25162  chpval2  25163  chpchtsum  25164  logexprlim  25170  logfacrlim2  25171  perfectlem2  25175  dchrsum2  25213  sumdchr2  25215  dchrhash  25216  dchr2sum  25218  sum2dchr  25219  pcbcctr  25221  bposlem2  25230  lgsquadlem1  25325  lgsquadlem2  25326  chebbnd1lem1  25378  rplogsumlem1  25393  rplogsumlem2  25394  rpvmasumlem  25396  dchrisumlem1  25398  dchrisumlem2  25399  dchrmusum2  25403  dchrvmasumlem1  25404  dchrvmasum2lem  25405  dchrvmasum2if  25406  dchrvmasumiflem1  25410  dchrvmasumiflem2  25411  dchrisum0flblem1  25417  dchrisum0fno1  25420  rpvmasum2  25421  dchrisum0lem2a  25426  dchrisum0lem2  25427  dchrisum0lem3  25428  dchrisum0  25429  rplogsum  25436  mudivsum  25439  mulogsumlem  25440  mulogsum  25441  mulog2sumlem1  25443  mulog2sumlem2  25444  mulog2sumlem3  25445  vmalogdivsum2  25447  vmalogdivsum  25448  2vmadivsumlem  25449  logsqvma  25451  logsqvma2  25452  selberglem1  25454  selberglem2  25455  selberg  25457  selberg2  25460  selberg3lem1  25466  selberg4lem1  25469  selberg4  25470  pntrsumo1  25474  selbergr  25477  selberg3r  25478  selberg4r  25479  selberg34r  25480  pntsval2  25485  pntrlog2bndlem4  25489  pntrlog2bndlem5  25490  pntpbnd1  25495  pntlemk  25515  pntlemo  25516  axcgrrflx  26014  axcgrid  26016  axsegconlem1  26017  axsegconlem9  26025  ax5seglem1  26028  ax5seglem2  26029  ax5seglem9  26037  axlowdimlem16  26057  axlowdimlem17  26058  ecgrtg  26083  finsumvtxdg2ssteplem3  26677  rusgrnumwwlks  27122  fusgrhashclwwlkn  27236  fusgreghash2wsp  27519  numclwwlk6  27584  indsum  30414  indsumin  30415  eulerpartlemsv1  30749  eulerpartlemsf  30752  eulerpartlemgs2  30773  eulerpartlemn  30774  plymulx0  30955  signsvfn  30990  fsum2dsub  31016  reprsuc  31024  hashreprin  31029  reprpmtf1o  31035  breprexplema  31039  breprexplemc  31041  breprexp  31042  breprexpnat  31043  vtsprod  31048  circlemeth  31049  circlemethnat  31050  circlevma  31051  circlemethhgt  31052  hgt750lemd  31057  hgt750lemb  31065  hgt750lema  31066  subfaclim  31498  fwddifnp1  32598  knoppndvlem6  32830  rrnmet  33941  jm2.22  38064  jm2.23  38065  flcidc  38246  binomcxplemnn0  39049  binomcxplemdvsum  39055  binomcxplemnotnn0  39056  mccllem  40310  isumneg  40315  sumnnodd  40343  dvnmul  40639  dvnprodlem2  40643  dvnprodlem3  40644  stoweidlem37  40734  dirkertrigeqlem2  40796  dirkertrigeqlem3  40797  fourierdlem81  40884  fourierdlem83  40886  fourierdlem93  40896  fourierdlem103  40906  fourierdlem104  40907  elaa2lem  40930  etransclem23  40954  etransclem24  40955  etransclem31  40962  etransclem32  40963  etransclem35  40966  etransclem46  40977  rrxtopnfi  40986  rrndistlt  40990  sge0z  41072  sge0fsummpt  41087  sge0sup  41088  sge0resplit  41103  sge0split  41106  sge0ltfirpmpt2  41123  omeiunltfirp  41216  carageniuncllem2  41219  hoidmvlelem2  41293  hoidmvlelem3  41294  pwdif  42077  perfectALTVlem2  42207  nnsum3primesprm  42254  nnsum3primesgbe  42256  nnsum4primeseven  42264  altgsumbc  42699  altgsumbcALT  42700  nn0sumshdiglemA  42982  nn0sumshdiglemB  42983  nn0sumshdig  42986  aacllem  43119  amgmwlem  43120
  Copyright terms: Public domain W3C validator