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

Theorem sumex 12436
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 12435 . 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 5394 . 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 2474 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 2667   _Vcvv 2916   [_csb 3211    C_ wss 3280   ifcif 3699   class class class wbr 4172    e. cmpt 4226   iotacio 5375   -1-1-onto->wf1o 5412   ` cfv 5413  (class class class)co 6040   0cc0 8946   1c1 8947    + caddc 8949   NNcn 9956   ZZcz 10238   ZZ>=cuz 10444   ...cfz 10999    seq cseq 11278    ~~> cli 12233   sum_csu 12434
This theorem is referenced by:  fsumrlim  12545  fsumo1  12546  efval  12637  efcvgfsum  12643  eftlub  12665  bitsinv2  12910  bitsinv  12915  lebnumlem3  18941  isi1f  19519  itg1val  19528  itg1climres  19559  itgex  19615  itgfsum  19671  dvmptfsum  19812  plyeq0lem  20082  plyaddlem1  20085  plymullem1  20086  coeeulem  20096  coeid2  20111  plyco  20113  coemullem  20121  coemul  20123  aareccl  20196  aaliou3lem5  20217  aaliou3lem6  20218  aaliou3lem7  20219  taylpval  20236  psercn  20295  pserdvlem2  20297  pserdv  20298  abelthlem6  20305  abelthlem8  20308  abelthlem9  20309  logtayl  20504  leibpi  20735  basellem3  20818  chtval  20846  chpval  20858  sgmval  20878  muinv  20931  dchrvmasumlem1  21142  dchrisum0fval  21152  dchrisum0fno1  21158  dchrisum0lem3  21166  dchrisum0  21167  mulogsum  21179  logsqvma2  21190  selberglem1  21192  pntsval  21219  esumpcvgval  24421  esumcvg  24429  stoweidlem11  27627  stoweidlem26  27642
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 2385  ax-nul 4298
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 2258  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-v 2918  df-sbc 3122  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-sn 3780  df-pr 3781  df-uni 3976  df-iota 5377  df-sum 12435
  Copyright terms: Public domain W3C validator