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

Theorem sumex 13161
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 13160 . 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 5395 . 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 2511 1  |-  sum_ k  e.  A  B  e.  _V
Colors of variables: wff setvar class
Syntax hints:    \/ wo 368    /\ wa 369    = wceq 1364   E.wex 1591    e. wcel 1761   E.wrex 2714   _Vcvv 2970   [_csb 3285    C_ wss 3325   ifcif 3788   class class class wbr 4289    e. cmpt 4347   iotacio 5376   -1-1-onto->wf1o 5414   ` cfv 5415  (class class class)co 6090   0cc0 9278   1c1 9279    + caddc 9281   NNcn 10318   ZZcz 10642   ZZ>=cuz 10857   ...cfz 11433    seqcseq 11802    ~~> cli 12958   sum_csu 13159
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-nul 4418
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-eu 2263  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-ral 2718  df-rex 2719  df-v 2972  df-sbc 3184  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-nul 3635  df-sn 3875  df-pr 3877  df-uni 4089  df-iota 5378  df-sum 13160
This theorem is referenced by:  fsumrlim  13270  fsumo1  13271  efval  13361  efcvgfsum  13367  eftlub  13389  bitsinv2  13635  bitsinv  13640  lebnumlem3  20435  isi1f  21052  itg1val  21061  itg1climres  21092  itgex  21148  itgfsum  21204  dvmptfsum  21347  plyeq0lem  21621  plyaddlem1  21624  plymullem1  21625  coeeulem  21635  coeid2  21650  plyco  21652  coemullem  21660  coemul  21662  aareccl  21735  aaliou3lem5  21756  aaliou3lem6  21757  aaliou3lem7  21758  taylpval  21775  psercn  21834  pserdvlem2  21836  pserdv  21837  abelthlem6  21844  abelthlem8  21847  abelthlem9  21848  logtayl  22048  leibpi  22280  basellem3  22363  chtval  22391  chpval  22403  sgmval  22423  muinv  22476  dchrvmasumlem1  22687  dchrisum0fval  22697  dchrisum0fno1  22703  dchrisum0lem3  22711  dchrisum0  22712  mulogsum  22724  logsqvma2  22735  selberglem1  22737  pntsval  22764  ecgrtg  23148  esumpcvgval  26447  esumcvg  26455  eulerpartlemsv1  26653  signsplypnf  26865  signsvvfval  26893  stoweidlem11  29715  stoweidlem26  29730
  Copyright terms: Public domain W3C validator