Theorem zsum 14449

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

Hypotheses

Ref	Expression
zsum.1	|- Z = ( ZZ>= ` M )
zsum.2	|- ( ph -> M e. ZZ )
zsum.3	|- ( ph -> A C_ Z )
zsum.4	|- ( ( ph /\ k e. Z ) -> ( F ` k ) = if ( k e. A , B , 0 ) )
zsum.5	|- ( ( ph /\ k e. A ) -> B e. CC )

Assertion

Ref	Expression
zsum	|- ( ph -> sum_ k e. A B = ( ~~> ` seq M ( + , F ) ) )

Distinct variable groups:   A, k   k, F   ph, k   k, Z   k, M

Allowed substitution hint:   B( k)

Proof of Theorem zsum

Dummy variables f g i j m n x are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eleq1 2689	. . . . . . . . . . . 12 |- ( n = i -> ( n e. A <-> i e. A ) )
2		csbeq1 3536	. . . . . . . . . . . 12 |- ( n = i -> [_ n / k ]_ B = [_ i / k ]_ B )
3	1, 2	ifbieq1d 4109	. . . . . . . . . . 11 |- ( n = i -> if ( n e. A , [_ n / k ]_ B , 0 ) = if ( i e. A , [_ i / k ]_ B , 0 ) )
4	3	cbvmptv 4750	. . . . . . . . . 10 |- ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) = ( i e. ZZ |-> if ( i e. A , [_ i / k ]_ B , 0 ) )
5		simpll 790	. . . . . . . . . . 11 |- ( ( ( ph /\ m e. ZZ ) /\ A C_ ( ZZ>= ` m ) ) -> ph )
6		zsum.5	. . . . . . . . . . . . 13 |- ( ( ph /\ k e. A ) -> B e. CC )
7	6	ralrimiva 2966	. . . . . . . . . . . 12 |- ( ph -> A. k e. A B e. CC )
8		nfcsb1v 3549	. . . . . . . . . . . . . 14 |- F/_ k [_ i / k ]_ B
9	8	nfel1 2779	. . . . . . . . . . . . 13 |- F/ k [_ i / k ]_ B e. CC
10		csbeq1a 3542	. . . . . . . . . . . . . 14 |- ( k = i -> B = [_ i / k ]_ B )
11	10	eleq1d 2686	. . . . . . . . . . . . 13 |- ( k = i -> ( B e. CC <-> [_ i / k ]_ B e. CC ) )
12	9, 11	rspc 3303	. . . . . . . . . . . 12 |- ( i e. A -> ( A. k e. A B e. CC -> [_ i / k ]_ B e. CC ) )
13	7, 12	syl5 34	. . . . . . . . . . 11 |- ( i e. A -> ( ph -> [_ i / k ]_ B e. CC ) )
14	5, 13	mpan9 486	. . . . . . . . . 10 |- ( ( ( ( ph /\ m e. ZZ ) /\ A C_ ( ZZ>= ` m ) ) /\ i e. A ) -> [_ i / k ]_ B e. CC )
15		simplr 792	. . . . . . . . . 10 |- ( ( ( ph /\ m e. ZZ ) /\ A C_ ( ZZ>= ` m ) ) -> m e. ZZ )
16		zsum.2	. . . . . . . . . . 11 |- ( ph -> M e. ZZ )
17	16	ad2antrr 762	. . . . . . . . . 10 |- ( ( ( ph /\ m e. ZZ ) /\ A C_ ( ZZ>= ` m ) ) -> M e. ZZ )
18		simpr 477	. . . . . . . . . 10 |- ( ( ( ph /\ m e. ZZ ) /\ A C_ ( ZZ>= ` m ) ) -> A C_ ( ZZ>= ` m ) )
19		zsum.3	. . . . . . . . . . . 12 |- ( ph -> A C_ Z )
20		zsum.1	. . . . . . . . . . . 12 |- Z = ( ZZ>= ` M )
21	19, 20	syl6sseq 3651	. . . . . . . . . . 11 |- ( ph -> A C_ ( ZZ>= ` M ) )
22	21	ad2antrr 762	. . . . . . . . . 10 |- ( ( ( ph /\ m e. ZZ ) /\ A C_ ( ZZ>= ` m ) ) -> A C_ ( ZZ>= ` M ) )
23	4, 14, 15, 17, 18, 22	sumrb 14444	. . . . . . . . 9 |- ( ( ( ph /\ m e. ZZ ) /\ A C_ ( ZZ>= ` m ) ) -> ( seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x <-> seq M ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) )
24	23	biimpd 219	. . . . . . . 8 |- ( ( ( ph /\ m e. ZZ ) /\ A C_ ( ZZ>= ` m ) ) -> ( seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x -> seq M ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) )
25	24	expimpd 629	. . . . . . 7 |- ( ( ph /\ m e. ZZ ) -> ( ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) -> seq M ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) )
26	25	rexlimdva 3031	. . . . . 6 |- ( ph -> ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) -> seq M ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) )
27	19	ad2antrr 762	. . . . . . . . . . . . 13 |- ( ( ( ph /\ m e. NN ) /\ f : ( 1 ... m ) -1-1-onto-> A ) -> A C_ Z )
28		uzssz 11707	. . . . . . . . . . . . . . . 16 |- ( ZZ>= ` M ) C_ ZZ
29	20, 28	eqsstri 3635	. . . . . . . . . . . . . . 15 |- Z C_ ZZ
30		zssre 11384	. . . . . . . . . . . . . . 15 |- ZZ C_ RR
31	29, 30	sstri 3612	. . . . . . . . . . . . . 14 |- Z C_ RR
32		ltso 10118	. . . . . . . . . . . . . 14 |- < Or RR
33		soss 5053	. . . . . . . . . . . . . 14 |- ( Z C_ RR -> ( < Or RR -> < Or Z ) )
34	31, 32, 33	mp2 9	. . . . . . . . . . . . 13 |- < Or Z
35		soss 5053	. . . . . . . . . . . . 13 |- ( A C_ Z -> ( < Or Z -> < Or A ) )
36	27, 34, 35	mpisyl 21	. . . . . . . . . . . 12 |- ( ( ( ph /\ m e. NN ) /\ f : ( 1 ... m ) -1-1-onto-> A ) -> < Or A )
37		fzfi 12771	. . . . . . . . . . . . 13 |- ( 1 ... m ) e. Fin
38		ovex 6678	. . . . . . . . . . . . . . . 16 |- ( 1 ... m ) e. _V
39	38	f1oen 7976	. . . . . . . . . . . . . . 15 |- ( f : ( 1 ... m ) -1-1-onto-> A -> ( 1 ... m ) ~~ A )
40	39	adantl 482	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ m e. NN ) /\ f : ( 1 ... m ) -1-1-onto-> A ) -> ( 1 ... m ) ~~ A )
41	40	ensymd 8007	. . . . . . . . . . . . 13 |- ( ( ( ph /\ m e. NN ) /\ f : ( 1 ... m ) -1-1-onto-> A ) -> A ~~ ( 1 ... m ) )
42		enfii 8177	. . . . . . . . . . . . 13 |- ( ( ( 1 ... m ) e. Fin /\ A ~~ ( 1 ... m ) ) -> A e. Fin )
43	37, 41, 42	sylancr 695	. . . . . . . . . . . 12 |- ( ( ( ph /\ m e. NN ) /\ f : ( 1 ... m ) -1-1-onto-> A ) -> A e. Fin )
44		fz1iso 13246	. . . . . . . . . . . 12 |- ( ( < Or A /\ A e. Fin ) -> E. g g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) )
45	36, 43, 44	syl2anc 693	. . . . . . . . . . 11 |- ( ( ( ph /\ m e. NN ) /\ f : ( 1 ... m ) -1-1-onto-> A ) -> E. g g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) )
46		simpll 790	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. NN ) /\ ( f : ( 1 ... m ) -1-1-onto-> A /\ g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) ) ) -> ph )
47	46, 13	mpan9 486	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ m e. NN ) /\ ( f : ( 1 ... m ) -1-1-onto-> A /\ g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) ) ) /\ i e. A ) -> [_ i / k ]_ B e. CC )
48		fveq2 6191	. . . . . . . . . . . . . . . . 17 |- ( n = j -> ( f ` n ) = ( f ` j ) )
49	48	csbeq1d 3540	. . . . . . . . . . . . . . . 16 |- ( n = j -> [_ ( f ` n ) / k ]_ B = [_ ( f ` j ) / k ]_ B )
50		csbco 3543	. . . . . . . . . . . . . . . 16 |- [_ ( f ` j ) / i ]_ [_ i / k ]_ B = [_ ( f ` j ) / k ]_ B
51	49, 50	syl6eqr 2674	. . . . . . . . . . . . . . 15 |- ( n = j -> [_ ( f ` n ) / k ]_ B = [_ ( f ` j ) / i ]_ [_ i / k ]_ B )
52	51	cbvmptv 4750	. . . . . . . . . . . . . 14 |- ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) = ( j e. NN |-> [_ ( f ` j ) / i ]_ [_ i / k ]_ B )
53		eqid 2622	. . . . . . . . . . . . . 14 |- ( j e. NN |-> [_ ( g ` j ) / i ]_ [_ i / k ]_ B ) = ( j e. NN |-> [_ ( g ` j ) / i ]_ [_ i / k ]_ B )
54		simplr 792	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ m e. NN ) /\ ( f : ( 1 ... m ) -1-1-onto-> A /\ g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) ) ) -> m e. NN )
55	16	ad2antrr 762	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ m e. NN ) /\ ( f : ( 1 ... m ) -1-1-onto-> A /\ g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) ) ) -> M e. ZZ )
56	21	ad2antrr 762	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ m e. NN ) /\ ( f : ( 1 ... m ) -1-1-onto-> A /\ g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) ) ) -> A C_ ( ZZ>= ` M ) )
57		simprl 794	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ m e. NN ) /\ ( f : ( 1 ... m ) -1-1-onto-> A /\ g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) ) ) -> f : ( 1 ... m ) -1-1-onto-> A )
58		simprr 796	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ m e. NN ) /\ ( f : ( 1 ... m ) -1-1-onto-> A /\ g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) ) ) -> g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) )
59	4, 47, 52, 53, 54, 55, 56, 57, 58	summolem2a 14446	. . . . . . . . . . . . 13 |- ( ( ( ph /\ m e. NN ) /\ ( f : ( 1 ... m ) -1-1-onto-> A /\ g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) ) ) -> seq M ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) )
60	59	expr 643	. . . . . . . . . . . 12 |- ( ( ( ph /\ m e. NN ) /\ f : ( 1 ... m ) -1-1-onto-> A ) -> ( g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) -> seq M ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) )
61	60	exlimdv 1861	. . . . . . . . . . 11 |- ( ( ( ph /\ m e. NN ) /\ f : ( 1 ... m ) -1-1-onto-> A ) -> ( E. g g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) -> seq M ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) )
62	45, 61	mpd 15	. . . . . . . . . 10 |- ( ( ( ph /\ m e. NN ) /\ f : ( 1 ... m ) -1-1-onto-> A ) -> seq M ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) )
63		breq2 4657	. . . . . . . . . 10 |- ( x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) -> ( seq M ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x <-> seq M ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) )
64	62, 63	syl5ibrcom 237	. . . . . . . . 9 |- ( ( ( ph /\ m e. NN ) /\ f : ( 1 ... m ) -1-1-onto-> A ) -> ( x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) -> seq M ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) )
65	64	expimpd 629	. . . . . . . 8 |- ( ( ph /\ m e. NN ) -> ( ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) -> seq M ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) )
66	65	exlimdv 1861	. . . . . . 7 |- ( ( ph /\ m e. NN ) -> ( E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) -> seq M ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) )
67	66	rexlimdva 3031	. . . . . 6 |- ( ph -> ( E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) -> seq M ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) )
68	26, 67	jaod 395	. . . . 5 |- ( ph -> ( ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) -> seq M ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) )
69	16	adantr 481	. . . . . . . 8 |- ( ( ph /\ seq M ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) -> M e. ZZ )
70	21	adantr 481	. . . . . . . 8 |- ( ( ph /\ seq M ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) -> A C_ ( ZZ>= ` M ) )
71		simpr 477	. . . . . . . 8 |- ( ( ph /\ seq M ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) -> seq M ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x )
72		fveq2 6191	. . . . . . . . . . 11 |- ( m = M -> ( ZZ>= ` m ) = ( ZZ>= ` M ) )
73	72	sseq2d 3633	. . . . . . . . . 10 |- ( m = M -> ( A C_ ( ZZ>= ` m ) <-> A C_ ( ZZ>= ` M ) ) )
74		seqeq1 12804	. . . . . . . . . . 11 |- ( m = M -> seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) = seq M ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) )
75	74	breq1d 4663	. . . . . . . . . 10 |- ( m = M -> ( seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x <-> seq M ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) )
76	73, 75	anbi12d 747	. . . . . . . . 9 |- ( m = M -> ( ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) <-> ( A C_ ( ZZ>= ` M ) /\ seq M ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) ) )
77	76	rspcev 3309	. . . . . . . 8 |- ( ( M e. ZZ /\ ( A C_ ( ZZ>= ` M ) /\ seq M ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) ) -> E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) )
78	69, 70, 71, 77	syl12anc 1324	. . . . . . 7 |- ( ( ph /\ seq M ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) -> E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) )
79	78	orcd 407	. . . . . 6 |- ( ( ph /\ seq M ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) -> ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) )
80	79	ex 450	. . . . 5 |- ( ph -> ( seq M ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x -> ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) ) )
81	68, 80	impbid 202	. . . 4 |- ( ph -> ( ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) <-> seq M ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) )
82		simpr 477	. . . . . . . . 9 |- ( ( ph /\ j e. ( ZZ>= ` M ) ) -> j e. ( ZZ>= ` M ) )
83	28, 82	sseldi 3601	. . . . . . . 8 |- ( ( ph /\ j e. ( ZZ>= ` M ) ) -> j e. ZZ )
84	82, 20	syl6eleqr 2712	. . . . . . . . . 10 |- ( ( ph /\ j e. ( ZZ>= ` M ) ) -> j e. Z )
85		zsum.4	. . . . . . . . . . . 12 |- ( ( ph /\ k e. Z ) -> ( F ` k ) = if ( k e. A , B , 0 ) )
86	85	ralrimiva 2966	. . . . . . . . . . 11 |- ( ph -> A. k e. Z ( F ` k ) = if ( k e. A , B , 0 ) )
87	86	adantr 481	. . . . . . . . . 10 |- ( ( ph /\ j e. ( ZZ>= ` M ) ) -> A. k e. Z ( F ` k ) = if ( k e. A , B , 0 ) )
88		nfcsb1v 3549	. . . . . . . . . . . 12 |- F/_ k [_ j / k ]_ if ( k e. A , B , 0 )
89	88	nfeq2 2780	. . . . . . . . . . 11 |- F/ k ( F ` j ) = [_ j / k ]_ if ( k e. A , B , 0 )
90		fveq2 6191	. . . . . . . . . . . 12 |- ( k = j -> ( F ` k ) = ( F ` j ) )
91		csbeq1a 3542	. . . . . . . . . . . 12 |- ( k = j -> if ( k e. A , B , 0 ) = [_ j / k ]_ if ( k e. A , B , 0 ) )
92	90, 91	eqeq12d 2637	. . . . . . . . . . 11 |- ( k = j -> ( ( F ` k ) = if ( k e. A , B , 0 ) <-> ( F ` j ) = [_ j / k ]_ if ( k e. A , B , 0 ) ) )
93	89, 92	rspc 3303	. . . . . . . . . 10 |- ( j e. Z -> ( A. k e. Z ( F ` k ) = if ( k e. A , B , 0 ) -> ( F ` j ) = [_ j / k ]_ if ( k e. A , B , 0 ) ) )
94	84, 87, 93	sylc 65	. . . . . . . . 9 |- ( ( ph /\ j e. ( ZZ>= ` M ) ) -> ( F ` j ) = [_ j / k ]_ if ( k e. A , B , 0 ) )
95		fvex 6201	. . . . . . . . 9 |- ( F ` j ) e. _V
96	94, 95	syl6eqelr 2710	. . . . . . . 8 |- ( ( ph /\ j e. ( ZZ>= ` M ) ) -> [_ j / k ]_ if ( k e. A , B , 0 ) e. _V )
97		nfcv 2764	. . . . . . . . . . 11 |- F/_ n if ( k e. A , B , 0 )
98		nfv 1843	. . . . . . . . . . . 12 |- F/ k n e. A
99		nfcsb1v 3549	. . . . . . . . . . . 12 |- F/_ k [_ n / k ]_ B
100		nfcv 2764	. . . . . . . . . . . 12 |- F/_ k 0
101	98, 99, 100	nfif 4115	. . . . . . . . . . 11 |- F/_ k if ( n e. A , [_ n / k ]_ B , 0 )
102		eleq1 2689	. . . . . . . . . . . 12 |- ( k = n -> ( k e. A <-> n e. A ) )
103		csbeq1a 3542	. . . . . . . . . . . 12 |- ( k = n -> B = [_ n / k ]_ B )
104	102, 103	ifbieq1d 4109	. . . . . . . . . . 11 |- ( k = n -> if ( k e. A , B , 0 ) = if ( n e. A , [_ n / k ]_ B , 0 ) )
105	97, 101, 104	cbvmpt 4749	. . . . . . . . . 10 |- ( k e. ZZ |-> if ( k e. A , B , 0 ) ) = ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) )
106	105	eqcomi 2631	. . . . . . . . 9 |- ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) = ( k e. ZZ |-> if ( k e. A , B , 0 ) )
107	106	fvmpts 6285	. . . . . . . 8 |- ( ( j e. ZZ /\ [_ j / k ]_ if ( k e. A , B , 0 ) e. _V ) -> ( ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ` j ) = [_ j / k ]_ if ( k e. A , B , 0 ) )
108	83, 96, 107	syl2anc 693	. . . . . . 7 |- ( ( ph /\ j e. ( ZZ>= ` M ) ) -> ( ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ` j ) = [_ j / k ]_ if ( k e. A , B , 0 ) )
109	108, 94	eqtr4d 2659	. . . . . 6 |- ( ( ph /\ j e. ( ZZ>= ` M ) ) -> ( ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ` j ) = ( F ` j ) )
110	16, 109	seqfeq 12826	. . . . 5 |- ( ph -> seq M ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) = seq M ( + , F ) )
111	110	breq1d 4663	. . . 4 |- ( ph -> ( seq M ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x <-> seq M ( + , F ) ~~> x ) )
112	81, 111	bitrd 268	. . 3 |- ( ph -> ( ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) <-> seq M ( + , F ) ~~> x ) )
113	112	iotabidv 5872	. 2 |- ( ph -> ( iota x ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) ) = ( iota x seq M ( + , F ) ~~> x ) )
114		df-sum 14417	. 2 |- sum_ k e. A B = ( iota x ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) )
115		df-fv 5896	. 2 |- ( ~~> ` seq M ( + , F ) ) = ( iota x seq M ( + , F ) ~~> x )
116	113, 114, 115	3eqtr4g 2681	1 |- ( ph -> sum_ k e. A B = ( ~~> ` seq M ( + , F ) ) )

Syntax hints:   -> wi 4   \/ wo 383   /\ wa 384   = wceq 1483   E.wex 1704   e. wcel 1990   A.wral 2912   E.wrex 2913   _Vcvv 3200   [_csb 3533   C_ wss 3574   ifcif 4086   class class class wbr 4653   |-> cmpt 4729   Or wor 5034   iotacio 5849   -1-1-onto->wf1o 5887   ` cfv 5888   Isom wiso 5889  (class class class)co 6650   ~~ cen 7952   Fincfn 7955   CCcc 9934   RRcr 9935   0cc0 9936   1c1 9937   + caddc 9939   < clt 10074   NNcn 11020   ZZcz 11377   ZZ>=cuz 11687   ...cfz 12326   seqcseq 12801   #chash 13117   ~~> cli 14215   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

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  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-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  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-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-sum 14417

This theorem is referenced by:  isum  14450  sum0  14452  sumz  14453  sumss  14455  fsumsers  14459