# Metamath Proof Explorer

## Theorem fsumrlim

Description: Limit of a finite sum of converging sequences. Note that C ( k ) is a collection of functions with implicit parameter k , each of which converges to D ( k ) as n ~> +oo . (Contributed by Mario Carneiro, 22-May-2016)

Ref Expression
Hypotheses fsumrlim.1 ${⊢}{\phi }\to {A}\subseteq ℝ$
fsumrlim.2 ${⊢}{\phi }\to {B}\in \mathrm{Fin}$
fsumrlim.3 ${⊢}\left({\phi }\wedge \left({x}\in {A}\wedge {k}\in {B}\right)\right)\to {C}\in {V}$
fsumrlim.4
Assertion fsumrlim

### Proof

Step Hyp Ref Expression
1 fsumrlim.1 ${⊢}{\phi }\to {A}\subseteq ℝ$
2 fsumrlim.2 ${⊢}{\phi }\to {B}\in \mathrm{Fin}$
3 fsumrlim.3 ${⊢}\left({\phi }\wedge \left({x}\in {A}\wedge {k}\in {B}\right)\right)\to {C}\in {V}$
4 fsumrlim.4
5 ssid ${⊢}{B}\subseteq {B}$
6 sseq1 ${⊢}{w}=\varnothing \to \left({w}\subseteq {B}↔\varnothing \subseteq {B}\right)$
7 sumeq1 ${⊢}{w}=\varnothing \to \sum _{{k}\in {w}}{C}=\sum _{{k}\in \varnothing }{C}$
8 sum0 ${⊢}\sum _{{k}\in \varnothing }{C}=0$
9 7 8 eqtrdi ${⊢}{w}=\varnothing \to \sum _{{k}\in {w}}{C}=0$
10 9 mpteq2dv ${⊢}{w}=\varnothing \to \left({x}\in {A}⟼\sum _{{k}\in {w}}{C}\right)=\left({x}\in {A}⟼0\right)$
11 sumeq1 ${⊢}{w}=\varnothing \to \sum _{{k}\in {w}}{D}=\sum _{{k}\in \varnothing }{D}$
12 sum0 ${⊢}\sum _{{k}\in \varnothing }{D}=0$
13 11 12 eqtrdi ${⊢}{w}=\varnothing \to \sum _{{k}\in {w}}{D}=0$
14 10 13 breq12d
15 6 14 imbi12d
16 15 imbi2d
17 sseq1 ${⊢}{w}={y}\to \left({w}\subseteq {B}↔{y}\subseteq {B}\right)$
18 sumeq1 ${⊢}{w}={y}\to \sum _{{k}\in {w}}{C}=\sum _{{k}\in {y}}{C}$
19 18 mpteq2dv ${⊢}{w}={y}\to \left({x}\in {A}⟼\sum _{{k}\in {w}}{C}\right)=\left({x}\in {A}⟼\sum _{{k}\in {y}}{C}\right)$
20 sumeq1 ${⊢}{w}={y}\to \sum _{{k}\in {w}}{D}=\sum _{{k}\in {y}}{D}$
21 19 20 breq12d
22 17 21 imbi12d
23 22 imbi2d
24 sseq1 ${⊢}{w}={y}\cup \left\{{z}\right\}\to \left({w}\subseteq {B}↔{y}\cup \left\{{z}\right\}\subseteq {B}\right)$
25 sumeq1 ${⊢}{w}={y}\cup \left\{{z}\right\}\to \sum _{{k}\in {w}}{C}=\sum _{{k}\in {y}\cup \left\{{z}\right\}}{C}$
26 25 mpteq2dv ${⊢}{w}={y}\cup \left\{{z}\right\}\to \left({x}\in {A}⟼\sum _{{k}\in {w}}{C}\right)=\left({x}\in {A}⟼\sum _{{k}\in {y}\cup \left\{{z}\right\}}{C}\right)$
27 sumeq1 ${⊢}{w}={y}\cup \left\{{z}\right\}\to \sum _{{k}\in {w}}{D}=\sum _{{k}\in {y}\cup \left\{{z}\right\}}{D}$
28 26 27 breq12d
29 24 28 imbi12d
30 29 imbi2d
31 sseq1 ${⊢}{w}={B}\to \left({w}\subseteq {B}↔{B}\subseteq {B}\right)$
32 sumeq1 ${⊢}{w}={B}\to \sum _{{k}\in {w}}{C}=\sum _{{k}\in {B}}{C}$
33 32 mpteq2dv ${⊢}{w}={B}\to \left({x}\in {A}⟼\sum _{{k}\in {w}}{C}\right)=\left({x}\in {A}⟼\sum _{{k}\in {B}}{C}\right)$
34 sumeq1 ${⊢}{w}={B}\to \sum _{{k}\in {w}}{D}=\sum _{{k}\in {B}}{D}$
35 33 34 breq12d
36 31 35 imbi12d
37 36 imbi2d
38 0cn ${⊢}0\in ℂ$
39 rlimconst
40 1 38 39 sylancl
41 40 a1d
42 ssun1 ${⊢}{y}\subseteq {y}\cup \left\{{z}\right\}$
43 sstr ${⊢}\left({y}\subseteq {y}\cup \left\{{z}\right\}\wedge {y}\cup \left\{{z}\right\}\subseteq {B}\right)\to {y}\subseteq {B}$
44 42 43 mpan ${⊢}{y}\cup \left\{{z}\right\}\subseteq {B}\to {y}\subseteq {B}$
45 44 imim1i
46 sumex
47 46 a1i
48 simprr ${⊢}\left({\phi }\wedge \left(¬{z}\in {y}\wedge {y}\cup \left\{{z}\right\}\subseteq {B}\right)\right)\to {y}\cup \left\{{z}\right\}\subseteq {B}$
49 48 unssbd ${⊢}\left({\phi }\wedge \left(¬{z}\in {y}\wedge {y}\cup \left\{{z}\right\}\subseteq {B}\right)\right)\to \left\{{z}\right\}\subseteq {B}$
50 vex ${⊢}{z}\in \mathrm{V}$
51 50 snss ${⊢}{z}\in {B}↔\left\{{z}\right\}\subseteq {B}$
52 49 51 sylibr ${⊢}\left({\phi }\wedge \left(¬{z}\in {y}\wedge {y}\cup \left\{{z}\right\}\subseteq {B}\right)\right)\to {z}\in {B}$
53 52 adantr ${⊢}\left(\left({\phi }\wedge \left(¬{z}\in {y}\wedge {y}\cup \left\{{z}\right\}\subseteq {B}\right)\right)\wedge {x}\in {A}\right)\to {z}\in {B}$
54 3 anass1rs ${⊢}\left(\left({\phi }\wedge {k}\in {B}\right)\wedge {x}\in {A}\right)\to {C}\in {V}$
55 54 4 rlimmptrcl ${⊢}\left(\left({\phi }\wedge {k}\in {B}\right)\wedge {x}\in {A}\right)\to {C}\in ℂ$
56 55 an32s ${⊢}\left(\left({\phi }\wedge {x}\in {A}\right)\wedge {k}\in {B}\right)\to {C}\in ℂ$
57 56 adantllr ${⊢}\left(\left(\left({\phi }\wedge \left(¬{z}\in {y}\wedge {y}\cup \left\{{z}\right\}\subseteq {B}\right)\right)\wedge {x}\in {A}\right)\wedge {k}\in {B}\right)\to {C}\in ℂ$
58 57 ralrimiva ${⊢}\left(\left({\phi }\wedge \left(¬{z}\in {y}\wedge {y}\cup \left\{{z}\right\}\subseteq {B}\right)\right)\wedge {x}\in {A}\right)\to \forall {k}\in {B}\phantom{\rule{.4em}{0ex}}{C}\in ℂ$
59 nfcsb1v
60 59 nfel1
61 csbeq1a
62 61 eleq1d
63 60 62 rspc
64 53 58 63 sylc
65 64 ralrimiva
67 nfcsb1v
68 67 nfel1
69 csbeq1a
70 69 eleq1d
71 68 70 rspc
72 66 71 mpan9
73 72 elexd
74 nfcv ${⊢}\underset{_}{Ⅎ}{w}\phantom{\rule{.4em}{0ex}}\sum _{{k}\in {y}}{C}$
75 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{y}$
76 nfcsb1v
77 75 76 nfsum
78 csbeq1a
79 78 sumeq2sdv
80 74 77 79 cbvmpt
81 simpr
82 80 81 eqbrtrrid
83 nfcv
84 83 67 69 cbvmpt
85 4 ralrimiva
87 nfcv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{A}$
88 87 59 nfmpt
89 nfcv
90 nfcsb1v
91 88 89 90 nfbr
92 61 mpteq2dv
93 csbeq1a
94 92 93 breq12d
95 91 94 rspc
96 52 86 95 sylc
98 84 97 eqbrtrrid
99 47 73 82 98 rlimadd
100 simprl ${⊢}\left({\phi }\wedge \left(¬{z}\in {y}\wedge {y}\cup \left\{{z}\right\}\subseteq {B}\right)\right)\to ¬{z}\in {y}$
101 disjsn ${⊢}{y}\cap \left\{{z}\right\}=\varnothing ↔¬{z}\in {y}$
102 100 101 sylibr ${⊢}\left({\phi }\wedge \left(¬{z}\in {y}\wedge {y}\cup \left\{{z}\right\}\subseteq {B}\right)\right)\to {y}\cap \left\{{z}\right\}=\varnothing$
103 102 adantr ${⊢}\left(\left({\phi }\wedge \left(¬{z}\in {y}\wedge {y}\cup \left\{{z}\right\}\subseteq {B}\right)\right)\wedge {x}\in {A}\right)\to {y}\cap \left\{{z}\right\}=\varnothing$
104 eqidd ${⊢}\left(\left({\phi }\wedge \left(¬{z}\in {y}\wedge {y}\cup \left\{{z}\right\}\subseteq {B}\right)\right)\wedge {x}\in {A}\right)\to {y}\cup \left\{{z}\right\}={y}\cup \left\{{z}\right\}$
105 2 adantr ${⊢}\left({\phi }\wedge \left(¬{z}\in {y}\wedge {y}\cup \left\{{z}\right\}\subseteq {B}\right)\right)\to {B}\in \mathrm{Fin}$
106 105 48 ssfid ${⊢}\left({\phi }\wedge \left(¬{z}\in {y}\wedge {y}\cup \left\{{z}\right\}\subseteq {B}\right)\right)\to {y}\cup \left\{{z}\right\}\in \mathrm{Fin}$
107 106 adantr ${⊢}\left(\left({\phi }\wedge \left(¬{z}\in {y}\wedge {y}\cup \left\{{z}\right\}\subseteq {B}\right)\right)\wedge {x}\in {A}\right)\to {y}\cup \left\{{z}\right\}\in \mathrm{Fin}$
108 48 sselda ${⊢}\left(\left({\phi }\wedge \left(¬{z}\in {y}\wedge {y}\cup \left\{{z}\right\}\subseteq {B}\right)\right)\wedge {k}\in \left({y}\cup \left\{{z}\right\}\right)\right)\to {k}\in {B}$
109 108 adantlr ${⊢}\left(\left(\left({\phi }\wedge \left(¬{z}\in {y}\wedge {y}\cup \left\{{z}\right\}\subseteq {B}\right)\right)\wedge {x}\in {A}\right)\wedge {k}\in \left({y}\cup \left\{{z}\right\}\right)\right)\to {k}\in {B}$
110 109 57 syldan ${⊢}\left(\left(\left({\phi }\wedge \left(¬{z}\in {y}\wedge {y}\cup \left\{{z}\right\}\subseteq {B}\right)\right)\wedge {x}\in {A}\right)\wedge {k}\in \left({y}\cup \left\{{z}\right\}\right)\right)\to {C}\in ℂ$
111 103 104 107 110 fsumsplit ${⊢}\left(\left({\phi }\wedge \left(¬{z}\in {y}\wedge {y}\cup \left\{{z}\right\}\subseteq {B}\right)\right)\wedge {x}\in {A}\right)\to \sum _{{k}\in {y}\cup \left\{{z}\right\}}{C}=\sum _{{k}\in {y}}{C}+\sum _{{k}\in \left\{{z}\right\}}{C}$
112 nfcv ${⊢}\underset{_}{Ⅎ}{w}\phantom{\rule{.4em}{0ex}}{C}$
113 nfcsb1v
114 csbeq1a
115 112 113 114 cbvsumi
116 csbeq1
117 116 sumsn
118 53 64 117 syl2anc
119 115 118 syl5eq
120 119 oveq2d
121 111 120 eqtrd
122 121 mpteq2dva
124 nfcv
125 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}+$
126 77 125 67 nfov
127 79 69 oveq12d
128 124 126 127 cbvmpt
129 123 128 eqtrdi
130 eqidd ${⊢}\left({\phi }\wedge \left(¬{z}\in {y}\wedge {y}\cup \left\{{z}\right\}\subseteq {B}\right)\right)\to {y}\cup \left\{{z}\right\}={y}\cup \left\{{z}\right\}$
131 rlimcl
132 4 131 syl ${⊢}\left({\phi }\wedge {k}\in {B}\right)\to {D}\in ℂ$
133 132 adantlr ${⊢}\left(\left({\phi }\wedge \left(¬{z}\in {y}\wedge {y}\cup \left\{{z}\right\}\subseteq {B}\right)\right)\wedge {k}\in {B}\right)\to {D}\in ℂ$
134 108 133 syldan ${⊢}\left(\left({\phi }\wedge \left(¬{z}\in {y}\wedge {y}\cup \left\{{z}\right\}\subseteq {B}\right)\right)\wedge {k}\in \left({y}\cup \left\{{z}\right\}\right)\right)\to {D}\in ℂ$
135 102 130 106 134 fsumsplit ${⊢}\left({\phi }\wedge \left(¬{z}\in {y}\wedge {y}\cup \left\{{z}\right\}\subseteq {B}\right)\right)\to \sum _{{k}\in {y}\cup \left\{{z}\right\}}{D}=\sum _{{k}\in {y}}{D}+\sum _{{k}\in \left\{{z}\right\}}{D}$
136 nfcv ${⊢}\underset{_}{Ⅎ}{w}\phantom{\rule{.4em}{0ex}}{D}$
137 nfcsb1v
138 csbeq1a
139 136 137 138 cbvsumi
140 133 ralrimiva ${⊢}\left({\phi }\wedge \left(¬{z}\in {y}\wedge {y}\cup \left\{{z}\right\}\subseteq {B}\right)\right)\to \forall {k}\in {B}\phantom{\rule{.4em}{0ex}}{D}\in ℂ$
141 90 nfel1
142 93 eleq1d
143 141 142 rspc
144 52 140 143 sylc
145 csbeq1
146 145 sumsn
147 52 144 146 syl2anc
148 139 147 syl5eq
149 148 oveq2d
150 135 149 eqtrd