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

Theorem sumex 13473
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 13472 . 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 5568 . 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 2551 1  |-  sum_ k  e.  A  B  e.  _V
Colors of variables: wff setvar class
Syntax hints:    \/ wo 368    /\ wa 369    = wceq 1379   E.wex 1596    e. wcel 1767   E.wrex 2815   _Vcvv 3113   [_csb 3435    C_ wss 3476   ifcif 3939   class class class wbr 4447    |-> cmpt 4505   iotacio 5549   -1-1-onto->wf1o 5587   ` cfv 5588  (class class class)co 6284   0cc0 9492   1c1 9493    + caddc 9495   NNcn 10536   ZZcz 10864   ZZ>=cuz 11082   ...cfz 11672    seqcseq 12075    ~~> cli 13270   sum_csu 13471
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-nul 4576
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-v 3115  df-sbc 3332  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-sn 4028  df-pr 4030  df-uni 4246  df-iota 5551  df-sum 13472
This theorem is referenced by:  fsumrlim  13588  fsumo1  13589  efval  13677  efcvgfsum  13683  eftlub  13705  bitsinv2  13952  bitsinv  13957  lebnumlem3  21226  isi1f  21844  itg1val  21853  itg1climres  21884  itgex  21940  itgfsum  21996  dvmptfsum  22139  plyeq0lem  22370  plyaddlem1  22373  plymullem1  22374  coeeulem  22384  coeid2  22399  plyco  22401  coemullem  22409  coemul  22411  aareccl  22484  aaliou3lem5  22505  aaliou3lem6  22506  aaliou3lem7  22507  taylpval  22524  psercn  22583  pserdvlem2  22585  pserdv  22586  abelthlem6  22593  abelthlem8  22596  abelthlem9  22597  logtayl  22797  leibpi  23029  basellem3  23112  chtval  23140  chpval  23152  sgmval  23172  muinv  23225  dchrvmasumlem1  23436  dchrisum0fval  23446  dchrisum0fno1  23452  dchrisum0lem3  23460  dchrisum0  23461  mulogsum  23473  logsqvma2  23484  selberglem1  23486  pntsval  23513  ecgrtg  23990  esumpcvgval  27752  esumcvg  27760  eulerpartlemsv1  27963  signsplypnf  28175  signsvvfval  28203  stoweidlem11  31339  stoweidlem26  31354  fourierdlem112  31547
  Copyright terms: Public domain W3C validator