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

Theorem sumex 15024
 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 15023 . 2 Σ𝑘𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))))
2 iotaex 6311 . 2 (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚)))) ∈ V
31, 2eqeltri 2907 1 Σ𝑘𝐴 𝐵 ∈ V
 Colors of variables: wff setvar class Syntax hints:   ∧ wa 398   ∨ wo 843   = wceq 1537  ∃wex 1780   ∈ wcel 2114  ∃wrex 3126  Vcvv 3473  ⦋csb 3860   ⊆ wss 3913  ifcif 4443   class class class wbr 5042   ↦ cmpt 5122  ℩cio 6288  –1-1-onto→wf1o 6330  ‘cfv 6331  (class class class)co 7133  0cc0 10515  1c1 10516   + caddc 10518  ℕcn 11616  ℤcz 11960  ℤ≥cuz 12222  ...cfz 12876  seqcseq 13353   ⇝ cli 14821  Σcsu 15022 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792  ax-nul 5186 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-ral 3130  df-rex 3131  df-v 3475  df-sbc 3753  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4270  df-sn 4544  df-pr 4546  df-uni 4815  df-iota 6290  df-sum 15023 This theorem is referenced by:  fsumrlim  15146  fsumo1  15147  efval  15413  efcvgfsum  15419  eftlub  15442  bitsinv2  15770  bitsinv  15775  lebnumlem3  23547  isi1f  24257  itg1val  24266  itg1climres  24297  itgex  24353  itgfsum  24409  dvmptfsum  24557  plyeq0lem  24786  plyaddlem1  24789  plymullem1  24790  coeeulem  24800  coeid2  24815  plyco  24817  coemullem  24826  coemul  24828  aareccl  24901  aaliou3lem5  24922  aaliou3lem6  24923  aaliou3lem7  24924  taylpval  24941  psercn  25000  pserdvlem2  25002  pserdv  25003  abelthlem6  25010  abelthlem8  25013  abelthlem9  25014  logtayl  25230  leibpi  25507  basellem3  25647  chtval  25674  chpval  25686  sgmval  25706  muinv  25757  dchrvmasumlem1  26058  dchrisum0fval  26068  dchrisum0fno1  26074  dchrisum0lem3  26082  dchrisum0  26083  mulogsum  26095  logsqvma2  26106  selberglem1  26108  pntsval  26135  ecgrtg  26756  esumpcvgval  31345  esumcvg  31353  eulerpartlemsv1  31622  signsplypnf  31828  signsvvfval  31856  vtsval  31916  circlemeth  31919  fwddifnval  33632  knoppndvlem6  33864  binomcxplemnotnn0  40843  stoweidlem11  42444  stoweidlem26  42459  fourierdlem112  42651  fsumlesge0  42807  sge0sn  42809  sge0f1o  42812  sge0supre  42819  sge0resplit  42836  sge0reuz  42877  sge0reuzb  42878  aacllem  45089
 Copyright terms: Public domain W3C validator