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

Theorem sumex 12440
Description: A sum is a set. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jul-2013.)
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 12439 . 2  |-  sum_ k  e.  A  B  =  ( iota x ( E. m  e.  ZZ  ( A  C_  ( ZZ>= `  m
)  /\  seq  m (  +  ,  ( k  e.  ZZ  |->  if ( k  e.  A ,  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 5398 . 2  |-  ( iota
x ( E. m  e.  ZZ  ( A  C_  ( ZZ>= `  m )  /\  seq  m (  +  ,  ( k  e.  ZZ  |->  if ( k  e.  A ,  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 2478 1  |-  sum_ k  e.  A  B  e.  _V
Colors of variables: wff set class
Syntax hints:    \/ wo 358    /\ wa 359   E.wex 1547    = wceq 1649    e. wcel 1721   E.wrex 2671   _Vcvv 2920   [_csb 3215    C_ wss 3284   ifcif 3703   class class class wbr 4176    e. cmpt 4230   iotacio 5379   -1-1-onto->wf1o 5416   ` cfv 5417  (class class class)co 6044   0cc0 8950   1c1 8951    + caddc 8953   NNcn 9960   ZZcz 10242   ZZ>=cuz 10448   ...cfz 11003    seq cseq 11282    ~~> cli 12237   sum_csu 12438
This theorem is referenced by:  fsumrlim  12549  fsumo1  12550  efval  12641  efcvgfsum  12647  eftlub  12669  bitsinv2  12914  bitsinv  12919  lebnumlem3  18945  isi1f  19523  itg1val  19532  itg1climres  19563  itgex  19619  itgfsum  19675  dvmptfsum  19816  plyeq0lem  20086  plyaddlem1  20089  plymullem1  20090  coeeulem  20100  coeid2  20115  plyco  20117  coemullem  20125  coemul  20127  aareccl  20200  aaliou3lem5  20221  aaliou3lem6  20222  aaliou3lem7  20223  taylpval  20240  psercn  20299  pserdvlem2  20301  pserdv  20302  abelthlem6  20309  abelthlem8  20312  abelthlem9  20313  logtayl  20508  leibpi  20739  basellem3  20822  chtval  20850  chpval  20862  sgmval  20882  muinv  20935  dchrvmasumlem1  21146  dchrisum0fval  21156  dchrisum0fno1  21162  dchrisum0lem3  21170  dchrisum0  21171  mulogsum  21183  logsqvma2  21194  selberglem1  21196  pntsval  21223  esumpcvgval  24425  esumcvg  24433  stoweidlem11  27631  stoweidlem26  27646
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2389  ax-nul 4302
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2262  df-clab 2395  df-cleq 2401  df-clel 2404  df-nfc 2533  df-ne 2573  df-ral 2675  df-rex 2676  df-v 2922  df-sbc 3126  df-dif 3287  df-un 3289  df-in 3291  df-ss 3298  df-nul 3593  df-sn 3784  df-pr 3785  df-uni 3980  df-iota 5381  df-sum 12439
  Copyright terms: Public domain W3C validator