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

Theorem sumex 12486
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 12485 . 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 5438 . 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 2508 1  |-  sum_ k  e.  A  B  e.  _V
Colors of variables: wff set class
Syntax hints:    \/ wo 359    /\ wa 360   E.wex 1551    = wceq 1653    e. wcel 1726   E.wrex 2708   _Vcvv 2958   [_csb 3253    C_ wss 3322   ifcif 3741   class class class wbr 4215    e. cmpt 4269   iotacio 5419   -1-1-onto->wf1o 5456   ` cfv 5457  (class class class)co 6084   0cc0 8995   1c1 8996    + caddc 8998   NNcn 10005   ZZcz 10287   ZZ>=cuz 10493   ...cfz 11048    seq cseq 11328    ~~> cli 12283   sum_csu 12484
This theorem is referenced by:  fsumrlim  12595  fsumo1  12596  efval  12687  efcvgfsum  12693  eftlub  12715  bitsinv2  12960  bitsinv  12965  lebnumlem3  18993  isi1f  19569  itg1val  19578  itg1climres  19609  itgex  19665  itgfsum  19721  dvmptfsum  19864  plyeq0lem  20134  plyaddlem1  20137  plymullem1  20138  coeeulem  20148  coeid2  20163  plyco  20165  coemullem  20173  coemul  20175  aareccl  20248  aaliou3lem5  20269  aaliou3lem6  20270  aaliou3lem7  20271  taylpval  20288  psercn  20347  pserdvlem2  20349  pserdv  20350  abelthlem6  20357  abelthlem8  20360  abelthlem9  20361  logtayl  20556  leibpi  20787  basellem3  20870  chtval  20898  chpval  20910  sgmval  20930  muinv  20983  dchrvmasumlem1  21194  dchrisum0fval  21204  dchrisum0fno1  21210  dchrisum0lem3  21218  dchrisum0  21219  mulogsum  21231  logsqvma2  21242  selberglem1  21244  pntsval  21271  esumpcvgval  24473  esumcvg  24481  stoweidlem11  27750  stoweidlem26  27765
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-nul 4341
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2712  df-rex 2713  df-v 2960  df-sbc 3164  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-sn 3822  df-pr 3823  df-uni 4018  df-iota 5421  df-sum 12485
  Copyright terms: Public domain W3C validator