Theorem summodclem3 10988

Description: Lemma for summodc 10991. (Contributed by Mario Carneiro, 29-Mar-2014.) (Revised by Jim Kingdon, 9-Apr-2023.)

Hypotheses

Ref	Expression
isummo.1	|- F = ( k e. ZZ |-> if ( k e. A , B , 0 ) )
isummo.2	|- ( ( ph /\ k e. A ) -> B e. CC )
isummolem3.5	|- ( ph -> ( M e. NN /\ N e. NN ) )
isummolem3.6	|- ( ph -> f : ( 1 ... M ) -1-1-onto-> A )
isummolem3.7	|- ( ph -> K : ( 1 ... N ) -1-1-onto-> A )
isummolem3.g	|- G = ( n e. NN |-> if ( n <_ M , [_ ( f ` n ) / k ]_ B , 0 ) )
isummolem3.4	|- H = ( n e. NN |-> if ( n <_ N , [_ ( K ` n ) / k ]_ B , 0 ) )

Assertion

Ref	Expression
summodclem3	|- ( ph -> ( seq 1 ( + , G ) ` M ) = ( seq 1 ( + , H ) ` N ) )

Distinct variable groups:   k, n, A   n, F   k, N, n   ph, k, n   k, M, n   B, n   k, K, n   f, k, n

Allowed substitution hints:   ph( f)   A( f)   B( f, k)   F( f, k)   G( f, k, n)   H( f, k, n)   K( f)   M( f)   N( f)

Proof of Theorem summodclem3

