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

Theorem sumex 14368
 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 14367 . 2 Σ𝑘𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))))
2 iotaex 5837 . 2 (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚)))) ∈ V
31, 2eqeltri 2694 1 Σ𝑘𝐴 𝐵 ∈ V
 Colors of variables: wff setvar class Syntax hints:   ∨ wo 383   ∧ wa 384   = wceq 1480  ∃wex 1701   ∈ wcel 1987  ∃wrex 2909  Vcvv 3190  ⦋csb 3519   ⊆ wss 3560  ifcif 4064   class class class wbr 4623   ↦ cmpt 4683  ℩cio 5818  –1-1-onto→wf1o 5856  ‘cfv 5857  (class class class)co 6615  0cc0 9896  1c1 9897   + caddc 9899  ℕcn 10980  ℤcz 11337  ℤ≥cuz 11647  ...cfz 12284  seqcseq 12757   ⇝ cli 14165  Σcsu 14366 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-nul 4759 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2913  df-rex 2914  df-v 3192  df-sbc 3423  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3898  df-sn 4156  df-pr 4158  df-uni 4410  df-iota 5820  df-sum 14367 This theorem is referenced by:  fsumrlim  14489  fsumo1  14490  efval  14754  efcvgfsum  14760  eftlub  14783  bitsinv2  15108  bitsinv  15113  lebnumlem3  22702  isi1f  23381  itg1val  23390  itg1climres  23421  itgex  23477  itgfsum  23533  dvmptfsum  23676  plyeq0lem  23904  plyaddlem1  23907  plymullem1  23908  coeeulem  23918  coeid2  23933  plyco  23935  coemullem  23944  coemul  23946  aareccl  24019  aaliou3lem5  24040  aaliou3lem6  24041  aaliou3lem7  24042  taylpval  24059  psercn  24118  pserdvlem2  24120  pserdv  24121  abelthlem6  24128  abelthlem8  24131  abelthlem9  24132  logtayl  24340  leibpi  24603  basellem3  24743  chtval  24770  chpval  24782  sgmval  24802  muinv  24853  dchrvmasumlem1  25118  dchrisum0fval  25128  dchrisum0fno1  25134  dchrisum0lem3  25142  dchrisum0  25143  mulogsum  25155  logsqvma2  25166  selberglem1  25168  pntsval  25195  ecgrtg  25797  esumpcvgval  29963  esumcvg  29971  eulerpartlemsv1  30241  signsplypnf  30449  signsvvfval  30477  fwddifnval  31965  knoppndvlem6  32203  binomcxplemnotnn0  38076  stoweidlem11  39565  stoweidlem26  39580  fourierdlem112  39772  fsumlesge0  39931  sge0sn  39933  sge0f1o  39936  sge0supre  39943  sge0resplit  39960  sge0reuz  40001  sge0reuzb  40002  aacllem  41880
 Copyright terms: Public domain W3C validator