Theorem seq3coll 10755

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 9989	. . . 4 |- ( N e. ( 1 ... (♯ ` A ) ) -> N e. NN )
3	1, 2	syl 14	. . 3 |- ( ph -> N e. NN )
4		eleq1 2229	. . . . . 6 |- ( y = 1 -> ( y e. ( 1 ... (♯ ` A ) ) <-> 1 e. ( 1 ... (♯ ` A ) ) ) )
5		2fveq3 5491	. . . . . . 7 |- ( y = 1 -> ( seq M ( .+ , F ) ` ( G ` y ) ) = ( seq M ( .+ , F ) ` ( G ` 1 ) ) )
6		fveq2 5486	. . . . . . 7 |- ( y = 1 -> ( seq 1 ( .+ , H ) ` y ) = ( seq 1 ( .+ , H ) ` 1 ) )
7	5, 6	eqeq12d 2180	. . . . . 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 233	. . . . 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 229	. . . 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 2229	. . . . . 6 |- ( y = m -> ( y e. ( 1 ... (♯ ` A ) ) <-> m e. ( 1 ... (♯ ` A ) ) ) )
11		2fveq3 5491	. . . . . . 7 |- ( y = m -> ( seq M ( .+ , F ) ` ( G ` y ) ) = ( seq M ( .+ , F ) ` ( G ` m ) ) )
12		fveq2 5486	. . . . . . 7 |- ( y = m -> ( seq 1 ( .+ , H ) ` y ) = ( seq 1 ( .+ , H ) ` m ) )
13	11, 12	eqeq12d 2180	. . . . . 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 233	. . . . 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 229	. . . 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 2229	. . . . . 6 |- ( y = ( m + 1 ) -> ( y e. ( 1 ... (♯ ` A ) ) <-> ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) )
17		2fveq3 5491	. . . . . . 7 |- ( y = ( m + 1 ) -> ( seq M ( .+ , F ) ` ( G ` y ) ) = ( seq M ( .+ , F ) ` ( G ` ( m + 1 ) ) ) )
18		fveq2 5486	. . . . . . 7 |- ( y = ( m + 1 ) -> ( seq 1 ( .+ , H ) ` y ) = ( seq 1 ( .+ , H ) ` ( m + 1 ) ) )
19	17, 18	eqeq12d 2180	. . . . . 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 233	. . . . 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 229	. . . 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 2229	. . . . . 6 |- ( y = N -> ( y e. ( 1 ... (♯ ` A ) ) <-> N e. ( 1 ... (♯ ` A ) ) ) )
23		2fveq3 5491	. . . . . . 7 |- ( y = N -> ( seq M ( .+ , F ) ` ( G ` y ) ) = ( seq M ( .+ , F ) ` ( G ` N ) ) )
24		fveq2 5486	. . . . . . 7 |- ( y = N -> ( seq 1 ( .+ , H ) ` y ) = ( seq 1 ( .+ , H ) ` N ) )
25	23, 24	eqeq12d 2180	. . . . . 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 233	. . . . 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 229	. . . 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 5775	. . . . . . . . . . . . 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 5432	. . . . . . . . . . . 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 9964	. . . . . . . . . . . . 13 |- ( N e. ( 1 ... (♯ ` A ) ) -> (♯ ` A ) e. ( ZZ>= ` 1 ) )
37	1, 36	syl 14	. . . . . . . . . . . 12 |- ( ph -> (♯ ` A ) e. ( ZZ>= ` 1 ) )
38		eluzfz1 9966	. . . . . . . . . . . 12 |- ( (♯ ` A ) e. ( ZZ>= ` 1 ) -> 1 e. ( 1 ... (♯ ` A ) ) )
39	37, 38	syl 14	. . . . . . . . . . 11 |- ( ph -> 1 e. ( 1 ... (♯ ` A ) ) )
40	35, 39	ffvelrnd 5621	. . . . . . . . . 10 |- ( ph -> ( G ` 1 ) e. A )
41	30, 40	sseldd 3143	. . . . . . . . 9 |- ( ph -> ( G ` 1 ) e. ( ZZ>= ` M ) )
42		eluzle 9478	. . . . . . . . . . . . 13 |- ( (♯ ` A ) e. ( ZZ>= ` 1 ) -> 1 <_ (♯ ` A ) )
43	37, 42	syl 14	. . . . . . . . . . . 12 |- ( ph -> 1 <_ (♯ ` A ) )
44		elfzelz 9960	. . . . . . . . . . . . . . . . 17 |- ( k e. ( 1 ... (♯ ` A ) ) -> k e. ZZ )
45	44	ssriv 3146	. . . . . . . . . . . . . . . 16 |- ( 1 ... (♯ ` A ) ) C_ ZZ
46		zssre 9198	. . . . . . . . . . . . . . . 16 |- ZZ C_ RR
47	45, 46	sstri 3151	. . . . . . . . . . . . . . 15 |- ( 1 ... (♯ ` A ) ) C_ RR
48	47	a1i 9	. . . . . . . . . . . . . 14 |- ( ph -> ( 1 ... (♯ ` A ) ) C_ RR )
49		ressxr 7942	. . . . . . . . . . . . . 14 |- RR C_ RR*
50	48, 49	sstrdi 3154	. . . . . . . . . . . . 13 |- ( ph -> ( 1 ... (♯ ` A ) ) C_ RR* )
51		eluzelre 9476	. . . . . . . . . . . . . . . 16 |- ( k e. ( ZZ>= ` M ) -> k e. RR )
52	51	ssriv 3146	. . . . . . . . . . . . . . 15 |- ( ZZ>= ` M ) C_ RR
53	30, 52	sstrdi 3154	. . . . . . . . . . . . . 14 |- ( ph -> A C_ RR )
54	53, 49	sstrdi 3154	. . . . . . . . . . . . 13 |- ( ph -> A C_ RR* )
55		eluzfz2 9967	. . . . . . . . . . . . . 14 |- ( (♯ ` A ) e. ( ZZ>= ` 1 ) -> (♯ ` A ) e. ( 1 ... (♯ ` A ) ) )
56	37, 55	syl 14	. . . . . . . . . . . . 13 |- ( ph -> (♯ ` A ) e. ( 1 ... (♯ ` A ) ) )
57		leisorel 10750	. . . . . . . . . . . . 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 1237	. . . . . . . . . . . 12 |- ( ph -> ( 1 <_ (♯ ` A ) <-> ( G ` 1 ) <_ ( G ` (♯ ` A ) ) ) )
59	43, 58	mpbid 146	. . . . . . . . . . 11 |- ( ph -> ( G ` 1 ) <_ ( G ` (♯ ` A ) ) )
60	35, 56	ffvelrnd 5621	. . . . . . . . . . . . . 14 |- ( ph -> ( G ` (♯ ` A ) ) e. A )
61	30, 60	sseldd 3143	. . . . . . . . . . . . 13 |- ( ph -> ( G ` (♯ ` A ) ) e. ( ZZ>= ` M ) )
62		eluzelz 9475	. . . . . . . . . . . . 13 |- ( ( G ` (♯ ` A ) ) e. ( ZZ>= ` M ) -> ( G ` (♯ ` A ) ) e. ZZ )
63	61, 62	syl 14	. . . . . . . . . . . 12 |- ( ph -> ( G ` (♯ ` A ) ) e. ZZ )
64		elfz5 9952	. . . . . . . . . . . 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 409	. . . . . . . . . . 11 |- ( ph -> ( ( G ` 1 ) e. ( M ... ( G ` (♯ ` A ) ) ) <-> ( G ` 1 ) <_ ( G ` (♯ ` A ) ) ) )
66	59, 65	mpbird 166	. . . . . . . . . 10 |- ( ph -> ( G ` 1 ) e. ( M ... ( G ` (♯ ` A ) ) ) )
67		fveq2 5486	. . . . . . . . . . . . 13 |- ( k = ( G ` 1 ) -> ( F ` k ) = ( F ` ( G ` 1 ) ) )
68	67	eleq1d 2235	. . . . . . . . . . . 12 |- ( k = ( G ` 1 ) -> ( ( F ` k ) e. S <-> ( F ` ( G ` 1 ) ) e. S ) )
69	68	imbi2d 229	. . . . . . . . . . 11 |- ( k = ( G ` 1 ) -> ( ( ph -> ( F ` k ) e. S ) <-> ( ph -> ( F ` ( G ` 1 ) ) e. S ) ) )
70		elfzuz 9956	. . . . . . . . . . . 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 115	. . . . . . . . . . . 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 2792	. . . . . . . . . 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 9475	. . . . . . . . . . . . . . . . . 18 |- ( ( G ` 1 ) e. ( ZZ>= ` M ) -> ( G ` 1 ) e. ZZ )
77	41, 76	syl 14	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( G ` 1 ) e. ZZ )
78		peano2zm 9229	. . . . . . . . . . . . . . . . 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 9313	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( G ` 1 ) - 1 ) e. RR )
81	77	zred 9313	. . . . . . . . . . . . . . 15 |- ( ph -> ( G ` 1 ) e. RR )
82	63	zred 9313	. . . . . . . . . . . . . . 15 |- ( ph -> ( G ` (♯ ` A ) ) e. RR )
83	81	lem1d 8828	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( G ` 1 ) - 1 ) <_ ( G ` 1 ) )
84	80, 81, 82, 83, 59	letrd 8022	. . . . . . . . . . . . . 14 |- ( ph -> ( ( G ` 1 ) - 1 ) <_ ( G ` (♯ ` A ) ) )
85		eluz 9479	. . . . . . . . . . . . . . 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 409	. . . . . . . . . . . . . 14 |- ( ph -> ( ( G ` (♯ ` A ) ) e. ( ZZ>= ` ( ( G ` 1 ) - 1 ) ) <-> ( ( G ` 1 ) - 1 ) <_ ( G ` (♯ ` A ) ) ) )
87	84, 86	mpbird 166	. . . . . . . . . . . . 13 |- ( ph -> ( G ` (♯ ` A ) ) e. ( ZZ>= ` ( ( G ` 1 ) - 1 ) ) )
88		fzss2 9999	. . . . . . . . . . . . 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 3142	. . . . . . . . . . 11 |- ( ( ph /\ k e. ( M ... ( ( G ` 1 ) - 1 ) ) ) -> k e. ( M ... ( G ` (♯ ` A ) ) ) )
91		eluzel2 9471	. . . . . . . . . . . . . . 15 |- ( ( G ` 1 ) e. ( ZZ>= ` M ) -> M e. ZZ )
92	41, 91	syl 14	. . . . . . . . . . . . . 14 |- ( ph -> M e. ZZ )
93		elfzm11 10026	. . . . . . . . . . . . . 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 409	. . . . . . . . . . . . 13 |- ( ph -> ( k e. ( M ... ( ( G ` 1 ) - 1 ) ) <-> ( k e. ZZ /\ M <_ k /\ k < ( G ` 1 ) ) ) )
95		simp3 989	. . . . . . . . . . . . . 14 |- ( ( k e. ZZ /\ M <_ k /\ k < ( G ` 1 ) ) -> k < ( G ` 1 ) )
96	81	adantr 274	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ k e. A ) -> ( G ` 1 ) e. RR )
97	53	sselda 3142	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ k e. A ) -> k e. RR )
98		f1ocnv 5445	. . . . . . . . . . . . . . . . . . . . . . . 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 5432	. . . . . . . . . . . . . . . . . . . . . . 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	ffvelrnda 5620	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ k e. A ) -> ( `' G ` k ) e. ( 1 ... (♯ ` A ) ) )
103		elfznn 9989	. . . . . . . . . . . . . . . . . . . . 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 8900	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ k e. A ) -> 1 <_ ( `' G ` k ) )
106	31	adantr 274	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ k e. A ) -> G Isom < , < ( ( 1 ... (♯ ` A ) ) , A ) )
107	50	adantr 274	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ k e. A ) -> ( 1 ... (♯ ` A ) ) C_ RR* )
108	54	adantr 274	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ k e. A ) -> A C_ RR* )
109	39	adantr 274	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ k e. A ) -> 1 e. ( 1 ... (♯ ` A ) ) )
110		leisorel 10750	. . . . . . . . . . . . . . . . . . . 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 1237	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ k e. A ) -> ( 1 <_ ( `' G ` k ) <-> ( G ` 1 ) <_ ( G ` ( `' G ` k ) ) ) )
112	105, 111	mpbid 146	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ k e. A ) -> ( G ` 1 ) <_ ( G ` ( `' G ` k ) ) )
113		f1ocnvfv2 5746	. . . . . . . . . . . . . . . . . . 19 |- ( ( G : ( 1 ... (♯ ` A ) ) -1-1-onto-> A /\ k e. A ) -> ( G ` ( `' G ` k ) ) = k )
114	33, 113	sylan 281	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ k e. A ) -> ( G ` ( `' G ` k ) ) = k )
115	112, 114	breqtrd 4008	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ k e. A ) -> ( G ` 1 ) <_ k )
116	96, 97, 115	lensymd 8020	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ k e. A ) -> -. k < ( G ` 1 ) )
117	116	ex 114	. . . . . . . . . . . . . . 15 |- ( ph -> ( k e. A -> -. k < ( G ` 1 ) ) )
118	117	con2d 614	. . . . . . . . . . . . . 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 149	. . . . . . . . . . . 12 |- ( ph -> ( k e. ( M ... ( ( G ` 1 ) - 1 ) ) -> -. k e. A ) )
121	120	imp 123	. . . . . . . . . . 11 |- ( ( ph /\ k e. ( M ... ( ( G ` 1 ) - 1 ) ) ) -> -. k e. A )
122	90, 121	eldifd 3126	. . . . . . . . . 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 280	. . . . . . . . 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 10443	. . . . . . . 8 |- ( ph -> ( seq M ( .+ , F ) |` ( ZZ>= ` ( G ` 1 ) ) ) = seq ( G ` 1 ) ( .+ , F ) )
127	126	fveq1d 5488	. . . . . . 7 |- ( ph -> ( ( seq M ( .+ , F ) |` ( ZZ>= ` ( G ` 1 ) ) ) ` ( G ` 1 ) ) = ( seq ( G ` 1 ) ( .+ , F ) ` ( G ` 1 ) ) )
128		uzid 9480	. . . . . . . . 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 5510	. . . . . . . 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 274	. . . . . . . . . . 11 |- ( ( ph /\ k e. ( ZZ>= ` ( G ` 1 ) ) ) -> M e. ZZ )
133		eluzelz 9475	. . . . . . . . . . . 12 |- ( k e. ( ZZ>= ` ( G ` 1 ) ) -> k e. ZZ )
134	133	adantl 275	. . . . . . . . . . 11 |- ( ( ph /\ k e. ( ZZ>= ` ( G ` 1 ) ) ) -> k e. ZZ )
135	132	zred 9313	. . . . . . . . . . . 12 |- ( ( ph /\ k e. ( ZZ>= ` ( G ` 1 ) ) ) -> M e. RR )
136	81	adantr 274	. . . . . . . . . . . 12 |- ( ( ph /\ k e. ( ZZ>= ` ( G ` 1 ) ) ) -> ( G ` 1 ) e. RR )
137	134	zred 9313	. . . . . . . . . . . 12 |- ( ( ph /\ k e. ( ZZ>= ` ( G ` 1 ) ) ) -> k e. RR )
138		eluzle 9478	. . . . . . . . . . . . . 14 |- ( ( G ` 1 ) e. ( ZZ>= ` M ) -> M <_ ( G ` 1 ) )
139	41, 138	syl 14	. . . . . . . . . . . . 13 |- ( ph -> M <_ ( G ` 1 ) )
140	139	adantr 274	. . . . . . . . . . . 12 |- ( ( ph /\ k e. ( ZZ>= ` ( G ` 1 ) ) ) -> M <_ ( G ` 1 ) )
141		eluzle 9478	. . . . . . . . . . . . 13 |- ( k e. ( ZZ>= ` ( G ` 1 ) ) -> ( G ` 1 ) <_ k )
142	141	adantl 275	. . . . . . . . . . . 12 |- ( ( ph /\ k e. ( ZZ>= ` ( G ` 1 ) ) ) -> ( G ` 1 ) <_ k )
143	135, 136, 137, 140, 142	letrd 8022	. . . . . . . . . . 11 |- ( ( ph /\ k e. ( ZZ>= ` ( G ` 1 ) ) ) -> M <_ k )
144		eluz2 9472	. . . . . . . . . . 11 |- ( k e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ k e. ZZ /\ M <_ k ) )
145	132, 134, 143, 144	syl3anbrc 1171	. . . . . . . . . 10 |- ( ( ph /\ k e. ( ZZ>= ` ( G ` 1 ) ) ) -> k e. ( ZZ>= ` M ) )
146	145, 71	syldan 280	. . . . . . . . 9 |- ( ( ph /\ k e. ( ZZ>= ` ( G ` 1 ) ) ) -> ( F ` k ) e. S )
147	77, 146, 125	seq3-1 10395	. . . . . . . 8 |- ( ph -> ( seq ( G ` 1 ) ( .+ , F ) ` ( G ` 1 ) ) = ( F ` ( G ` 1 ) ) )
148		fveq2 5486	. . . . . . . . . . . 12 |- ( n = 1 -> ( H ` n ) = ( H ` 1 ) )
149		2fveq3 5491	. . . . . . . . . . . 12 |- ( n = 1 -> ( F ` ( G ` n ) ) = ( F ` ( G ` 1 ) ) )
150	148, 149	eqeq12d 2180	. . . . . . . . . . 11 |- ( n = 1 -> ( ( H ` n ) = ( F ` ( G ` n ) ) <-> ( H ` 1 ) = ( F ` ( G ` 1 ) ) ) )
151	150	imbi2d 229	. . . . . . . . . 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 115	. . . . . . . . . 10 |- ( n e. ( 1 ... (♯ ` A ) ) -> ( ph -> ( H ` n ) = ( F ` ( G ` n ) ) ) )
154	151, 153	vtoclga 2792	. . . . . . . . 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 2201	. . . . . . 7 |- ( ph -> ( seq ( G ` 1 ) ( .+ , F ) ` ( G ` 1 ) ) = ( H ` 1 ) )
157	127, 131, 156	3eqtr3d 2206	. . . . . 6 |- ( ph -> ( seq M ( .+ , F ) ` ( G ` 1 ) ) = ( H ` 1 ) )
158		1zzd 9218	. . . . . . 7 |- ( ph -> 1 e. ZZ )
159		seqcoll.hcl	. . . . . . 7 |- ( ( ph /\ k e. ( ZZ>= ` 1 ) ) -> ( H ` k ) e. S )
160	158, 159, 125	seq3-1 10395	. . . . . 6 |- ( ph -> ( seq 1 ( .+ , H ) ` 1 ) = ( H ` 1 ) )
161	157, 160	eqtr4d 2201	. . . . 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 520	. . . . . . . . . . 11 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> m e. NN )
164		nnuz 9501	. . . . . . . . . . 11 |- NN = ( ZZ>= ` 1 )
165	163, 164	eleqtrdi 2259	. . . . . . . . . 10 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> m e. ( ZZ>= ` 1 ) )
166		nnz 9210	. . . . . . . . . . . 12 |- ( m e. NN -> m e. ZZ )
167	166	ad2antlr 481	. . . . . . . . . . 11 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> m e. ZZ )
168		elfzuz3 9957	. . . . . . . . . . . 12 |- ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) -> (♯ ` A ) e. ( ZZ>= ` ( m + 1 ) ) )
169	168	adantl 275	. . . . . . . . . . 11 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> (♯ ` A ) e. ( ZZ>= ` ( m + 1 ) ) )
170		peano2uzr 9523	. . . . . . . . . . 11 |- ( ( m e. ZZ /\ (♯ ` A ) e. ( ZZ>= ` ( m + 1 ) ) ) -> (♯ ` A ) e. ( ZZ>= ` m ) )
171	167, 169, 170	syl2anc 409	. . . . . . . . . 10 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> (♯ ` A ) e. ( ZZ>= ` m ) )
172		elfzuzb 9954	. . . . . . . . . 10 |- ( m e. ( 1 ... (♯ ` A ) ) <-> ( m e. ( ZZ>= ` 1 ) /\ (♯ ` A ) e. ( ZZ>= ` m ) ) )
173	165, 171, 172	sylanbrc 414	. . . . . . . . 9 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> m e. ( 1 ... (♯ ` A ) ) )
174	173	ex 114	. . . . . . . 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 5849	. . . . . . . . . 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 519	. . . . . . . . . . . . . . 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 281	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) /\ k e. S ) -> ( k .+ Z ) = k )
180	30	ad2antrr 480	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> A C_ ( ZZ>= ` M ) )
181	35	ad2antrr 480	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> G : ( 1 ... (♯ ` A ) ) --> A )
182	181, 173	ffvelrnd 5621	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( G ` m ) e. A )
183	180, 182	sseldd 3143	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( G ` m ) e. ( ZZ>= ` M ) )
184		nnre 8864	. . . . . . . . . . . . . . . . . . 19 |- ( m e. NN -> m e. RR )
185	184	ad2antlr 481	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> m e. RR )
186	185	ltp1d 8825	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> m < ( m + 1 ) )
187	31	ad2antrr 480	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> G Isom < , < ( ( 1 ... (♯ ` A ) ) , A ) )
188		simpr 109	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( m + 1 ) e. ( 1 ... (♯ ` A ) ) )
189		isorel 5776	. . . . . . . . . . . . . . . . . 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 1226	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( m < ( m + 1 ) <-> ( G ` m ) < ( G ` ( m + 1 ) ) ) )
191	186, 190	mpbid 146	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( G ` m ) < ( G ` ( m + 1 ) ) )
192		eluzelz 9475	. . . . . . . . . . . . . . . . . 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	ffvelrnd 5621	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( G ` ( m + 1 ) ) e. A )
195	180, 194	sseldd 3143	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( G ` ( m + 1 ) ) e. ( ZZ>= ` M ) )
196		eluzelz 9475	. . . . . . . . . . . . . . . . . 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 9248	. . . . . . . . . . . . . . . . 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 409	. . . . . . . . . . . . . . . 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 146	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( G ` m ) <_ ( ( G ` ( m + 1 ) ) - 1 ) )
201		peano2zm 9229	. . . . . . . . . . . . . . . . 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 9479	. . . . . . . . . . . . . . . 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 409	. . . . . . . . . . . . . . 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 166	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( ( G ` ( m + 1 ) ) - 1 ) e. ( ZZ>= ` ( G ` m ) ) )
206		eqid 2165	. . . . . . . . . . . . . . . 16 |- ( ZZ>= ` M ) = ( ZZ>= ` M )
207	92	ad2antrr 480	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> M e. ZZ )
208	177, 71	sylan 281	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) /\ k e. ( ZZ>= ` M ) ) -> ( F ` k ) e. S )
209	177, 125	sylan 281	. . . . . . . . . . . . . . . 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 10396	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> seq M ( .+ , F ) : ( ZZ>= ` M ) --> S )
211	210, 183	ffvelrnd 5621	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( seq M ( .+ , F ) ` ( G ` m ) ) e. S )
212		simplll 523	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) /\ k e. ( ( ( G ` m ) + 1 ) ... ( ( G ` ( m + 1 ) ) - 1 ) ) ) -> ph )
213		elfzuz 9956	. . . . . . . . . . . . . . . . . 18 |- ( k e. ( ( ( G ` m ) + 1 ) ... ( ( G ` ( m + 1 ) ) - 1 ) ) -> k e. ( ZZ>= ` ( ( G ` m ) + 1 ) ) )
214		peano2uz 9521	. . . . . . . . . . . . . . . . . . 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 9482	. . . . . . . . . . . . . . . . . 18 |- ( ( k e. ( ZZ>= ` ( ( G ` m ) + 1 ) ) /\ ( ( G ` m ) + 1 ) e. ( ZZ>= ` M ) ) -> k e. ( ZZ>= ` M ) )
217	213, 215, 216	syl2anr 288	. . . . . . . . . . . . . . . . 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 9313	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( ( G ` ( m + 1 ) ) - 1 ) e. RR )
219	197	zred 9313	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( G ` ( m + 1 ) ) e. RR )
220	82	ad2antrr 480	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( G ` (♯ ` A ) ) e. RR )
221	219	lem1d 8828	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( ( G ` ( m + 1 ) ) - 1 ) <_ ( G ` ( m + 1 ) ) )
222		elfzle2 9963	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) -> ( m + 1 ) <_ (♯ ` A ) )
223	222	adantl 275	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( m + 1 ) <_ (♯ ` A ) )
224	50	ad2antrr 480	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( 1 ... (♯ ` A ) ) C_ RR* )
225	54	ad2antrr 480	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> A C_ RR* )
226	56	ad2antrr 480	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> (♯ ` A ) e. ( 1 ... (♯ ` A ) ) )
227		leisorel 10750	. . . . . . . . . . . . . . . . . . . . . 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 1237	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( ( m + 1 ) <_ (♯ ` A ) <-> ( G ` ( m + 1 ) ) <_ ( G ` (♯ ` A ) ) ) )
229	223, 228	mpbid 146	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( G ` ( m + 1 ) ) <_ ( G ` (♯ ` A ) ) )
230	218, 219, 220, 221, 229	letrd 8022	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( ( G ` ( m + 1 ) ) - 1 ) <_ ( G ` (♯ ` A ) ) )
231	63	ad2antrr 480	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( G ` (♯ ` A ) ) e. ZZ )
232		eluz 9479	. . . . . . . . . . . . . . . . . . . 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 409	. . . . . . . . . . . . . . . . . . 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 166	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( G ` (♯ ` A ) ) e. ( ZZ>= ` ( ( G ` ( m + 1 ) ) - 1 ) ) )
235		elfzuz3 9957	. . . . . . . . . . . . . . . . . 18 |- ( k e. ( ( ( G ` m ) + 1 ) ... ( ( G ` ( m + 1 ) ) - 1 ) ) -> ( ( G ` ( m + 1 ) ) - 1 ) e. ( ZZ>= ` k ) )
236		uztrn 9482	. . . . . . . . . . . . . . . . . 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 287	. . . . . . . . . . . . . . . . 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 9954	. . . . . . . . . . . . . . . . 17 |- ( k e. ( M ... ( G ` (♯ ` A ) ) ) <-> ( k e. ( ZZ>= ` M ) /\ ( G ` (♯ ` A ) ) e. ( ZZ>= ` k ) ) )
239	217, 237, 238	sylanbrc 414	. . . . . . . . . . . . . . . 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 481	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) /\ k e. A ) ) -> m e. ZZ )
241	101	ad2antrr 480	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) /\ k e. A ) ) -> `' G : A --> ( 1 ... (♯ ` A ) ) )
242		simprr 522	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) /\ k e. A ) ) -> k e. A )
243	241, 242	ffvelrnd 5621	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) /\ k e. A ) ) -> ( `' G ` k ) e. ( 1 ... (♯ ` A ) ) )
244		elfzelz 9960	. . . . . . . . . . . . . . . . . . . . . 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 9285	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( m e. ZZ /\ m < ( `' G ` k ) /\ ( `' G ` k ) < ( m + 1 ) ) -> -. ( `' G ` k ) e. ZZ )
247	246	3expib 1196	. . . . . . . . . . . . . . . . . . . . . 22 |- ( m e. ZZ -> ( ( m < ( `' G ` k ) /\ ( `' G ` k ) < ( m + 1 ) ) -> -. ( `' G ` k ) e. ZZ ) )
248	247	con2d 614	. . . . . . . . . . . . . . . . . . . . 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 480	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) /\ k e. A ) ) -> G Isom < , < ( ( 1 ... (♯ ` A ) ) , A ) )
251	173	adantrr 471	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) /\ k e. A ) ) -> m e. ( 1 ... (♯ ` A ) ) )
252		isorel 5776	. . . . . . . . . . . . . . . . . . . . . . 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 1226	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) /\ k e. A ) ) -> ( m < ( `' G ` k ) <-> ( G ` m ) < ( G ` ( `' G ` k ) ) ) )
254	33	ad2antrr 480	. . . . . . . . . . . . . . . . . . . . . . . 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 409	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) /\ k e. A ) ) -> ( G ` ( `' G ` k ) ) = k )
256	255	breq2d 3994	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) /\ k e. A ) ) -> ( ( G ` m ) < ( G ` ( `' G ` k ) ) <-> ( G ` m ) < k ) )
257	193	adantrr 471	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) /\ k e. A ) ) -> ( G ` m ) e. ZZ )
258	30	ad2antrr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) /\ k e. A ) ) -> A C_ ( ZZ>= ` M ) )
259	258, 242	sseldd 3143	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) /\ k e. A ) ) -> k e. ( ZZ>= ` M ) )
260		eluzelz 9475	. . . . . . . . . . . . . . . . . . . . . . . 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 9245	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( G ` m ) e. ZZ /\ k e. ZZ ) -> ( ( G ` m ) < k <-> ( ( G ` m ) + 1 ) <_ k ) )
263	257, 261, 262	syl2anc 409	. . . . . . . . . . . . . . . . . . . . . 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 213	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) /\ k e. A ) ) -> ( m < ( `' G ` k ) <-> ( ( G ` m ) + 1 ) <_ k ) )
265	188	adantrr 471	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) /\ k e. A ) ) -> ( m + 1 ) e. ( 1 ... (♯ ` A ) ) )
266		isorel 5776	. . . . . . . . . . . . . . . . . . . . . . 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 1226	. . . . . . . . . . . . . . . . . . . . . 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 3992	. . . . . . . . . . . . . . . . . . . . . 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 471	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) /\ k e. A ) ) -> ( G ` ( m + 1 ) ) e. ZZ )
270		zltlem1 9248	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( k e. ZZ /\ ( G ` ( m + 1 ) ) e. ZZ ) -> ( k < ( G ` ( m + 1 ) ) <-> k <_ ( ( G ` ( m + 1 ) ) - 1 ) ) )
271	261, 269, 270	syl2anc 409	. . . . . . . . . . . . . . . . . . . . . 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 213	. . . . . . . . . . . . . . . . . . . . 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 465	. . . . . . . . . . . . . . . . . . . 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 662	. . . . . . . . . . . . . . . . . . 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 373	. . . . . . . . . . . . . . . . . 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 614	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( ( ( ( G ` m ) + 1 ) <_ k /\ k <_ ( ( G ` ( m + 1 ) ) - 1 ) ) -> -. k e. A ) )
277		elfzle1 9962	. . . . . . . . . . . . . . . . . 18 |- ( k e. ( ( ( G ` m ) + 1 ) ... ( ( G ` ( m + 1 ) ) - 1 ) ) -> ( ( G ` m ) + 1 ) <_ k )
278		elfzle2 9963	. . . . . . . . . . . . . . . . . 18 |- ( k e. ( ( ( G ` m ) + 1 ) ... ( ( G ` ( m + 1 ) ) - 1 ) ) -> k <_ ( ( G ` ( m + 1 ) ) - 1 ) )
279	277, 278	jca 304	. . . . . . . . . . . . . . . . 17 |- ( k e. ( ( ( G ` m ) + 1 ) ... ( ( G ` ( m + 1 ) ) - 1 ) ) -> ( ( ( G ` m ) + 1 ) <_ k /\ k <_ ( ( G ` ( m + 1 ) ) - 1 ) ) )
280	276, 279	impel 278	. . . . . . . . . . . . . . . 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 3126	. . . . . . . . . . . . . . 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 409	. . . . . . . . . . . . . 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 10444	. . . . . . . . . . . . 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 5857	. . . . . . . . . . . 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 5486	. . . . . . . . . . . . . . . . . 18 |- ( n = ( m + 1 ) -> ( H ` n ) = ( H ` ( m + 1 ) ) )
286		2fveq3 5491	. . . . . . . . . . . . . . . . . 18 |- ( n = ( m + 1 ) -> ( F ` ( G ` n ) ) = ( F ` ( G ` ( m + 1 ) ) ) )
287	285, 286	eqeq12d 2180	. . . . . . . . . . . . . . . . 17 |- ( n = ( m + 1 ) -> ( ( H ` n ) = ( F ` ( G ` n ) ) <-> ( H ` ( m + 1 ) ) = ( F ` ( G ` ( m + 1 ) ) ) ) )
288	287	imbi2d 229	. . . . . . . . . . . . . . . 16 |- ( n = ( m + 1 ) -> ( ( ph -> ( H ` n ) = ( F ` ( G ` n ) ) ) <-> ( ph -> ( H ` ( m + 1 ) ) = ( F ` ( G ` ( m + 1 ) ) ) ) ) )
289	288, 153	vtoclga 2792	. . . . . . . . . . . . . . 15 |- ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) -> ( ph -> ( H ` ( m + 1 ) ) = ( F ` ( G ` ( m + 1 ) ) ) ) )
290	289	impcom 124	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( H ` ( m + 1 ) ) = ( F ` ( G ` ( m + 1 ) ) ) )
291	290	adantlr 469	. . . . . . . . . . . . 13 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( H ` ( m + 1 ) ) = ( F ` ( G ` ( m + 1 ) ) ) )
292	291	oveq2d 5858	. . . . . . . . . . . 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 9314	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( G ` ( m + 1 ) ) e. CC )
294		ax-1cn 7846	. . . . . . . . . . . . . . 15 |- 1 e. CC
295		npcan 8107	. . . . . . . . . . . . . . 15 |- ( ( ( G ` ( m + 1 ) ) e. CC /\ 1 e. CC ) -> ( ( ( G ` ( m + 1 ) ) - 1 ) + 1 ) = ( G ` ( m + 1 ) ) )
296	293, 294, 295	sylancl 410	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( ( ( G ` ( m + 1 ) ) - 1 ) + 1 ) = ( G ` ( m + 1 ) ) )
297		uztrn 9482	. . . . . . . . . . . . . . . 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 409	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( ( G ` ( m + 1 ) ) - 1 ) e. ( ZZ>= ` M ) )
299		eluzp1p1 9491	. . . . . . . . . . . . . . 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 2244	. . . . . . . . . . . . 13 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( G ` ( m + 1 ) ) e. ( ZZ>= ` ( M + 1 ) ) )
302	207, 301, 208, 209	seq3m1 10403	. . . . . . . . . . . 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 2209	. . . . . . . . . . 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 281	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) /\ k e. ( ZZ>= ` 1 ) ) -> ( H ` k ) e. S )
305	165, 304, 209	seq3p1 10397	. . . . . . . . . . 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 2180	. . . . . . . . . 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	syl5ibr 155	. . . . . . . . 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 114	. . . . . . . 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 115	. . . . 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 8873	. . 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 103   <-> wb 104   /\ w3a 968   = wceq 1343   e. wcel 2136   \ cdif 3113   C_ wss 3116   class class class wbr 3982   `'ccnv 4603   |` cres 4606   -->wf 5184   -1-1-onto->wf1o 5187   ` cfv 5188   Isom wiso 5189  (class class class)co 5842   CCcc 7751   RRcr 7752   1c1 7754   + caddc 7756   RR*cxr 7932   < clt 7933   <_ cle 7934   - cmin 8069   NNcn 8857   ZZcz 9191   ZZ>=cuz 9466   ...cfz 9944   seqcseq 10380  ♯chash 10688

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-13 2138  ax-14 2139  ax-ext 2147  ax-coll 4097  ax-sep 4100  ax-nul 4108  ax-pow 4153  ax-pr 4187  ax-un 4411  ax-setind 4514  ax-iinf 4565  ax-cnex 7844  ax-resscn 7845  ax-1cn 7846  ax-1re 7847  ax-icn 7848  ax-addcl 7849  ax-addrcl 7850  ax-mulcl 7851  ax-addcom 7853  ax-addass 7855  ax-distr 7857  ax-i2m1 7858  ax-0lt1 7859  ax-0id 7861  ax-rnegex 7862  ax-cnre 7864  ax-pre-ltirr 7865  ax-pre-ltwlin 7866  ax-pre-lttrn 7867  ax-pre-ltadd 7869

This theorem depends on definitions:  df-bi 116  df-3or 969  df-3an 970  df-tru 1346  df-fal 1349  df-nf 1449  df-sb 1751  df-eu 2017  df-mo 2018  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2297  df-ne 2337  df-nel 2432  df-ral 2449  df-rex 2450  df-reu 2451  df-rab 2453  df-v 2728  df-sbc 2952  df-csb 3046  df-dif 3118  df-un 3120  df-in 3122  df-ss 3129  df-nul 3410  df-pw 3561  df-sn 3582  df-pr 3583  df-op 3585  df-uni 3790  df-int 3825  df-iun 3868  df-br 3983  df-opab 4044  df-mpt 4045  df-tr 4081  df-id 4271  df-iord 4344  df-on 4346  df-ilim 4347  df-suc 4349  df-iom 4568  df-xp 4610  df-rel 4611  df-cnv 4612  df-co 4613  df-dm 4614  df-rn 4615  df-res 4616  df-ima 4617  df-iota 5153  df-fun 5190  df-fn 5191  df-f 5192  df-f1 5193  df-fo 5194  df-f1o 5195  df-fv 5196  df-isom 5197  df-riota 5798  df-ov 5845  df-oprab 5846  df-mpo 5847  df-1st 6108  df-2nd 6109  df-recs 6273  df-frec 6359  df-pnf 7935  df-mnf 7936  df-xr 7937  df-ltxr 7938  df-le 7939  df-sub 8071  df-neg 8072  df-inn 8858  df-n0 9115  df-z 9192  df-uz 9467  df-fz 9945  df-fzo 10078  df-seqfrec 10381

This theorem is referenced by:  summodclem2a  11322  prodmodclem2a  11517