Theorem seq3coll 10585

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 9834	. . . 4 |- ( N e. ( 1 ... (♯ ` A ) ) -> N e. NN )
3	1, 2	syl 14	. . 3 |- ( ph -> N e. NN )
4		eleq1 2202	. . . . . 6 |- ( y = 1 -> ( y e. ( 1 ... (♯ ` A ) ) <-> 1 e. ( 1 ... (♯ ` A ) ) ) )
5		2fveq3 5426	. . . . . . 7 |- ( y = 1 -> ( seq M ( .+ , F ) ` ( G ` y ) ) = ( seq M ( .+ , F ) ` ( G ` 1 ) ) )
6		fveq2 5421	. . . . . . 7 |- ( y = 1 -> ( seq 1 ( .+ , H ) ` y ) = ( seq 1 ( .+ , H ) ` 1 ) )
7	5, 6	eqeq12d 2154	. . . . . 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 2202	. . . . . 6 |- ( y = m -> ( y e. ( 1 ... (♯ ` A ) ) <-> m e. ( 1 ... (♯ ` A ) ) ) )
11		2fveq3 5426	. . . . . . 7 |- ( y = m -> ( seq M ( .+ , F ) ` ( G ` y ) ) = ( seq M ( .+ , F ) ` ( G ` m ) ) )
12		fveq2 5421	. . . . . . 7 |- ( y = m -> ( seq 1 ( .+ , H ) ` y ) = ( seq 1 ( .+ , H ) ` m ) )
13	11, 12	eqeq12d 2154	. . . . . 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 2202	. . . . . 6 |- ( y = ( m + 1 ) -> ( y e. ( 1 ... (♯ ` A ) ) <-> ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) )
17		2fveq3 5426	. . . . . . 7 |- ( y = ( m + 1 ) -> ( seq M ( .+ , F ) ` ( G ` y ) ) = ( seq M ( .+ , F ) ` ( G ` ( m + 1 ) ) ) )
18		fveq2 5421	. . . . . . 7 |- ( y = ( m + 1 ) -> ( seq 1 ( .+ , H ) ` y ) = ( seq 1 ( .+ , H ) ` ( m + 1 ) ) )
19	17, 18	eqeq12d 2154	. . . . . 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 2202	. . . . . 6 |- ( y = N -> ( y e. ( 1 ... (♯ ` A ) ) <-> N e. ( 1 ... (♯ ` A ) ) ) )
23		2fveq3 5426	. . . . . . 7 |- ( y = N -> ( seq M ( .+ , F ) ` ( G ` y ) ) = ( seq M ( .+ , F ) ` ( G ` N ) ) )
24		fveq2 5421	. . . . . . 7 |- ( y = N -> ( seq 1 ( .+ , H ) ` y ) = ( seq 1 ( .+ , H ) ` N ) )
25	23, 24	eqeq12d 2154	. . . . . 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 5708	. . . . . . . . . . . . 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 5367	. . . . . . . . . . . 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 9809	. . . . . . . . . . . . 13 |- ( N e. ( 1 ... (♯ ` A ) ) -> (♯ ` A ) e. ( ZZ>= ` 1 ) )
37	1, 36	syl 14	. . . . . . . . . . . 12 |- ( ph -> (♯ ` A ) e. ( ZZ>= ` 1 ) )
38		eluzfz1 9811	. . . . . . . . . . . 12 |- ( (♯ ` A ) e. ( ZZ>= ` 1 ) -> 1 e. ( 1 ... (♯ ` A ) ) )
39	37, 38	syl 14	. . . . . . . . . . 11 |- ( ph -> 1 e. ( 1 ... (♯ ` A ) ) )
40	35, 39	ffvelrnd 5556	. . . . . . . . . 10 |- ( ph -> ( G ` 1 ) e. A )
41	30, 40	sseldd 3098	. . . . . . . . 9 |- ( ph -> ( G ` 1 ) e. ( ZZ>= ` M ) )
42		eluzle 9338	. . . . . . . . . . . . 13 |- ( (♯ ` A ) e. ( ZZ>= ` 1 ) -> 1 <_ (♯ ` A ) )
43	37, 42	syl 14	. . . . . . . . . . . 12 |- ( ph -> 1 <_ (♯ ` A ) )
44		elfzelz 9806	. . . . . . . . . . . . . . . . 17 |- ( k e. ( 1 ... (♯ ` A ) ) -> k e. ZZ )
45	44	ssriv 3101	. . . . . . . . . . . . . . . 16 |- ( 1 ... (♯ ` A ) ) C_ ZZ
46		zssre 9061	. . . . . . . . . . . . . . . 16 |- ZZ C_ RR
47	45, 46	sstri 3106	. . . . . . . . . . . . . . 15 |- ( 1 ... (♯ ` A ) ) C_ RR
48	47	a1i 9	. . . . . . . . . . . . . 14 |- ( ph -> ( 1 ... (♯ ` A ) ) C_ RR )
49		ressxr 7809	. . . . . . . . . . . . . 14 |- RR C_ RR*
50	48, 49	sstrdi 3109	. . . . . . . . . . . . 13 |- ( ph -> ( 1 ... (♯ ` A ) ) C_ RR* )
51		eluzelre 9336	. . . . . . . . . . . . . . . 16 |- ( k e. ( ZZ>= ` M ) -> k e. RR )
52	51	ssriv 3101	. . . . . . . . . . . . . . 15 |- ( ZZ>= ` M ) C_ RR
53	30, 52	sstrdi 3109	. . . . . . . . . . . . . 14 |- ( ph -> A C_ RR )
54	53, 49	sstrdi 3109	. . . . . . . . . . . . 13 |- ( ph -> A C_ RR* )
55		eluzfz2 9812	. . . . . . . . . . . . . 14 |- ( (♯ ` A ) e. ( ZZ>= ` 1 ) -> (♯ ` A ) e. ( 1 ... (♯ ` A ) ) )
56	37, 55	syl 14	. . . . . . . . . . . . 13 |- ( ph -> (♯ ` A ) e. ( 1 ... (♯ ` A ) ) )
57		leisorel 10580	. . . . . . . . . . . . 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 1225	. . . . . . . . . . . 12 |- ( ph -> ( 1 <_ (♯ ` A ) <-> ( G ` 1 ) <_ ( G ` (♯ ` A ) ) ) )
59	43, 58	mpbid 146	. . . . . . . . . . 11 |- ( ph -> ( G ` 1 ) <_ ( G ` (♯ ` A ) ) )
60	35, 56	ffvelrnd 5556	. . . . . . . . . . . . . 14 |- ( ph -> ( G ` (♯ ` A ) ) e. A )
61	30, 60	sseldd 3098	. . . . . . . . . . . . 13 |- ( ph -> ( G ` (♯ ` A ) ) e. ( ZZ>= ` M ) )
62		eluzelz 9335	. . . . . . . . . . . . 13 |- ( ( G ` (♯ ` A ) ) e. ( ZZ>= ` M ) -> ( G ` (♯ ` A ) ) e. ZZ )
63	61, 62	syl 14	. . . . . . . . . . . 12 |- ( ph -> ( G ` (♯ ` A ) ) e. ZZ )
64		elfz5 9798	. . . . . . . . . . . 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 408	. . . . . . . . . . 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 5421	. . . . . . . . . . . . 13 |- ( k = ( G ` 1 ) -> ( F ` k ) = ( F ` ( G ` 1 ) ) )
68	67	eleq1d 2208	. . . . . . . . . . . 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 9802	. . . . . . . . . . . 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 2752	. . . . . . . . . 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 9335	. . . . . . . . . . . . . . . . . 18 |- ( ( G ` 1 ) e. ( ZZ>= ` M ) -> ( G ` 1 ) e. ZZ )
77	41, 76	syl 14	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( G ` 1 ) e. ZZ )
78		peano2zm 9092	. . . . . . . . . . . . . . . . 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 9173	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( G ` 1 ) - 1 ) e. RR )
81	77	zred 9173	. . . . . . . . . . . . . . 15 |- ( ph -> ( G ` 1 ) e. RR )
82	63	zred 9173	. . . . . . . . . . . . . . 15 |- ( ph -> ( G ` (♯ ` A ) ) e. RR )
83	81	lem1d 8691	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( G ` 1 ) - 1 ) <_ ( G ` 1 ) )
84	80, 81, 82, 83, 59	letrd 7886	. . . . . . . . . . . . . 14 |- ( ph -> ( ( G ` 1 ) - 1 ) <_ ( G ` (♯ ` A ) ) )
85		eluz 9339	. . . . . . . . . . . . . . 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 408	. . . . . . . . . . . . . 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 9844	. . . . . . . . . . . . 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 3097	. . . . . . . . . . 11 |- ( ( ph /\ k e. ( M ... ( ( G ` 1 ) - 1 ) ) ) -> k e. ( M ... ( G ` (♯ ` A ) ) ) )
91		eluzel2 9331	. . . . . . . . . . . . . . 15 |- ( ( G ` 1 ) e. ( ZZ>= ` M ) -> M e. ZZ )
92	41, 91	syl 14	. . . . . . . . . . . . . 14 |- ( ph -> M e. ZZ )
93		elfzm11 9871	. . . . . . . . . . . . . 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 408	. . . . . . . . . . . . 13 |- ( ph -> ( k e. ( M ... ( ( G ` 1 ) - 1 ) ) <-> ( k e. ZZ /\ M <_ k /\ k < ( G ` 1 ) ) ) )
95		simp3 983	. . . . . . . . . . . . . 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 3097	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ k e. A ) -> k e. RR )
98		f1ocnv 5380	. . . . . . . . . . . . . . . . . . . . . . . 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 5367	. . . . . . . . . . . . . . . . . . . . . . 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 5555	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ k e. A ) -> ( `' G ` k ) e. ( 1 ... (♯ ` A ) ) )
103		elfznn 9834	. . . . . . . . . . . . . . . . . . . . 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 8763	. . . . . . . . . . . . . . . . . . 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 10580	. . . . . . . . . . . . . . . . . . . 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 1225	. . . . . . . . . . . . . . . . . . 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 5679	. . . . . . . . . . . . . . . . . . 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 3954	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ k e. A ) -> ( G ` 1 ) <_ k )
116	96, 97, 115	lensymd 7884	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ k e. A ) -> -. k < ( G ` 1 ) )
117	116	ex 114	. . . . . . . . . . . . . . 15 |- ( ph -> ( k e. A -> -. k < ( G ` 1 ) ) )
118	117	con2d 613	. . . . . . . . . . . . . 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 3081	. . . . . . . . . 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 10281	. . . . . . . 8 |- ( ph -> ( seq M ( .+ , F ) |` ( ZZ>= ` ( G ` 1 ) ) ) = seq ( G ` 1 ) ( .+ , F ) )
127	126	fveq1d 5423	. . . . . . 7 |- ( ph -> ( ( seq M ( .+ , F ) |` ( ZZ>= ` ( G ` 1 ) ) ) ` ( G ` 1 ) ) = ( seq ( G ` 1 ) ( .+ , F ) ` ( G ` 1 ) ) )
128		uzid 9340	. . . . . . . . 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 5445	. . . . . . . 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 9335	. . . . . . . . . . . 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 9173	. . . . . . . . . . . 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 9173	. . . . . . . . . . . 12 |- ( ( ph /\ k e. ( ZZ>= ` ( G ` 1 ) ) ) -> k e. RR )
138		eluzle 9338	. . . . . . . . . . . . . 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 9338	. . . . . . . . . . . . 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 7886	. . . . . . . . . . 11 |- ( ( ph /\ k e. ( ZZ>= ` ( G ` 1 ) ) ) -> M <_ k )
144		eluz2 9332	. . . . . . . . . . 11 |- ( k e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ k e. ZZ /\ M <_ k ) )
145	132, 134, 143, 144	syl3anbrc 1165	. . . . . . . . . 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 10233	. . . . . . . 8 |- ( ph -> ( seq ( G ` 1 ) ( .+ , F ) ` ( G ` 1 ) ) = ( F ` ( G ` 1 ) ) )
148		fveq2 5421	. . . . . . . . . . . 12 |- ( n = 1 -> ( H ` n ) = ( H ` 1 ) )
149		2fveq3 5426	. . . . . . . . . . . 12 |- ( n = 1 -> ( F ` ( G ` n ) ) = ( F ` ( G ` 1 ) ) )
150	148, 149	eqeq12d 2154	. . . . . . . . . . 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 2752	. . . . . . . . 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 2175	. . . . . . 7 |- ( ph -> ( seq ( G ` 1 ) ( .+ , F ) ` ( G ` 1 ) ) = ( H ` 1 ) )
157	127, 131, 156	3eqtr3d 2180	. . . . . 6 |- ( ph -> ( seq M ( .+ , F ) ` ( G ` 1 ) ) = ( H ` 1 ) )
158		1zzd 9081	. . . . . . 7 |- ( ph -> 1 e. ZZ )
159		seqcoll.hcl	. . . . . . 7 |- ( ( ph /\ k e. ( ZZ>= ` 1 ) ) -> ( H ` k ) e. S )
160	158, 159, 125	seq3-1 10233	. . . . . 6 |- ( ph -> ( seq 1 ( .+ , H ) ` 1 ) = ( H ` 1 ) )
161	157, 160	eqtr4d 2175	. . . . 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 519	. . . . . . . . . . 11 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> m e. NN )
164		nnuz 9361	. . . . . . . . . . 11 |- NN = ( ZZ>= ` 1 )
165	163, 164	eleqtrdi 2232	. . . . . . . . . 10 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> m e. ( ZZ>= ` 1 ) )
166		nnz 9073	. . . . . . . . . . . 12 |- ( m e. NN -> m e. ZZ )
167	166	ad2antlr 480	. . . . . . . . . . 11 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> m e. ZZ )
168		elfzuz3 9803	. . . . . . . . . . . 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 9380	. . . . . . . . . . 11 |- ( ( m e. ZZ /\ (♯ ` A ) e. ( ZZ>= ` ( m + 1 ) ) ) -> (♯ ` A ) e. ( ZZ>= ` m ) )
171	167, 169, 170	syl2anc 408	. . . . . . . . . 10 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> (♯ ` A ) e. ( ZZ>= ` m ) )
172		elfzuzb 9800	. . . . . . . . . 10 |- ( m e. ( 1 ... (♯ ` A ) ) <-> ( m e. ( ZZ>= ` 1 ) /\ (♯ ` A ) e. ( ZZ>= ` m ) ) )
173	165, 171, 172	sylanbrc 413	. . . . . . . . 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 5781	. . . . . . . . . 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 518	. . . . . . . . . . . . . . 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 479	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> A C_ ( ZZ>= ` M ) )
181	35	ad2antrr 479	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> G : ( 1 ... (♯ ` A ) ) --> A )
182	181, 173	ffvelrnd 5556	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( G ` m ) e. A )
183	180, 182	sseldd 3098	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( G ` m ) e. ( ZZ>= ` M ) )
184		nnre 8727	. . . . . . . . . . . . . . . . . . 19 |- ( m e. NN -> m e. RR )
185	184	ad2antlr 480	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> m e. RR )
186	185	ltp1d 8688	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> m < ( m + 1 ) )
187	31	ad2antrr 479	. . . . . . . . . . . . . . . . . 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 5709	. . . . . . . . . . . . . . . . . 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 1214	. . . . . . . . . . . . . . . . 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 9335	. . . . . . . . . . . . . . . . . 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 5556	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( G ` ( m + 1 ) ) e. A )
195	180, 194	sseldd 3098	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( G ` ( m + 1 ) ) e. ( ZZ>= ` M ) )
196		eluzelz 9335	. . . . . . . . . . . . . . . . . 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 9111	. . . . . . . . . . . . . . . . 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 408	. . . . . . . . . . . . . . . 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 9092	. . . . . . . . . . . . . . . . 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 9339	. . . . . . . . . . . . . . . 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 408	. . . . . . . . . . . . . . 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 2139	. . . . . . . . . . . . . . . 16 |- ( ZZ>= ` M ) = ( ZZ>= ` M )
207	92	ad2antrr 479	. . . . . . . . . . . . . . . 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 10234	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> seq M ( .+ , F ) : ( ZZ>= ` M ) --> S )
211	210, 183	ffvelrnd 5556	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( seq M ( .+ , F ) ` ( G ` m ) ) e. S )
212		simplll 522	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) /\ k e. ( ( ( G ` m ) + 1 ) ... ( ( G ` ( m + 1 ) ) - 1 ) ) ) -> ph )
213		elfzuz 9802	. . . . . . . . . . . . . . . . . 18 |- ( k e. ( ( ( G ` m ) + 1 ) ... ( ( G ` ( m + 1 ) ) - 1 ) ) -> k e. ( ZZ>= ` ( ( G ` m ) + 1 ) ) )
214		peano2uz 9378	. . . . . . . . . . . . . . . . . . 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 9342	. . . . . . . . . . . . . . . . . 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 9173	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( ( G ` ( m + 1 ) ) - 1 ) e. RR )
219	197	zred 9173	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( G ` ( m + 1 ) ) e. RR )
220	82	ad2antrr 479	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( G ` (♯ ` A ) ) e. RR )
221	219	lem1d 8691	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( ( G ` ( m + 1 ) ) - 1 ) <_ ( G ` ( m + 1 ) ) )
222		elfzle2 9808	. . . . . . . . . . . . . . . . . . . . . 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 479	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( 1 ... (♯ ` A ) ) C_ RR* )
225	54	ad2antrr 479	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> A C_ RR* )
226	56	ad2antrr 479	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> (♯ ` A ) e. ( 1 ... (♯ ` A ) ) )
227		leisorel 10580	. . . . . . . . . . . . . . . . . . . . . 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 1225	. . . . . . . . . . . . . . . . . . . . 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 7886	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( ( G ` ( m + 1 ) ) - 1 ) <_ ( G ` (♯ ` A ) ) )
231	63	ad2antrr 479	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( G ` (♯ ` A ) ) e. ZZ )
232		eluz 9339	. . . . . . . . . . . . . . . . . . . 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 408	. . . . . . . . . . . . . . . . . . 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 9803	. . . . . . . . . . . . . . . . . 18 |- ( k e. ( ( ( G ` m ) + 1 ) ... ( ( G ` ( m + 1 ) ) - 1 ) ) -> ( ( G ` ( m + 1 ) ) - 1 ) e. ( ZZ>= ` k ) )
236		uztrn 9342	. . . . . . . . . . . . . . . . . 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 9800	. . . . . . . . . . . . . . . . 17 |- ( k e. ( M ... ( G ` (♯ ` A ) ) ) <-> ( k e. ( ZZ>= ` M ) /\ ( G ` (♯ ` A ) ) e. ( ZZ>= ` k ) ) )
239	217, 237, 238	sylanbrc 413	. . . . . . . . . . . . . . . 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 480	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) /\ k e. A ) ) -> m e. ZZ )
241	101	ad2antrr 479	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) /\ k e. A ) ) -> `' G : A --> ( 1 ... (♯ ` A ) ) )
242		simprr 521	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) /\ k e. A ) ) -> k e. A )
243	241, 242	ffvelrnd 5556	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) /\ k e. A ) ) -> ( `' G ` k ) e. ( 1 ... (♯ ` A ) ) )
244		elfzelz 9806	. . . . . . . . . . . . . . . . . . . . . 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 9145	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( m e. ZZ /\ m < ( `' G ` k ) /\ ( `' G ` k ) < ( m + 1 ) ) -> -. ( `' G ` k ) e. ZZ )
247	246	3expib 1184	. . . . . . . . . . . . . . . . . . . . . 22 |- ( m e. ZZ -> ( ( m < ( `' G ` k ) /\ ( `' G ` k ) < ( m + 1 ) ) -> -. ( `' G ` k ) e. ZZ ) )
248	247	con2d 613	. . . . . . . . . . . . . . . . . . . . 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 479	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) /\ k e. A ) ) -> G Isom < , < ( ( 1 ... (♯ ` A ) ) , A ) )
251	173	adantrr 470	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) /\ k e. A ) ) -> m e. ( 1 ... (♯ ` A ) ) )
252		isorel 5709	. . . . . . . . . . . . . . . . . . . . . . 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 1214	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) /\ k e. A ) ) -> ( m < ( `' G ` k ) <-> ( G ` m ) < ( G ` ( `' G ` k ) ) ) )
254	33	ad2antrr 479	. . . . . . . . . . . . . . . . . . . . . . . 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 408	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) /\ k e. A ) ) -> ( G ` ( `' G ` k ) ) = k )
256	255	breq2d 3941	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) /\ k e. A ) ) -> ( ( G ` m ) < ( G ` ( `' G ` k ) ) <-> ( G ` m ) < k ) )
257	193	adantrr 470	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) /\ k e. A ) ) -> ( G ` m ) e. ZZ )
258	30	ad2antrr 479	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) /\ k e. A ) ) -> A C_ ( ZZ>= ` M ) )
259	258, 242	sseldd 3098	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) /\ k e. A ) ) -> k e. ( ZZ>= ` M ) )
260		eluzelz 9335	. . . . . . . . . . . . . . . . . . . . . . . 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 9108	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( G ` m ) e. ZZ /\ k e. ZZ ) -> ( ( G ` m ) < k <-> ( ( G ` m ) + 1 ) <_ k ) )
263	257, 261, 262	syl2anc 408	. . . . . . . . . . . . . . . . . . . . . 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 470	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) /\ k e. A ) ) -> ( m + 1 ) e. ( 1 ... (♯ ` A ) ) )
266		isorel 5709	. . . . . . . . . . . . . . . . . . . . . . 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 1214	. . . . . . . . . . . . . . . . . . . . . 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 3939	. . . . . . . . . . . . . . . . . . . . . 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 470	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) /\ k e. A ) ) -> ( G ` ( m + 1 ) ) e. ZZ )
270		zltlem1 9111	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( k e. ZZ /\ ( G ` ( m + 1 ) ) e. ZZ ) -> ( k < ( G ` ( m + 1 ) ) <-> k <_ ( ( G ` ( m + 1 ) ) - 1 ) ) )
271	261, 269, 270	syl2anc 408	. . . . . . . . . . . . . . . . . . . . . 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 464	. . . . . . . . . . . . . . . . . . . 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 661	. . . . . . . . . . . . . . . . . . 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 372	. . . . . . . . . . . . . . . . . 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 613	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( ( ( ( G ` m ) + 1 ) <_ k /\ k <_ ( ( G ` ( m + 1 ) ) - 1 ) ) -> -. k e. A ) )
277		elfzle1 9807	. . . . . . . . . . . . . . . . . 18 |- ( k e. ( ( ( G ` m ) + 1 ) ... ( ( G ` ( m + 1 ) ) - 1 ) ) -> ( ( G ` m ) + 1 ) <_ k )
278		elfzle2 9808	. . . . . . . . . . . . . . . . . 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 3081	. . . . . . . . . . . . . . 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 408	. . . . . . . . . . . . . 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 10282	. . . . . . . . . . . . 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 5789	. . . . . . . . . . . 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 5421	. . . . . . . . . . . . . . . . . 18 |- ( n = ( m + 1 ) -> ( H ` n ) = ( H ` ( m + 1 ) ) )
286		2fveq3 5426	. . . . . . . . . . . . . . . . . 18 |- ( n = ( m + 1 ) -> ( F ` ( G ` n ) ) = ( F ` ( G ` ( m + 1 ) ) ) )
287	285, 286	eqeq12d 2154	. . . . . . . . . . . . . . . . 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 2752	. . . . . . . . . . . . . . 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 468	. . . . . . . . . . . . 13 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( H ` ( m + 1 ) ) = ( F ` ( G ` ( m + 1 ) ) ) )
292	291	oveq2d 5790	. . . . . . . . . . . 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 9174	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( G ` ( m + 1 ) ) e. CC )
294		ax-1cn 7713	. . . . . . . . . . . . . . 15 |- 1 e. CC
295		npcan 7971	. . . . . . . . . . . . . . 15 |- ( ( ( G ` ( m + 1 ) ) e. CC /\ 1 e. CC ) -> ( ( ( G ` ( m + 1 ) ) - 1 ) + 1 ) = ( G ` ( m + 1 ) ) )
296	293, 294, 295	sylancl 409	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( ( ( G ` ( m + 1 ) ) - 1 ) + 1 ) = ( G ` ( m + 1 ) ) )
297		uztrn 9342	. . . . . . . . . . . . . . . 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 408	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( ( G ` ( m + 1 ) ) - 1 ) e. ( ZZ>= ` M ) )
299		eluzp1p1 9351	. . . . . . . . . . . . . . 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 2217	. . . . . . . . . . . . 13 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( G ` ( m + 1 ) ) e. ( ZZ>= ` ( M + 1 ) ) )
302	207, 301, 208, 209	seq3m1 10241	. . . . . . . . . . . 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 2183	. . . . . . . . . . 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 10235	. . . . . . . . . . 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 2154	. . . . . . . . . 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 8736	. . 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 962   = wceq 1331   e. wcel 1480   \ cdif 3068   C_ wss 3071   class class class wbr 3929   `'ccnv 4538   |` cres 4541   -->wf 5119   -1-1-onto->wf1o 5122   ` cfv 5123   Isom wiso 5124  (class class class)co 5774   CCcc 7618   RRcr 7619   1c1 7621   + caddc 7623   RR*cxr 7799   < clt 7800   <_ cle 7801   - cmin 7933   NNcn 8720   ZZcz 9054   ZZ>=cuz 9326   ...cfz 9790   seqcseq 10218  ♯chash 10521

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 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-13 1491  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-coll 4043  ax-sep 4046  ax-nul 4054  ax-pow 4098  ax-pr 4131  ax-un 4355  ax-setind 4452  ax-iinf 4502  ax-cnex 7711  ax-resscn 7712  ax-1cn 7713  ax-1re 7714  ax-icn 7715  ax-addcl 7716  ax-addrcl 7717  ax-mulcl 7718  ax-addcom 7720  ax-addass 7722  ax-distr 7724  ax-i2m1 7725  ax-0lt1 7726  ax-0id 7728  ax-rnegex 7729  ax-cnre 7731  ax-pre-ltirr 7732  ax-pre-ltwlin 7733  ax-pre-lttrn 7734  ax-pre-ltadd 7736

This theorem depends on definitions:  df-bi 116  df-3or 963  df-3an 964  df-tru 1334  df-fal 1337  df-nf 1437  df-sb 1736  df-eu 2002  df-mo 2003  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ne 2309  df-nel 2404  df-ral 2421  df-rex 2422  df-reu 2423  df-rab 2425  df-v 2688  df-sbc 2910  df-csb 3004  df-dif 3073  df-un 3075  df-in 3077  df-ss 3084  df-nul 3364  df-pw 3512  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3737  df-int 3772  df-iun 3815  df-br 3930  df-opab 3990  df-mpt 3991  df-tr 4027  df-id 4215  df-iord 4288  df-on 4290  df-ilim 4291  df-suc 4293  df-iom 4505  df-xp 4545  df-rel 4546  df-cnv 4547  df-co 4548  df-dm 4549  df-rn 4550  df-res 4551  df-ima 4552  df-iota 5088  df-fun 5125  df-fn 5126  df-f 5127  df-f1 5128  df-fo 5129  df-f1o 5130  df-fv 5131  df-isom 5132  df-riota 5730  df-ov 5777  df-oprab 5778  df-mpo 5779  df-1st 6038  df-2nd 6039  df-recs 6202  df-frec 6288  df-pnf 7802  df-mnf 7803  df-xr 7804  df-ltxr 7805  df-le 7806  df-sub 7935  df-neg 7936  df-inn 8721  df-n0 8978  df-z 9055  df-uz 9327  df-fz 9791  df-fzo 9920  df-seqfrec 10219

This theorem is referenced by:  summodclem2a  11150  prodmodclem2a  11345