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

Theorem sumex 12368
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 12367 . 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 5339 . 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 2436 1  |-  sum_ k  e.  A  B  e.  _V
Colors of variables: wff set class
Syntax hints:    \/ wo 357    /\ wa 358   E.wex 1546    = wceq 1647    e. wcel 1715   E.wrex 2629   _Vcvv 2873   [_csb 3167    C_ wss 3238   ifcif 3654   class class class wbr 4125    e. cmpt 4179   iotacio 5320   -1-1-onto->wf1o 5357   ` cfv 5358  (class class class)co 5981   0cc0 8884   1c1 8885    + caddc 8887   NNcn 9893   ZZcz 10175   ZZ>=cuz 10381   ...cfz 10935    seq cseq 11210    ~~> cli 12165   sum_csu 12366
This theorem is referenced by:  fsumrlim  12477  fsumo1  12478  efval  12569  efcvgfsum  12575  eftlub  12597  bitsinv2  12842  bitsinv  12847  lebnumlem3  18676  isi1f  19244  itg1val  19253  itg1climres  19284  itgex  19340  itgfsum  19396  dvmptfsum  19537  plyeq0lem  19807  plyaddlem1  19810  plymullem1  19811  coeeulem  19821  coeid2  19836  plyco  19838  coemullem  19846  coemul  19848  aareccl  19921  aaliou3lem5  19942  aaliou3lem6  19943  aaliou3lem7  19944  taylpval  19961  psercn  20020  pserdvlem2  20022  pserdv  20023  abelthlem6  20030  abelthlem8  20033  abelthlem9  20034  logtayl  20229  leibpi  20460  basellem3  20543  chtval  20571  chpval  20583  sgmval  20603  muinv  20656  dchrvmasumlem1  20867  dchrisum0fval  20877  dchrisum0fno1  20883  dchrisum0lem3  20891  dchrisum0  20892  mulogsum  20904  logsqvma2  20915  selberglem1  20917  pntsval  20944  esumpcvgval  24054  esumcvg  24062  stoweidlem11  27351  stoweidlem26  27366
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347  ax-nul 4251
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-eu 2221  df-clab 2353  df-cleq 2359  df-clel 2362  df-nfc 2491  df-ne 2531  df-ral 2633  df-rex 2634  df-v 2875  df-sbc 3078  df-dif 3241  df-un 3243  df-in 3245  df-ss 3252  df-nul 3544  df-sn 3735  df-pr 3736  df-uni 3930  df-iota 5322  df-sum 12367
  Copyright terms: Public domain W3C validator