Dummy variables i j m y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		addcl 7617	. . . 4 |- ( ( m e. CC /\ j e. CC ) -> ( m + j ) e. CC )
2	1	adantl 273	. . 3 |- ( ( ph /\ ( m e. CC /\ j e. CC ) ) -> ( m + j ) e. CC )
3		addcom 7770	. . . 4 |- ( ( m e. CC /\ j e. CC ) -> ( m + j ) = ( j + m ) )
4	3	adantl 273	. . 3 |- ( ( ph /\ ( m e. CC /\ j e. CC ) ) -> ( m + j ) = ( j + m ) )
5		addass 7622	. . . 4 |- ( ( m e. CC /\ j e. CC /\ y e. CC ) -> ( ( m + j ) + y ) = ( m + ( j + y ) ) )
6	5	adantl 273	. . 3 |- ( ( ph /\ ( m e. CC /\ j e. CC /\ y e. CC ) ) -> ( ( m + j ) + y ) = ( m + ( j + y ) ) )
7		isummolem3.5	. . . . 5 |- ( ph -> ( M e. NN /\ N e. NN ) )
8	7	simpld 111	. . . 4 |- ( ph -> M e. NN )
9		nnuz 9211	. . . 4 |- NN = ( ZZ>= ` 1 )
10	8, 9	syl6eleq 2192	. . 3 |- ( ph -> M e. ( ZZ>= ` 1 ) )
11		isummolem3.6	. . . . . 6 |- ( ph -> f : ( 1 ... M ) -1-1-onto-> A )
12		f1ocnv 5314	. . . . . 6 |- ( f : ( 1 ... M ) -1-1-onto-> A -> `' f : A -1-1-onto-> ( 1 ... M ) )
13	11, 12	syl 14	. . . . 5 |- ( ph -> `' f : A -1-1-onto-> ( 1 ... M ) )
14		isummolem3.7	. . . . 5 |- ( ph -> K : ( 1 ... N ) -1-1-onto-> A )
15		f1oco 5324	. . . . 5 |- ( ( `' f : A -1-1-onto-> ( 1 ... M ) /\ K : ( 1 ... N ) -1-1-onto-> A ) -> ( `' f o. K ) : ( 1 ... N ) -1-1-onto-> ( 1 ... M ) )
16	13, 14, 15	syl2anc 406	. . . 4 |- ( ph -> ( `' f o. K ) : ( 1 ... N ) -1-1-onto-> ( 1 ... M ) )
17		isummo.1	. . . . . . . 8 |- F = ( k e. ZZ |-> if ( k e. A , B , 0 ) )
18		isummo.2	. . . . . . . 8 |- ( ( ph /\ k e. A ) -> B e. CC )
19	17, 18, 7, 11, 14	isummolemnm 10987	. . . . . . 7 |- ( ph -> N = M )
20	19	eqcomd 2105	. . . . . 6 |- ( ph -> M = N )
21	20	oveq2d 5722	. . . . 5 |- ( ph -> ( 1 ... M ) = ( 1 ... N ) )
22		f1oeq2 5293	. . . . 5 |- ( ( 1 ... M ) = ( 1 ... N ) -> ( ( `' f o. K ) : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) <-> ( `' f o. K ) : ( 1 ... N ) -1-1-onto-> ( 1 ... M ) ) )
23	21, 22	syl 14	. . . 4 |- ( ph -> ( ( `' f o. K ) : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) <-> ( `' f o. K ) : ( 1 ... N ) -1-1-onto-> ( 1 ... M ) ) )
24	16, 23	mpbird 166	. . 3 |- ( ph -> ( `' f o. K ) : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) )
25		elnnuz 9212	. . . 4 |- ( m e. NN <-> m e. ( ZZ>= ` 1 ) )
26		isummolem3.g	. . . . . . 7 |- G = ( n e. NN |-> if ( n <_ M , [_ ( f ` n ) / k ]_ B , 0 ) )
27		breq1 3878	. . . . . . . 8 |- ( n = m -> ( n <_ M <-> m <_ M ) )
28		fveq2 5353	. . . . . . . . 9 |- ( n = m -> ( f ` n ) = ( f ` m ) )
29	28	csbeq1d 2961	. . . . . . . 8 |- ( n = m -> [_ ( f ` n ) / k ]_ B = [_ ( f ` m ) / k ]_ B )
30	27, 29	ifbieq1d 3441	. . . . . . 7 |- ( n = m -> if ( n <_ M , [_ ( f ` n ) / k ]_ B , 0 ) = if ( m <_ M , [_ ( f ` m ) / k ]_ B , 0 ) )
31		simplr 500	. . . . . . 7 |- ( ( ( ph /\ m e. NN ) /\ m e. ( 1 ... M ) ) -> m e. NN )
32		elfzle2 9649	. . . . . . . . . 10 |- ( m e. ( 1 ... M ) -> m <_ M )
33	32	adantl 273	. . . . . . . . 9 |- ( ( ( ph /\ m e. NN ) /\ m e. ( 1 ... M ) ) -> m <_ M )
34	33	iftrued 3428	. . . . . . . 8 |- ( ( ( ph /\ m e. NN ) /\ m e. ( 1 ... M ) ) -> if ( m <_ M , [_ ( f ` m ) / k ]_ B , 0 ) = [_ ( f ` m ) / k ]_ B )
35		f1of 5301	. . . . . . . . . . . 12 |- ( f : ( 1 ... M ) -1-1-onto-> A -> f : ( 1 ... M ) --> A )
36	11, 35	syl 14	. . . . . . . . . . 11 |- ( ph -> f : ( 1 ... M ) --> A )
37	36	ffvelrnda 5487	. . . . . . . . . 10 |- ( ( ph /\ m e. ( 1 ... M ) ) -> ( f ` m ) e. A )
38	18	ralrimiva 2464	. . . . . . . . . . 11 |- ( ph -> A. k e. A B e. CC )
39	38	adantr 272	. . . . . . . . . 10 |- ( ( ph /\ m e. ( 1 ... M ) ) -> A. k e. A B e. CC )
40		nfcsb1v 2985	. . . . . . . . . . . 12 |- F/_ k [_ ( f ` m ) / k ]_ B
41	40	nfel1 2251	. . . . . . . . . . 11 |- F/ k [_ ( f ` m ) / k ]_ B e. CC
42		csbeq1a 2963	. . . . . . . . . . . 12 |- ( k = ( f ` m ) -> B = [_ ( f ` m ) / k ]_ B )
43	42	eleq1d 2168	. . . . . . . . . . 11 |- ( k = ( f ` m ) -> ( B e. CC <-> [_ ( f ` m ) / k ]_ B e. CC ) )
44	41, 43	rspc 2738	. . . . . . . . . 10 |- ( ( f ` m ) e. A -> ( A. k e. A B e. CC -> [_ ( f ` m ) / k ]_ B e. CC ) )
45	37, 39, 44	sylc 62	. . . . . . . . 9 |- ( ( ph /\ m e. ( 1 ... M ) ) -> [_ ( f ` m ) / k ]_ B e. CC )
46	45	adantlr 464	. . . . . . . 8 |- ( ( ( ph /\ m e. NN ) /\ m e. ( 1 ... M ) ) -> [_ ( f ` m ) / k ]_ B e. CC )
47	34, 46	eqeltrd 2176	. . . . . . 7 |- ( ( ( ph /\ m e. NN ) /\ m e. ( 1 ... M ) ) -> if ( m <_ M , [_ ( f ` m ) / k ]_ B , 0 ) e. CC )
48	26, 30, 31, 47	fvmptd3 5446	. . . . . 6 |- ( ( ( ph /\ m e. NN ) /\ m e. ( 1 ... M ) ) -> ( G ` m ) = if ( m <_ M , [_ ( f ` m ) / k ]_ B , 0 ) )
49	48, 47	eqeltrd 2176	. . . . 5 |- ( ( ( ph /\ m e. NN ) /\ m e. ( 1 ... M ) ) -> ( G ` m ) e. CC )
50		simplr 500	. . . . . . 7 |- ( ( ( ph /\ m e. NN ) /\ m e. ( ZZ>= ` ( M + 1 ) ) ) -> m e. NN )
51	8	ad2antrr 475	. . . . . . . . . . . 12 |- ( ( ( ph /\ m e. NN ) /\ m e. ( ZZ>= ` ( M + 1 ) ) ) -> M e. NN )
52	51	nnzd 9024	. . . . . . . . . . 11 |- ( ( ( ph /\ m e. NN ) /\ m e. ( ZZ>= ` ( M + 1 ) ) ) -> M e. ZZ )
53		eluzp1l 9200	. . . . . . . . . . 11 |- ( ( M e. ZZ /\ m e. ( ZZ>= ` ( M + 1 ) ) ) -> M < m )
54	52, 53	sylancom 414	. . . . . . . . . 10 |- ( ( ( ph /\ m e. NN ) /\ m e. ( ZZ>= ` ( M + 1 ) ) ) -> M < m )
55	50	nnzd 9024	. . . . . . . . . . 11 |- ( ( ( ph /\ m e. NN ) /\ m e. ( ZZ>= ` ( M + 1 ) ) ) -> m e. ZZ )
56		zltnle 8952	. . . . . . . . . . 11 |- ( ( M e. ZZ /\ m e. ZZ ) -> ( M < m <-> -. m <_ M ) )
57	52, 55, 56	syl2anc 406	. . . . . . . . . 10 |- ( ( ( ph /\ m e. NN ) /\ m e. ( ZZ>= ` ( M + 1 ) ) ) -> ( M < m <-> -. m <_ M ) )
58	54, 57	mpbid 146	. . . . . . . . 9 |- ( ( ( ph /\ m e. NN ) /\ m e. ( ZZ>= ` ( M + 1 ) ) ) -> -. m <_ M )
59	58	iffalsed 3431	. . . . . . . 8 |- ( ( ( ph /\ m e. NN ) /\ m e. ( ZZ>= ` ( M + 1 ) ) ) -> if ( m <_ M , [_ ( f ` m ) / k ]_ B , 0 ) = 0 )
60		0cn 7630	. . . . . . . 8 |- 0 e. CC
61	59, 60	syl6eqel 2190	. . . . . . 7 |- ( ( ( ph /\ m e. NN ) /\ m e. ( ZZ>= ` ( M + 1 ) ) ) -> if ( m <_ M , [_ ( f ` m ) / k ]_ B , 0 ) e. CC )
62	26, 30, 50, 61	fvmptd3 5446	. . . . . 6 |- ( ( ( ph /\ m e. NN ) /\ m e. ( ZZ>= ` ( M + 1 ) ) ) -> ( G ` m ) = if ( m <_ M , [_ ( f ` m ) / k ]_ B , 0 ) )
63	62, 61	eqeltrd 2176	. . . . 5 |- ( ( ( ph /\ m e. NN ) /\ m e. ( ZZ>= ` ( M + 1 ) ) ) -> ( G ` m ) e. CC )
64		nnsplit 9755	. . . . . . . . 9 |- ( M e. NN -> NN = ( ( 1 ... M ) u. ( ZZ>= ` ( M + 1 ) ) ) )
65	8, 64	syl 14	. . . . . . . 8 |- ( ph -> NN = ( ( 1 ... M ) u. ( ZZ>= ` ( M + 1 ) ) ) )
66	65	eleq2d 2169	. . . . . . 7 |- ( ph -> ( m e. NN <-> m e. ( ( 1 ... M ) u. ( ZZ>= ` ( M + 1 ) ) ) ) )
67	66	biimpa 292	. . . . . 6 |- ( ( ph /\ m e. NN ) -> m e. ( ( 1 ... M ) u. ( ZZ>= ` ( M + 1 ) ) ) )
68		elun 3164	. . . . . 6 |- ( m e. ( ( 1 ... M ) u. ( ZZ>= ` ( M + 1 ) ) ) <-> ( m e. ( 1 ... M ) \/ m e. ( ZZ>= ` ( M + 1 ) ) ) )
69	67, 68	sylib 121	. . . . 5 |- ( ( ph /\ m e. NN ) -> ( m e. ( 1 ... M ) \/ m e. ( ZZ>= ` ( M + 1 ) ) ) )
70	49, 63, 69	mpjaodan 753	. . . 4 |- ( ( ph /\ m e. NN ) -> ( G ` m ) e. CC )
71	25, 70	sylan2br 284	. . 3 |- ( ( ph /\ m e. ( ZZ>= ` 1 ) ) -> ( G ` m ) e. CC )
72	19	oveq2d 5722	. . . . . . . . 9 |- ( ph -> ( 1 ... N ) = ( 1 ... M ) )
73	72	eleq2d 2169	. . . . . . . 8 |- ( ph -> ( m e. ( 1 ... N ) <-> m e. ( 1 ... M ) ) )
74	73	adantr 272	. . . . . . 7 |- ( ( ph /\ m e. NN ) -> ( m e. ( 1 ... N ) <-> m e. ( 1 ... M ) ) )
75	74	pm5.32i 445	. . . . . 6 |- ( ( ( ph /\ m e. NN ) /\ m e. ( 1 ... N ) ) <-> ( ( ph /\ m e. NN ) /\ m e. ( 1 ... M ) ) )
76		isummolem3.4	. . . . . . . 8 |- H = ( n e. NN |-> if ( n <_ N , [_ ( K ` n ) / k ]_ B , 0 ) )
77		breq1 3878	. . . . . . . . 9 |- ( n = m -> ( n <_ N <-> m <_ N ) )
78		fveq2 5353	. . . . . . . . . 10 |- ( n = m -> ( K ` n ) = ( K ` m ) )
79	78	csbeq1d 2961	. . . . . . . . 9 |- ( n = m -> [_ ( K ` n ) / k ]_ B = [_ ( K ` m ) / k ]_ B )
80	77, 79	ifbieq1d 3441	. . . . . . . 8 |- ( n = m -> if ( n <_ N , [_ ( K ` n ) / k ]_ B , 0 ) = if ( m <_ N , [_ ( K ` m ) / k ]_ B , 0 ) )
81		simplr 500	. . . . . . . 8 |- ( ( ( ph /\ m e. NN ) /\ m e. ( 1 ... N ) ) -> m e. NN )
82		elfzle2 9649	. . . . . . . . . . 11 |- ( m e. ( 1 ... N ) -> m <_ N )
83	82	adantl 273	. . . . . . . . . 10 |- ( ( ( ph /\ m e. NN ) /\ m e. ( 1 ... N ) ) -> m <_ N )
84	83	iftrued 3428	. . . . . . . . 9 |- ( ( ( ph /\ m e. NN ) /\ m e. ( 1 ... N ) ) -> if ( m <_ N , [_ ( K ` m ) / k ]_ B , 0 ) = [_ ( K ` m ) / k ]_ B )
85		f1of 5301	. . . . . . . . . . . . 13 |- ( K : ( 1 ... N ) -1-1-onto-> A -> K : ( 1 ... N ) --> A )
86	14, 85	syl 14	. . . . . . . . . . . 12 |- ( ph -> K : ( 1 ... N ) --> A )
87	86	ffvelrnda 5487	. . . . . . . . . . 11 |- ( ( ph /\ m e. ( 1 ... N ) ) -> ( K ` m ) e. A )
88	38	adantr 272	. . . . . . . . . . 11 |- ( ( ph /\ m e. ( 1 ... N ) ) -> A. k e. A B e. CC )
89		nfcsb1v 2985	. . . . . . . . . . . . 13 |- F/_ k [_ ( K ` m ) / k ]_ B
90	89	nfel1 2251	. . . . . . . . . . . 12 |- F/ k [_ ( K ` m ) / k ]_ B e. CC
91		csbeq1a 2963	. . . . . . . . . . . . 13 |- ( k = ( K ` m ) -> B = [_ ( K ` m ) / k ]_ B )
92	91	eleq1d 2168	. . . . . . . . . . . 12 |- ( k = ( K ` m ) -> ( B e. CC <-> [_ ( K ` m ) / k ]_ B e. CC ) )
93	90, 92	rspc 2738	. . . . . . . . . . 11 |- ( ( K ` m ) e. A -> ( A. k e. A B e. CC -> [_ ( K ` m ) / k ]_ B e. CC ) )
94	87, 88, 93	sylc 62	. . . . . . . . . 10 |- ( ( ph /\ m e. ( 1 ... N ) ) -> [_ ( K ` m ) / k ]_ B e. CC )
95	94	adantlr 464	. . . . . . . . 9 |- ( ( ( ph /\ m e. NN ) /\ m e. ( 1 ... N ) ) -> [_ ( K ` m ) / k ]_ B e. CC )
96	84, 95	eqeltrd 2176	. . . . . . . 8 |- ( ( ( ph /\ m e. NN ) /\ m e. ( 1 ... N ) ) -> if ( m <_ N , [_ ( K ` m ) / k ]_ B , 0 ) e. CC )
97	76, 80, 81, 96	fvmptd3 5446	. . . . . . 7 |- ( ( ( ph /\ m e. NN ) /\ m e. ( 1 ... N ) ) -> ( H ` m ) = if ( m <_ N , [_ ( K ` m ) / k ]_ B , 0 ) )
98	97, 96	eqeltrd 2176	. . . . . 6 |- ( ( ( ph /\ m e. NN ) /\ m e. ( 1 ... N ) ) -> ( H ` m ) e. CC )
99	75, 98	sylbir 134	. . . . 5 |- ( ( ( ph /\ m e. NN ) /\ m e. ( 1 ... M ) ) -> ( H ` m ) e. CC )
100	19	breq2d 3887	. . . . . . . . . . . 12 |- ( ph -> ( m <_ N <-> m <_ M ) )
101	100	notbid 633	. . . . . . . . . . 11 |- ( ph -> ( -. m <_ N <-> -. m <_ M ) )
102	101	ad2antrr 475	. . . . . . . . . 10 |- ( ( ( ph /\ m e. NN ) /\ m e. ( ZZ>= ` ( M + 1 ) ) ) -> ( -. m <_ N <-> -. m <_ M ) )
103	58, 102	mpbird 166	. . . . . . . . 9 |- ( ( ( ph /\ m e. NN ) /\ m e. ( ZZ>= ` ( M + 1 ) ) ) -> -. m <_ N )
104	103	iffalsed 3431	. . . . . . . 8 |- ( ( ( ph /\ m e. NN ) /\ m e. ( ZZ>= ` ( M + 1 ) ) ) -> if ( m <_ N , [_ ( K ` m ) / k ]_ B , 0 ) = 0 )
105	104, 60	syl6eqel 2190	. . . . . . 7 |- ( ( ( ph /\ m e. NN ) /\ m e. ( ZZ>= ` ( M + 1 ) ) ) -> if ( m <_ N , [_ ( K ` m ) / k ]_ B , 0 ) e. CC )
106	76, 80, 50, 105	fvmptd3 5446	. . . . . 6 |- ( ( ( ph /\ m e. NN ) /\ m e. ( ZZ>= ` ( M + 1 ) ) ) -> ( H ` m ) = if ( m <_ N , [_ ( K ` m ) / k ]_ B , 0 ) )
107	106, 105	eqeltrd 2176	. . . . 5 |- ( ( ( ph /\ m e. NN ) /\ m e. ( ZZ>= ` ( M + 1 ) ) ) -> ( H ` m ) e. CC )
108	99, 107, 69	mpjaodan 753	. . . 4 |- ( ( ph /\ m e. NN ) -> ( H ` m ) e. CC )
109	25, 108	sylan2br 284	. . 3 |- ( ( ph /\ m e. ( ZZ>= ` 1 ) ) -> ( H ` m ) e. CC )
110		f1oeq2 5293	. . . . . . . . . . 11 |- ( ( 1 ... M ) = ( 1 ... N ) -> ( K : ( 1 ... M ) -1-1-onto-> A <-> K : ( 1 ... N ) -1-1-onto-> A ) )
111	21, 110	syl 14	. . . . . . . . . 10 |- ( ph -> ( K : ( 1 ... M ) -1-1-onto-> A <-> K : ( 1 ... N ) -1-1-onto-> A ) )
112	14, 111	mpbird 166	. . . . . . . . 9 |- ( ph -> K : ( 1 ... M ) -1-1-onto-> A )
113		f1of 5301	. . . . . . . . 9 |- ( K : ( 1 ... M ) -1-1-onto-> A -> K : ( 1 ... M ) --> A )
114	112, 113	syl 14	. . . . . . . 8 |- ( ph -> K : ( 1 ... M ) --> A )
115		fvco3 5424	. . . . . . . 8 |- ( ( K : ( 1 ... M ) --> A /\ i e. ( 1 ... M ) ) -> ( ( `' f o. K ) ` i ) = ( `' f ` ( K ` i ) ) )
116	114, 115	sylan 279	. . . . . . 7 |- ( ( ph /\ i e. ( 1 ... M ) ) -> ( ( `' f o. K ) ` i ) = ( `' f ` ( K ` i ) ) )
117	116	fveq2d 5357	. . . . . 6 |- ( ( ph /\ i e. ( 1 ... M ) ) -> ( f ` ( ( `' f o. K ) ` i ) ) = ( f ` ( `' f ` ( K ` i ) ) ) )
118	11	adantr 272	. . . . . . 7 |- ( ( ph /\ i e. ( 1 ... M ) ) -> f : ( 1 ... M ) -1-1-onto-> A )
119	114	ffvelrnda 5487	. . . . . . 7 |- ( ( ph /\ i e. ( 1 ... M ) ) -> ( K ` i ) e. A )
120		f1ocnvfv2 5611	. . . . . . 7 |- ( ( f : ( 1 ... M ) -1-1-onto-> A /\ ( K ` i ) e. A ) -> ( f ` ( `' f ` ( K ` i ) ) ) = ( K ` i ) )
121	118, 119, 120	syl2anc 406	. . . . . 6 |- ( ( ph /\ i e. ( 1 ... M ) ) -> ( f ` ( `' f ` ( K ` i ) ) ) = ( K ` i ) )
122	117, 121	eqtr2d 2133	. . . . 5 |- ( ( ph /\ i e. ( 1 ... M ) ) -> ( K ` i ) = ( f ` ( ( `' f o. K ) ` i ) ) )
123	122	csbeq1d 2961	. . . 4 |- ( ( ph /\ i e. ( 1 ... M ) ) -> [_ ( K ` i ) / k ]_ B = [_ ( f ` ( ( `' f o. K ) ` i ) ) / k ]_ B )
124		elfznn 9675	. . . . . 6 |- ( i e. ( 1 ... M ) -> i e. NN )
125		elfzle2 9649	. . . . . . . . . 10 |- ( i e. ( 1 ... M ) -> i <_ M )
126	125	adantl 273	. . . . . . . . 9 |- ( ( ph /\ i e. ( 1 ... M ) ) -> i <_ M )
127	20	breq2d 3887	. . . . . . . . . 10 |- ( ph -> ( i <_ M <-> i <_ N ) )
128	127	adantr 272	. . . . . . . . 9 |- ( ( ph /\ i e. ( 1 ... M ) ) -> ( i <_ M <-> i <_ N ) )
129	126, 128	mpbid 146	. . . . . . . 8 |- ( ( ph /\ i e. ( 1 ... M ) ) -> i <_ N )
130	129	iftrued 3428	. . . . . . 7 |- ( ( ph /\ i e. ( 1 ... M ) ) -> if ( i <_ N , [_ ( K ` i ) / k ]_ B , 0 ) = [_ ( K ` i ) / k ]_ B )
131	38	adantr 272	. . . . . . . 8 |- ( ( ph /\ i e. ( 1 ... M ) ) -> A. k e. A B e. CC )
132		nfcsb1v 2985	. . . . . . . . . 10 |- F/_ k [_ ( K ` i ) / k ]_ B
133	132	nfel1 2251	. . . . . . . . 9 |- F/ k [_ ( K ` i ) / k ]_ B e. CC
134		csbeq1a 2963	. . . . . . . . . 10 |- ( k = ( K ` i ) -> B = [_ ( K ` i ) / k ]_ B )
135	134	eleq1d 2168	. . . . . . . . 9 |- ( k = ( K ` i ) -> ( B e. CC <-> [_ ( K ` i ) / k ]_ B e. CC ) )
136	133, 135	rspc 2738	. . . . . . . 8 |- ( ( K ` i ) e. A -> ( A. k e. A B e. CC -> [_ ( K ` i ) / k ]_ B e. CC ) )
137	119, 131, 136	sylc 62	. . . . . . 7 |- ( ( ph /\ i e. ( 1 ... M ) ) -> [_ ( K ` i ) / k ]_ B e. CC )
138	130, 137	eqeltrd 2176	. . . . . 6 |- ( ( ph /\ i e. ( 1 ... M ) ) -> if ( i <_ N , [_ ( K ` i ) / k ]_ B , 0 ) e. CC )
139		breq1 3878	. . . . . . . 8 |- ( n = i -> ( n <_ N <-> i <_ N ) )
140		fveq2 5353	. . . . . . . . 9 |- ( n = i -> ( K ` n ) = ( K ` i ) )
141	140	csbeq1d 2961	. . . . . . . 8 |- ( n = i -> [_ ( K ` n ) / k ]_ B = [_ ( K ` i ) / k ]_ B )
142	139, 141	ifbieq1d 3441	. . . . . . 7 |- ( n = i -> if ( n <_ N , [_ ( K ` n ) / k ]_ B , 0 ) = if ( i <_ N , [_ ( K ` i ) / k ]_ B , 0 ) )
143	142, 76	fvmptg 5429	. . . . . 6 |- ( ( i e. NN /\ if ( i <_ N , [_ ( K ` i ) / k ]_ B , 0 ) e. CC ) -> ( H ` i ) = if ( i <_ N , [_ ( K ` i ) / k ]_ B , 0 ) )
144	124, 138, 143	syl2an2 564	. . . . 5 |- ( ( ph /\ i e. ( 1 ... M ) ) -> ( H ` i ) = if ( i <_ N , [_ ( K ` i ) / k ]_ B , 0 ) )
145	144, 130	eqtrd 2132	. . . 4 |- ( ( ph /\ i e. ( 1 ... M ) ) -> ( H ` i ) = [_ ( K ` i ) / k ]_ B )
146		breq1 3878	. . . . . . 7 |- ( n = ( ( `' f o. K ) ` i ) -> ( n <_ M <-> ( ( `' f o. K ) ` i ) <_ M ) )
147		fveq2 5353	. . . . . . . 8 |- ( n = ( ( `' f o. K ) ` i ) -> ( f ` n ) = ( f ` ( ( `' f o. K ) ` i ) ) )
148	147	csbeq1d 2961	. . . . . . 7 |- ( n = ( ( `' f o. K ) ` i ) -> [_ ( f ` n ) / k ]_ B = [_ ( f ` ( ( `' f o. K ) ` i ) ) / k ]_ B )
149	146, 148	ifbieq1d 3441	. . . . . 6 |- ( n = ( ( `' f o. K ) ` i ) -> if ( n <_ M , [_ ( f ` n ) / k ]_ B , 0 ) = if ( ( ( `' f o. K ) ` i ) <_ M , [_ ( f ` ( ( `' f o. K ) ` i ) ) / k ]_ B , 0 ) )
150		f1of 5301	. . . . . . . . 9 |- ( ( `' f o. K ) : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) -> ( `' f o. K ) : ( 1 ... M ) --> ( 1 ... M ) )
151	24, 150	syl 14	. . . . . . . 8 |- ( ph -> ( `' f o. K ) : ( 1 ... M ) --> ( 1 ... M ) )
152	151	ffvelrnda 5487	. . . . . . 7 |- ( ( ph /\ i e. ( 1 ... M ) ) -> ( ( `' f o. K ) ` i ) e. ( 1 ... M ) )
153		elfznn 9675	. . . . . . 7 |- ( ( ( `' f o. K ) ` i ) e. ( 1 ... M ) -> ( ( `' f o. K ) ` i ) e. NN )
154	152, 153	syl 14	. . . . . 6 |- ( ( ph /\ i e. ( 1 ... M ) ) -> ( ( `' f o. K ) ` i ) e. NN )
155		elfzle2 9649	. . . . . . . . . 10 |- ( ( ( `' f o. K ) ` i ) e. ( 1 ... M ) -> ( ( `' f o. K ) ` i ) <_ M )
156	152, 155	syl 14	. . . . . . . . 9 |- ( ( ph /\ i e. ( 1 ... M ) ) -> ( ( `' f o. K ) ` i ) <_ M )
157	156	iftrued 3428	. . . . . . . 8 |- ( ( ph /\ i e. ( 1 ... M ) ) -> if ( ( ( `' f o. K ) ` i ) <_ M , [_ ( f ` ( ( `' f o. K ) ` i ) ) / k ]_ B , 0 ) = [_ ( f ` ( ( `' f o. K ) ` i ) ) / k ]_ B )
158	157, 123	eqtr4d 2135	. . . . . . 7 |- ( ( ph /\ i e. ( 1 ... M ) ) -> if ( ( ( `' f o. K ) ` i ) <_ M , [_ ( f ` ( ( `' f o. K ) ` i ) ) / k ]_ B , 0 ) = [_ ( K ` i ) / k ]_ B )
159	158, 137	eqeltrd 2176	. . . . . 6 |- ( ( ph /\ i e. ( 1 ... M ) ) -> if ( ( ( `' f o. K ) ` i ) <_ M , [_ ( f ` ( ( `' f o. K ) ` i ) ) / k ]_ B , 0 ) e. CC )
160	26, 149, 154, 159	fvmptd3 5446	. . . . 5 |- ( ( ph /\ i e. ( 1 ... M ) ) -> ( G ` ( ( `' f o. K ) ` i ) ) = if ( ( ( `' f o. K ) ` i ) <_ M , [_ ( f ` ( ( `' f o. K ) ` i ) ) / k ]_ B , 0 ) )
161	160, 157	eqtrd 2132	. . . 4 |- ( ( ph /\ i e. ( 1 ... M ) ) -> ( G ` ( ( `' f o. K ) ` i ) ) = [_ ( f ` ( ( `' f o. K ) ` i ) ) / k ]_ B )
162	123, 145, 161	3eqtr4d 2142	. . 3 |- ( ( ph /\ i e. ( 1 ... M ) ) -> ( H ` i ) = ( G ` ( ( `' f o. K ) ` i ) ) )
163	2, 4, 6, 10, 24, 71, 109, 162	seq3f1o 10118	. 2 |- ( ph -> ( seq 1 ( + , H ) ` M ) = ( seq 1 ( + , G ) ` M ) )
164	20	fveq2d 5357	. 2 |- ( ph -> ( seq 1 ( + , H ) ` M ) = ( seq 1 ( + , H ) ` N ) )
165	163, 164	eqtr3d 2134	1 |- ( ph -> ( seq 1 ( + , G ) ` M ) = ( seq 1 ( + , H ) ` N ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 103   <-> wb 104   \/ wo 670   /\ w3a 930   = wceq 1299   e. wcel 1448   A.wral 2375   [_csb 2955   u. cun 3019   ifcif 3421   class class class wbr 3875   |-> cmpt 3929   `'ccnv 4476   o. ccom 4481   -->wf 5055   -1-1-onto->wf1o 5058   ` cfv 5059  (class class class)co 5706   CCcc 7498   0cc0 7500   1c1 7501   + caddc 7503   < clt 7672   <_ cle 7673   NNcn 8578   ZZcz 8906   ZZ>=cuz 9176   ...cfz 9631   seqcseq 10059

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 584  ax-in2 585  ax-io 671  ax-5 1391  ax-7 1392  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-10 1451  ax-11 1452  ax-i12 1453  ax-bndl 1454  ax-4 1455  ax-13 1459  ax-14 1460  ax-17 1474  ax-i9 1478  ax-ial 1482  ax-i5r 1483  ax-ext 2082  ax-coll 3983  ax-sep 3986  ax-nul 3994  ax-pow 4038  ax-pr 4069  ax-un 4293  ax-setind 4390  ax-iinf 4440  ax-cnex 7586  ax-resscn 7587  ax-1cn 7588  ax-1re 7589  ax-icn 7590  ax-addcl 7591  ax-addrcl 7592  ax-mulcl 7593  ax-addcom 7595  ax-addass 7597  ax-distr 7599  ax-i2m1 7600  ax-0lt1 7601  ax-0id 7603  ax-rnegex 7604  ax-cnre 7606  ax-pre-ltirr 7607  ax-pre-ltwlin 7608  ax-pre-lttrn 7609  ax-pre-apti 7610  ax-pre-ltadd 7611

This theorem depends on definitions:  df-bi 116  df-dc 787  df-3or 931  df-3an 932  df-tru 1302  df-fal 1305  df-nf 1405  df-sb 1704  df-eu 1963  df-mo 1964  df-clab 2087  df-cleq 2093  df-clel 2096  df-nfc 2229  df-ne 2268  df-nel 2363  df-ral 2380  df-rex 2381  df-reu 2382  df-rab 2384  df-v 2643  df-sbc 2863  df-csb 2956  df-dif 3023  df-un 3025  df-in 3027  df-ss 3034  df-nul 3311  df-if 3422  df-pw 3459  df-sn 3480  df-pr 3481  df-op 3483  df-uni 3684  df-int 3719  df-iun 3762  df-br 3876  df-opab 3930  df-mpt 3931  df-tr 3967  df-id 4153  df-iord 4226  df-on 4228  df-ilim 4229  df-suc 4231  df-iom 4443  df-xp 4483  df-rel 4484  df-cnv 4485  df-co 4486  df-dm 4487  df-rn 4488  df-res 4489  df-ima 4490  df-iota 5024  df-fun 5061  df-fn 5062  df-f 5063  df-f1 5064  df-fo 5065  df-f1o 5066  df-fv 5067  df-riota 5662  df-ov 5709  df-oprab 5710  df-mpo 5711  df-1st 5969  df-2nd 5970  df-recs 6132  df-frec 6218  df-1o 6243  df-er 6359  df-en 6565  df-dom 6566  df-fin 6567  df-pnf 7674  df-mnf 7675  df-xr 7676  df-ltxr 7677  df-le 7678  df-sub 7806  df-neg 7807  df-inn 8579  df-n0 8830  df-z 8907  df-uz 9177  df-fz 9632  df-fzo 9761  df-seqfrec 10060  df-ihash 10363

This theorem is referenced by:  summodclem2a  10989  summodc  10991