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

Theorem sumex 14615
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 14614 . 2 Σ𝑘𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))))
2 iotaex 6027 . 2 (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚)))) ∈ V
31, 2eqeltri 2833 1 Σ𝑘𝐴 𝐵 ∈ V
Colors of variables: wff setvar class
Syntax hints:  wo 382  wa 383   = wceq 1630  wex 1851  wcel 2137  wrex 3049  Vcvv 3338  csb 3672  wss 3713  ifcif 4228   class class class wbr 4802  cmpt 4879  cio 6008  1-1-ontowf1o 6046  cfv 6047  (class class class)co 6811  0cc0 10126  1c1 10127   + caddc 10129  cn 11210  cz 11567  cuz 11877  ...cfz 12517  seqcseq 12993  cli 14412  Σcsu 14613
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-ext 2738  ax-nul 4939
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2045  df-eu 2609  df-clab 2745  df-cleq 2751  df-clel 2754  df-nfc 2889  df-ral 3053  df-rex 3054  df-v 3340  df-sbc 3575  df-dif 3716  df-un 3718  df-in 3720  df-ss 3727  df-nul 4057  df-sn 4320  df-pr 4322  df-uni 4587  df-iota 6010  df-sum 14614
This theorem is referenced by:  fsumrlim  14740  fsumo1  14741  efval  15007  efcvgfsum  15013  eftlub  15036  bitsinv2  15365  bitsinv  15370  lebnumlem3  22961  isi1f  23638  itg1val  23647  itg1climres  23678  itgex  23734  itgfsum  23790  dvmptfsum  23935  plyeq0lem  24163  plyaddlem1  24166  plymullem1  24167  coeeulem  24177  coeid2  24192  plyco  24194  coemullem  24203  coemul  24205  aareccl  24278  aaliou3lem5  24299  aaliou3lem6  24300  aaliou3lem7  24301  taylpval  24318  psercn  24377  pserdvlem2  24379  pserdv  24380  abelthlem6  24387  abelthlem8  24390  abelthlem9  24391  logtayl  24603  leibpi  24866  basellem3  25006  chtval  25033  chpval  25045  sgmval  25065  muinv  25116  dchrvmasumlem1  25381  dchrisum0fval  25391  dchrisum0fno1  25397  dchrisum0lem3  25405  dchrisum0  25406  mulogsum  25418  logsqvma2  25429  selberglem1  25431  pntsval  25458  ecgrtg  26060  esumpcvgval  30447  esumcvg  30455  eulerpartlemsv1  30725  signsplypnf  30934  signsvvfval  30962  vtsval  31022  circlemeth  31025  fwddifnval  32574  knoppndvlem6  32812  binomcxplemnotnn0  39055  stoweidlem11  40729  stoweidlem26  40744  fourierdlem112  40936  fsumlesge0  41095  sge0sn  41097  sge0f1o  41100  sge0supre  41107  sge0resplit  41124  sge0reuz  41165  sge0reuzb  41166  aacllem  43058
  Copyright terms: Public domain W3C validator