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

Theorem sumex 13165
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 13164 . 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 5398 . 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 2513 1  |-  sum_ k  e.  A  B  e.  _V
Colors of variables: wff setvar class
Syntax hints:    \/ wo 368    /\ wa 369    = wceq 1369   E.wex 1586    e. wcel 1756   E.wrex 2716   _Vcvv 2972   [_csb 3288    C_ wss 3328   ifcif 3791   class class class wbr 4292    e. cmpt 4350   iotacio 5379   -1-1-onto->wf1o 5417   ` cfv 5418  (class class class)co 6091   0cc0 9282   1c1 9283    + caddc 9285   NNcn 10322   ZZcz 10646   ZZ>=cuz 10861   ...cfz 11437    seqcseq 11806    ~~> cli 12962   sum_csu 13163
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-nul 4421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-ral 2720  df-rex 2721  df-v 2974  df-sbc 3187  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-nul 3638  df-sn 3878  df-pr 3880  df-uni 4092  df-iota 5381  df-sum 13164
This theorem is referenced by:  fsumrlim  13274  fsumo1  13275  efval  13365  efcvgfsum  13371  eftlub  13393  bitsinv2  13639  bitsinv  13644  lebnumlem3  20535  isi1f  21152  itg1val  21161  itg1climres  21192  itgex  21248  itgfsum  21304  dvmptfsum  21447  plyeq0lem  21678  plyaddlem1  21681  plymullem1  21682  coeeulem  21692  coeid2  21707  plyco  21709  coemullem  21717  coemul  21719  aareccl  21792  aaliou3lem5  21813  aaliou3lem6  21814  aaliou3lem7  21815  taylpval  21832  psercn  21891  pserdvlem2  21893  pserdv  21894  abelthlem6  21901  abelthlem8  21904  abelthlem9  21905  logtayl  22105  leibpi  22337  basellem3  22420  chtval  22448  chpval  22460  sgmval  22480  muinv  22533  dchrvmasumlem1  22744  dchrisum0fval  22754  dchrisum0fno1  22760  dchrisum0lem3  22768  dchrisum0  22769  mulogsum  22781  logsqvma2  22792  selberglem1  22794  pntsval  22821  ecgrtg  23229  esumpcvgval  26527  esumcvg  26535  eulerpartlemsv1  26739  signsplypnf  26951  signsvvfval  26979  stoweidlem11  29806  stoweidlem26  29821
  Copyright terms: Public domain W3C validator