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

Theorem sumex 13592
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 13591 . 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 5551 . 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 2538 1  |-  sum_ k  e.  A  B  e.  _V
Colors of variables: wff setvar class
Syntax hints:    \/ wo 366    /\ wa 367    = wceq 1398   E.wex 1617    e. wcel 1823   E.wrex 2805   _Vcvv 3106   [_csb 3420    C_ wss 3461   ifcif 3929   class class class wbr 4439    |-> cmpt 4497   iotacio 5532   -1-1-onto->wf1o 5569   ` cfv 5570  (class class class)co 6270   0cc0 9481   1c1 9482    + caddc 9484   NNcn 10531   ZZcz 10860   ZZ>=cuz 11082   ...cfz 11675    seqcseq 12089    ~~> cli 13389   sum_csu 13590
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-nul 4568
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-v 3108  df-sbc 3325  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-sn 4017  df-pr 4019  df-uni 4236  df-iota 5534  df-sum 13591
This theorem is referenced by:  fsumrlim  13707  fsumo1  13708  efval  13897  efcvgfsum  13903  eftlub  13926  bitsinv2  14177  bitsinv  14182  lebnumlem3  21629  isi1f  22247  itg1val  22256  itg1climres  22287  itgex  22343  itgfsum  22399  dvmptfsum  22542  plyeq0lem  22773  plyaddlem1  22776  plymullem1  22777  coeeulem  22787  coeid2  22802  plyco  22804  coemullem  22813  coemul  22815  aareccl  22888  aaliou3lem5  22909  aaliou3lem6  22910  aaliou3lem7  22911  taylpval  22928  psercn  22987  pserdvlem2  22989  pserdv  22990  abelthlem6  22997  abelthlem8  23000  abelthlem9  23001  logtayl  23209  leibpi  23470  basellem3  23554  chtval  23582  chpval  23594  sgmval  23614  muinv  23667  dchrvmasumlem1  23878  dchrisum0fval  23888  dchrisum0fno1  23894  dchrisum0lem3  23902  dchrisum0  23903  mulogsum  23915  logsqvma2  23926  selberglem1  23928  pntsval  23955  ecgrtg  24488  esumpcvgval  28307  esumcvg  28315  eulerpartlemsv1  28559  signsplypnf  28771  signsvvfval  28799  binomcxplemnotnn0  31502  stoweidlem11  32032  stoweidlem26  32047  fourierdlem112  32240  aacllem  33604
  Copyright terms: Public domain W3C validator