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

Theorem sumeq2dv 15050
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 3182 . 2 (𝜑 → ∀𝑘𝐴 𝐵 = 𝐶)
32sumeq2d 15049 1 (𝜑 → Σ𝑘𝐴 𝐵 = Σ𝑘𝐴 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1528  wcel 2105  Σcsu 15032
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7450  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 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-fal 1541  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3497  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-pss 3953  df-nul 4291  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  df-uni 4833  df-iun 4914  df-br 5059  df-opab 5121  df-mpt 5139  df-tr 5165  df-id 5454  df-eprel 5459  df-po 5468  df-so 5469  df-fr 5508  df-we 5510  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-pred 6142  df-ord 6188  df-on 6189  df-lim 6190  df-suc 6191  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-om 7569  df-1st 7680  df-2nd 7681  df-wrecs 7938  df-recs 7999  df-rdg 8037  df-er 8279  df-en 8499  df-dom 8500  df-sdom 8501  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-nn 11628  df-n0 11887  df-z 11971  df-uz 12233  df-fz 12883  df-seq 13360  df-sum 15033
This theorem is referenced by:  2sumeq2dv  15052  sumeq12dv  15053  sumeq12rdv  15054  fsumf1o  15070  fsumss  15072  fsumsplit  15087  isummulc1  15108  isumdivc  15109  isumge0  15111  fsum2dlem  15115  fsumshftm  15126  fsum0diag2  15128  fsummulc1  15130  fsumdivc  15131  fsumneg  15132  fsumsub  15133  fsum2mul  15134  telfsumo2  15148  fsumparts  15151  hashiun  15167  hash2iun  15168  hash2iun1dif1  15169  ackbijnn  15173  binomlem  15174  binom1p  15176  incexclem  15181  incexc  15182  incexc2  15183  isum1p  15186  arisum  15205  trireciplem  15207  geoserg  15211  pwdif  15213  geo2sum  15219  mertenslem1  15230  mertenslem2  15231  mertens  15232  binomfallfaclem2  15384  binomrisefac  15386  bpolylem  15392  bpolydiflem  15398  fsumkthpow  15400  efaddlem  15436  rpnnen2lem10  15566  rpnnen2lem11  15567  fsumdvds  15648  pwp1fsum  15732  phisum  16117  pcfac  16225  ramcl  16355  lagsubg2  18281  sylow2a  18675  rrxcph  23924  trirn  23932  rrxmval  23937  rrxmet  23940  ovoliunnul  24037  ovolicc2lem4  24050  uniioombllem4  24116  vitalilem5  24142  itg1addlem4  24229  itg1addlem5  24230  itg1mulc  24234  itg10a  24240  itg1climres  24244  itgss  24341  itgeqa  24343  itgsplit  24365  elply2  24715  elplyd  24721  plyeq0lem  24729  plyaddlem1  24732  plymullem1  24733  coeeulem  24743  coeeq2  24761  coemullem  24769  coe1termlem  24777  plycjlem  24795  plyrecj  24798  dvply1  24802  elqaalem3  24839  aareccl  24844  aannenlem1  24846  taylpval  24884  dvtaylp  24887  pserdvlem2  24945  pserdv2  24947  abelthlem8  24956  abelthlem9  24957  abelth  24958  logtayl  25170  leibpi  25448  birthdaylem2  25458  amgmlem  25495  emcllem5  25505  fsumharmonic  25517  lgamcvg2  25560  ftalem5  25582  basellem3  25588  basellem8  25593  sgmval2  25648  fsumdvdscom  25690  dvdsflsumcom  25693  musum  25696  musumsum  25697  muinv  25698  fsumdvdsmul  25700  sgmppw  25701  1sgmprm  25703  chtlepsi  25710  pclogsum  25719  vmasum  25720  logfac2  25721  chpval2  25722  chpchtsum  25723  logexprlim  25729  logfacrlim2  25730  perfectlem2  25734  dchrsum2  25772  sumdchr2  25774  dchrhash  25775  dchr2sum  25777  sum2dchr  25778  pcbcctr  25780  bposlem2  25789  lgsquadlem1  25884  lgsquadlem2  25885  chebbnd1lem1  25973  rplogsumlem1  25988  rplogsumlem2  25989  rpvmasumlem  25991  dchrisumlem1  25993  dchrisumlem2  25994  dchrmusum2  25998  dchrvmasumlem1  25999  dchrvmasum2lem  26000  dchrvmasum2if  26001  dchrvmasumiflem1  26005  dchrvmasumiflem2  26006  dchrisum0flblem1  26012  dchrisum0fno1  26015  rpvmasum2  26016  dchrisum0lem2a  26021  dchrisum0lem2  26022  dchrisum0lem3  26023  dchrisum0  26024  rplogsum  26031  mudivsum  26034  mulogsumlem  26035  mulogsum  26036  mulog2sumlem1  26038  mulog2sumlem2  26039  mulog2sumlem3  26040  vmalogdivsum2  26042  vmalogdivsum  26043  2vmadivsumlem  26044  logsqvma  26046  logsqvma2  26047  selberglem1  26049  selberglem2  26050  selberg  26052  selberg2  26055  selberg3lem1  26061  selberg4lem1  26064  selberg4  26065  pntrsumo1  26069  selbergr  26072  selberg3r  26073  selberg4r  26074  selberg34r  26075  pntsval2  26080  pntrlog2bndlem4  26084  pntrlog2bndlem5  26085  pntpbnd1  26090  pntlemk  26110  pntlemo  26111  axcgrrflx  26628  axcgrid  26630  axsegconlem1  26631  axsegconlem9  26639  ax5seglem1  26642  ax5seglem2  26643  ax5seglem9  26651  axlowdimlem16  26671  axlowdimlem17  26672  ecgrtg  26697  finsumvtxdg2ssteplem3  27257  rusgrnumwwlks  27681  fusgrhashclwwlkn  27786  fusgreghash2wsp  28045  numclwwlk6  28097  indsum  31180  indsumin  31181  eulerpartlemsv1  31514  eulerpartlemsf  31517  eulerpartlemgs2  31538  eulerpartlemn  31539  plymulx0  31717  signsvfn  31752  fsum2dsub  31778  reprsuc  31786  hashreprin  31791  reprpmtf1o  31797  breprexplema  31801  breprexplemc  31803  breprexp  31804  breprexpnat  31805  vtsprod  31810  circlemeth  31811  circlemethnat  31812  circlevma  31813  circlemethhgt  31814  hgt750lemd  31819  hgt750lemb  31827  hgt750lema  31828  subfaclim  32333  fwddifnp1  33524  knoppndvlem6  33754  rrnmet  34990  fltnltalem  39154  jm2.22  39472  jm2.23  39473  flcidc  39654  binomcxplemnn0  40561  binomcxplemdvsum  40567  binomcxplemnotnn0  40568  mccllem  41758  isumneg  41763  sumnnodd  41791  dvnmul  42108  dvnprodlem2  42112  dvnprodlem3  42113  stoweidlem37  42203  dirkertrigeqlem2  42265  dirkertrigeqlem3  42266  fourierdlem81  42353  fourierdlem83  42355  fourierdlem93  42365  fourierdlem103  42375  fourierdlem104  42376  elaa2lem  42399  etransclem23  42423  etransclem24  42424  etransclem31  42431  etransclem32  42432  etransclem35  42435  etransclem46  42446  rrxtopnfi  42453  rrndistlt  42456  sge0z  42538  sge0fsummpt  42553  sge0sup  42554  sge0resplit  42569  sge0split  42572  sge0ltfirpmpt2  42589  omeiunltfirp  42682  carageniuncllem2  42685  hoidmvlelem2  42759  hoidmvlelem3  42760  perfectALTVlem2  43734  nnsum3primesprm  43802  nnsum3primesgbe  43804  nnsum4primeseven  43812  altgsumbc  44298  altgsumbcALT  44299  nn0sumshdiglemA  44577  nn0sumshdiglemB  44578  nn0sumshdig  44581  aacllem  44800  amgmwlem  44801
  Copyright terms: Public domain W3C validator