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	$⊢ φ \to A \subseteq ℝ$
	fsumrlim.2	$⊢ φ \to B \in Fin$
	fsumrlim.3	$⊢ (φ \land (x \in A \land k \in B)) \to C \in V$
	fsumrlim.4	$⊢ (φ \land k \in B) \to (x \in A ⟼ C) \underset{ℝ}{⇝} D$
Assertion	fsumrlim	$⊢ φ \to (x \in A ⟼ \sum_{k \in B} C) \underset{ℝ}{⇝} \sum_{k \in B} D$

Proof

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

Metamath Proof Explorer

Theorem fsumrlim

Proof