Theorem seq3coll 10951

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 10146	. . . 4 |- ( N e. ( 1 ... (♯ ` A ) ) -> N e. NN )
3	1, 2	syl 14	. . 3 |- ( ph -> N e. NN )
4		eleq1 2259	. . . . . 6 |- ( y = 1 -> ( y e. ( 1 ... (♯ ` A ) ) <-> 1 e. ( 1 ... (♯ ` A ) ) ) )
5		2fveq3 5566	. . . . . . 7 |- ( y = 1 -> ( seq M ( .+ , F ) ` ( G ` y ) ) = ( seq M ( .+ , F ) ` ( G ` 1 ) ) )
6		fveq2 5561	. . . . . . 7 |- ( y = 1 -> ( seq 1 ( .+ , H ) ` y ) = ( seq 1 ( .+ , H ) ` 1 ) )
7	5, 6	eqeq12d 2211	. . . . . 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 2259	. . . . . 6 |- ( y = m -> ( y e. ( 1 ... (♯ ` A ) ) <-> m e. ( 1 ... (♯ ` A ) ) ) )
11		2fveq3 5566	. . . . . . 7 |- ( y = m -> ( seq M ( .+ , F ) ` ( G ` y ) ) = ( seq M ( .+ , F ) ` ( G ` m ) ) )
12		fveq2 5561	. . . . . . 7 |- ( y = m -> ( seq 1 ( .+ , H ) ` y ) = ( seq 1 ( .+ , H ) ` m ) )
13	11, 12	eqeq12d 2211	. . . . . 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 2259	. . . . . 6 |- ( y = ( m + 1 ) -> ( y e. ( 1 ... (♯ ` A ) ) <-> ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) )
17		2fveq3 5566	. . . . . . 7 |- ( y = ( m + 1 ) -> ( seq M ( .+ , F ) ` ( G ` y ) ) = ( seq M ( .+ , F ) ` ( G ` ( m + 1 ) ) ) )
18		fveq2 5561	. . . . . . 7 |- ( y = ( m + 1 ) -> ( seq 1 ( .+ , H ) ` y ) = ( seq 1 ( .+ , H ) ` ( m + 1 ) ) )
19	17, 18	eqeq12d 2211	. . . . . 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 2259	. . . . . 6 |- ( y = N -> ( y e. ( 1 ... (♯ ` A ) ) <-> N e. ( 1 ... (♯ ` A ) ) ) )
23		2fveq3 5566	. . . . . . 7 |- ( y = N -> ( seq M ( .+ , F ) ` ( G ` y ) ) = ( seq M ( .+ , F ) ` ( G ` N ) ) )
24		fveq2 5561	. . . . . . 7 |- ( y = N -> ( seq 1 ( .+ , H ) ` y ) = ( seq 1 ( .+ , H ) ` N ) )
25	23, 24	eqeq12d 2211	. . . . . 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 5857	. . . . . . . . . . . . 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 5507	. . . . . . . . . . . 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 10121	. . . . . . . . . . . . 13 |- ( N e. ( 1 ... (♯ ` A ) ) -> (♯ ` A ) e. ( ZZ>= ` 1 ) )
37	1, 36	syl 14	. . . . . . . . . . . 12 |- ( ph -> (♯ ` A ) e. ( ZZ>= ` 1 ) )
38		eluzfz1 10123	. . . . . . . . . . . 12 |- ( (♯ ` A ) e. ( ZZ>= ` 1 ) -> 1 e. ( 1 ... (♯ ` A ) ) )
39	37, 38	syl 14	. . . . . . . . . . 11 |- ( ph -> 1 e. ( 1 ... (♯ ` A ) ) )
40	35, 39	ffvelcdmd 5701	. . . . . . . . . 10 |- ( ph -> ( G ` 1 ) e. A )
41	30, 40	sseldd 3185	. . . . . . . . 9 |- ( ph -> ( G ` 1 ) e. ( ZZ>= ` M ) )
42		eluzle 9630	. . . . . . . . . . . . 13 |- ( (♯ ` A ) e. ( ZZ>= ` 1 ) -> 1 <_ (♯ ` A ) )
43	37, 42	syl 14	. . . . . . . . . . . 12 |- ( ph -> 1 <_ (♯ ` A ) )
44		elfzelz 10117	. . . . . . . . . . . . . . . . 17 |- ( k e. ( 1 ... (♯ ` A ) ) -> k e. ZZ )
45	44	ssriv 3188	. . . . . . . . . . . . . . . 16 |- ( 1 ... (♯ ` A ) ) C_ ZZ
46		zssre 9350	. . . . . . . . . . . . . . . 16 |- ZZ C_ RR
47	45, 46	sstri 3193	. . . . . . . . . . . . . . 15 |- ( 1 ... (♯ ` A ) ) C_ RR
48	47	a1i 9	. . . . . . . . . . . . . 14 |- ( ph -> ( 1 ... (♯ ` A ) ) C_ RR )
49		ressxr 8087	. . . . . . . . . . . . . 14 |- RR C_ RR*
50	48, 49	sstrdi 3196	. . . . . . . . . . . . 13 |- ( ph -> ( 1 ... (♯ ` A ) ) C_ RR* )
51		eluzelre 9628	. . . . . . . . . . . . . . . 16 |- ( k e. ( ZZ>= ` M ) -> k e. RR )
52	51	ssriv 3188	. . . . . . . . . . . . . . 15 |- ( ZZ>= ` M ) C_ RR
53	30, 52	sstrdi 3196	. . . . . . . . . . . . . 14 |- ( ph -> A C_ RR )
54	53, 49	sstrdi 3196	. . . . . . . . . . . . 13 |- ( ph -> A C_ RR* )
55		eluzfz2 10124	. . . . . . . . . . . . . 14 |- ( (♯ ` A ) e. ( ZZ>= ` 1 ) -> (♯ ` A ) e. ( 1 ... (♯ ` A ) ) )
56	37, 55	syl 14	. . . . . . . . . . . . 13 |- ( ph -> (♯ ` A ) e. ( 1 ... (♯ ` A ) ) )
57		leisorel 10946	. . . . . . . . . . . . 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 1258	. . . . . . . . . . . 12 |- ( ph -> ( 1 <_ (♯ ` A ) <-> ( G ` 1 ) <_ ( G ` (♯ ` A ) ) ) )
59	43, 58	mpbid 147	. . . . . . . . . . 11 |- ( ph -> ( G ` 1 ) <_ ( G ` (♯ ` A ) ) )
60	35, 56	ffvelcdmd 5701	. . . . . . . . . . . . . 14 |- ( ph -> ( G ` (♯ ` A ) ) e. A )
61	30, 60	sseldd 3185	. . . . . . . . . . . . 13 |- ( ph -> ( G ` (♯ ` A ) ) e. ( ZZ>= ` M ) )
62		eluzelz 9627	. . . . . . . . . . . . 13 |- ( ( G ` (♯ ` A ) ) e. ( ZZ>= ` M ) -> ( G ` (♯ ` A ) ) e. ZZ )
63	61, 62	syl 14	. . . . . . . . . . . 12 |- ( ph -> ( G ` (♯ ` A ) ) e. ZZ )
64		elfz5 10109	. . . . . . . . . . . 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 5561	. . . . . . . . . . . . 13 |- ( k = ( G ` 1 ) -> ( F ` k ) = ( F ` ( G ` 1 ) ) )
68	67	eleq1d 2265	. . . . . . . . . . . 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 10113	. . . . . . . . . . . 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 2830	. . . . . . . . . 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 9627	. . . . . . . . . . . . . . . . . 18 |- ( ( G ` 1 ) e. ( ZZ>= ` M ) -> ( G ` 1 ) e. ZZ )
77	41, 76	syl 14	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( G ` 1 ) e. ZZ )
78		peano2zm 9381	. . . . . . . . . . . . . . . . 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 9465	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( G ` 1 ) - 1 ) e. RR )
81	77	zred 9465	. . . . . . . . . . . . . . 15 |- ( ph -> ( G ` 1 ) e. RR )
82	63	zred 9465	. . . . . . . . . . . . . . 15 |- ( ph -> ( G ` (♯ ` A ) ) e. RR )
83	81	lem1d 8977	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( G ` 1 ) - 1 ) <_ ( G ` 1 ) )
84	80, 81, 82, 83, 59	letrd 8167	. . . . . . . . . . . . . 14 |- ( ph -> ( ( G ` 1 ) - 1 ) <_ ( G ` (♯ ` A ) ) )
85		eluz 9631	. . . . . . . . . . . . . . 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 10156	. . . . . . . . . . . . 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 3184	. . . . . . . . . . 11 |- ( ( ph /\ k e. ( M ... ( ( G ` 1 ) - 1 ) ) ) -> k e. ( M ... ( G ` (♯ ` A ) ) ) )
91		eluzel2 9623	. . . . . . . . . . . . . . 15 |- ( ( G ` 1 ) e. ( ZZ>= ` M ) -> M e. ZZ )
92	41, 91	syl 14	. . . . . . . . . . . . . 14 |- ( ph -> M e. ZZ )
93		elfzm11 10183	. . . . . . . . . . . . . 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 1001	. . . . . . . . . . . . . 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 3184	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ k e. A ) -> k e. RR )
98		f1ocnv 5520	. . . . . . . . . . . . . . . . . . . . . . . 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 5507	. . . . . . . . . . . . . . . . . . . . . . 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 5700	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ k e. A ) -> ( `' G ` k ) e. ( 1 ... (♯ ` A ) ) )
103		elfznn 10146	. . . . . . . . . . . . . . . . . . . . 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 9050	. . . . . . . . . . . . . . . . . . 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 10946	. . . . . . . . . . . . . . . . . . . 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 1258	. . . . . . . . . . . . . . . . . . 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 5828	. . . . . . . . . . . . . . . . . . 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 4060	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ k e. A ) -> ( G ` 1 ) <_ k )
116	96, 97, 115	lensymd 8165	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ k e. A ) -> -. k < ( G ` 1 ) )
117	116	ex 115	. . . . . . . . . . . . . . 15 |- ( ph -> ( k e. A -> -. k < ( G ` 1 ) ) )
118	117	con2d 625	. . . . . . . . . . . . . 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 3167	. . . . . . . . . 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 10634	. . . . . . . 8 |- ( ph -> ( seq M ( .+ , F ) |` ( ZZ>= ` ( G ` 1 ) ) ) = seq ( G ` 1 ) ( .+ , F ) )
127	126	fveq1d 5563	. . . . . . 7 |- ( ph -> ( ( seq M ( .+ , F ) |` ( ZZ>= ` ( G ` 1 ) ) ) ` ( G ` 1 ) ) = ( seq ( G ` 1 ) ( .+ , F ) ` ( G ` 1 ) ) )
128		uzid 9632	. . . . . . . . 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 5585	. . . . . . . 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 9627	. . . . . . . . . . . 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 9465	. . . . . . . . . . . 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 9465	. . . . . . . . . . . 12 |- ( ( ph /\ k e. ( ZZ>= ` ( G ` 1 ) ) ) -> k e. RR )
138		eluzle 9630	. . . . . . . . . . . . . 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 9630	. . . . . . . . . . . . 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 8167	. . . . . . . . . . 11 |- ( ( ph /\ k e. ( ZZ>= ` ( G ` 1 ) ) ) -> M <_ k )
144		eluz2 9624	. . . . . . . . . . 11 |- ( k e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ k e. ZZ /\ M <_ k ) )
145	132, 134, 143, 144	syl3anbrc 1183	. . . . . . . . . 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 10571	. . . . . . . 8 |- ( ph -> ( seq ( G ` 1 ) ( .+ , F ) ` ( G ` 1 ) ) = ( F ` ( G ` 1 ) ) )
148		fveq2 5561	. . . . . . . . . . . 12 |- ( n = 1 -> ( H ` n ) = ( H ` 1 ) )
149		2fveq3 5566	. . . . . . . . . . . 12 |- ( n = 1 -> ( F ` ( G ` n ) ) = ( F ` ( G ` 1 ) ) )
150	148, 149	eqeq12d 2211	. . . . . . . . . . 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 2830	. . . . . . . . 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 2232	. . . . . . 7 |- ( ph -> ( seq ( G ` 1 ) ( .+ , F ) ` ( G ` 1 ) ) = ( H ` 1 ) )
157	127, 131, 156	3eqtr3d 2237	. . . . . 6 |- ( ph -> ( seq M ( .+ , F ) ` ( G ` 1 ) ) = ( H ` 1 ) )
158		1zzd 9370	. . . . . . 7 |- ( ph -> 1 e. ZZ )
159		seqcoll.hcl	. . . . . . 7 |- ( ( ph /\ k e. ( ZZ>= ` 1 ) ) -> ( H ` k ) e. S )
160	158, 159, 125	seq3-1 10571	. . . . . 6 |- ( ph -> ( seq 1 ( .+ , H ) ` 1 ) = ( H ` 1 ) )
161	157, 160	eqtr4d 2232	. . . . 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 9654	. . . . . . . . . . 11 |- NN = ( ZZ>= ` 1 )
165	163, 164	eleqtrdi 2289	. . . . . . . . . 10 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> m e. ( ZZ>= ` 1 ) )
166		nnz 9362	. . . . . . . . . . . 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 10114	. . . . . . . . . . . 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 9676	. . . . . . . . . . 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 10111	. . . . . . . . . 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 5932	. . . . . . . . . 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 5701	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( G ` m ) e. A )
183	180, 182	sseldd 3185	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( G ` m ) e. ( ZZ>= ` M ) )
184		nnre 9014	. . . . . . . . . . . . . . . . . . 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 8974	. . . . . . . . . . . . . . . . 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 5858	. . . . . . . . . . . . . . . . . 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 1247	. . . . . . . . . . . . . . . . 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 9627	. . . . . . . . . . . . . . . . . 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 5701	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( G ` ( m + 1 ) ) e. A )
195	180, 194	sseldd 3185	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( G ` ( m + 1 ) ) e. ( ZZ>= ` M ) )
196		eluzelz 9627	. . . . . . . . . . . . . . . . . 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 9400	. . . . . . . . . . . . . . . . 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 9381	. . . . . . . . . . . . . . . . 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 9631	. . . . . . . . . . . . . . . 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 2196	. . . . . . . . . . . . . . . 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 10573	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> seq M ( .+ , F ) : ( ZZ>= ` M ) --> S )
211	210, 183	ffvelcdmd 5701	. . . . . . . . . . . . . 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 10113	. . . . . . . . . . . . . . . . . 18 |- ( k e. ( ( ( G ` m ) + 1 ) ... ( ( G ` ( m + 1 ) ) - 1 ) ) -> k e. ( ZZ>= ` ( ( G ` m ) + 1 ) ) )
214		peano2uz 9674	. . . . . . . . . . . . . . . . . . 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 9635	. . . . . . . . . . . . . . . . . 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 9465	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( ( G ` ( m + 1 ) ) - 1 ) e. RR )
219	197	zred 9465	. . . . . . . . . . . . . . . . . . . 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 8977	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( ( G ` ( m + 1 ) ) - 1 ) <_ ( G ` ( m + 1 ) ) )
222		elfzle2 10120	. . . . . . . . . . . . . . . . . . . . . 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 10946	. . . . . . . . . . . . . . . . . . . . . 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 1258	. . . . . . . . . . . . . . . . . . . . 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 8167	. . . . . . . . . . . . . . . . . . 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 9631	. . . . . . . . . . . . . . . . . . . 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 10114	. . . . . . . . . . . . . . . . . 18 |- ( k e. ( ( ( G ` m ) + 1 ) ... ( ( G ` ( m + 1 ) ) - 1 ) ) -> ( ( G ` ( m + 1 ) ) - 1 ) e. ( ZZ>= ` k ) )
236		uztrn 9635	. . . . . . . . . . . . . . . . . 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 10111	. . . . . . . . . . . . . . . . 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 5701	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) /\ k e. A ) ) -> ( `' G ` k ) e. ( 1 ... (♯ ` A ) ) )
244		elfzelz 10117	. . . . . . . . . . . . . . . . . . . . . 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 9437	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( m e. ZZ /\ m < ( `' G ` k ) /\ ( `' G ` k ) < ( m + 1 ) ) -> -. ( `' G ` k ) e. ZZ )
247	246	3expib 1208	. . . . . . . . . . . . . . . . . . . . . 22 |- ( m e. ZZ -> ( ( m < ( `' G ` k ) /\ ( `' G ` k ) < ( m + 1 ) ) -> -. ( `' G ` k ) e. ZZ ) )
248	247	con2d 625	. . . . . . . . . . . . . . . . . . . . 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 5858	. . . . . . . . . . . . . . . . . . . . . . 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 1247	. . . . . . . . . . . . . . . . . . . . . 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 4046	. . . . . . . . . . . . . . . . . . . . . 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 3185	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) /\ k e. A ) ) -> k e. ( ZZ>= ` M ) )
260		eluzelz 9627	. . . . . . . . . . . . . . . . . . . . . . . 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 9397	. . . . . . . . . . . . . . . . . . . . . . 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 5858	. . . . . . . . . . . . . . . . . . . . . . 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 1247	. . . . . . . . . . . . . . . . . . . . . 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 4044	. . . . . . . . . . . . . . . . . . . . . 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 9400	. . . . . . . . . . . . . . . . . . . . . . 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 673	. . . . . . . . . . . . . . . . . . 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 625	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( ( ( ( G ` m ) + 1 ) <_ k /\ k <_ ( ( G ` ( m + 1 ) ) - 1 ) ) -> -. k e. A ) )
277		elfzle1 10119	. . . . . . . . . . . . . . . . . 18 |- ( k e. ( ( ( G ` m ) + 1 ) ... ( ( G ` ( m + 1 ) ) - 1 ) ) -> ( ( G ` m ) + 1 ) <_ k )
278		elfzle2 10120	. . . . . . . . . . . . . . . . . 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 3167	. . . . . . . . . . . . . . 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 10635	. . . . . . . . . . . . 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 5940	. . . . . . . . . . . 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 5561	. . . . . . . . . . . . . . . . . 18 |- ( n = ( m + 1 ) -> ( H ` n ) = ( H ` ( m + 1 ) ) )
286		2fveq3 5566	. . . . . . . . . . . . . . . . . 18 |- ( n = ( m + 1 ) -> ( F ` ( G ` n ) ) = ( F ` ( G ` ( m + 1 ) ) ) )
287	285, 286	eqeq12d 2211	. . . . . . . . . . . . . . . . 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 2830	. . . . . . . . . . . . . . 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 5941	. . . . . . . . . . . 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 9466	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( G ` ( m + 1 ) ) e. CC )
294		ax-1cn 7989	. . . . . . . . . . . . . . 15 |- 1 e. CC
295		npcan 8252	. . . . . . . . . . . . . . 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 9635	. . . . . . . . . . . . . . . 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 9644	. . . . . . . . . . . . . . 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 2274	. . . . . . . . . . . . 13 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( G ` ( m + 1 ) ) e. ( ZZ>= ` ( M + 1 ) ) )
302	207, 301, 208, 209	seq3m1 10582	. . . . . . . . . . . 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 2240	. . . . . . . . . . 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 10574	. . . . . . . . . . 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 2211	. . . . . . . . . 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 9023	. . 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 980   = wceq 1364   e. wcel 2167   \ cdif 3154   C_ wss 3157   class class class wbr 4034   `'ccnv 4663   |` cres 4666   -->wf 5255   -1-1-onto->wf1o 5258   ` cfv 5259   Isom wiso 5260  (class class class)co 5925   CCcc 7894   RRcr 7895   1c1 7897   + caddc 7899   RR*cxr 8077   < clt 8078   <_ cle 8079   - cmin 8214   NNcn 9007   ZZcz 9343   ZZ>=cuz 9618   ...cfz 10100   seqcseq 10556  ♯chash 10884

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 615  ax-in2 616  ax-io 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-13 2169  ax-14 2170  ax-ext 2178  ax-coll 4149  ax-sep 4152  ax-nul 4160  ax-pow 4208  ax-pr 4243  ax-un 4469  ax-setind 4574  ax-iinf 4625  ax-cnex 7987  ax-resscn 7988  ax-1cn 7989  ax-1re 7990  ax-icn 7991  ax-addcl 7992  ax-addrcl 7993  ax-mulcl 7994  ax-addcom 7996  ax-addass 7998  ax-distr 8000  ax-i2m1 8001  ax-0lt1 8002  ax-0id 8004  ax-rnegex 8005  ax-cnre 8007  ax-pre-ltirr 8008  ax-pre-ltwlin 8009  ax-pre-lttrn 8010  ax-pre-ltadd 8012

This theorem depends on definitions:  df-bi 117  df-3or 981  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1475  df-sb 1777  df-eu 2048  df-mo 2049  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ne 2368  df-nel 2463  df-ral 2480  df-rex 2481  df-reu 2482  df-rab 2484  df-v 2765  df-sbc 2990  df-csb 3085  df-dif 3159  df-un 3161  df-in 3163  df-ss 3170  df-nul 3452  df-pw 3608  df-sn 3629  df-pr 3630  df-op 3632  df-uni 3841  df-int 3876  df-iun 3919  df-br 4035  df-opab 4096  df-mpt 4097  df-tr 4133  df-id 4329  df-iord 4402  df-on 4404  df-ilim 4405  df-suc 4407  df-iom 4628  df-xp 4670  df-rel 4671  df-cnv 4672  df-co 4673  df-dm 4674  df-rn 4675  df-res 4676  df-ima 4677  df-iota 5220  df-fun 5261  df-fn 5262  df-f 5263  df-f1 5264  df-fo 5265  df-f1o 5266  df-fv 5267  df-isom 5268  df-riota 5880  df-ov 5928  df-oprab 5929  df-mpo 5930  df-1st 6207  df-2nd 6208  df-recs 6372  df-frec 6458  df-pnf 8080  df-mnf 8081  df-xr 8082  df-ltxr 8083  df-le 8084  df-sub 8216  df-neg 8217  df-inn 9008  df-n0 9267  df-z 9344  df-uz 9619  df-fz 10101  df-fzo 10235  df-seqfrec 10557

This theorem is referenced by:  summodclem2a  11563  prodmodclem2a  11758