# Metamath Proof Explorer

## Theorem zsum

Description: Series sum with index set a subset of the upper integers. (Contributed by Mario Carneiro, 13-Jun-2019)

Ref Expression
Hypotheses zsum.1 ${⊢}{Z}={ℤ}_{\ge {M}}$
zsum.2 ${⊢}{\phi }\to {M}\in ℤ$
zsum.3 ${⊢}{\phi }\to {A}\subseteq {Z}$
zsum.4 ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {F}\left({k}\right)=if\left({k}\in {A},{B},0\right)$
zsum.5 ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}\in ℂ$
Assertion zsum ${⊢}{\phi }\to \sum _{{k}\in {A}}{B}=⇝\left(seq{M}\left(+,{F}\right)\right)$

### Proof

Step Hyp Ref Expression
1 zsum.1 ${⊢}{Z}={ℤ}_{\ge {M}}$
2 zsum.2 ${⊢}{\phi }\to {M}\in ℤ$
3 zsum.3 ${⊢}{\phi }\to {A}\subseteq {Z}$
4 zsum.4 ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {F}\left({k}\right)=if\left({k}\in {A},{B},0\right)$
5 zsum.5 ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}\in ℂ$
6 eleq1w ${⊢}{n}={i}\to \left({n}\in {A}↔{i}\in {A}\right)$
7 csbeq1
8 6 7 ifbieq1d
9 8 cbvmptv
10 simpll ${⊢}\left(\left({\phi }\wedge {m}\in ℤ\right)\wedge {A}\subseteq {ℤ}_{\ge {m}}\right)\to {\phi }$
11 5 ralrimiva ${⊢}{\phi }\to \forall {k}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in ℂ$
12 nfcsb1v
13 12 nfel1
14 csbeq1a
15 14 eleq1d
16 13 15 rspc
17 11 16 syl5
18 10 17 mpan9
19 simplr ${⊢}\left(\left({\phi }\wedge {m}\in ℤ\right)\wedge {A}\subseteq {ℤ}_{\ge {m}}\right)\to {m}\in ℤ$
20 2 ad2antrr ${⊢}\left(\left({\phi }\wedge {m}\in ℤ\right)\wedge {A}\subseteq {ℤ}_{\ge {m}}\right)\to {M}\in ℤ$
21 simpr ${⊢}\left(\left({\phi }\wedge {m}\in ℤ\right)\wedge {A}\subseteq {ℤ}_{\ge {m}}\right)\to {A}\subseteq {ℤ}_{\ge {m}}$
22 3 1 sseqtrdi ${⊢}{\phi }\to {A}\subseteq {ℤ}_{\ge {M}}$
23 22 ad2antrr ${⊢}\left(\left({\phi }\wedge {m}\in ℤ\right)\wedge {A}\subseteq {ℤ}_{\ge {m}}\right)\to {A}\subseteq {ℤ}_{\ge {M}}$
24 9 18 19 20 21 23 sumrb
25 24 biimpd
26 25 expimpd
27 26 rexlimdva
28 3 ad2antrr ${⊢}\left(\left({\phi }\wedge {m}\in ℕ\right)\wedge {f}:\left(1\dots {m}\right)\underset{1-1 onto}{⟶}{A}\right)\to {A}\subseteq {Z}$
29 uzssz ${⊢}{ℤ}_{\ge {M}}\subseteq ℤ$
30 1 29 eqsstri ${⊢}{Z}\subseteq ℤ$
31 zssre ${⊢}ℤ\subseteq ℝ$
32 30 31 sstri ${⊢}{Z}\subseteq ℝ$
33 ltso ${⊢}<\mathrm{Or}ℝ$
34 soss ${⊢}{Z}\subseteq ℝ\to \left(<\mathrm{Or}ℝ\to <\mathrm{Or}{Z}\right)$
35 32 33 34 mp2 ${⊢}<\mathrm{Or}{Z}$
36 soss ${⊢}{A}\subseteq {Z}\to \left(<\mathrm{Or}{Z}\to <\mathrm{Or}{A}\right)$
37 28 35 36 mpisyl ${⊢}\left(\left({\phi }\wedge {m}\in ℕ\right)\wedge {f}:\left(1\dots {m}\right)\underset{1-1 onto}{⟶}{A}\right)\to <\mathrm{Or}{A}$
38 fzfi ${⊢}\left(1\dots {m}\right)\in \mathrm{Fin}$
39 ovex ${⊢}\left(1\dots {m}\right)\in \mathrm{V}$
40 39 f1oen ${⊢}{f}:\left(1\dots {m}\right)\underset{1-1 onto}{⟶}{A}\to \left(1\dots {m}\right)\approx {A}$
41 40 adantl ${⊢}\left(\left({\phi }\wedge {m}\in ℕ\right)\wedge {f}:\left(1\dots {m}\right)\underset{1-1 onto}{⟶}{A}\right)\to \left(1\dots {m}\right)\approx {A}$
42 41 ensymd ${⊢}\left(\left({\phi }\wedge {m}\in ℕ\right)\wedge {f}:\left(1\dots {m}\right)\underset{1-1 onto}{⟶}{A}\right)\to {A}\approx \left(1\dots {m}\right)$
43 enfii ${⊢}\left(\left(1\dots {m}\right)\in \mathrm{Fin}\wedge {A}\approx \left(1\dots {m}\right)\right)\to {A}\in \mathrm{Fin}$
44 38 42 43 sylancr ${⊢}\left(\left({\phi }\wedge {m}\in ℕ\right)\wedge {f}:\left(1\dots {m}\right)\underset{1-1 onto}{⟶}{A}\right)\to {A}\in \mathrm{Fin}$
45 fz1iso ${⊢}\left(<\mathrm{Or}{A}\wedge {A}\in \mathrm{Fin}\right)\to \exists {g}\phantom{\rule{.4em}{0ex}}{g}{Isom}_{<,<}\left(\left(1\dots \left|{A}\right|\right),{A}\right)$
46 37 44 45 syl2anc ${⊢}\left(\left({\phi }\wedge {m}\in ℕ\right)\wedge {f}:\left(1\dots {m}\right)\underset{1-1 onto}{⟶}{A}\right)\to \exists {g}\phantom{\rule{.4em}{0ex}}{g}{Isom}_{<,<}\left(\left(1\dots \left|{A}\right|\right),{A}\right)$
47 simpll ${⊢}\left(\left({\phi }\wedge {m}\in ℕ\right)\wedge \left({f}:\left(1\dots {m}\right)\underset{1-1 onto}{⟶}{A}\wedge {g}{Isom}_{<,<}\left(\left(1\dots \left|{A}\right|\right),{A}\right)\right)\right)\to {\phi }$
48 47 17 mpan9
49 fveq2 ${⊢}{n}={j}\to {f}\left({n}\right)={f}\left({j}\right)$
50 49 csbeq1d
51 csbcow
52 50 51 syl6eqr
53 52 cbvmptv
54 eqid
55 simplr ${⊢}\left(\left({\phi }\wedge {m}\in ℕ\right)\wedge \left({f}:\left(1\dots {m}\right)\underset{1-1 onto}{⟶}{A}\wedge {g}{Isom}_{<,<}\left(\left(1\dots \left|{A}\right|\right),{A}\right)\right)\right)\to {m}\in ℕ$
56 2 ad2antrr ${⊢}\left(\left({\phi }\wedge {m}\in ℕ\right)\wedge \left({f}:\left(1\dots {m}\right)\underset{1-1 onto}{⟶}{A}\wedge {g}{Isom}_{<,<}\left(\left(1\dots \left|{A}\right|\right),{A}\right)\right)\right)\to {M}\in ℤ$
57 22 ad2antrr ${⊢}\left(\left({\phi }\wedge {m}\in ℕ\right)\wedge \left({f}:\left(1\dots {m}\right)\underset{1-1 onto}{⟶}{A}\wedge {g}{Isom}_{<,<}\left(\left(1\dots \left|{A}\right|\right),{A}\right)\right)\right)\to {A}\subseteq {ℤ}_{\ge {M}}$
58 simprl ${⊢}\left(\left({\phi }\wedge {m}\in ℕ\right)\wedge \left({f}:\left(1\dots {m}\right)\underset{1-1 onto}{⟶}{A}\wedge {g}{Isom}_{<,<}\left(\left(1\dots \left|{A}\right|\right),{A}\right)\right)\right)\to {f}:\left(1\dots {m}\right)\underset{1-1 onto}{⟶}{A}$
59 simprr ${⊢}\left(\left({\phi }\wedge {m}\in ℕ\right)\wedge \left({f}:\left(1\dots {m}\right)\underset{1-1 onto}{⟶}{A}\wedge {g}{Isom}_{<,<}\left(\left(1\dots \left|{A}\right|\right),{A}\right)\right)\right)\to {g}{Isom}_{<,<}\left(\left(1\dots \left|{A}\right|\right),{A}\right)$
60 9 48 53 54 55 56 57 58 59 summolem2a
61 60 expr
62 61 exlimdv
63 46 62 mpd
64 breq2
65 63 64 syl5ibrcom
66 65 expimpd
67 66 exlimdv
68 67 rexlimdva
69 27 68 jaod
72 simpr
73 fveq2 ${⊢}{m}={M}\to {ℤ}_{\ge {m}}={ℤ}_{\ge {M}}$
74 73 sseq2d ${⊢}{m}={M}\to \left({A}\subseteq {ℤ}_{\ge {m}}↔{A}\subseteq {ℤ}_{\ge {M}}\right)$
75 seqeq1
76 75 breq1d
77 74 76 anbi12d
78 77 rspcev
79 70 71 72 78 syl12anc
80 79 orcd
81 80 ex
82 69 81 impbid
83 simpr ${⊢}\left({\phi }\wedge {j}\in {ℤ}_{\ge {M}}\right)\to {j}\in {ℤ}_{\ge {M}}$
84 29 83 sseldi ${⊢}\left({\phi }\wedge {j}\in {ℤ}_{\ge {M}}\right)\to {j}\in ℤ$
85 83 1 eleqtrrdi ${⊢}\left({\phi }\wedge {j}\in {ℤ}_{\ge {M}}\right)\to {j}\in {Z}$
86 4 ralrimiva ${⊢}{\phi }\to \forall {k}\in {Z}\phantom{\rule{.4em}{0ex}}{F}\left({k}\right)=if\left({k}\in {A},{B},0\right)$
87 86 adantr ${⊢}\left({\phi }\wedge {j}\in {ℤ}_{\ge {M}}\right)\to \forall {k}\in {Z}\phantom{\rule{.4em}{0ex}}{F}\left({k}\right)=if\left({k}\in {A},{B},0\right)$
88 nfcsb1v
89 88 nfeq2
90 fveq2 ${⊢}{k}={j}\to {F}\left({k}\right)={F}\left({j}\right)$
91 csbeq1a
92 90 91 eqeq12d
93 89 92 rspc
94 85 87 93 sylc
95 fvex ${⊢}{F}\left({j}\right)\in \mathrm{V}$
96 94 95 eqeltrrdi
97 nfcv ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}if\left({k}\in {A},{B},0\right)$
98 nfv ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{n}\in {A}$
99 nfcsb1v
100 nfcv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}0$
101 98 99 100 nfif
102 eleq1w ${⊢}{k}={n}\to \left({k}\in {A}↔{n}\in {A}\right)$
103 csbeq1a
104 102 103 ifbieq1d
105 97 101 104 cbvmpt
106 105 eqcomi
107 106 fvmpts
108 84 96 107 syl2anc
109 108 94 eqtr4d
110 2 109 seqfeq
111 110 breq1d
112 82 111 bitrd
113 112 iotabidv
114 df-sum
115 df-fv ${⊢}⇝\left(seq{M}\left(+,{F}\right)\right)=\left(\iota {x}|seq{M}\left(+,{F}\right)⇝{x}\right)$
116 113 114 115 3eqtr4g ${⊢}{\phi }\to \sum _{{k}\in {A}}{B}=⇝\left(seq{M}\left(+,{F}\right)\right)$