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

Theorem sumex 15724
Description: A sum is a set. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.)
Assertion
Ref Expression
sumex Σ𝑘𝐴 𝐵 ∈ V

Proof of Theorem sumex
Dummy variables 𝑓 𝑚 𝑛 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-sum 15723 . 2 Σ𝑘𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))))
2 iotaex 6534 . 2 (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚)))) ∈ V
31, 2eqeltri 2837 1 Σ𝑘𝐴 𝐵 ∈ V
Colors of variables: wff setvar class
Syntax hints:  wa 395  wo 848   = wceq 1540  wex 1779  wcel 2108  wrex 3070  Vcvv 3480  csb 3899  wss 3951  ifcif 4525   class class class wbr 5143  cmpt 5225  cio 6512  1-1-ontowf1o 6560  cfv 6561  (class class class)co 7431  0cc0 11155  1c1 11156   + caddc 11158  cn 12266  cz 12613  cuz 12878  ...cfz 13547  seqcseq 14042  cli 15520  Σcsu 15722
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-nul 5306
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-sn 4627  df-pr 4629  df-uni 4908  df-iota 6514  df-sum 15723
This theorem is referenced by:  fsumrlim  15847  fsumo1  15848  efval  16115  efcvgfsum  16122  eftlub  16145  bitsinv2  16480  bitsinv  16485  lebnumlem3  24995  isi1f  25709  itg1val  25718  itg1climres  25749  itgex  25805  itgfsum  25862  dvmptfsum  26013  plyeq0lem  26249  plyaddlem1  26252  plymullem1  26253  coeeulem  26263  coeid2  26278  plyco  26280  coemullem  26289  coemul  26291  aareccl  26368  aaliou3lem5  26389  aaliou3lem6  26390  aaliou3lem7  26391  taylpval  26408  psercn  26470  pserdvlem2  26472  pserdv  26473  abelthlem6  26480  abelthlem8  26483  abelthlem9  26484  logtayl  26702  leibpi  26985  basellem3  27126  chtval  27153  chpval  27165  sgmval  27185  muinv  27236  dchrvmasumlem1  27539  dchrisum0fval  27549  dchrisum0fno1  27555  dchrisum0lem3  27563  dchrisum0  27564  mulogsum  27576  logsqvma2  27587  selberglem1  27589  pntsval  27616  ecgrtg  28998  esumpcvgval  34079  esumcvg  34087  eulerpartlemsv1  34358  signsplypnf  34565  signsvvfval  34593  vtsval  34652  circlemeth  34655  fwddifnval  36164  knoppndvlem6  36518  binomcxplemnotnn0  44375  stoweidlem11  46026  stoweidlem26  46041  fourierdlem112  46233  fsumlesge0  46392  sge0sn  46394  sge0f1o  46397  sge0supre  46404  sge0resplit  46421  sge0reuz  46462  sge0reuzb  46463  aacllem  49320
  Copyright terms: Public domain W3C validator