| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > sumex | Structured version Visualization version GIF version | ||
| Description: A sum is a set. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.) |
| Ref | Expression |
|---|---|
| sumex | ⊢ Σ𝑘 ∈ 𝐴 𝐵 ∈ V |
| Step | Hyp | Ref | 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 | |
| 3 | 1, 2 | eqeltri 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-onto→wf1o 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 |