Theorem fsumrlim 14543

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.)

Hypotheses

Ref	Expression
fsumrlim.1	|- ( ph -> A C_ RR )
fsumrlim.2	|- ( ph -> B e. Fin )
fsumrlim.3	|- ( ( ph /\ ( x e. A /\ k e. B ) ) -> C e. V )
fsumrlim.4	|- ( ( ph /\ k e. B ) -> ( x e. A |-> C ) ~~> r D )

Assertion

Ref	Expression
fsumrlim	|- ( ph -> ( x e. A |-> sum_ k e. B C ) ~~> r sum_ k e. B D )

Distinct variable groups:   x, k, A   B, k, x   ph, k, x

Allowed substitution hints:   C( x, k)   D( x, k)   V( x, k)

Proof of Theorem fsumrlim

Dummy variables w y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ssid 3624	. 2 |- B C_ B
2		fsumrlim.2	. . 3 |- ( ph -> B e. Fin )
3		sseq1 3626	. . . . . 6 |- ( w = (/) -> ( w C_ B <-> (/) C_ B ) )
4		sumeq1 14419	. . . . . . . . 9 |- ( w = (/) -> sum_ k e. w C = sum_ k e. (/) C )
5		sum0 14452	. . . . . . . . 9 |- sum_ k e. (/) C = 0
6	4, 5	syl6eq 2672	. . . . . . . 8 |- ( w = (/) -> sum_ k e. w C = 0 )
7	6	mpteq2dv 4745	. . . . . . 7 |- ( w = (/) -> ( x e. A |-> sum_ k e. w C ) = ( x e. A |-> 0 ) )
8		sumeq1 14419	. . . . . . . 8 |- ( w = (/) -> sum_ k e. w D = sum_ k e. (/) D )
9		sum0 14452	. . . . . . . 8 |- sum_ k e. (/) D = 0
10	8, 9	syl6eq 2672	. . . . . . 7 |- ( w = (/) -> sum_ k e. w D = 0 )
11	7, 10	breq12d 4666	. . . . . 6 |- ( w = (/) -> ( ( x e. A |-> sum_ k e. w C ) ~~> r sum_ k e. w D <-> ( x e. A |-> 0 ) ~~> r 0 ) )
12	3, 11	imbi12d 334	. . . . 5 |- ( w = (/) -> ( ( w C_ B -> ( x e. A |-> sum_ k e. w C ) ~~> r sum_ k e. w D ) <-> ( (/) C_ B -> ( x e. A |-> 0 ) ~~> r 0 ) ) )
13	12	imbi2d 330	. . . 4 |- ( w = (/) -> ( ( ph -> ( w C_ B -> ( x e. A |-> sum_ k e. w C ) ~~> r sum_ k e. w D ) ) <-> ( ph -> ( (/) C_ B -> ( x e. A |-> 0 ) ~~> r 0 ) ) ) )
14		sseq1 3626	. . . . . 6 |- ( w = y -> ( w C_ B <-> y C_ B ) )
15		sumeq1 14419	. . . . . . . 8 |- ( w = y -> sum_ k e. w C = sum_ k e. y C )
16	15	mpteq2dv 4745	. . . . . . 7 |- ( w = y -> ( x e. A |-> sum_ k e. w C ) = ( x e. A |-> sum_ k e. y C ) )
17		sumeq1 14419	. . . . . . 7 |- ( w = y -> sum_ k e. w D = sum_ k e. y D )
18	16, 17	breq12d 4666	. . . . . 6 |- ( w = y -> ( ( x e. A |-> sum_ k e. w C ) ~~> r sum_ k e. w D <-> ( x e. A |-> sum_ k e. y C ) ~~> r sum_ k e. y D ) )
19	14, 18	imbi12d 334	. . . . 5 |- ( w = y -> ( ( w C_ B -> ( x e. A |-> sum_ k e. w C ) ~~> r sum_ k e. w D ) <-> ( y C_ B -> ( x e. A |-> sum_ k e. y C ) ~~> r sum_ k e. y D ) ) )
20	19	imbi2d 330	. . . 4 |- ( w = y -> ( ( ph -> ( w C_ B -> ( x e. A |-> sum_ k e. w C ) ~~> r sum_ k e. w D ) ) <-> ( ph -> ( y C_ B -> ( x e. A |-> sum_ k e. y C ) ~~> r sum_ k e. y D ) ) ) )
21		sseq1 3626	. . . . . 6 |- ( w = ( y u. { z } ) -> ( w C_ B <-> ( y u. { z } ) C_ B ) )
22		sumeq1 14419	. . . . . . . 8 |- ( w = ( y u. { z } ) -> sum_ k e. w C = sum_ k e. ( y u. { z } ) C )
23	22	mpteq2dv 4745	. . . . . . 7 |- ( w = ( y u. { z } ) -> ( x e. A |-> sum_ k e. w C ) = ( x e. A |-> sum_ k e. ( y u. { z } ) C ) )
24		sumeq1 14419	. . . . . . 7 |- ( w = ( y u. { z } ) -> sum_ k e. w D = sum_ k e. ( y u. { z } ) D )
25	23, 24	breq12d 4666	. . . . . 6 |- ( w = ( y u. { z } ) -> ( ( x e. A |-> sum_ k e. w C ) ~~> r sum_ k e. w D <-> ( x e. A |-> sum_ k e. ( y u. { z } ) C ) ~~> r sum_ k e. ( y u. { z } ) D ) )
26	21, 25	imbi12d 334	. . . . 5 |- ( w = ( y u. { z } ) -> ( ( w C_ B -> ( x e. A |-> sum_ k e. w C ) ~~> r sum_ k e. w D ) <-> ( ( y u. { z } ) C_ B -> ( x e. A |-> sum_ k e. ( y u. { z } ) C ) ~~> r sum_ k e. ( y u. { z } ) D ) ) )
27	26	imbi2d 330	. . . 4 |- ( w = ( y u. { z } ) -> ( ( ph -> ( w C_ B -> ( x e. A |-> sum_ k e. w C ) ~~> r sum_ k e. w D ) ) <-> ( ph -> ( ( y u. { z } ) C_ B -> ( x e. A |-> sum_ k e. ( y u. { z } ) C ) ~~> r sum_ k e. ( y u. { z } ) D ) ) ) )
28		sseq1 3626	. . . . . 6 |- ( w = B -> ( w C_ B <-> B C_ B ) )
29		sumeq1 14419	. . . . . . . 8 |- ( w = B -> sum_ k e. w C = sum_ k e. B C )
30	29	mpteq2dv 4745	. . . . . . 7 |- ( w = B -> ( x e. A |-> sum_ k e. w C ) = ( x e. A |-> sum_ k e. B C ) )
31		sumeq1 14419	. . . . . . 7 |- ( w = B -> sum_ k e. w D = sum_ k e. B D )
32	30, 31	breq12d 4666	. . . . . 6 |- ( w = B -> ( ( x e. A |-> sum_ k e. w C ) ~~> r sum_ k e. w D <-> ( x e. A |-> sum_ k e. B C ) ~~> r sum_ k e. B D ) )
33	28, 32	imbi12d 334	. . . . 5 |- ( w = B -> ( ( w C_ B -> ( x e. A |-> sum_ k e. w C ) ~~> r sum_ k e. w D ) <-> ( B C_ B -> ( x e. A |-> sum_ k e. B C ) ~~> r sum_ k e. B D ) ) )
34	33	imbi2d 330	. . . 4 |- ( w = B -> ( ( ph -> ( w C_ B -> ( x e. A |-> sum_ k e. w C ) ~~> r sum_ k e. w D ) ) <-> ( ph -> ( B C_ B -> ( x e. A |-> sum_ k e. B C ) ~~> r sum_ k e. B D ) ) ) )
35		fsumrlim.1	. . . . . 6 |- ( ph -> A C_ RR )
36		0cn 10032	. . . . . 6 |- 0 e. CC
37		rlimconst 14275	. . . . . 6 |- ( ( A C_ RR /\ 0 e. CC ) -> ( x e. A |-> 0 ) ~~> r 0 )
38	35, 36, 37	sylancl 694	. . . . 5 |- ( ph -> ( x e. A |-> 0 ) ~~> r 0 )
39	38	a1d 25	. . . 4 |- ( ph -> ( (/) C_ B -> ( x e. A |-> 0 ) ~~> r 0 ) )
40		ssun1 3776	. . . . . . . . . 10 |- y C_ ( y u. { z } )
41		sstr 3611	. . . . . . . . . 10 |- ( ( y C_ ( y u. { z } ) /\ ( y u. { z } ) C_ B ) -> y C_ B )
42	40, 41	mpan 706	. . . . . . . . 9 |- ( ( y u. { z } ) C_ B -> y C_ B )
43	42	imim1i 63	. . . . . . . 8 |- ( ( y C_ B -> ( x e. A |-> sum_ k e. y C ) ~~> r sum_ k e. y D ) -> ( ( y u. { z } ) C_ B -> ( x e. A |-> sum_ k e. y C ) ~~> r sum_ k e. y D ) )
44		sumex 14418	. . . . . . . . . . . . . 14 |- sum_ k e. y [_ w / x ]_ C e. _V
45	44	a1i 11	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ ( x e. A |-> sum_ k e. y C ) ~~> r sum_ k e. y D ) /\ w e. A ) -> sum_ k e. y [_ w / x ]_ C e. _V )
46		simprr 796	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) -> ( y u. { z } ) C_ B )
47	46	unssbd 3791	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) -> { z } C_ B )
48		vex 3203	. . . . . . . . . . . . . . . . . . . . 21 |- z e. _V
49	48	snss 4316	. . . . . . . . . . . . . . . . . . . 20 |- ( z e. B <-> { z } C_ B )
50	47, 49	sylibr 224	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) -> z e. B )
51	50	adantr 481	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ x e. A ) -> z e. B )
52		fsumrlim.3	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ ( x e. A /\ k e. B ) ) -> C e. V )
53	52	anass1rs 849	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ k e. B ) /\ x e. A ) -> C e. V )
54		fsumrlim.4	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ k e. B ) -> ( x e. A |-> C ) ~~> r D )
55	53, 54	rlimmptrcl 14338	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ k e. B ) /\ x e. A ) -> C e. CC )
56	55	an32s 846	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ x e. A ) /\ k e. B ) -> C e. CC )
57	56	adantllr 755	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ x e. A ) /\ k e. B ) -> C e. CC )
58	57	ralrimiva 2966	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ x e. A ) -> A. k e. B C e. CC )
59		nfcsb1v 3549	. . . . . . . . . . . . . . . . . . . 20 |- F/_ k [_ z / k ]_ C
60	59	nfel1 2779	. . . . . . . . . . . . . . . . . . 19 |- F/ k [_ z / k ]_ C e. CC
61		csbeq1a 3542	. . . . . . . . . . . . . . . . . . . 20 |- ( k = z -> C = [_ z / k ]_ C )
62	61	eleq1d 2686	. . . . . . . . . . . . . . . . . . 19 |- ( k = z -> ( C e. CC <-> [_ z / k ]_ C e. CC ) )
63	60, 62	rspc 3303	. . . . . . . . . . . . . . . . . 18 |- ( z e. B -> ( A. k e. B C e. CC -> [_ z / k ]_ C e. CC ) )
64	51, 58, 63	sylc 65	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ x e. A ) -> [_ z / k ]_ C e. CC )
65	64	ralrimiva 2966	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) -> A. x e. A [_ z / k ]_ C e. CC )
66	65	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ ( x e. A |-> sum_ k e. y C ) ~~> r sum_ k e. y D ) -> A. x e. A [_ z / k ]_ C e. CC )
67		nfcsb1v 3549	. . . . . . . . . . . . . . . . 17 |- F/_ x [_ w / x ]_ [_ z / k ]_ C
68	67	nfel1 2779	. . . . . . . . . . . . . . . 16 |- F/ x [_ w / x ]_ [_ z / k ]_ C e. CC
69		csbeq1a 3542	. . . . . . . . . . . . . . . . 17 |- ( x = w -> [_ z / k ]_ C = [_ w / x ]_ [_ z / k ]_ C )
70	69	eleq1d 2686	. . . . . . . . . . . . . . . 16 |- ( x = w -> ( [_ z / k ]_ C e. CC <-> [_ w / x ]_ [_ z / k ]_ C e. CC ) )
71	68, 70	rspc 3303	. . . . . . . . . . . . . . 15 |- ( w e. A -> ( A. x e. A [_ z / k ]_ C e. CC -> [_ w / x ]_ [_ z / k ]_ C e. CC ) )
72	66, 71	mpan9 486	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ ( x e. A |-> sum_ k e. y C ) ~~> r sum_ k e. y D ) /\ w e. A ) -> [_ w / x ]_ [_ z / k ]_ C e. CC )
73		elex 3212	. . . . . . . . . . . . . 14 |- ( [_ w / x ]_ [_ z / k ]_ C e. CC -> [_ w / x ]_ [_ z / k ]_ C e. _V )
74	72, 73	syl 17	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ ( x e. A |-> sum_ k e. y C ) ~~> r sum_ k e. y D ) /\ w e. A ) -> [_ w / x ]_ [_ z / k ]_ C e. _V )
75		nfcv 2764	. . . . . . . . . . . . . . 15 |- F/_ w sum_ k e. y C
76		nfcv 2764	. . . . . . . . . . . . . . . 16 |- F/_ x y
77		nfcsb1v 3549	. . . . . . . . . . . . . . . 16 |- F/_ x [_ w / x ]_ C
78	76, 77	nfsum 14421	. . . . . . . . . . . . . . 15 |- F/_ x sum_ k e. y [_ w / x ]_ C
79		csbeq1a 3542	. . . . . . . . . . . . . . . 16 |- ( x = w -> C = [_ w / x ]_ C )
80	79	sumeq2sdv 14435	. . . . . . . . . . . . . . 15 |- ( x = w -> sum_ k e. y C = sum_ k e. y [_ w / x ]_ C )
81	75, 78, 80	cbvmpt 4749	. . . . . . . . . . . . . 14 |- ( x e. A |-> sum_ k e. y C ) = ( w e. A |-> sum_ k e. y [_ w / x ]_ C )
82		simpr 477	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ ( x e. A |-> sum_ k e. y C ) ~~> r sum_ k e. y D ) -> ( x e. A |-> sum_ k e. y C ) ~~> r sum_ k e. y D )
83	81, 82	syl5eqbrr 4689	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ ( x e. A |-> sum_ k e. y C ) ~~> r sum_ k e. y D ) -> ( w e. A |-> sum_ k e. y [_ w / x ]_ C ) ~~> r sum_ k e. y D )
84		nfcv 2764	. . . . . . . . . . . . . . 15 |- F/_ w [_ z / k ]_ C
85	84, 67, 69	cbvmpt 4749	. . . . . . . . . . . . . 14 |- ( x e. A |-> [_ z / k ]_ C ) = ( w e. A |-> [_ w / x ]_ [_ z / k ]_ C )
86	54	ralrimiva 2966	. . . . . . . . . . . . . . . . 17 |- ( ph -> A. k e. B ( x e. A |-> C ) ~~> r D )
87	86	adantr 481	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) -> A. k e. B ( x e. A |-> C ) ~~> r D )
88		nfcv 2764	. . . . . . . . . . . . . . . . . . 19 |- F/_ k A
89	88, 59	nfmpt 4746	. . . . . . . . . . . . . . . . . 18 |- F/_ k ( x e. A |-> [_ z / k ]_ C )
90		nfcv 2764	. . . . . . . . . . . . . . . . . 18 |- F/_ k ~~> r
91		nfcsb1v 3549	. . . . . . . . . . . . . . . . . 18 |- F/_ k [_ z / k ]_ D
92	89, 90, 91	nfbr 4699	. . . . . . . . . . . . . . . . 17 |- F/ k ( x e. A |-> [_ z / k ]_ C ) ~~> r [_ z / k ]_ D
93	61	mpteq2dv 4745	. . . . . . . . . . . . . . . . . 18 |- ( k = z -> ( x e. A |-> C ) = ( x e. A |-> [_ z / k ]_ C ) )
94		csbeq1a 3542	. . . . . . . . . . . . . . . . . 18 |- ( k = z -> D = [_ z / k ]_ D )
95	93, 94	breq12d 4666	. . . . . . . . . . . . . . . . 17 |- ( k = z -> ( ( x e. A |-> C ) ~~> r D <-> ( x e. A |-> [_ z / k ]_ C ) ~~> r [_ z / k ]_ D ) )
96	92, 95	rspc 3303	. . . . . . . . . . . . . . . 16 |- ( z e. B -> ( A. k e. B ( x e. A |-> C ) ~~> r D -> ( x e. A |-> [_ z / k ]_ C ) ~~> r [_ z / k ]_ D ) )
97	50, 87, 96	sylc 65	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) -> ( x e. A |-> [_ z / k ]_ C ) ~~> r [_ z / k ]_ D )
98	97	adantr 481	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ ( x e. A |-> sum_ k e. y C ) ~~> r sum_ k e. y D ) -> ( x e. A |-> [_ z / k ]_ C ) ~~> r [_ z / k ]_ D )
99	85, 98	syl5eqbrr 4689	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ ( x e. A |-> sum_ k e. y C ) ~~> r sum_ k e. y D ) -> ( w e. A |-> [_ w / x ]_ [_ z / k ]_ C ) ~~> r [_ z / k ]_ D )
100	45, 74, 83, 99	rlimadd 14373	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ ( x e. A |-> sum_ k e. y C ) ~~> r sum_ k e. y D ) -> ( w e. A |-> ( sum_ k e. y [_ w / x ]_ C + [_ w / x ]_ [_ z / k ]_ C ) ) ~~> r ( sum_ k e. y D + [_ z / k ]_ D ) )
101		simprl 794	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) -> -. z e. y )
102		disjsn 4246	. . . . . . . . . . . . . . . . . . 19 |- ( ( y i^i { z } ) = (/) <-> -. z e. y )
103	101, 102	sylibr 224	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) -> ( y i^i { z } ) = (/) )
104	103	adantr 481	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ x e. A ) -> ( y i^i { z } ) = (/) )
105		eqidd 2623	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ x e. A ) -> ( y u. { z } ) = ( y u. { z } ) )
106	2	adantr 481	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) -> B e. Fin )
107		ssfi 8180	. . . . . . . . . . . . . . . . . . 19 |- ( ( B e. Fin /\ ( y u. { z } ) C_ B ) -> ( y u. { z } ) e. Fin )
108	106, 46, 107	syl2anc 693	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) -> ( y u. { z } ) e. Fin )
109	108	adantr 481	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ x e. A ) -> ( y u. { z } ) e. Fin )
110	46	sselda 3603	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ k e. ( y u. { z } ) ) -> k e. B )
111	110	adantlr 751	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ x e. A ) /\ k e. ( y u. { z } ) ) -> k e. B )
112	111, 57	syldan 487	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ x e. A ) /\ k e. ( y u. { z } ) ) -> C e. CC )
113	104, 105, 109, 112	fsumsplit 14471	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ x e. A ) -> sum_ k e. ( y u. { z } ) C = ( sum_ k e. y C + sum_ k e. { z } C ) )
114		nfcv 2764	. . . . . . . . . . . . . . . . . . 19 |- F/_ w C
115		nfcsb1v 3549	. . . . . . . . . . . . . . . . . . 19 |- F/_ k [_ w / k ]_ C
116		csbeq1a 3542	. . . . . . . . . . . . . . . . . . 19 |- ( k = w -> C = [_ w / k ]_ C )
117	114, 115, 116	cbvsumi 14427	. . . . . . . . . . . . . . . . . 18 |- sum_ k e. { z } C = sum_ w e. { z } [_ w / k ]_ C
118		csbeq1 3536	. . . . . . . . . . . . . . . . . . . 20 |- ( w = z -> [_ w / k ]_ C = [_ z / k ]_ C )
119	118	sumsn 14475	. . . . . . . . . . . . . . . . . . 19 |- ( ( z e. B /\ [_ z / k ]_ C e. CC ) -> sum_ w e. { z } [_ w / k ]_ C = [_ z / k ]_ C )
120	51, 64, 119	syl2anc 693	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ x e. A ) -> sum_ w e. { z } [_ w / k ]_ C = [_ z / k ]_ C )
121	117, 120	syl5eq 2668	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ x e. A ) -> sum_ k e. { z } C = [_ z / k ]_ C )
122	121	oveq2d 6666	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ x e. A ) -> ( sum_ k e. y C + sum_ k e. { z } C ) = ( sum_ k e. y C + [_ z / k ]_ C ) )
123	113, 122	eqtrd 2656	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ x e. A ) -> sum_ k e. ( y u. { z } ) C = ( sum_ k e. y C + [_ z / k ]_ C ) )
124	123	mpteq2dva 4744	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) -> ( x e. A |-> sum_ k e. ( y u. { z } ) C ) = ( x e. A |-> ( sum_ k e. y C + [_ z / k ]_ C ) ) )
125	124	adantr 481	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ ( x e. A |-> sum_ k e. y C ) ~~> r sum_ k e. y D ) -> ( x e. A |-> sum_ k e. ( y u. { z } ) C ) = ( x e. A |-> ( sum_ k e. y C + [_ z / k ]_ C ) ) )
126		nfcv 2764	. . . . . . . . . . . . . 14 |- F/_ w ( sum_ k e. y C + [_ z / k ]_ C )
127		nfcv 2764	. . . . . . . . . . . . . . 15 |- F/_ x +
128	78, 127, 67	nfov 6676	. . . . . . . . . . . . . 14 |- F/_ x ( sum_ k e. y [_ w / x ]_ C + [_ w / x ]_ [_ z / k ]_ C )
129	80, 69	oveq12d 6668	. . . . . . . . . . . . . 14 |- ( x = w -> ( sum_ k e. y C + [_ z / k ]_ C ) = ( sum_ k e. y [_ w / x ]_ C + [_ w / x ]_ [_ z / k ]_ C ) )
130	126, 128, 129	cbvmpt 4749	. . . . . . . . . . . . 13 |- ( x e. A |-> ( sum_ k e. y C + [_ z / k ]_ C ) ) = ( w e. A |-> ( sum_ k e. y [_ w / x ]_ C + [_ w / x ]_ [_ z / k ]_ C ) )
131	125, 130	syl6eq 2672	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ ( x e. A |-> sum_ k e. y C ) ~~> r sum_ k e. y D ) -> ( x e. A |-> sum_ k e. ( y u. { z } ) C ) = ( w e. A |-> ( sum_ k e. y [_ w / x ]_ C + [_ w / x ]_ [_ z / k ]_ C ) ) )
132		eqidd 2623	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) -> ( y u. { z } ) = ( y u. { z } ) )
133		rlimcl 14234	. . . . . . . . . . . . . . . . . 18 |- ( ( x e. A |-> C ) ~~> r D -> D e. CC )
134	54, 133	syl 17	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ k e. B ) -> D e. CC )
135	134	adantlr 751	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ k e. B ) -> D e. CC )
136	110, 135	syldan 487	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ k e. ( y u. { z } ) ) -> D e. CC )
137	103, 132, 108, 136	fsumsplit 14471	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) -> sum_ k e. ( y u. { z } ) D = ( sum_ k e. y D + sum_ k e. { z } D ) )
138		nfcv 2764	. . . . . . . . . . . . . . . . 17 |- F/_ w D
139		nfcsb1v 3549	. . . . . . . . . . . . . . . . 17 |- F/_ k [_ w / k ]_ D
140		csbeq1a 3542	. . . . . . . . . . . . . . . . 17 |- ( k = w -> D = [_ w / k ]_ D )
141	138, 139, 140	cbvsumi 14427	. . . . . . . . . . . . . . . 16 |- sum_ k e. { z } D = sum_ w e. { z } [_ w / k ]_ D
142	135	ralrimiva 2966	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) -> A. k e. B D e. CC )
143	91	nfel1 2779	. . . . . . . . . . . . . . . . . . 19 |- F/ k [_ z / k ]_ D e. CC
144	94	eleq1d 2686	. . . . . . . . . . . . . . . . . . 19 |- ( k = z -> ( D e. CC <-> [_ z / k ]_ D e. CC ) )
145	143, 144	rspc 3303	. . . . . . . . . . . . . . . . . 18 |- ( z e. B -> ( A. k e. B D e. CC -> [_ z / k ]_ D e. CC ) )
146	50, 142, 145	sylc 65	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) -> [_ z / k ]_ D e. CC )
147		csbeq1 3536	. . . . . . . . . . . . . . . . . 18 |- ( w = z -> [_ w / k ]_ D = [_ z / k ]_ D )
148	147	sumsn 14475	. . . . . . . . . . . . . . . . 17 |- ( ( z e. B /\ [_ z / k ]_ D e. CC ) -> sum_ w e. { z } [_ w / k ]_ D = [_ z / k ]_ D )
149	50, 146, 148	syl2anc 693	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) -> sum_ w e. { z } [_ w / k ]_ D = [_ z / k ]_ D )
150	141, 149	syl5eq 2668	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) -> sum_ k e. { z } D = [_ z / k ]_ D )
151	150	oveq2d 6666	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) -> ( sum_ k e. y D + sum_ k e. { z } D ) = ( sum_ k e. y D + [_ z / k ]_ D ) )
152	137, 151	eqtrd 2656	. . . . . . . . . . . . 13 |- ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) -> sum_ k e. ( y u. { z } ) D = ( sum_ k e. y D + [_ z / k ]_ D ) )
153	152	adantr 481	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ ( x e. A |-> sum_ k e. y C ) ~~> r sum_ k e. y D ) -> sum_ k e. ( y u. { z } ) D = ( sum_ k e. y D + [_ z / k ]_ D ) )
154	100, 131, 153	3brtr4d 4685	. . . . . . . . . . 11 |- ( ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) /\ ( x e. A |-> sum_ k e. y C ) ~~> r sum_ k e. y D ) -> ( x e. A |-> sum_ k e. ( y u. { z } ) C ) ~~> r sum_ k e. ( y u. { z } ) D )
155	154	ex 450	. . . . . . . . . 10 |- ( ( ph /\ ( -. z e. y /\ ( y u. { z } ) C_ B ) ) -> ( ( x e. A |-> sum_ k e. y C ) ~~> r sum_ k e. y D -> ( x e. A |-> sum_ k e. ( y u. { z } ) C ) ~~> r sum_ k e. ( y u. { z } ) D ) )
156	155	expr 643	. . . . . . . . 9 |- ( ( ph /\ -. z e. y ) -> ( ( y u. { z } ) C_ B -> ( ( x e. A |-> sum_ k e. y C ) ~~> r sum_ k e. y D -> ( x e. A |-> sum_ k e. ( y u. { z } ) C ) ~~> r sum_ k e. ( y u. { z } ) D ) ) )
157	156	a2d 29	. . . . . . . 8 |- ( ( ph /\ -. z e. y ) -> ( ( ( y u. { z } ) C_ B -> ( x e. A |-> sum_ k e. y C ) ~~> r sum_ k e. y D ) -> ( ( y u. { z } ) C_ B -> ( x e. A |-> sum_ k e. ( y u. { z } ) C ) ~~> r sum_ k e. ( y u. { z } ) D ) ) )
158	43, 157	syl5 34	. . . . . . 7 |- ( ( ph /\ -. z e. y ) -> ( ( y C_ B -> ( x e. A |-> sum_ k e. y C ) ~~> r sum_ k e. y D ) -> ( ( y u. { z } ) C_ B -> ( x e. A |-> sum_ k e. ( y u. { z } ) C ) ~~> r sum_ k e. ( y u. { z } ) D ) ) )
159	158	expcom 451	. . . . . 6 |- ( -. z e. y -> ( ph -> ( ( y C_ B -> ( x e. A |-> sum_ k e. y C ) ~~> r sum_ k e. y D ) -> ( ( y u. { z } ) C_ B -> ( x e. A |-> sum_ k e. ( y u. { z } ) C ) ~~> r sum_ k e. ( y u. { z } ) D ) ) ) )
160	159	a2d 29	. . . . 5 |- ( -. z e. y -> ( ( ph -> ( y C_ B -> ( x e. A |-> sum_ k e. y C ) ~~> r sum_ k e. y D ) ) -> ( ph -> ( ( y u. { z } ) C_ B -> ( x e. A |-> sum_ k e. ( y u. { z } ) C ) ~~> r sum_ k e. ( y u. { z } ) D ) ) ) )
161	160	adantl 482	. . . 4 |- ( ( y e. Fin /\ -. z e. y ) -> ( ( ph -> ( y C_ B -> ( x e. A |-> sum_ k e. y C ) ~~> r sum_ k e. y D ) ) -> ( ph -> ( ( y u. { z } ) C_ B -> ( x e. A |-> sum_ k e. ( y u. { z } ) C ) ~~> r sum_ k e. ( y u. { z } ) D ) ) ) )
162	13, 20, 27, 34, 39, 161	findcard2s 8201	. . 3 |- ( B e. Fin -> ( ph -> ( B C_ B -> ( x e. A |-> sum_ k e. B C ) ~~> r sum_ k e. B D ) ) )
163	2, 162	mpcom 38	. 2 |- ( ph -> ( B C_ B -> ( x e. A |-> sum_ k e. B C ) ~~> r sum_ k e. B D ) )
164	1, 163	mpi 20	1 |- ( ph -> ( x e. A |-> sum_ k e. B C ) ~~> r sum_ k e. B D )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 384   = wceq 1483   e. wcel 1990   A.wral 2912   _Vcvv 3200   [_csb 3533   u. cun 3572   i^i cin 3573   C_ wss 3574   (/)c0 3915   {csn 4177   class class class wbr 4653   |-> cmpt 4729  (class class class)co 6650   Fincfn 7955   CCcc 9934   RRcr 9935   0cc0 9936   + caddc 9939   ~~> r crli 14216   sum_csu 14416

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-inf2 8538  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013  ax-pre-sup 10014  ax-addf 10015

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-fal 1489  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-se 5074  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-isom 5897  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-oadd 7564  df-er 7742  df-pm 7860  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-sup 8348  df-oi 8415  df-card 8765  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-div 10685  df-nn 11021  df-2 11079  df-3 11080  df-n0 11293  df-z 11378  df-uz 11688  df-rp 11833  df-fz 12327  df-fzo 12466  df-seq 12802  df-exp 12861  df-hash 13118  df-cj 13839  df-re 13840  df-im 13841  df-sqrt 13975  df-abs 13976  df-clim 14219  df-rlim 14220  df-sum 14417

This theorem is referenced by:  climfsum  14552  logexprlim  24950  signsplypnf  30627