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

Theorem sumex 14212
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 14211 . 2 Σ𝑘𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))))
2 iotaex 5771 . 2 (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚)))) ∈ V
31, 2eqeltri 2683 1 Σ𝑘𝐴 𝐵 ∈ V
Colors of variables: wff setvar class
Syntax hints:  wo 381  wa 382   = wceq 1474  wex 1694  wcel 1976  wrex 2896  Vcvv 3172  csb 3498  wss 3539  ifcif 4035   class class class wbr 4577  cmpt 4637  cio 5752  1-1-ontowf1o 5789  cfv 5790  (class class class)co 6527  0cc0 9792  1c1 9793   + caddc 9795  cn 10867  cz 11210  cuz 11519  ...cfz 12152  seqcseq 12618  cli 14009  Σcsu 14210
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2232  ax-ext 2589  ax-nul 4712
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ral 2900  df-rex 2901  df-v 3174  df-sbc 3402  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-sn 4125  df-pr 4127  df-uni 4367  df-iota 5754  df-sum 14211
This theorem is referenced by:  fsumrlim  14330  fsumo1  14331  efval  14595  efcvgfsum  14601  eftlub  14624  bitsinv2  14949  bitsinv  14954  lebnumlem3  22501  isi1f  23164  itg1val  23173  itg1climres  23204  itgex  23260  itgfsum  23316  dvmptfsum  23459  plyeq0lem  23687  plyaddlem1  23690  plymullem1  23691  coeeulem  23701  coeid2  23716  plyco  23718  coemullem  23727  coemul  23729  aareccl  23802  aaliou3lem5  23823  aaliou3lem6  23824  aaliou3lem7  23825  taylpval  23842  psercn  23901  pserdvlem2  23903  pserdv  23904  abelthlem6  23911  abelthlem8  23914  abelthlem9  23915  logtayl  24123  leibpi  24386  basellem3  24526  chtval  24553  chpval  24565  sgmval  24585  muinv  24636  dchrvmasumlem1  24901  dchrisum0fval  24911  dchrisum0fno1  24917  dchrisum0lem3  24925  dchrisum0  24926  mulogsum  24938  logsqvma2  24949  selberglem1  24951  pntsval  24978  ecgrtg  25581  esumpcvgval  29273  esumcvg  29281  eulerpartlemsv1  29551  signsplypnf  29759  signsvvfval  29787  fwddifnval  31246  knoppndvlem6  31484  binomcxplemnotnn0  37380  stoweidlem11  38708  stoweidlem26  38723  fourierdlem112  38915  fsumlesge0  39074  sge0sn  39076  sge0f1o  39079  sge0supre  39086  sge0resplit  39103  sge0reuz  39144  sge0reuzb  39145  aacllem  42319
  Copyright terms: Public domain W3C validator