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

Theorem sumeq2dv 15299
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 3108 . 2 (𝜑 → ∀𝑘𝐴 𝐵 = 𝐶)
32sumeq2d 15298 1 (𝜑 → Σ𝑘𝐴 𝐵 = Σ𝑘𝐴 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399   = wceq 1543  wcel 2112  Σcsu 15281
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2710  ax-sep 5208  ax-nul 5215  ax-pow 5274  ax-pr 5338  ax-un 7544  ax-cnex 10814  ax-resscn 10815  ax-1cn 10816  ax-icn 10817  ax-addcl 10818  ax-addrcl 10819  ax-mulcl 10820  ax-mulrcl 10821  ax-mulcom 10822  ax-addass 10823  ax-mulass 10824  ax-distr 10825  ax-i2m1 10826  ax-1ne0 10827  ax-1rid 10828  ax-rnegex 10829  ax-rrecex 10830  ax-cnre 10831  ax-pre-lttri 10832  ax-pre-lttrn 10833  ax-pre-ltadd 10834  ax-pre-mulgt0 10835
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2818  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-reu 3071  df-rab 3073  df-v 3425  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4456  df-pw 4531  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4836  df-iun 4922  df-br 5070  df-opab 5132  df-mpt 5152  df-tr 5178  df-id 5471  df-eprel 5477  df-po 5485  df-so 5486  df-fr 5526  df-we 5528  df-xp 5574  df-rel 5575  df-cnv 5576  df-co 5577  df-dm 5578  df-rn 5579  df-res 5580  df-ima 5581  df-pred 6178  df-ord 6236  df-on 6237  df-lim 6238  df-suc 6239  df-iota 6358  df-fun 6402  df-fn 6403  df-f 6404  df-f1 6405  df-fo 6406  df-f1o 6407  df-fv 6408  df-riota 7191  df-ov 7237  df-oprab 7238  df-mpo 7239  df-om 7666  df-1st 7782  df-2nd 7783  df-wrecs 8070  df-recs 8131  df-rdg 8169  df-er 8414  df-en 8650  df-dom 8651  df-sdom 8652  df-pnf 10898  df-mnf 10899  df-xr 10900  df-ltxr 10901  df-le 10902  df-sub 11093  df-neg 11094  df-nn 11860  df-n0 12120  df-z 12206  df-uz 12468  df-fz 13125  df-seq 13606  df-sum 15282
This theorem is referenced by:  2sumeq2dv  15301  sumeq12dv  15302  sumeq12rdv  15303  fsumf1o  15319  fsumss  15321  fsumsplit  15337  isummulc1  15359  isumdivc  15360  isumge0  15362  fsum2dlem  15366  fsumshftm  15377  fsum0diag2  15379  fsummulc1  15381  fsumdivc  15382  fsumneg  15383  fsumsub  15384  fsum2mul  15385  telfsumo2  15399  fsumparts  15402  hashiun  15418  hash2iun  15419  hash2iun1dif1  15420  ackbijnn  15424  binomlem  15425  binom1p  15427  incexclem  15432  incexc  15433  incexc2  15434  isum1p  15437  arisum  15456  trireciplem  15458  geoserg  15462  pwdif  15464  geo2sum  15469  mertenslem1  15480  mertenslem2  15481  mertens  15482  binomfallfaclem2  15634  binomrisefac  15636  bpolylem  15642  bpolydiflem  15648  fsumkthpow  15650  efaddlem  15686  rpnnen2lem10  15816  rpnnen2lem11  15817  fsumdvds  15901  pwp1fsum  15984  phisum  16375  pcfac  16484  ramcl  16614  lagsubg2  18637  sylow2a  19040  rrxcph  24320  trirn  24328  rrxmval  24333  rrxmet  24336  ovoliunnul  24435  ovolicc2lem4  24448  uniioombllem4  24514  vitalilem5  24540  itg1addlem4  24627  itg1addlem4OLD  24628  itg1addlem5  24629  itg1mulc  24633  itg10a  24639  itg1climres  24643  itgss  24740  itgeqa  24742  itgsplit  24764  elply2  25121  elplyd  25127  plyeq0lem  25135  plyaddlem1  25138  plymullem1  25139  coeeulem  25149  coeeq2  25167  coemullem  25175  coe1termlem  25183  plycjlem  25201  plyrecj  25204  dvply1  25208  elqaalem3  25245  aareccl  25250  aannenlem1  25252  taylpval  25290  dvtaylp  25293  pserdvlem2  25351  pserdv2  25353  abelthlem8  25362  abelthlem9  25363  abelth  25364  logtayl  25579  leibpi  25856  birthdaylem2  25866  amgmlem  25903  emcllem5  25913  fsumharmonic  25925  lgamcvg2  25968  ftalem5  25990  basellem3  25996  basellem8  26001  sgmval2  26056  fsumdvdscom  26098  dvdsflsumcom  26101  musum  26104  musumsum  26105  muinv  26106  fsumdvdsmul  26108  sgmppw  26109  1sgmprm  26111  chtlepsi  26118  pclogsum  26127  vmasum  26128  logfac2  26129  chpval2  26130  chpchtsum  26131  logexprlim  26137  logfacrlim2  26138  perfectlem2  26142  dchrsum2  26180  sumdchr2  26182  dchrhash  26183  dchr2sum  26185  sum2dchr  26186  pcbcctr  26188  bposlem2  26197  lgsquadlem1  26292  lgsquadlem2  26293  chebbnd1lem1  26381  rplogsumlem1  26396  rplogsumlem2  26397  rpvmasumlem  26399  dchrisumlem1  26401  dchrisumlem2  26402  dchrmusum2  26406  dchrvmasumlem1  26407  dchrvmasum2lem  26408  dchrvmasum2if  26409  dchrvmasumiflem1  26413  dchrvmasumiflem2  26414  dchrisum0flblem1  26420  dchrisum0fno1  26423  rpvmasum2  26424  dchrisum0lem2a  26429  dchrisum0lem2  26430  dchrisum0lem3  26431  dchrisum0  26432  rplogsum  26439  mudivsum  26442  mulogsumlem  26443  mulogsum  26444  mulog2sumlem1  26446  mulog2sumlem2  26447  mulog2sumlem3  26448  vmalogdivsum2  26450  vmalogdivsum  26451  2vmadivsumlem  26452  logsqvma  26454  logsqvma2  26455  selberglem1  26457  selberglem2  26458  selberg  26460  selberg2  26463  selberg3lem1  26469  selberg4lem1  26472  selberg4  26473  pntrsumo1  26477  selbergr  26480  selberg3r  26481  selberg4r  26482  selberg34r  26483  pntsval2  26488  pntrlog2bndlem4  26492  pntrlog2bndlem5  26493  pntpbnd1  26498  pntlemk  26518  pntlemo  26519  axcgrrflx  27036  axcgrid  27038  axsegconlem1  27039  axsegconlem9  27047  ax5seglem1  27050  ax5seglem2  27051  ax5seglem9  27059  axlowdimlem16  27079  axlowdimlem17  27080  ecgrtg  27105  finsumvtxdg2ssteplem3  27666  rusgrnumwwlks  28089  fusgrhashclwwlkn  28193  fusgreghash2wsp  28452  numclwwlk6  28504  indsum  31732  indsumin  31733  eulerpartlemsv1  32066  eulerpartlemsf  32069  eulerpartlemgs2  32090  eulerpartlemn  32091  plymulx0  32269  signsvfn  32304  fsum2dsub  32330  reprsuc  32338  hashreprin  32343  reprpmtf1o  32349  breprexplema  32353  breprexplemc  32355  breprexp  32356  breprexpnat  32357  vtsprod  32362  circlemeth  32363  circlemethnat  32364  circlevma  32365  circlemethhgt  32366  hgt750lemd  32371  hgt750lemb  32379  hgt750lema  32380  subfaclim  32893  fwddifnp1  34237  knoppndvlem6  34467  rrnmet  35760  3factsumint2  39800  3factsumint3  39801  lcmineqlem1  39807  lcmineqlem3  39809  lcmineqlem6  39812  sticksstones8  39872  sticksstones9  39873  sticksstones10  39874  sticksstones11  39875  sticksstones12a  39876  sticksstones12  39877  sticksstones17  39882  sticksstones18  39883  sticksstones19  39884  fltnltalem  40249  jm2.22  40567  jm2.23  40568  flcidc  40749  binomcxplemnn0  41687  binomcxplemdvsum  41693  binomcxplemnotnn0  41694  mccllem  42858  isumneg  42863  sumnnodd  42891  dvnmul  43204  dvnprodlem2  43208  dvnprodlem3  43209  stoweidlem37  43298  dirkertrigeqlem2  43360  dirkertrigeqlem3  43361  fourierdlem81  43448  fourierdlem83  43450  fourierdlem93  43460  fourierdlem103  43470  fourierdlem104  43471  elaa2lem  43494  etransclem23  43518  etransclem24  43519  etransclem31  43526  etransclem32  43527  etransclem35  43530  etransclem46  43541  rrxtopnfi  43548  rrndistlt  43551  sge0z  43633  sge0fsummpt  43648  sge0sup  43649  sge0resplit  43664  sge0split  43667  sge0ltfirpmpt2  43684  omeiunltfirp  43777  carageniuncllem2  43780  hoidmvlelem2  43854  hoidmvlelem3  43855  perfectALTVlem2  44892  nnsum3primesprm  44960  nnsum3primesgbe  44962  nnsum4primeseven  44970  altgsumbc  45406  altgsumbcALT  45407  nn0sumshdiglemA  45683  nn0sumshdiglemB  45684  nn0sumshdig  45687  aacllem  46221  amgmwlem  46222
  Copyright terms: Public domain W3C validator