MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sumex Structured version   Unicode version

Theorem sumex 13747
Description: A sum is a set. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.)
Assertion
Ref Expression
sumex  |-  sum_ k  e.  A  B  e.  _V

Proof of Theorem sumex
Dummy variables  f  m  n  x are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-sum 13746 . 2  |-  sum_ k  e.  A  B  =  ( iota x ( E. m  e.  ZZ  ( A  C_  ( ZZ>= `  m
)  /\  seq m
(  +  ,  ( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) ) )  ~~>  x )  \/  E. m  e.  NN  E. f ( f : ( 1 ... m ) -1-1-onto-> A  /\  x  =  (  seq 1 (  +  , 
( n  e.  NN  |->  [_ ( f `  n
)  /  k ]_ B ) ) `  m ) ) ) )
2 iotaex 5580 . 2  |-  ( iota
x ( E. m  e.  ZZ  ( A  C_  ( ZZ>= `  m )  /\  seq m (  +  ,  ( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) ) )  ~~>  x )  \/ 
E. m  e.  NN  E. f ( f : ( 1 ... m
)
-1-1-onto-> A  /\  x  =  (  seq 1 (  +  ,  ( n  e.  NN  |->  [_ ( f `  n )  /  k ]_ B ) ) `  m ) ) ) )  e.  _V
31, 2eqeltri 2507 1  |-  sum_ k  e.  A  B  e.  _V
Colors of variables: wff setvar class
Syntax hints:    \/ wo 370    /\ wa 371    = wceq 1438   E.wex 1660    e. wcel 1869   E.wrex 2777   _Vcvv 3082   [_csb 3396    C_ wss 3437   ifcif 3910   class class class wbr 4421    |-> cmpt 4480   iotacio 5561   -1-1-onto->wf1o 5598   ` cfv 5599  (class class class)co 6303   0cc0 9541   1c1 9542    + caddc 9544   NNcn 10611   ZZcz 10939   ZZ>=cuz 11161   ...cfz 11786    seqcseq 12214    ~~> cli 13541   sum_csu 13745
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-nul 4553
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-eu 2270  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-ral 2781  df-rex 2782  df-v 3084  df-sbc 3301  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-nul 3763  df-sn 3998  df-pr 4000  df-uni 4218  df-iota 5563  df-sum 13746
This theorem is referenced by:  fsumrlim  13864  fsumo1  13865  efval  14127  efcvgfsum  14133  eftlub  14156  bitsinv2  14410  bitsinv  14415  lebnumlem3  21983  lebnumlem3OLD  21986  isi1f  22624  itg1val  22633  itg1climres  22664  itgex  22720  itgfsum  22776  dvmptfsum  22919  plyeq0lem  23156  plyaddlem1  23159  plymullem1  23160  coeeulem  23170  coeid2  23185  plyco  23187  coemullem  23196  coemul  23198  aareccl  23274  aaliou3lem5  23295  aaliou3lem6  23296  aaliou3lem7  23297  taylpval  23314  psercn  23373  pserdvlem2  23375  pserdv  23376  abelthlem6  23383  abelthlem8  23386  abelthlem9  23387  logtayl  23597  leibpi  23860  basellem3  24001  chtval  24029  chpval  24041  sgmval  24061  muinv  24114  dchrvmasumlem1  24325  dchrisum0fval  24335  dchrisum0fno1  24341  dchrisum0lem3  24349  dchrisum0  24350  mulogsum  24362  logsqvma2  24373  selberglem1  24375  pntsval  24402  ecgrtg  25005  esumpcvgval  28901  esumcvg  28909  eulerpartlemsv1  29191  signsplypnf  29441  signsvvfval  29469  fwddifnval  30929  binomcxplemnotnn0  36607  stoweidlem11  37735  stoweidlem26  37750  fourierdlem112  37946  fsumlesge0  38051  sge0sn  38053  sge0f1o  38056  sge0supre  38063  sge0resplit  38080  aacllem  39884
  Copyright terms: Public domain W3C validator