Theorem seq3coll 10824

Description: The function F contains a sparse set of nonzero values to be summed. The function G is an order isomorphism from the set of nonzero values of F to a 1-based finite sequence, and H collects these nonzero values together. Under these conditions, the sum over the values in H yields the same result as the sum over the original set F. (Contributed by Mario Carneiro, 2-Apr-2014.) (Revised by Jim Kingdon, 9-Apr-2023.)

Hypotheses

Ref	Expression
seqcoll.1	|- ( ( ph /\ k e. S ) -> ( Z .+ k ) = k )
seqcoll.1b	|- ( ( ph /\ k e. S ) -> ( k .+ Z ) = k )
seqcoll.c	|- ( ( ph /\ ( k e. S /\ n e. S ) ) -> ( k .+ n ) e. S )
seqcoll.a	|- ( ph -> Z e. S )
seqcoll.2	|- ( ph -> G Isom < , < ( ( 1 ... (♯ ` A ) ) , A ) )
seqcoll.3	|- ( ph -> N e. ( 1 ... (♯ ` A ) ) )
seqcoll.4	|- ( ph -> A C_ ( ZZ>= ` M ) )
seqcoll.5	|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( F ` k ) e. S )
seqcoll.hcl	|- ( ( ph /\ k e. ( ZZ>= ` 1 ) ) -> ( H ` k ) e. S )
seqcoll.6	|- ( ( ph /\ k e. ( ( M ... ( G ` (♯ ` A ) ) ) \ A ) ) -> ( F ` k ) = Z )
seqcoll.7	|- ( ( ph /\ n e. ( 1 ... (♯ ` A ) ) ) -> ( H ` n ) = ( F ` ( G ` n ) ) )

Assertion

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

Distinct variable groups:   k, n, A   k, F, n   k, G, n   k, H, n   k, M, n   .+ , k, n   ph, k, n   S, k, n   k, Z, n

Allowed substitution hints:   N( k, n)

Proof of Theorem seq3coll

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

Step	Hyp	Ref	Expression
1		seqcoll.3	. 2 |- ( ph -> N e. ( 1 ... (♯ ` A ) ) )
2		elfznn 10056	. . . 4 |- ( N e. ( 1 ... (♯ ` A ) ) -> N e. NN )
3	1, 2	syl 14	. . 3 |- ( ph -> N e. NN )
4		eleq1 2240	. . . . . 6 |- ( y = 1 -> ( y e. ( 1 ... (♯ ` A ) ) <-> 1 e. ( 1 ... (♯ ` A ) ) ) )
5		2fveq3 5522	. . . . . . 7 |- ( y = 1 -> ( seq M ( .+ , F ) ` ( G ` y ) ) = ( seq M ( .+ , F ) ` ( G ` 1 ) ) )
6		fveq2 5517	. . . . . . 7 |- ( y = 1 -> ( seq 1 ( .+ , H ) ` y ) = ( seq 1 ( .+ , H ) ` 1 ) )
7	5, 6	eqeq12d 2192	. . . . . 6 |- ( y = 1 -> ( ( seq M ( .+ , F ) ` ( G ` y ) ) = ( seq 1 ( .+ , H ) ` y ) <-> ( seq M ( .+ , F ) ` ( G ` 1 ) ) = ( seq 1 ( .+ , H ) ` 1 ) ) )
8	4, 7	imbi12d 234	. . . . 5 |- ( y = 1 -> ( ( y e. ( 1 ... (♯ ` A ) ) -> ( seq M ( .+ , F ) ` ( G ` y ) ) = ( seq 1 ( .+ , H ) ` y ) ) <-> ( 1 e. ( 1 ... (♯ ` A ) ) -> ( seq M ( .+ , F ) ` ( G ` 1 ) ) = ( seq 1 ( .+ , H ) ` 1 ) ) ) )
9	8	imbi2d 230	. . . 4 |- ( y = 1 -> ( ( ph -> ( y e. ( 1 ... (♯ ` A ) ) -> ( seq M ( .+ , F ) ` ( G ` y ) ) = ( seq 1 ( .+ , H ) ` y ) ) ) <-> ( ph -> ( 1 e. ( 1 ... (♯ ` A ) ) -> ( seq M ( .+ , F ) ` ( G ` 1 ) ) = ( seq 1 ( .+ , H ) ` 1 ) ) ) ) )
10		eleq1 2240	. . . . . 6 |- ( y = m -> ( y e. ( 1 ... (♯ ` A ) ) <-> m e. ( 1 ... (♯ ` A ) ) ) )
11		2fveq3 5522	. . . . . . 7 |- ( y = m -> ( seq M ( .+ , F ) ` ( G ` y ) ) = ( seq M ( .+ , F ) ` ( G ` m ) ) )
12		fveq2 5517	. . . . . . 7 |- ( y = m -> ( seq 1 ( .+ , H ) ` y ) = ( seq 1 ( .+ , H ) ` m ) )
13	11, 12	eqeq12d 2192	. . . . . 6 |- ( y = m -> ( ( seq M ( .+ , F ) ` ( G ` y ) ) = ( seq 1 ( .+ , H ) ` y ) <-> ( seq M ( .+ , F ) ` ( G ` m ) ) = ( seq 1 ( .+ , H ) ` m ) ) )
14	10, 13	imbi12d 234	. . . . 5 |- ( y = m -> ( ( y e. ( 1 ... (♯ ` A ) ) -> ( seq M ( .+ , F ) ` ( G ` y ) ) = ( seq 1 ( .+ , H ) ` y ) ) <-> ( m e. ( 1 ... (♯ ` A ) ) -> ( seq M ( .+ , F ) ` ( G ` m ) ) = ( seq 1 ( .+ , H ) ` m ) ) ) )
15	14	imbi2d 230	. . . 4 |- ( y = m -> ( ( ph -> ( y e. ( 1 ... (♯ ` A ) ) -> ( seq M ( .+ , F ) ` ( G ` y ) ) = ( seq 1 ( .+ , H ) ` y ) ) ) <-> ( ph -> ( m e. ( 1 ... (♯ ` A ) ) -> ( seq M ( .+ , F ) ` ( G ` m ) ) = ( seq 1 ( .+ , H ) ` m ) ) ) ) )
16		eleq1 2240	. . . . . 6 |- ( y = ( m + 1 ) -> ( y e. ( 1 ... (♯ ` A ) ) <-> ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) )
17		2fveq3 5522	. . . . . . 7 |- ( y = ( m + 1 ) -> ( seq M ( .+ , F ) ` ( G ` y ) ) = ( seq M ( .+ , F ) ` ( G ` ( m + 1 ) ) ) )
18		fveq2 5517	. . . . . . 7 |- ( y = ( m + 1 ) -> ( seq 1 ( .+ , H ) ` y ) = ( seq 1 ( .+ , H ) ` ( m + 1 ) ) )
19	17, 18	eqeq12d 2192	. . . . . 6 |- ( y = ( m + 1 ) -> ( ( seq M ( .+ , F ) ` ( G ` y ) ) = ( seq 1 ( .+ , H ) ` y ) <-> ( seq M ( .+ , F ) ` ( G ` ( m + 1 ) ) ) = ( seq 1 ( .+ , H ) ` ( m + 1 ) ) ) )
20	16, 19	imbi12d 234	. . . . 5 |- ( y = ( m + 1 ) -> ( ( y e. ( 1 ... (♯ ` A ) ) -> ( seq M ( .+ , F ) ` ( G ` y ) ) = ( seq 1 ( .+ , H ) ` y ) ) <-> ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) -> ( seq M ( .+ , F ) ` ( G ` ( m + 1 ) ) ) = ( seq 1 ( .+ , H ) ` ( m + 1 ) ) ) ) )
21	20	imbi2d 230	. . . 4 |- ( y = ( m + 1 ) -> ( ( ph -> ( y e. ( 1 ... (♯ ` A ) ) -> ( seq M ( .+ , F ) ` ( G ` y ) ) = ( seq 1 ( .+ , H ) ` y ) ) ) <-> ( ph -> ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) -> ( seq M ( .+ , F ) ` ( G ` ( m + 1 ) ) ) = ( seq 1 ( .+ , H ) ` ( m + 1 ) ) ) ) ) )
22		eleq1 2240	. . . . . 6 |- ( y = N -> ( y e. ( 1 ... (♯ ` A ) ) <-> N e. ( 1 ... (♯ ` A ) ) ) )
23		2fveq3 5522	. . . . . . 7 |- ( y = N -> ( seq M ( .+ , F ) ` ( G ` y ) ) = ( seq M ( .+ , F ) ` ( G ` N ) ) )
24		fveq2 5517	. . . . . . 7 |- ( y = N -> ( seq 1 ( .+ , H ) ` y ) = ( seq 1 ( .+ , H ) ` N ) )
25	23, 24	eqeq12d 2192	. . . . . 6 |- ( y = N -> ( ( seq M ( .+ , F ) ` ( G ` y ) ) = ( seq 1 ( .+ , H ) ` y ) <-> ( seq M ( .+ , F ) ` ( G ` N ) ) = ( seq 1 ( .+ , H ) ` N ) ) )
26	22, 25	imbi12d 234	. . . . 5 |- ( y = N -> ( ( y e. ( 1 ... (♯ ` A ) ) -> ( seq M ( .+ , F ) ` ( G ` y ) ) = ( seq 1 ( .+ , H ) ` y ) ) <-> ( N e. ( 1 ... (♯ ` A ) ) -> ( seq M ( .+ , F ) ` ( G ` N ) ) = ( seq 1 ( .+ , H ) ` N ) ) ) )
27	26	imbi2d 230	. . . 4 |- ( y = N -> ( ( ph -> ( y e. ( 1 ... (♯ ` A ) ) -> ( seq M ( .+ , F ) ` ( G ` y ) ) = ( seq 1 ( .+ , H ) ` y ) ) ) <-> ( ph -> ( N e. ( 1 ... (♯ ` A ) ) -> ( seq M ( .+ , F ) ` ( G ` N ) ) = ( seq 1 ( .+ , H ) ` N ) ) ) ) )
28		seqcoll.1	. . . . . . . . 9 |- ( ( ph /\ k e. S ) -> ( Z .+ k ) = k )
29		seqcoll.a	. . . . . . . . 9 |- ( ph -> Z e. S )
30		seqcoll.4	. . . . . . . . . 10 |- ( ph -> A C_ ( ZZ>= ` M ) )
31		seqcoll.2	. . . . . . . . . . . . 13 |- ( ph -> G Isom < , < ( ( 1 ... (♯ ` A ) ) , A ) )
32		isof1o 5810	. . . . . . . . . . . . 13 |- ( G Isom < , < ( ( 1 ... (♯ ` A ) ) , A ) -> G : ( 1 ... (♯ ` A ) ) -1-1-onto-> A )
33	31, 32	syl 14	. . . . . . . . . . . 12 |- ( ph -> G : ( 1 ... (♯ ` A ) ) -1-1-onto-> A )
34		f1of 5463	. . . . . . . . . . . 12 |- ( G : ( 1 ... (♯ ` A ) ) -1-1-onto-> A -> G : ( 1 ... (♯ ` A ) ) --> A )
35	33, 34	syl 14	. . . . . . . . . . 11 |- ( ph -> G : ( 1 ... (♯ ` A ) ) --> A )
36		elfzuz2 10031	. . . . . . . . . . . . 13 |- ( N e. ( 1 ... (♯ ` A ) ) -> (♯ ` A ) e. ( ZZ>= ` 1 ) )
37	1, 36	syl 14	. . . . . . . . . . . 12 |- ( ph -> (♯ ` A ) e. ( ZZ>= ` 1 ) )
38		eluzfz1 10033	. . . . . . . . . . . 12 |- ( (♯ ` A ) e. ( ZZ>= ` 1 ) -> 1 e. ( 1 ... (♯ ` A ) ) )
39	37, 38	syl 14	. . . . . . . . . . 11 |- ( ph -> 1 e. ( 1 ... (♯ ` A ) ) )
40	35, 39	ffvelcdmd 5654	. . . . . . . . . 10 |- ( ph -> ( G ` 1 ) e. A )
41	30, 40	sseldd 3158	. . . . . . . . 9 |- ( ph -> ( G ` 1 ) e. ( ZZ>= ` M ) )
42		eluzle 9542	. . . . . . . . . . . . 13 |- ( (♯ ` A ) e. ( ZZ>= ` 1 ) -> 1 <_ (♯ ` A ) )
43	37, 42	syl 14	. . . . . . . . . . . 12 |- ( ph -> 1 <_ (♯ ` A ) )
44		elfzelz 10027	. . . . . . . . . . . . . . . . 17 |- ( k e. ( 1 ... (♯ ` A ) ) -> k e. ZZ )
45	44	ssriv 3161	. . . . . . . . . . . . . . . 16 |- ( 1 ... (♯ ` A ) ) C_ ZZ
46		zssre 9262	. . . . . . . . . . . . . . . 16 |- ZZ C_ RR
47	45, 46	sstri 3166	. . . . . . . . . . . . . . 15 |- ( 1 ... (♯ ` A ) ) C_ RR
48	47	a1i 9	. . . . . . . . . . . . . 14 |- ( ph -> ( 1 ... (♯ ` A ) ) C_ RR )
49		ressxr 8003	. . . . . . . . . . . . . 14 |- RR C_ RR*
50	48, 49	sstrdi 3169	. . . . . . . . . . . . 13 |- ( ph -> ( 1 ... (♯ ` A ) ) C_ RR* )
51		eluzelre 9540	. . . . . . . . . . . . . . . 16 |- ( k e. ( ZZ>= ` M ) -> k e. RR )
52	51	ssriv 3161	. . . . . . . . . . . . . . 15 |- ( ZZ>= ` M ) C_ RR
53	30, 52	sstrdi 3169	. . . . . . . . . . . . . 14 |- ( ph -> A C_ RR )
54	53, 49	sstrdi 3169	. . . . . . . . . . . . 13 |- ( ph -> A C_ RR* )
55		eluzfz2 10034	. . . . . . . . . . . . . 14 |- ( (♯ ` A ) e. ( ZZ>= ` 1 ) -> (♯ ` A ) e. ( 1 ... (♯ ` A ) ) )
56	37, 55	syl 14	. . . . . . . . . . . . 13 |- ( ph -> (♯ ` A ) e. ( 1 ... (♯ ` A ) ) )
57		leisorel 10819	. . . . . . . . . . . . 13 |- ( ( G Isom < , < ( ( 1 ... (♯ ` A ) ) , A ) /\ ( ( 1 ... (♯ ` A ) ) C_ RR* /\ A C_ RR* ) /\ ( 1 e. ( 1 ... (♯ ` A ) ) /\ (♯ ` A ) e. ( 1 ... (♯ ` A ) ) ) ) -> ( 1 <_ (♯ ` A ) <-> ( G ` 1 ) <_ ( G ` (♯ ` A ) ) ) )
58	31, 50, 54, 39, 56, 57	syl122anc 1247	. . . . . . . . . . . 12 |- ( ph -> ( 1 <_ (♯ ` A ) <-> ( G ` 1 ) <_ ( G ` (♯ ` A ) ) ) )
59	43, 58	mpbid 147	. . . . . . . . . . 11 |- ( ph -> ( G ` 1 ) <_ ( G ` (♯ ` A ) ) )
60	35, 56	ffvelcdmd 5654	. . . . . . . . . . . . . 14 |- ( ph -> ( G ` (♯ ` A ) ) e. A )
61	30, 60	sseldd 3158	. . . . . . . . . . . . 13 |- ( ph -> ( G ` (♯ ` A ) ) e. ( ZZ>= ` M ) )
62		eluzelz 9539	. . . . . . . . . . . . 13 |- ( ( G ` (♯ ` A ) ) e. ( ZZ>= ` M ) -> ( G ` (♯ ` A ) ) e. ZZ )
63	61, 62	syl 14	. . . . . . . . . . . 12 |- ( ph -> ( G ` (♯ ` A ) ) e. ZZ )
64		elfz5 10019	. . . . . . . . . . . 12 |- ( ( ( G ` 1 ) e. ( ZZ>= ` M ) /\ ( G ` (♯ ` A ) ) e. ZZ ) -> ( ( G ` 1 ) e. ( M ... ( G ` (♯ ` A ) ) ) <-> ( G ` 1 ) <_ ( G ` (♯ ` A ) ) ) )
65	41, 63, 64	syl2anc 411	. . . . . . . . . . 11 |- ( ph -> ( ( G ` 1 ) e. ( M ... ( G ` (♯ ` A ) ) ) <-> ( G ` 1 ) <_ ( G ` (♯ ` A ) ) ) )
66	59, 65	mpbird 167	. . . . . . . . . 10 |- ( ph -> ( G ` 1 ) e. ( M ... ( G ` (♯ ` A ) ) ) )
67		fveq2 5517	. . . . . . . . . . . . 13 |- ( k = ( G ` 1 ) -> ( F ` k ) = ( F ` ( G ` 1 ) ) )
68	67	eleq1d 2246	. . . . . . . . . . . 12 |- ( k = ( G ` 1 ) -> ( ( F ` k ) e. S <-> ( F ` ( G ` 1 ) ) e. S ) )
69	68	imbi2d 230	. . . . . . . . . . 11 |- ( k = ( G ` 1 ) -> ( ( ph -> ( F ` k ) e. S ) <-> ( ph -> ( F ` ( G ` 1 ) ) e. S ) ) )
70		elfzuz 10023	. . . . . . . . . . . 12 |- ( k e. ( M ... ( G ` (♯ ` A ) ) ) -> k e. ( ZZ>= ` M ) )
71		seqcoll.5	. . . . . . . . . . . . 13 |- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( F ` k ) e. S )
72	71	expcom 116	. . . . . . . . . . . 12 |- ( k e. ( ZZ>= ` M ) -> ( ph -> ( F ` k ) e. S ) )
73	70, 72	syl 14	. . . . . . . . . . 11 |- ( k e. ( M ... ( G ` (♯ ` A ) ) ) -> ( ph -> ( F ` k ) e. S ) )
74	69, 73	vtoclga 2805	. . . . . . . . . 10 |- ( ( G ` 1 ) e. ( M ... ( G ` (♯ ` A ) ) ) -> ( ph -> ( F ` ( G ` 1 ) ) e. S ) )
75	66, 74	mpcom 36	. . . . . . . . 9 |- ( ph -> ( F ` ( G ` 1 ) ) e. S )
76		eluzelz 9539	. . . . . . . . . . . . . . . . . 18 |- ( ( G ` 1 ) e. ( ZZ>= ` M ) -> ( G ` 1 ) e. ZZ )
77	41, 76	syl 14	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( G ` 1 ) e. ZZ )
78		peano2zm 9293	. . . . . . . . . . . . . . . . 17 |- ( ( G ` 1 ) e. ZZ -> ( ( G ` 1 ) - 1 ) e. ZZ )
79	77, 78	syl 14	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( G ` 1 ) - 1 ) e. ZZ )
80	79	zred 9377	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( G ` 1 ) - 1 ) e. RR )
81	77	zred 9377	. . . . . . . . . . . . . . 15 |- ( ph -> ( G ` 1 ) e. RR )
82	63	zred 9377	. . . . . . . . . . . . . . 15 |- ( ph -> ( G ` (♯ ` A ) ) e. RR )
83	81	lem1d 8892	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( G ` 1 ) - 1 ) <_ ( G ` 1 ) )
84	80, 81, 82, 83, 59	letrd 8083	. . . . . . . . . . . . . 14 |- ( ph -> ( ( G ` 1 ) - 1 ) <_ ( G ` (♯ ` A ) ) )
85		eluz 9543	. . . . . . . . . . . . . . 15 |- ( ( ( ( G ` 1 ) - 1 ) e. ZZ /\ ( G ` (♯ ` A ) ) e. ZZ ) -> ( ( G ` (♯ ` A ) ) e. ( ZZ>= ` ( ( G ` 1 ) - 1 ) ) <-> ( ( G ` 1 ) - 1 ) <_ ( G ` (♯ ` A ) ) ) )
86	79, 63, 85	syl2anc 411	. . . . . . . . . . . . . 14 |- ( ph -> ( ( G ` (♯ ` A ) ) e. ( ZZ>= ` ( ( G ` 1 ) - 1 ) ) <-> ( ( G ` 1 ) - 1 ) <_ ( G ` (♯ ` A ) ) ) )
87	84, 86	mpbird 167	. . . . . . . . . . . . 13 |- ( ph -> ( G ` (♯ ` A ) ) e. ( ZZ>= ` ( ( G ` 1 ) - 1 ) ) )
88		fzss2 10066	. . . . . . . . . . . . 13 |- ( ( G ` (♯ ` A ) ) e. ( ZZ>= ` ( ( G ` 1 ) - 1 ) ) -> ( M ... ( ( G ` 1 ) - 1 ) ) C_ ( M ... ( G ` (♯ ` A ) ) ) )
89	87, 88	syl 14	. . . . . . . . . . . 12 |- ( ph -> ( M ... ( ( G ` 1 ) - 1 ) ) C_ ( M ... ( G ` (♯ ` A ) ) ) )
90	89	sselda 3157	. . . . . . . . . . 11 |- ( ( ph /\ k e. ( M ... ( ( G ` 1 ) - 1 ) ) ) -> k e. ( M ... ( G ` (♯ ` A ) ) ) )
91		eluzel2 9535	. . . . . . . . . . . . . . 15 |- ( ( G ` 1 ) e. ( ZZ>= ` M ) -> M e. ZZ )
92	41, 91	syl 14	. . . . . . . . . . . . . 14 |- ( ph -> M e. ZZ )
93		elfzm11 10093	. . . . . . . . . . . . . 14 |- ( ( M e. ZZ /\ ( G ` 1 ) e. ZZ ) -> ( k e. ( M ... ( ( G ` 1 ) - 1 ) ) <-> ( k e. ZZ /\ M <_ k /\ k < ( G ` 1 ) ) ) )
94	92, 77, 93	syl2anc 411	. . . . . . . . . . . . 13 |- ( ph -> ( k e. ( M ... ( ( G ` 1 ) - 1 ) ) <-> ( k e. ZZ /\ M <_ k /\ k < ( G ` 1 ) ) ) )
95		simp3 999	. . . . . . . . . . . . . 14 |- ( ( k e. ZZ /\ M <_ k /\ k < ( G ` 1 ) ) -> k < ( G ` 1 ) )
96	81	adantr 276	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ k e. A ) -> ( G ` 1 ) e. RR )
97	53	sselda 3157	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ k e. A ) -> k e. RR )
98		f1ocnv 5476	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( G : ( 1 ... (♯ ` A ) ) -1-1-onto-> A -> `' G : A -1-1-onto-> ( 1 ... (♯ ` A ) ) )
99	33, 98	syl 14	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> `' G : A -1-1-onto-> ( 1 ... (♯ ` A ) ) )
100		f1of 5463	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( `' G : A -1-1-onto-> ( 1 ... (♯ ` A ) ) -> `' G : A --> ( 1 ... (♯ ` A ) ) )
101	99, 100	syl 14	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> `' G : A --> ( 1 ... (♯ ` A ) ) )
102	101	ffvelcdmda 5653	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ k e. A ) -> ( `' G ` k ) e. ( 1 ... (♯ ` A ) ) )
103		elfznn 10056	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( `' G ` k ) e. ( 1 ... (♯ ` A ) ) -> ( `' G ` k ) e. NN )
104	102, 103	syl 14	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ k e. A ) -> ( `' G ` k ) e. NN )
105	104	nnge1d 8964	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ k e. A ) -> 1 <_ ( `' G ` k ) )
106	31	adantr 276	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ k e. A ) -> G Isom < , < ( ( 1 ... (♯ ` A ) ) , A ) )
107	50	adantr 276	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ k e. A ) -> ( 1 ... (♯ ` A ) ) C_ RR* )
108	54	adantr 276	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ k e. A ) -> A C_ RR* )
109	39	adantr 276	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ k e. A ) -> 1 e. ( 1 ... (♯ ` A ) ) )
110		leisorel 10819	. . . . . . . . . . . . . . . . . . . 20 |- ( ( G Isom < , < ( ( 1 ... (♯ ` A ) ) , A ) /\ ( ( 1 ... (♯ ` A ) ) C_ RR* /\ A C_ RR* ) /\ ( 1 e. ( 1 ... (♯ ` A ) ) /\ ( `' G ` k ) e. ( 1 ... (♯ ` A ) ) ) ) -> ( 1 <_ ( `' G ` k ) <-> ( G ` 1 ) <_ ( G ` ( `' G ` k ) ) ) )
111	106, 107, 108, 109, 102, 110	syl122anc 1247	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ k e. A ) -> ( 1 <_ ( `' G ` k ) <-> ( G ` 1 ) <_ ( G ` ( `' G ` k ) ) ) )
112	105, 111	mpbid 147	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ k e. A ) -> ( G ` 1 ) <_ ( G ` ( `' G ` k ) ) )
113		f1ocnvfv2 5781	. . . . . . . . . . . . . . . . . . 19 |- ( ( G : ( 1 ... (♯ ` A ) ) -1-1-onto-> A /\ k e. A ) -> ( G ` ( `' G ` k ) ) = k )
114	33, 113	sylan 283	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ k e. A ) -> ( G ` ( `' G ` k ) ) = k )
115	112, 114	breqtrd 4031	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ k e. A ) -> ( G ` 1 ) <_ k )
116	96, 97, 115	lensymd 8081	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ k e. A ) -> -. k < ( G ` 1 ) )
117	116	ex 115	. . . . . . . . . . . . . . 15 |- ( ph -> ( k e. A -> -. k < ( G ` 1 ) ) )
118	117	con2d 624	. . . . . . . . . . . . . 14 |- ( ph -> ( k < ( G ` 1 ) -> -. k e. A ) )
119	95, 118	syl5 32	. . . . . . . . . . . . 13 |- ( ph -> ( ( k e. ZZ /\ M <_ k /\ k < ( G ` 1 ) ) -> -. k e. A ) )
120	94, 119	sylbid 150	. . . . . . . . . . . 12 |- ( ph -> ( k e. ( M ... ( ( G ` 1 ) - 1 ) ) -> -. k e. A ) )
121	120	imp 124	. . . . . . . . . . 11 |- ( ( ph /\ k e. ( M ... ( ( G ` 1 ) - 1 ) ) ) -> -. k e. A )
122	90, 121	eldifd 3141	. . . . . . . . . 10 |- ( ( ph /\ k e. ( M ... ( ( G ` 1 ) - 1 ) ) ) -> k e. ( ( M ... ( G ` (♯ ` A ) ) ) \ A ) )
123		seqcoll.6	. . . . . . . . . 10 |- ( ( ph /\ k e. ( ( M ... ( G ` (♯ ` A ) ) ) \ A ) ) -> ( F ` k ) = Z )
124	122, 123	syldan 282	. . . . . . . . 9 |- ( ( ph /\ k e. ( M ... ( ( G ` 1 ) - 1 ) ) ) -> ( F ` k ) = Z )
125		seqcoll.c	. . . . . . . . 9 |- ( ( ph /\ ( k e. S /\ n e. S ) ) -> ( k .+ n ) e. S )
126	28, 29, 41, 75, 124, 71, 125	seq3id 10510	. . . . . . . 8 |- ( ph -> ( seq M ( .+ , F ) |` ( ZZ>= ` ( G ` 1 ) ) ) = seq ( G ` 1 ) ( .+ , F ) )
127	126	fveq1d 5519	. . . . . . 7 |- ( ph -> ( ( seq M ( .+ , F ) |` ( ZZ>= ` ( G ` 1 ) ) ) ` ( G ` 1 ) ) = ( seq ( G ` 1 ) ( .+ , F ) ` ( G ` 1 ) ) )
128		uzid 9544	. . . . . . . . 9 |- ( ( G ` 1 ) e. ZZ -> ( G ` 1 ) e. ( ZZ>= ` ( G ` 1 ) ) )
129	77, 128	syl 14	. . . . . . . 8 |- ( ph -> ( G ` 1 ) e. ( ZZ>= ` ( G ` 1 ) ) )
130		fvres 5541	. . . . . . . 8 |- ( ( G ` 1 ) e. ( ZZ>= ` ( G ` 1 ) ) -> ( ( seq M ( .+ , F ) |` ( ZZ>= ` ( G ` 1 ) ) ) ` ( G ` 1 ) ) = ( seq M ( .+ , F ) ` ( G ` 1 ) ) )
131	129, 130	syl 14	. . . . . . 7 |- ( ph -> ( ( seq M ( .+ , F ) |` ( ZZ>= ` ( G ` 1 ) ) ) ` ( G ` 1 ) ) = ( seq M ( .+ , F ) ` ( G ` 1 ) ) )
132	92	adantr 276	. . . . . . . . . . 11 |- ( ( ph /\ k e. ( ZZ>= ` ( G ` 1 ) ) ) -> M e. ZZ )
133		eluzelz 9539	. . . . . . . . . . . 12 |- ( k e. ( ZZ>= ` ( G ` 1 ) ) -> k e. ZZ )
134	133	adantl 277	. . . . . . . . . . 11 |- ( ( ph /\ k e. ( ZZ>= ` ( G ` 1 ) ) ) -> k e. ZZ )
135	132	zred 9377	. . . . . . . . . . . 12 |- ( ( ph /\ k e. ( ZZ>= ` ( G ` 1 ) ) ) -> M e. RR )
136	81	adantr 276	. . . . . . . . . . . 12 |- ( ( ph /\ k e. ( ZZ>= ` ( G ` 1 ) ) ) -> ( G ` 1 ) e. RR )
137	134	zred 9377	. . . . . . . . . . . 12 |- ( ( ph /\ k e. ( ZZ>= ` ( G ` 1 ) ) ) -> k e. RR )
138		eluzle 9542	. . . . . . . . . . . . . 14 |- ( ( G ` 1 ) e. ( ZZ>= ` M ) -> M <_ ( G ` 1 ) )
139	41, 138	syl 14	. . . . . . . . . . . . 13 |- ( ph -> M <_ ( G ` 1 ) )
140	139	adantr 276	. . . . . . . . . . . 12 |- ( ( ph /\ k e. ( ZZ>= ` ( G ` 1 ) ) ) -> M <_ ( G ` 1 ) )
141		eluzle 9542	. . . . . . . . . . . . 13 |- ( k e. ( ZZ>= ` ( G ` 1 ) ) -> ( G ` 1 ) <_ k )
142	141	adantl 277	. . . . . . . . . . . 12 |- ( ( ph /\ k e. ( ZZ>= ` ( G ` 1 ) ) ) -> ( G ` 1 ) <_ k )
143	135, 136, 137, 140, 142	letrd 8083	. . . . . . . . . . 11 |- ( ( ph /\ k e. ( ZZ>= ` ( G ` 1 ) ) ) -> M <_ k )
144		eluz2 9536	. . . . . . . . . . 11 |- ( k e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ k e. ZZ /\ M <_ k ) )
145	132, 134, 143, 144	syl3anbrc 1181	. . . . . . . . . 10 |- ( ( ph /\ k e. ( ZZ>= ` ( G ` 1 ) ) ) -> k e. ( ZZ>= ` M ) )
146	145, 71	syldan 282	. . . . . . . . 9 |- ( ( ph /\ k e. ( ZZ>= ` ( G ` 1 ) ) ) -> ( F ` k ) e. S )
147	77, 146, 125	seq3-1 10462	. . . . . . . 8 |- ( ph -> ( seq ( G ` 1 ) ( .+ , F ) ` ( G ` 1 ) ) = ( F ` ( G ` 1 ) ) )
148		fveq2 5517	. . . . . . . . . . . 12 |- ( n = 1 -> ( H ` n ) = ( H ` 1 ) )
149		2fveq3 5522	. . . . . . . . . . . 12 |- ( n = 1 -> ( F ` ( G ` n ) ) = ( F ` ( G ` 1 ) ) )
150	148, 149	eqeq12d 2192	. . . . . . . . . . 11 |- ( n = 1 -> ( ( H ` n ) = ( F ` ( G ` n ) ) <-> ( H ` 1 ) = ( F ` ( G ` 1 ) ) ) )
151	150	imbi2d 230	. . . . . . . . . 10 |- ( n = 1 -> ( ( ph -> ( H ` n ) = ( F ` ( G ` n ) ) ) <-> ( ph -> ( H ` 1 ) = ( F ` ( G ` 1 ) ) ) ) )
152		seqcoll.7	. . . . . . . . . . 11 |- ( ( ph /\ n e. ( 1 ... (♯ ` A ) ) ) -> ( H ` n ) = ( F ` ( G ` n ) ) )
153	152	expcom 116	. . . . . . . . . 10 |- ( n e. ( 1 ... (♯ ` A ) ) -> ( ph -> ( H ` n ) = ( F ` ( G ` n ) ) ) )
154	151, 153	vtoclga 2805	. . . . . . . . 9 |- ( 1 e. ( 1 ... (♯ ` A ) ) -> ( ph -> ( H ` 1 ) = ( F ` ( G ` 1 ) ) ) )
155	39, 154	mpcom 36	. . . . . . . 8 |- ( ph -> ( H ` 1 ) = ( F ` ( G ` 1 ) ) )
156	147, 155	eqtr4d 2213	. . . . . . 7 |- ( ph -> ( seq ( G ` 1 ) ( .+ , F ) ` ( G ` 1 ) ) = ( H ` 1 ) )
157	127, 131, 156	3eqtr3d 2218	. . . . . 6 |- ( ph -> ( seq M ( .+ , F ) ` ( G ` 1 ) ) = ( H ` 1 ) )
158		1zzd 9282	. . . . . . 7 |- ( ph -> 1 e. ZZ )
159		seqcoll.hcl	. . . . . . 7 |- ( ( ph /\ k e. ( ZZ>= ` 1 ) ) -> ( H ` k ) e. S )
160	158, 159, 125	seq3-1 10462	. . . . . 6 |- ( ph -> ( seq 1 ( .+ , H ) ` 1 ) = ( H ` 1 ) )
161	157, 160	eqtr4d 2213	. . . . 5 |- ( ph -> ( seq M ( .+ , F ) ` ( G ` 1 ) ) = ( seq 1 ( .+ , H ) ` 1 ) )
162	161	a1d 22	. . . 4 |- ( ph -> ( 1 e. ( 1 ... (♯ ` A ) ) -> ( seq M ( .+ , F ) ` ( G ` 1 ) ) = ( seq 1 ( .+ , H ) ` 1 ) ) )
163		simplr 528	. . . . . . . . . . 11 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> m e. NN )
164		nnuz 9565	. . . . . . . . . . 11 |- NN = ( ZZ>= ` 1 )
165	163, 164	eleqtrdi 2270	. . . . . . . . . 10 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> m e. ( ZZ>= ` 1 ) )
166		nnz 9274	. . . . . . . . . . . 12 |- ( m e. NN -> m e. ZZ )
167	166	ad2antlr 489	. . . . . . . . . . 11 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> m e. ZZ )
168		elfzuz3 10024	. . . . . . . . . . . 12 |- ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) -> (♯ ` A ) e. ( ZZ>= ` ( m + 1 ) ) )
169	168	adantl 277	. . . . . . . . . . 11 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> (♯ ` A ) e. ( ZZ>= ` ( m + 1 ) ) )
170		peano2uzr 9587	. . . . . . . . . . 11 |- ( ( m e. ZZ /\ (♯ ` A ) e. ( ZZ>= ` ( m + 1 ) ) ) -> (♯ ` A ) e. ( ZZ>= ` m ) )
171	167, 169, 170	syl2anc 411	. . . . . . . . . 10 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> (♯ ` A ) e. ( ZZ>= ` m ) )
172		elfzuzb 10021	. . . . . . . . . 10 |- ( m e. ( 1 ... (♯ ` A ) ) <-> ( m e. ( ZZ>= ` 1 ) /\ (♯ ` A ) e. ( ZZ>= ` m ) ) )
173	165, 171, 172	sylanbrc 417	. . . . . . . . 9 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> m e. ( 1 ... (♯ ` A ) ) )
174	173	ex 115	. . . . . . . 8 |- ( ( ph /\ m e. NN ) -> ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) -> m e. ( 1 ... (♯ ` A ) ) ) )
175	174	imim1d 75	. . . . . . 7 |- ( ( ph /\ m e. NN ) -> ( ( m e. ( 1 ... (♯ ` A ) ) -> ( seq M ( .+ , F ) ` ( G ` m ) ) = ( seq 1 ( .+ , H ) ` m ) ) -> ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) -> ( seq M ( .+ , F ) ` ( G ` m ) ) = ( seq 1 ( .+ , H ) ` m ) ) ) )
176		oveq1 5884	. . . . . . . . . 10 |- ( ( seq M ( .+ , F ) ` ( G ` m ) ) = ( seq 1 ( .+ , H ) ` m ) -> ( ( seq M ( .+ , F ) ` ( G ` m ) ) .+ ( H ` ( m + 1 ) ) ) = ( ( seq 1 ( .+ , H ) ` m ) .+ ( H ` ( m + 1 ) ) ) )
177		simpll 527	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ph )
178		seqcoll.1b	. . . . . . . . . . . . . . 15 |- ( ( ph /\ k e. S ) -> ( k .+ Z ) = k )
179	177, 178	sylan 283	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) /\ k e. S ) -> ( k .+ Z ) = k )
180	30	ad2antrr 488	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> A C_ ( ZZ>= ` M ) )
181	35	ad2antrr 488	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> G : ( 1 ... (♯ ` A ) ) --> A )
182	181, 173	ffvelcdmd 5654	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( G ` m ) e. A )
183	180, 182	sseldd 3158	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( G ` m ) e. ( ZZ>= ` M ) )
184		nnre 8928	. . . . . . . . . . . . . . . . . . 19 |- ( m e. NN -> m e. RR )
185	184	ad2antlr 489	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> m e. RR )
186	185	ltp1d 8889	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> m < ( m + 1 ) )
187	31	ad2antrr 488	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> G Isom < , < ( ( 1 ... (♯ ` A ) ) , A ) )
188		simpr 110	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( m + 1 ) e. ( 1 ... (♯ ` A ) ) )
189		isorel 5811	. . . . . . . . . . . . . . . . . 18 |- ( ( G Isom < , < ( ( 1 ... (♯ ` A ) ) , A ) /\ ( m e. ( 1 ... (♯ ` A ) ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) ) -> ( m < ( m + 1 ) <-> ( G ` m ) < ( G ` ( m + 1 ) ) ) )
190	187, 173, 188, 189	syl12anc 1236	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( m < ( m + 1 ) <-> ( G ` m ) < ( G ` ( m + 1 ) ) ) )
191	186, 190	mpbid 147	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( G ` m ) < ( G ` ( m + 1 ) ) )
192		eluzelz 9539	. . . . . . . . . . . . . . . . . 18 |- ( ( G ` m ) e. ( ZZ>= ` M ) -> ( G ` m ) e. ZZ )
193	183, 192	syl 14	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( G ` m ) e. ZZ )
194	181, 188	ffvelcdmd 5654	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( G ` ( m + 1 ) ) e. A )
195	180, 194	sseldd 3158	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( G ` ( m + 1 ) ) e. ( ZZ>= ` M ) )
196		eluzelz 9539	. . . . . . . . . . . . . . . . . 18 |- ( ( G ` ( m + 1 ) ) e. ( ZZ>= ` M ) -> ( G ` ( m + 1 ) ) e. ZZ )
197	195, 196	syl 14	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( G ` ( m + 1 ) ) e. ZZ )
198		zltlem1 9312	. . . . . . . . . . . . . . . . 17 |- ( ( ( G ` m ) e. ZZ /\ ( G ` ( m + 1 ) ) e. ZZ ) -> ( ( G ` m ) < ( G ` ( m + 1 ) ) <-> ( G ` m ) <_ ( ( G ` ( m + 1 ) ) - 1 ) ) )
199	193, 197, 198	syl2anc 411	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( ( G ` m ) < ( G ` ( m + 1 ) ) <-> ( G ` m ) <_ ( ( G ` ( m + 1 ) ) - 1 ) ) )
200	191, 199	mpbid 147	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( G ` m ) <_ ( ( G ` ( m + 1 ) ) - 1 ) )
201		peano2zm 9293	. . . . . . . . . . . . . . . . 17 |- ( ( G ` ( m + 1 ) ) e. ZZ -> ( ( G ` ( m + 1 ) ) - 1 ) e. ZZ )
202	197, 201	syl 14	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( ( G ` ( m + 1 ) ) - 1 ) e. ZZ )
203		eluz 9543	. . . . . . . . . . . . . . . 16 |- ( ( ( G ` m ) e. ZZ /\ ( ( G ` ( m + 1 ) ) - 1 ) e. ZZ ) -> ( ( ( G ` ( m + 1 ) ) - 1 ) e. ( ZZ>= ` ( G ` m ) ) <-> ( G ` m ) <_ ( ( G ` ( m + 1 ) ) - 1 ) ) )
204	193, 202, 203	syl2anc 411	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( ( ( G ` ( m + 1 ) ) - 1 ) e. ( ZZ>= ` ( G ` m ) ) <-> ( G ` m ) <_ ( ( G ` ( m + 1 ) ) - 1 ) ) )
205	200, 204	mpbird 167	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( ( G ` ( m + 1 ) ) - 1 ) e. ( ZZ>= ` ( G ` m ) ) )
206		eqid 2177	. . . . . . . . . . . . . . . 16 |- ( ZZ>= ` M ) = ( ZZ>= ` M )
207	92	ad2antrr 488	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> M e. ZZ )
208	177, 71	sylan 283	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) /\ k e. ( ZZ>= ` M ) ) -> ( F ` k ) e. S )
209	177, 125	sylan 283	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) /\ ( k e. S /\ n e. S ) ) -> ( k .+ n ) e. S )
210	206, 207, 208, 209	seqf 10463	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> seq M ( .+ , F ) : ( ZZ>= ` M ) --> S )
211	210, 183	ffvelcdmd 5654	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( seq M ( .+ , F ) ` ( G ` m ) ) e. S )
212		simplll 533	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) /\ k e. ( ( ( G ` m ) + 1 ) ... ( ( G ` ( m + 1 ) ) - 1 ) ) ) -> ph )
213		elfzuz 10023	. . . . . . . . . . . . . . . . . 18 |- ( k e. ( ( ( G ` m ) + 1 ) ... ( ( G ` ( m + 1 ) ) - 1 ) ) -> k e. ( ZZ>= ` ( ( G ` m ) + 1 ) ) )
214		peano2uz 9585	. . . . . . . . . . . . . . . . . . 19 |- ( ( G ` m ) e. ( ZZ>= ` M ) -> ( ( G ` m ) + 1 ) e. ( ZZ>= ` M ) )
215	183, 214	syl 14	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( ( G ` m ) + 1 ) e. ( ZZ>= ` M ) )
216		uztrn 9546	. . . . . . . . . . . . . . . . . 18 |- ( ( k e. ( ZZ>= ` ( ( G ` m ) + 1 ) ) /\ ( ( G ` m ) + 1 ) e. ( ZZ>= ` M ) ) -> k e. ( ZZ>= ` M ) )
217	213, 215, 216	syl2anr 290	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) /\ k e. ( ( ( G ` m ) + 1 ) ... ( ( G ` ( m + 1 ) ) - 1 ) ) ) -> k e. ( ZZ>= ` M ) )
218	202	zred 9377	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( ( G ` ( m + 1 ) ) - 1 ) e. RR )
219	197	zred 9377	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( G ` ( m + 1 ) ) e. RR )
220	82	ad2antrr 488	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( G ` (♯ ` A ) ) e. RR )
221	219	lem1d 8892	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( ( G ` ( m + 1 ) ) - 1 ) <_ ( G ` ( m + 1 ) ) )
222		elfzle2 10030	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) -> ( m + 1 ) <_ (♯ ` A ) )
223	222	adantl 277	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( m + 1 ) <_ (♯ ` A ) )
224	50	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( 1 ... (♯ ` A ) ) C_ RR* )
225	54	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> A C_ RR* )
226	56	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> (♯ ` A ) e. ( 1 ... (♯ ` A ) ) )
227		leisorel 10819	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( G Isom < , < ( ( 1 ... (♯ ` A ) ) , A ) /\ ( ( 1 ... (♯ ` A ) ) C_ RR* /\ A C_ RR* ) /\ ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) /\ (♯ ` A ) e. ( 1 ... (♯ ` A ) ) ) ) -> ( ( m + 1 ) <_ (♯ ` A ) <-> ( G ` ( m + 1 ) ) <_ ( G ` (♯ ` A ) ) ) )
228	187, 224, 225, 188, 226, 227	syl122anc 1247	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( ( m + 1 ) <_ (♯ ` A ) <-> ( G ` ( m + 1 ) ) <_ ( G ` (♯ ` A ) ) ) )
229	223, 228	mpbid 147	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( G ` ( m + 1 ) ) <_ ( G ` (♯ ` A ) ) )
230	218, 219, 220, 221, 229	letrd 8083	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( ( G ` ( m + 1 ) ) - 1 ) <_ ( G ` (♯ ` A ) ) )
231	63	ad2antrr 488	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( G ` (♯ ` A ) ) e. ZZ )
232		eluz 9543	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( G ` ( m + 1 ) ) - 1 ) e. ZZ /\ ( G ` (♯ ` A ) ) e. ZZ ) -> ( ( G ` (♯ ` A ) ) e. ( ZZ>= ` ( ( G ` ( m + 1 ) ) - 1 ) ) <-> ( ( G ` ( m + 1 ) ) - 1 ) <_ ( G ` (♯ ` A ) ) ) )
233	202, 231, 232	syl2anc 411	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( ( G ` (♯ ` A ) ) e. ( ZZ>= ` ( ( G ` ( m + 1 ) ) - 1 ) ) <-> ( ( G ` ( m + 1 ) ) - 1 ) <_ ( G ` (♯ ` A ) ) ) )
234	230, 233	mpbird 167	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( G ` (♯ ` A ) ) e. ( ZZ>= ` ( ( G ` ( m + 1 ) ) - 1 ) ) )
235		elfzuz3 10024	. . . . . . . . . . . . . . . . . 18 |- ( k e. ( ( ( G ` m ) + 1 ) ... ( ( G ` ( m + 1 ) ) - 1 ) ) -> ( ( G ` ( m + 1 ) ) - 1 ) e. ( ZZ>= ` k ) )
236		uztrn 9546	. . . . . . . . . . . . . . . . . 18 |- ( ( ( G ` (♯ ` A ) ) e. ( ZZ>= ` ( ( G ` ( m + 1 ) ) - 1 ) ) /\ ( ( G ` ( m + 1 ) ) - 1 ) e. ( ZZ>= ` k ) ) -> ( G ` (♯ ` A ) ) e. ( ZZ>= ` k ) )
237	234, 235, 236	syl2an 289	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) /\ k e. ( ( ( G ` m ) + 1 ) ... ( ( G ` ( m + 1 ) ) - 1 ) ) ) -> ( G ` (♯ ` A ) ) e. ( ZZ>= ` k ) )
238		elfzuzb 10021	. . . . . . . . . . . . . . . . 17 |- ( k e. ( M ... ( G ` (♯ ` A ) ) ) <-> ( k e. ( ZZ>= ` M ) /\ ( G ` (♯ ` A ) ) e. ( ZZ>= ` k ) ) )
239	217, 237, 238	sylanbrc 417	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) /\ k e. ( ( ( G ` m ) + 1 ) ... ( ( G ` ( m + 1 ) ) - 1 ) ) ) -> k e. ( M ... ( G ` (♯ ` A ) ) ) )
240	166	ad2antlr 489	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) /\ k e. A ) ) -> m e. ZZ )
241	101	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) /\ k e. A ) ) -> `' G : A --> ( 1 ... (♯ ` A ) ) )
242		simprr 531	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) /\ k e. A ) ) -> k e. A )
243	241, 242	ffvelcdmd 5654	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) /\ k e. A ) ) -> ( `' G ` k ) e. ( 1 ... (♯ ` A ) ) )
244		elfzelz 10027	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( `' G ` k ) e. ( 1 ... (♯ ` A ) ) -> ( `' G ` k ) e. ZZ )
245	243, 244	syl 14	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) /\ k e. A ) ) -> ( `' G ` k ) e. ZZ )
246		btwnnz 9349	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( m e. ZZ /\ m < ( `' G ` k ) /\ ( `' G ` k ) < ( m + 1 ) ) -> -. ( `' G ` k ) e. ZZ )
247	246	3expib 1206	. . . . . . . . . . . . . . . . . . . . . 22 |- ( m e. ZZ -> ( ( m < ( `' G ` k ) /\ ( `' G ` k ) < ( m + 1 ) ) -> -. ( `' G ` k ) e. ZZ ) )
248	247	con2d 624	. . . . . . . . . . . . . . . . . . . . 21 |- ( m e. ZZ -> ( ( `' G ` k ) e. ZZ -> -. ( m < ( `' G ` k ) /\ ( `' G ` k ) < ( m + 1 ) ) ) )
249	240, 245, 248	sylc 62	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) /\ k e. A ) ) -> -. ( m < ( `' G ` k ) /\ ( `' G ` k ) < ( m + 1 ) ) )
250	31	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) /\ k e. A ) ) -> G Isom < , < ( ( 1 ... (♯ ` A ) ) , A ) )
251	173	adantrr 479	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) /\ k e. A ) ) -> m e. ( 1 ... (♯ ` A ) ) )
252		isorel 5811	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( G Isom < , < ( ( 1 ... (♯ ` A ) ) , A ) /\ ( m e. ( 1 ... (♯ ` A ) ) /\ ( `' G ` k ) e. ( 1 ... (♯ ` A ) ) ) ) -> ( m < ( `' G ` k ) <-> ( G ` m ) < ( G ` ( `' G ` k ) ) ) )
253	250, 251, 243, 252	syl12anc 1236	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) /\ k e. A ) ) -> ( m < ( `' G ` k ) <-> ( G ` m ) < ( G ` ( `' G ` k ) ) ) )
254	33	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) /\ k e. A ) ) -> G : ( 1 ... (♯ ` A ) ) -1-1-onto-> A )
255	254, 242, 113	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) /\ k e. A ) ) -> ( G ` ( `' G ` k ) ) = k )
256	255	breq2d 4017	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) /\ k e. A ) ) -> ( ( G ` m ) < ( G ` ( `' G ` k ) ) <-> ( G ` m ) < k ) )
257	193	adantrr 479	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) /\ k e. A ) ) -> ( G ` m ) e. ZZ )
258	30	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) /\ k e. A ) ) -> A C_ ( ZZ>= ` M ) )
259	258, 242	sseldd 3158	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) /\ k e. A ) ) -> k e. ( ZZ>= ` M ) )
260		eluzelz 9539	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( k e. ( ZZ>= ` M ) -> k e. ZZ )
261	259, 260	syl 14	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) /\ k e. A ) ) -> k e. ZZ )
262		zltp1le 9309	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( G ` m ) e. ZZ /\ k e. ZZ ) -> ( ( G ` m ) < k <-> ( ( G ` m ) + 1 ) <_ k ) )
263	257, 261, 262	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) /\ k e. A ) ) -> ( ( G ` m ) < k <-> ( ( G ` m ) + 1 ) <_ k ) )
264	253, 256, 263	3bitrd 214	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) /\ k e. A ) ) -> ( m < ( `' G ` k ) <-> ( ( G ` m ) + 1 ) <_ k ) )
265	188	adantrr 479	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) /\ k e. A ) ) -> ( m + 1 ) e. ( 1 ... (♯ ` A ) ) )
266		isorel 5811	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( G Isom < , < ( ( 1 ... (♯ ` A ) ) , A ) /\ ( ( `' G ` k ) e. ( 1 ... (♯ ` A ) ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) ) -> ( ( `' G ` k ) < ( m + 1 ) <-> ( G ` ( `' G ` k ) ) < ( G ` ( m + 1 ) ) ) )
267	250, 243, 265, 266	syl12anc 1236	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) /\ k e. A ) ) -> ( ( `' G ` k ) < ( m + 1 ) <-> ( G ` ( `' G ` k ) ) < ( G ` ( m + 1 ) ) ) )
268	255	breq1d 4015	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) /\ k e. A ) ) -> ( ( G ` ( `' G ` k ) ) < ( G ` ( m + 1 ) ) <-> k < ( G ` ( m + 1 ) ) ) )
269	197	adantrr 479	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) /\ k e. A ) ) -> ( G ` ( m + 1 ) ) e. ZZ )
270		zltlem1 9312	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( k e. ZZ /\ ( G ` ( m + 1 ) ) e. ZZ ) -> ( k < ( G ` ( m + 1 ) ) <-> k <_ ( ( G ` ( m + 1 ) ) - 1 ) ) )
271	261, 269, 270	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) /\ k e. A ) ) -> ( k < ( G ` ( m + 1 ) ) <-> k <_ ( ( G ` ( m + 1 ) ) - 1 ) ) )
272	267, 268, 271	3bitrd 214	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) /\ k e. A ) ) -> ( ( `' G ` k ) < ( m + 1 ) <-> k <_ ( ( G ` ( m + 1 ) ) - 1 ) ) )
273	264, 272	anbi12d 473	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) /\ k e. A ) ) -> ( ( m < ( `' G ` k ) /\ ( `' G ` k ) < ( m + 1 ) ) <-> ( ( ( G ` m ) + 1 ) <_ k /\ k <_ ( ( G ` ( m + 1 ) ) - 1 ) ) ) )
274	249, 273	mtbid 672	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) /\ k e. A ) ) -> -. ( ( ( G ` m ) + 1 ) <_ k /\ k <_ ( ( G ` ( m + 1 ) ) - 1 ) ) )
275	274	expr 375	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( k e. A -> -. ( ( ( G ` m ) + 1 ) <_ k /\ k <_ ( ( G ` ( m + 1 ) ) - 1 ) ) ) )
276	275	con2d 624	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( ( ( ( G ` m ) + 1 ) <_ k /\ k <_ ( ( G ` ( m + 1 ) ) - 1 ) ) -> -. k e. A ) )
277		elfzle1 10029	. . . . . . . . . . . . . . . . . 18 |- ( k e. ( ( ( G ` m ) + 1 ) ... ( ( G ` ( m + 1 ) ) - 1 ) ) -> ( ( G ` m ) + 1 ) <_ k )
278		elfzle2 10030	. . . . . . . . . . . . . . . . . 18 |- ( k e. ( ( ( G ` m ) + 1 ) ... ( ( G ` ( m + 1 ) ) - 1 ) ) -> k <_ ( ( G ` ( m + 1 ) ) - 1 ) )
279	277, 278	jca 306	. . . . . . . . . . . . . . . . 17 |- ( k e. ( ( ( G ` m ) + 1 ) ... ( ( G ` ( m + 1 ) ) - 1 ) ) -> ( ( ( G ` m ) + 1 ) <_ k /\ k <_ ( ( G ` ( m + 1 ) ) - 1 ) ) )
280	276, 279	impel 280	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) /\ k e. ( ( ( G ` m ) + 1 ) ... ( ( G ` ( m + 1 ) ) - 1 ) ) ) -> -. k e. A )
281	239, 280	eldifd 3141	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) /\ k e. ( ( ( G ` m ) + 1 ) ... ( ( G ` ( m + 1 ) ) - 1 ) ) ) -> k e. ( ( M ... ( G ` (♯ ` A ) ) ) \ A ) )
282	212, 281, 123	syl2anc 411	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) /\ k e. ( ( ( G ` m ) + 1 ) ... ( ( G ` ( m + 1 ) ) - 1 ) ) ) -> ( F ` k ) = Z )
283	179, 183, 205, 211, 282, 208, 209	seq3id2 10511	. . . . . . . . . . . . 13 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( seq M ( .+ , F ) ` ( G ` m ) ) = ( seq M ( .+ , F ) ` ( ( G ` ( m + 1 ) ) - 1 ) ) )
284	283	oveq1d 5892	. . . . . . . . . . . 12 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( ( seq M ( .+ , F ) ` ( G ` m ) ) .+ ( F ` ( G ` ( m + 1 ) ) ) ) = ( ( seq M ( .+ , F ) ` ( ( G ` ( m + 1 ) ) - 1 ) ) .+ ( F ` ( G ` ( m + 1 ) ) ) ) )
285		fveq2 5517	. . . . . . . . . . . . . . . . . 18 |- ( n = ( m + 1 ) -> ( H ` n ) = ( H ` ( m + 1 ) ) )
286		2fveq3 5522	. . . . . . . . . . . . . . . . . 18 |- ( n = ( m + 1 ) -> ( F ` ( G ` n ) ) = ( F ` ( G ` ( m + 1 ) ) ) )
287	285, 286	eqeq12d 2192	. . . . . . . . . . . . . . . . 17 |- ( n = ( m + 1 ) -> ( ( H ` n ) = ( F ` ( G ` n ) ) <-> ( H ` ( m + 1 ) ) = ( F ` ( G ` ( m + 1 ) ) ) ) )
288	287	imbi2d 230	. . . . . . . . . . . . . . . 16 |- ( n = ( m + 1 ) -> ( ( ph -> ( H ` n ) = ( F ` ( G ` n ) ) ) <-> ( ph -> ( H ` ( m + 1 ) ) = ( F ` ( G ` ( m + 1 ) ) ) ) ) )
289	288, 153	vtoclga 2805	. . . . . . . . . . . . . . 15 |- ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) -> ( ph -> ( H ` ( m + 1 ) ) = ( F ` ( G ` ( m + 1 ) ) ) ) )
290	289	impcom 125	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( H ` ( m + 1 ) ) = ( F ` ( G ` ( m + 1 ) ) ) )
291	290	adantlr 477	. . . . . . . . . . . . 13 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( H ` ( m + 1 ) ) = ( F ` ( G ` ( m + 1 ) ) ) )
292	291	oveq2d 5893	. . . . . . . . . . . 12 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( ( seq M ( .+ , F ) ` ( G ` m ) ) .+ ( H ` ( m + 1 ) ) ) = ( ( seq M ( .+ , F ) ` ( G ` m ) ) .+ ( F ` ( G ` ( m + 1 ) ) ) ) )
293	197	zcnd 9378	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( G ` ( m + 1 ) ) e. CC )
294		ax-1cn 7906	. . . . . . . . . . . . . . 15 |- 1 e. CC
295		npcan 8168	. . . . . . . . . . . . . . 15 |- ( ( ( G ` ( m + 1 ) ) e. CC /\ 1 e. CC ) -> ( ( ( G ` ( m + 1 ) ) - 1 ) + 1 ) = ( G ` ( m + 1 ) ) )
296	293, 294, 295	sylancl 413	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( ( ( G ` ( m + 1 ) ) - 1 ) + 1 ) = ( G ` ( m + 1 ) ) )
297		uztrn 9546	. . . . . . . . . . . . . . . 16 |- ( ( ( ( G ` ( m + 1 ) ) - 1 ) e. ( ZZ>= ` ( G ` m ) ) /\ ( G ` m ) e. ( ZZ>= ` M ) ) -> ( ( G ` ( m + 1 ) ) - 1 ) e. ( ZZ>= ` M ) )
298	205, 183, 297	syl2anc 411	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( ( G ` ( m + 1 ) ) - 1 ) e. ( ZZ>= ` M ) )
299		eluzp1p1 9555	. . . . . . . . . . . . . . 15 |- ( ( ( G ` ( m + 1 ) ) - 1 ) e. ( ZZ>= ` M ) -> ( ( ( G ` ( m + 1 ) ) - 1 ) + 1 ) e. ( ZZ>= ` ( M + 1 ) ) )
300	298, 299	syl 14	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( ( ( G ` ( m + 1 ) ) - 1 ) + 1 ) e. ( ZZ>= ` ( M + 1 ) ) )
301	296, 300	eqeltrrd 2255	. . . . . . . . . . . . 13 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( G ` ( m + 1 ) ) e. ( ZZ>= ` ( M + 1 ) ) )
302	207, 301, 208, 209	seq3m1 10470	. . . . . . . . . . . 12 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( seq M ( .+ , F ) ` ( G ` ( m + 1 ) ) ) = ( ( seq M ( .+ , F ) ` ( ( G ` ( m + 1 ) ) - 1 ) ) .+ ( F ` ( G ` ( m + 1 ) ) ) ) )
303	284, 292, 302	3eqtr4rd 2221	. . . . . . . . . . 11 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( seq M ( .+ , F ) ` ( G ` ( m + 1 ) ) ) = ( ( seq M ( .+ , F ) ` ( G ` m ) ) .+ ( H ` ( m + 1 ) ) ) )
304	177, 159	sylan 283	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) /\ k e. ( ZZ>= ` 1 ) ) -> ( H ` k ) e. S )
305	165, 304, 209	seq3p1 10464	. . . . . . . . . . 11 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( seq 1 ( .+ , H ) ` ( m + 1 ) ) = ( ( seq 1 ( .+ , H ) ` m ) .+ ( H ` ( m + 1 ) ) ) )
306	303, 305	eqeq12d 2192	. . . . . . . . . 10 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( ( seq M ( .+ , F ) ` ( G ` ( m + 1 ) ) ) = ( seq 1 ( .+ , H ) ` ( m + 1 ) ) <-> ( ( seq M ( .+ , F ) ` ( G ` m ) ) .+ ( H ` ( m + 1 ) ) ) = ( ( seq 1 ( .+ , H ) ` m ) .+ ( H ` ( m + 1 ) ) ) ) )
307	176, 306	imbitrrid 156	. . . . . . . . 9 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( ( seq M ( .+ , F ) ` ( G ` m ) ) = ( seq 1 ( .+ , H ) ` m ) -> ( seq M ( .+ , F ) ` ( G ` ( m + 1 ) ) ) = ( seq 1 ( .+ , H ) ` ( m + 1 ) ) ) )
308	307	ex 115	. . . . . . . 8 |- ( ( ph /\ m e. NN ) -> ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) -> ( ( seq M ( .+ , F ) ` ( G ` m ) ) = ( seq 1 ( .+ , H ) ` m ) -> ( seq M ( .+ , F ) ` ( G ` ( m + 1 ) ) ) = ( seq 1 ( .+ , H ) ` ( m + 1 ) ) ) ) )
309	308	a2d 26	. . . . . . 7 |- ( ( ph /\ m e. NN ) -> ( ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) -> ( seq M ( .+ , F ) ` ( G ` m ) ) = ( seq 1 ( .+ , H ) ` m ) ) -> ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) -> ( seq M ( .+ , F ) ` ( G ` ( m + 1 ) ) ) = ( seq 1 ( .+ , H ) ` ( m + 1 ) ) ) ) )
310	175, 309	syld 45	. . . . . 6 |- ( ( ph /\ m e. NN ) -> ( ( m e. ( 1 ... (♯ ` A ) ) -> ( seq M ( .+ , F ) ` ( G ` m ) ) = ( seq 1 ( .+ , H ) ` m ) ) -> ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) -> ( seq M ( .+ , F ) ` ( G ` ( m + 1 ) ) ) = ( seq 1 ( .+ , H ) ` ( m + 1 ) ) ) ) )
311	310	expcom 116	. . . . 5 |- ( m e. NN -> ( ph -> ( ( m e. ( 1 ... (♯ ` A ) ) -> ( seq M ( .+ , F ) ` ( G ` m ) ) = ( seq 1 ( .+ , H ) ` m ) ) -> ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) -> ( seq M ( .+ , F ) ` ( G ` ( m + 1 ) ) ) = ( seq 1 ( .+ , H ) ` ( m + 1 ) ) ) ) ) )
312	311	a2d 26	. . . 4 |- ( m e. NN -> ( ( ph -> ( m e. ( 1 ... (♯ ` A ) ) -> ( seq M ( .+ , F ) ` ( G ` m ) ) = ( seq 1 ( .+ , H ) ` m ) ) ) -> ( ph -> ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) -> ( seq M ( .+ , F ) ` ( G ` ( m + 1 ) ) ) = ( seq 1 ( .+ , H ) ` ( m + 1 ) ) ) ) ) )
313	9, 15, 21, 27, 162, 312	nnind 8937	. . 3 |- ( N e. NN -> ( ph -> ( N e. ( 1 ... (♯ ` A ) ) -> ( seq M ( .+ , F ) ` ( G ` N ) ) = ( seq 1 ( .+ , H ) ` N ) ) ) )
314	3, 313	mpcom 36	. 2 |- ( ph -> ( N e. ( 1 ... (♯ ` A ) ) -> ( seq M ( .+ , F ) ` ( G ` N ) ) = ( seq 1 ( .+ , H ) ` N ) ) )
315	1, 314	mpd 13	1 |- ( ph -> ( seq M ( .+ , F ) ` ( G ` N ) ) = ( seq 1 ( .+ , H ) ` N ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 104   <-> wb 105   /\ w3a 978   = wceq 1353   e. wcel 2148   \ cdif 3128   C_ wss 3131   class class class wbr 4005   `'ccnv 4627   |` cres 4630   -->wf 5214   -1-1-onto->wf1o 5217   ` cfv 5218   Isom wiso 5219  (class class class)co 5877   CCcc 7811   RRcr 7812   1c1 7814   + caddc 7816   RR*cxr 7993   < clt 7994   <_ cle 7995   - cmin 8130   NNcn 8921   ZZcz 9255   ZZ>=cuz 9530   ...cfz 10010   seqcseq 10447  ♯chash 10757

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4120  ax-sep 4123  ax-nul 4131  ax-pow 4176  ax-pr 4211  ax-un 4435  ax-setind 4538  ax-iinf 4589  ax-cnex 7904  ax-resscn 7905  ax-1cn 7906  ax-1re 7907  ax-icn 7908  ax-addcl 7909  ax-addrcl 7910  ax-mulcl 7911  ax-addcom 7913  ax-addass 7915  ax-distr 7917  ax-i2m1 7918  ax-0lt1 7919  ax-0id 7921  ax-rnegex 7922  ax-cnre 7924  ax-pre-ltirr 7925  ax-pre-ltwlin 7926  ax-pre-lttrn 7927  ax-pre-ltadd 7929

This theorem depends on definitions:  df-bi 117  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-nel 2443  df-ral 2460  df-rex 2461  df-reu 2462  df-rab 2464  df-v 2741  df-sbc 2965  df-csb 3060  df-dif 3133  df-un 3135  df-in 3137  df-ss 3144  df-nul 3425  df-pw 3579  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-int 3847  df-iun 3890  df-br 4006  df-opab 4067  df-mpt 4068  df-tr 4104  df-id 4295  df-iord 4368  df-on 4370  df-ilim 4371  df-suc 4373  df-iom 4592  df-xp 4634  df-rel 4635  df-cnv 4636  df-co 4637  df-dm 4638  df-rn 4639  df-res 4640  df-ima 4641  df-iota 5180  df-fun 5220  df-fn 5221  df-f 5222  df-f1 5223  df-fo 5224  df-f1o 5225  df-fv 5226  df-isom 5227  df-riota 5833  df-ov 5880  df-oprab 5881  df-mpo 5882  df-1st 6143  df-2nd 6144  df-recs 6308  df-frec 6394  df-pnf 7996  df-mnf 7997  df-xr 7998  df-ltxr 7999  df-le 8000  df-sub 8132  df-neg 8133  df-inn 8922  df-n0 9179  df-z 9256  df-uz 9531  df-fz 10011  df-fzo 10145  df-seqfrec 10448

This theorem is referenced by:  summodclem2a  11391  prodmodclem2a  11586