Theorem isummulc1ALT 7213

Description: Older isummulc1 7212 proved without using iserzmulc1 7136.

Hypothesis

Ref	Expression
isummulc1ALT.1	|- F e. V

Assertion

Ref	Expression
isummulc1ALT	|- (((M e. ZZ /\ C e. CC) /\ (A.k e. (ZZ>` M)(F` k) e. CC /\ E.x(<.M, + >. seq F) ~~> x)) -> (C x. sum_k e. (ZZ>` M)(F` k)) = sum_k e. (ZZ>` M)(C x. (F` k)))

Distinct variable groups:   x,k,C   k,F,x   k,M,x

Proof of Theorem isummulc1ALT

Step	Hyp	Ref	Expression
1		isummulc1ALT.1	. . . . . . . . 9 |- F e. V
2		visset 1813	. . . . . . . . 9 |- x e. V
3	1, 2	isumclimt 7196	. . . . . . . 8 |- ((M e. ZZ /\ (<.M, + >. seq F) ~~> x) -> sum_k e. (ZZ>` M)(F` k) = x)
4	3	opreq2d 3976	. . . . . . 7 |- ((M e. ZZ /\ (<.M, + >. seq F) ~~> x) -> (C x. sum_k e. (ZZ>` M)(F` k)) = (C x. x))
5	4	3ad2antl1 809	. . . . . 6 |- (((M e. ZZ /\ C e. CC /\ A.k e. (ZZ>` M)(F` k) e. CC) /\ (<.M, + >. seq F) ~~> x) -> (C x. sum_k e. (ZZ>` M)(F` k)) = (C x. x))
6		oprex 3983	. . . . . . . 8 |- (C x. (F` k)) e. V
7		eqid 1475	. . . . . . . 8 |- {<.k, y>. | (k e. (ZZ>` M) /\ y = (C x. (F` k)))} = {<.k, y>. | (k e. (ZZ>` M) /\ y = (C x. (F` k)))}
8		oprex 3983	. . . . . . . 8 |- (C x. x) e. V
9	6, 7, 8	isumclim4t 7201	. . . . . . 7 |- ((M e. ZZ /\ (<.M, + >. seq {<.k, y>. | (k e. (ZZ>` M) /\ y = (C x. (F` k)))}) ~~> (C x. x)) -> sum_k e. (ZZ>` M)(C x. (F` k)) = (C x. x))
10		3simp1 788	. . . . . . . 8 |- ((M e. ZZ /\ C e. CC /\ A.k e. (ZZ>` M)(F` k) e. CC) -> M e. ZZ)
11	10	adantr 389	. . . . . . 7 |- (((M e. ZZ /\ C e. CC /\ A.k e. (ZZ>` M)(F` k) e. CC) /\ (<.M, + >. seq F) ~~> x) -> M e. ZZ)
12		oprex 3983	. . . . . . . . 9 |- (<.M, + >. seq F) e. V
13		oprex 3983	. . . . . . . . 9 |- (<.M, + >. seq {<.k, y>. | (k e. (ZZ>` M) /\ y = (C x. (F` k)))}) e. V
14	12, 13, 2	climmulc2 7129	. . . . . . . 8 |- (((C e. CC /\ (<.M, + >. seq F) ~~> x) /\ (M e. ZZ /\ A.n e. (ZZ>` M)(((<.M, + >. seq F)` n) e. CC /\ ((<.M, + >. seq {<.k, y>. | (k e. (ZZ>` M) /\ y = (C x. (F` k)))})` n) = (C x. ((<.M, + >. seq F)` n))))) -> (<.M, + >. seq {<.k, y>. | (k e. (ZZ>` M) /\ y = (C x. (F` k)))}) ~~> (C x. x))
15		3simp2 789	. . . . . . . . 9 |- ((M e. ZZ /\ C e. CC /\ A.k e. (ZZ>` M)(F` k) e. CC) -> C e. CC)
16	15	anim1i 334	. . . . . . . 8 |- (((M e. ZZ /\ C e. CC /\ A.k e. (ZZ>` M)(F` k) e. CC) /\ (<.M, + >. seq F) ~~> x) -> (C e. CC /\ (<.M, + >. seq F) ~~> x))
17	1	serzcl2t 7049	. . . . . . . . . . . . . . . . 17 |- ((n e. (ZZ>` M) /\ A.m e. (ZZ>` M)(F` m) e. CC) -> ((<.M, + >. seq F)` n) e. CC)
18	17	3adant2 798	. . . . . . . . . . . . . . . 16 |- ((n e. (ZZ>` M) /\ C e. CC /\ A.m e. (ZZ>` M)(F` m) e. CC) -> ((<.M, + >. seq F)` n) e. CC)
19		fvex 3732	. . . . . . . . . . . . . . . . . . . 20 |- (ZZ>` M) e. V
20	19	opabex2 3610	. . . . . . . . . . . . . . . . . . 19 |- {<.k, y>. | (k e. (ZZ>` M) /\ y = (C x. (F` k)))} e. V
21	1, 20	serzmulc1 7057	. . . . . . . . . . . . . . . . . 18 |- ((n e. (ZZ>` M) /\ C e. CC /\ A.m e. (M...n)((F` m) e. CC /\ ({<.k, y>. | (k e. (ZZ>` M) /\ y = (C x. (F` k)))}` m) = (C x. (F` m)))) -> (C x. ((<.M, + >. seq F)` n)) = ((<.M, + >. seq {<.k, y>. | (k e. (ZZ>` M) /\ y = (C x. (F` k)))})` n))
22		fveq2 3724	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (k = m -> (F` k) = (F` m))
23	22	opreq2d 3976	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (k = m -> (C x. (F` k)) = (C x. (F` m)))
24		oprex 3983	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (C x. (F` m)) e. V
25	23, 7, 24	fvopab4 3780	. . . . . . . . . . . . . . . . . . . . . . 23 |- (m e. (ZZ>` M) -> ({<.k, y>. | (k e. (ZZ>` M) /\ y = (C x. (F` k)))}` m) = (C x. (F` m)))
26	25	anim2i 335	. . . . . . . . . . . . . . . . . . . . . 22 |- (((F` m) e. CC /\ m e. (ZZ>` M)) -> ((F` m) e. CC /\ ({<.k, y>. | (k e. (ZZ>` M) /\ y = (C x. (F` k)))}` m) = (C x. (F` m))))
27	26	expcom 374	. . . . . . . . . . . . . . . . . . . . 21 |- (m e. (ZZ>` M) -> ((F` m) e. CC -> ((F` m) e. CC /\ ({<.k, y>. | (k e. (ZZ>` M) /\ y = (C x. (F` k)))}` m) = (C x. (F` m)))))
28	27	a2i 9	. . . . . . . . . . . . . . . . . . . 20 |- ((m e. (ZZ>` M) -> (F` m) e. CC) -> (m e. (ZZ>` M) -> ((F` m) e. CC /\ ({<.k, y>. | (k e. (ZZ>` M) /\ y = (C x. (F` k)))}` m) = (C x. (F` m)))))
29		elfzuzt 6488	. . . . . . . . . . . . . . . . . . . 20 |- (m e. (M...n) -> m e. (ZZ>` M))
30	28, 29	syl5 21	. . . . . . . . . . . . . . . . . . 19 |- ((m e. (ZZ>` M) -> (F` m) e. CC) -> (m e. (M...n) -> ((F` m) e. CC /\ ({<.k, y>. | (k e. (ZZ>` M) /\ y = (C x. (F` k)))}` m) = (C x. (F` m)))))
31	30	r19.20i2 1703	. . . . . . . . . . . . . . . . . 18 |- (A.m e. (ZZ>` M)(F` m) e. CC -> A.m e. (M...n)((F` m) e. CC /\ ({<.k, y>. | (k e. (ZZ>` M) /\ y = (C x. (F` k)))}` m) = (C x. (F` m))))
32	21, 31	syl3an3 861	. . . . . . . . . . . . . . . . 17 |- ((n e. (ZZ>` M) /\ C e. CC /\ A.m e. (ZZ>` M)(F` m) e. CC) -> (C x. ((<.M, + >. seq F)` n)) = ((<.M, + >. seq {<.k, y>. | (k e. (ZZ>` M) /\ y = (C x. (F` k)))})` n))
33	32	eqcomd 1480	. . . . . . . . . . . . . . . 16 |- ((n e. (ZZ>` M) /\ C e. CC /\ A.m e. (ZZ>` M)(F` m) e. CC) -> ((<.M, + >. seq {<.k, y>. | (k e. (ZZ>` M) /\ y = (C x. (F` k)))})` n) = (C x. ((<.M, + >. seq F)` n)))
34	18, 33	jca 288	. . . . . . . . . . . . . . 15 |- ((n e. (ZZ>` M) /\ C e. CC /\ A.m e. (ZZ>` M)(F` m) e. CC) -> (((<.M, + >. seq F)` n) e. CC /\ ((<.M, + >. seq {<.k, y>. | (k e. (ZZ>` M) /\ y = (C x. (F` k)))})` n) = (C x. ((<.M, + >. seq F)` n))))
35	34	3coml 840	. . . . . . . . . . . . . 14 |- ((C e. CC /\ A.m e. (ZZ>` M)(F` m) e. CC /\ n e. (ZZ>` M)) -> (((<.M, + >. seq F)` n) e. CC /\ ((<.M, + >. seq {<.k, y>. | (k e. (ZZ>` M) /\ y = (C x. (F` k)))})` n) = (C x. ((<.M, + >. seq F)` n))))
36	35	3expa 833	. . . . . . . . . . . . 13 |- (((C e. CC /\ A.m e. (ZZ>` M)(F` m) e. CC) /\ n e. (ZZ>` M)) -> (((<.M, + >. seq F)` n) e. CC /\ ((<.M, + >. seq {<.k, y>. | (k e. (ZZ>` M) /\ y = (C x. (F` k)))})` n) = (C x. ((<.M, + >. seq F)