Theorem seq3coll 10777

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 10010	. . . 4 |- ( N e. ( 1 ... (♯ ` A ) ) -> N e. NN )
3	1, 2	syl 14	. . 3 |- ( ph -> N e. NN )
4		eleq1 2233	. . . . . 6 |- ( y = 1 -> ( y e. ( 1 ... (♯ ` A ) ) <-> 1 e. ( 1 ... (♯ ` A ) ) ) )
5		2fveq3 5501	. . . . . . 7 |- ( y = 1 -> ( seq M ( .+ , F ) ` ( G ` y ) ) = ( seq M ( .+ , F ) ` ( G ` 1 ) ) )
6		fveq2 5496	. . . . . . 7 |- ( y = 1 -> ( seq 1 ( .+ , H ) ` y ) = ( seq 1 ( .+ , H ) ` 1 ) )
7	5, 6	eqeq12d 2185	. . . . . 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 2233	. . . . . 6 |- ( y = m -> ( y e. ( 1 ... (♯ ` A ) ) <-> m e. ( 1 ... (♯ ` A ) ) ) )
11		2fveq3 5501	. . . . . . 7 |- ( y = m -> ( seq M ( .+ , F ) ` ( G ` y ) ) = ( seq M ( .+ , F ) ` ( G ` m ) ) )
12		fveq2 5496	. . . . . . 7 |- ( y = m -> ( seq 1 ( .+ , H ) ` y ) = ( seq 1 ( .+ , H ) ` m ) )
13	11, 12	eqeq12d 2185	. . . . . 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 2233	. . . . . 6 |- ( y = ( m + 1 ) -> ( y e. ( 1 ... (♯ ` A ) ) <-> ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) )
17		2fveq3 5501	. . . . . . 7 |- ( y = ( m + 1 ) -> ( seq M ( .+ , F ) ` ( G ` y ) ) = ( seq M ( .+ , F ) ` ( G ` ( m + 1 ) ) ) )
18		fveq2 5496	. . . . . . 7 |- ( y = ( m + 1 ) -> ( seq 1 ( .+ , H ) ` y ) = ( seq 1 ( .+ , H ) ` ( m + 1 ) ) )
19	17, 18	eqeq12d 2185	. . . . . 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 2233	. . . . . 6 |- ( y = N -> ( y e. ( 1 ... (♯ ` A ) ) <-> N e. ( 1 ... (♯ ` A ) ) ) )
23		2fveq3 5501	. . . . . . 7 |- ( y = N -> ( seq M ( .+ , F ) ` ( G ` y ) ) = ( seq M ( .+ , F ) ` ( G ` N ) ) )
24		fveq2 5496	. . . . . . 7 |- ( y = N -> ( seq 1 ( .+ , H ) ` y ) = ( seq 1 ( .+ , H ) ` N ) )
25	23, 24	eqeq12d 2185	. . . . . 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 5786	. . . . . . . . . . . . 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 5442	. . . . . . . . . . . 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 9985	. . . . . . . . . . . . 13 |- ( N e. ( 1 ... (♯ ` A ) ) -> (♯ ` A ) e. ( ZZ>= ` 1 ) )
37	1, 36	syl 14	. . . . . . . . . . . 12 |- ( ph -> (♯ ` A ) e. ( ZZ>= ` 1 ) )
38		eluzfz1 9987	. . . . . . . . . . . 12 |- ( (♯ ` A ) e. ( ZZ>= ` 1 ) -> 1 e. ( 1 ... (♯ ` A ) ) )
39	37, 38	syl 14	. . . . . . . . . . 11 |- ( ph -> 1 e. ( 1 ... (♯ ` A ) ) )
40	35, 39	ffvelrnd 5632	. . . . . . . . . 10 |- ( ph -> ( G ` 1 ) e. A )
41	30, 40	sseldd 3148	. . . . . . . . 9 |- ( ph -> ( G ` 1 ) e. ( ZZ>= ` M ) )
42		eluzle 9499	. . . . . . . . . . . . 13 |- ( (♯ ` A ) e. ( ZZ>= ` 1 ) -> 1 <_ (♯ ` A ) )
43	37, 42	syl 14	. . . . . . . . . . . 12 |- ( ph -> 1 <_ (♯ ` A ) )
44		elfzelz 9981	. . . . . . . . . . . . . . . . 17 |- ( k e. ( 1 ... (♯ ` A ) ) -> k e. ZZ )
45	44	ssriv 3151	. . . . . . . . . . . . . . . 16 |- ( 1 ... (♯ ` A ) ) C_ ZZ
46		zssre 9219	. . . . . . . . . . . . . . . 16 |- ZZ C_ RR
47	45, 46	sstri 3156	. . . . . . . . . . . . . . 15 |- ( 1 ... (♯ ` A ) ) C_ RR
48	47	a1i 9	. . . . . . . . . . . . . 14 |- ( ph -> ( 1 ... (♯ ` A ) ) C_ RR )
49		ressxr 7963	. . . . . . . . . . . . . 14 |- RR C_ RR*
50	48, 49	sstrdi 3159	. . . . . . . . . . . . 13 |- ( ph -> ( 1 ... (♯ ` A ) ) C_ RR* )
51		eluzelre 9497	. . . . . . . . . . . . . . . 16 |- ( k e. ( ZZ>= ` M ) -> k e. RR )
52	51	ssriv 3151	. . . . . . . . . . . . . . 15 |- ( ZZ>= ` M ) C_ RR
53	30, 52	sstrdi 3159	. . . . . . . . . . . . . 14 |- ( ph -> A C_ RR )
54	53, 49	sstrdi 3159	. . . . . . . . . . . . 13 |- ( ph -> A C_ RR* )
55		eluzfz2 9988	. . . . . . . . . . . . . 14 |- ( (♯ ` A ) e. ( ZZ>= ` 1 ) -> (♯ ` A ) e. ( 1 ... (♯ ` A ) ) )
56	37, 55	syl 14	. . . . . . . . . . . . 13 |- ( ph -> (♯ ` A ) e. ( 1 ... (♯ ` A ) ) )
57		leisorel 10772	. . . . . . . . . . . . 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 1242	. . . . . . . . . . . 12 |- ( ph -> ( 1 <_ (♯ ` A ) <-> ( G ` 1 ) <_ ( G ` (♯ ` A ) ) ) )
59	43, 58	mpbid 146	. . . . . . . . . . 11 |- ( ph -> ( G ` 1 ) <_ ( G ` (♯ ` A ) ) )
60	35, 56	ffvelrnd 5632	. . . . . . . . . . . . . 14 |- ( ph -> ( G ` (♯ ` A ) ) e. A )
61	30, 60	sseldd 3148	. . . . . . . . . . . . 13 |- ( ph -> ( G ` (♯ ` A ) ) e. ( ZZ>= ` M ) )
62		eluzelz 9496	. . . . . . . . . . . . 13 |- ( ( G ` (♯ ` A ) ) e. ( ZZ>= ` M ) -> ( G ` (♯ ` A ) ) e. ZZ )
63	61, 62	syl 14	. . . . . . . . . . . 12 |- ( ph -> ( G ` (♯ ` A ) ) e. ZZ )
64		elfz5 9973	. . . . . . . . . . . 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 5496	. . . . . . . . . . . . 13 |- ( k = ( G ` 1 ) -> ( F ` k ) = ( F ` ( G ` 1 ) ) )
68	67	eleq1d 2239	. . . . . . . . . . . 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 9977	. . . . . . . . . . . 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 2796	. . . . . . . . . 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 9496	. . . . . . . . . . . . . . . . . 18 |- ( ( G ` 1 ) e. ( ZZ>= ` M ) -> ( G ` 1 ) e. ZZ )
77	41, 76	syl 14	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( G ` 1 ) e. ZZ )
78		peano2zm 9250	. . . . . . . . . . . . . . . . 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 9334	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( G ` 1 ) - 1 ) e. RR )
81	77	zred 9334	. . . . . . . . . . . . . . 15 |- ( ph -> ( G ` 1 ) e. RR )
82	63	zred 9334	. . . . . . . . . . . . . . 15 |- ( ph -> ( G ` (♯ ` A ) ) e. RR )
83	81	lem1d 8849	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( G ` 1 ) - 1 ) <_ ( G ` 1 ) )
84	80, 81, 82, 83, 59	letrd 8043	. . . . . . . . . . . . . 14 |- ( ph -> ( ( G ` 1 ) - 1 ) <_ ( G ` (♯ ` A ) ) )
85		eluz 9500	. . . . . . . . . . . . . . 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 10020	. . . . . . . . . . . . 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 3147	. . . . . . . . . . 11 |- ( ( ph /\ k e. ( M ... ( ( G ` 1 ) - 1 ) ) ) -> k e. ( M ... ( G ` (♯ ` A ) ) ) )
91		eluzel2 9492	. . . . . . . . . . . . . . 15 |- ( ( G ` 1 ) e. ( ZZ>= ` M ) -> M e. ZZ )
92	41, 91	syl 14	. . . . . . . . . . . . . 14 |- ( ph -> M e. ZZ )
93		elfzm11 10047	. . . . . . . . . . . . . 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 994	. . . . . . . . . . . . . 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 3147	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ k e. A ) -> k e. RR )
98		f1ocnv 5455	. . . . . . . . . . . . . . . . . . . . . . . 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 5442	. . . . . . . . . . . . . . . . . . . . . . 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 5631	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ k e. A ) -> ( `' G ` k ) e. ( 1 ... (♯ ` A ) ) )
103		elfznn 10010	. . . . . . . . . . . . . . . . . . . . 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 8921	. . . . . . . . . . . . . . . . . . 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 10772	. . . . . . . . . . . . . . . . . . . 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 1242	. . . . . . . . . . . . . . . . . . 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 5757	. . . . . . . . . . . . . . . . . . 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 4015	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ k e. A ) -> ( G ` 1 ) <_ k )
116	96, 97, 115	lensymd 8041	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ k e. A ) -> -. k < ( G ` 1 ) )
117	116	ex 114	. . . . . . . . . . . . . . 15 |- ( ph -> ( k e. A -> -. k < ( G ` 1 ) ) )
118	117	con2d 619	. . . . . . . . . . . . . 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 3131	. . . . . . . . . 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 10464	. . . . . . . 8 |- ( ph -> ( seq M ( .+ , F ) |` ( ZZ>= ` ( G ` 1 ) ) ) = seq ( G ` 1 ) ( .+ , F ) )
127	126	fveq1d 5498	. . . . . . 7 |- ( ph -> ( ( seq M ( .+ , F ) |` ( ZZ>= ` ( G ` 1 ) ) ) ` ( G ` 1 ) ) = ( seq ( G ` 1 ) ( .+ , F ) ` ( G ` 1 ) ) )
128		uzid 9501	. . . . . . . . 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 5520	. . . . . . . 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 9496	. . . . . . . . . . . 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 9334	. . . . . . . . . . . 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 9334	. . . . . . . . . . . 12 |- ( ( ph /\ k e. ( ZZ>= ` ( G ` 1 ) ) ) -> k e. RR )
138		eluzle 9499	. . . . . . . . . . . . . 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 9499	. . . . . . . . . . . . 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 8043	. . . . . . . . . . 11 |- ( ( ph /\ k e. ( ZZ>= ` ( G ` 1 ) ) ) -> M <_ k )
144		eluz2 9493	. . . . . . . . . . 11 |- ( k e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ k e. ZZ /\ M <_ k ) )
145	132, 134, 143, 144	syl3anbrc 1176	. . . . . . . . . 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 10416	. . . . . . . 8 |- ( ph -> ( seq ( G ` 1 ) ( .+ , F ) ` ( G ` 1 ) ) = ( F ` ( G ` 1 ) ) )
148		fveq2 5496	. . . . . . . . . . . 12 |- ( n = 1 -> ( H ` n ) = ( H ` 1 ) )
149		2fveq3 5501	. . . . . . . . . . . 12 |- ( n = 1 -> ( F ` ( G ` n ) ) = ( F ` ( G ` 1 ) ) )
150	148, 149	eqeq12d 2185	. . . . . . . . . . 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 2796	. . . . . . . . 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 2206	. . . . . . 7 |- ( ph -> ( seq ( G ` 1 ) ( .+ , F ) ` ( G ` 1 ) ) = ( H ` 1 ) )
157	127, 131, 156	3eqtr3d 2211	. . . . . 6 |- ( ph -> ( seq M ( .+ , F ) ` ( G ` 1 ) ) = ( H ` 1 ) )
158		1zzd 9239	. . . . . . 7 |- ( ph -> 1 e. ZZ )
159		seqcoll.hcl	. . . . . . 7 |- ( ( ph /\ k e. ( ZZ>= ` 1 ) ) -> ( H ` k ) e. S )
160	158, 159, 125	seq3-1 10416	. . . . . 6 |- ( ph -> ( seq 1 ( .+ , H ) ` 1 ) = ( H ` 1 ) )
161	157, 160	eqtr4d 2206	. . . . 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 525	. . . . . . . . . . 11 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> m e. NN )
164		nnuz 9522	. . . . . . . . . . 11 |- NN = ( ZZ>= ` 1 )
165	163, 164	eleqtrdi 2263	. . . . . . . . . 10 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> m e. ( ZZ>= ` 1 ) )
166		nnz 9231	. . . . . . . . . . . 12 |- ( m e. NN -> m e. ZZ )
167	166	ad2antlr 486	. . . . . . . . . . 11 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> m e. ZZ )
168		elfzuz3 9978	. . . . . . . . . . . 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 9544	. . . . . . . . . . 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 9975	. . . . . . . . . 10 |- ( m e. ( 1 ... (♯ ` A ) ) <-> ( m e. ( ZZ>= ` 1 ) /\ (♯ ` A ) e. ( ZZ>= ` m ) ) )
173	165, 171, 172	sylanbrc 415	. . . . . . . . 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 5860	. . . . . . . . . 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 524	. . . . . . . . . . . . . . 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 485	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> A C_ ( ZZ>= ` M ) )
181	35	ad2antrr 485	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> G : ( 1 ... (♯ ` A ) ) --> A )
182	181, 173	ffvelrnd 5632	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( G ` m ) e. A )
183	180, 182	sseldd 3148	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( G ` m ) e. ( ZZ>= ` M ) )
184		nnre 8885	. . . . . . . . . . . . . . . . . . 19 |- ( m e. NN -> m e. RR )
185	184	ad2antlr 486	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> m e. RR )
186	185	ltp1d 8846	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> m < ( m + 1 ) )
187	31	ad2antrr 485	. . . . . . . . . . . . . . . . . 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 5787	. . . . . . . . . . . . . . . . . 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 1231	. . . . . . . . . . . . . . . . 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 9496	. . . . . . . . . . . . . . . . . 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 5632	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( G ` ( m + 1 ) ) e. A )
195	180, 194	sseldd 3148	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( G ` ( m + 1 ) ) e. ( ZZ>= ` M ) )
196		eluzelz 9496	. . . . . . . . . . . . . . . . . 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 9269	. . . . . . . . . . . . . . . . 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 9250	. . . . . . . . . . . . . . . . 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 9500	. . . . . . . . . . . . . . . 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 2170	. . . . . . . . . . . . . . . 16 |- ( ZZ>= ` M ) = ( ZZ>= ` M )
207	92	ad2antrr 485	. . . . . . . . . . . . . . . 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 10417	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> seq M ( .+ , F ) : ( ZZ>= ` M ) --> S )
211	210, 183	ffvelrnd 5632	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( seq M ( .+ , F ) ` ( G ` m ) ) e. S )
212		simplll 528	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) /\ k e. ( ( ( G ` m ) + 1 ) ... ( ( G ` ( m + 1 ) ) - 1 ) ) ) -> ph )
213		elfzuz 9977	. . . . . . . . . . . . . . . . . 18 |- ( k e. ( ( ( G ` m ) + 1 ) ... ( ( G ` ( m + 1 ) ) - 1 ) ) -> k e. ( ZZ>= ` ( ( G ` m ) + 1 ) ) )
214		peano2uz 9542	. . . . . . . . . . . . . . . . . . 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 9503	. . . . . . . . . . . . . . . . . 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 9334	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( ( G ` ( m + 1 ) ) - 1 ) e. RR )
219	197	zred 9334	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( G ` ( m + 1 ) ) e. RR )
220	82	ad2antrr 485	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( G ` (♯ ` A ) ) e. RR )
221	219	lem1d 8849	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( ( G ` ( m + 1 ) ) - 1 ) <_ ( G ` ( m + 1 ) ) )
222		elfzle2 9984	. . . . . . . . . . . . . . . . . . . . . 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 485	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( 1 ... (♯ ` A ) ) C_ RR* )
225	54	ad2antrr 485	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> A C_ RR* )
226	56	ad2antrr 485	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> (♯ ` A ) e. ( 1 ... (♯ ` A ) ) )
227		leisorel 10772	. . . . . . . . . . . . . . . . . . . . . 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 1242	. . . . . . . . . . . . . . . . . . . . 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 8043	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( ( G ` ( m + 1 ) ) - 1 ) <_ ( G ` (♯ ` A ) ) )
231	63	ad2antrr 485	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( G ` (♯ ` A ) ) e. ZZ )
232		eluz 9500	. . . . . . . . . . . . . . . . . . . 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 9978	. . . . . . . . . . . . . . . . . 18 |- ( k e. ( ( ( G ` m ) + 1 ) ... ( ( G ` ( m + 1 ) ) - 1 ) ) -> ( ( G ` ( m + 1 ) ) - 1 ) e. ( ZZ>= ` k ) )
236		uztrn 9503	. . . . . . . . . . . . . . . . . 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 9975	. . . . . . . . . . . . . . . . 17 |- ( k e. ( M ... ( G ` (♯ ` A ) ) ) <-> ( k e. ( ZZ>= ` M ) /\ ( G ` (♯ ` A ) ) e. ( ZZ>= ` k ) ) )
239	217, 237, 238	sylanbrc 415	. . . . . . . . . . . . . . . 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 486	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) /\ k e. A ) ) -> m e. ZZ )
241	101	ad2antrr 485	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) /\ k e. A ) ) -> `' G : A --> ( 1 ... (♯ ` A ) ) )
242		simprr 527	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) /\ k e. A ) ) -> k e. A )
243	241, 242	ffvelrnd 5632	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) /\ k e. A ) ) -> ( `' G ` k ) e. ( 1 ... (♯ ` A ) ) )
244		elfzelz 9981	. . . . . . . . . . . . . . . . . . . . . 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 9306	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( m e. ZZ /\ m < ( `' G ` k ) /\ ( `' G ` k ) < ( m + 1 ) ) -> -. ( `' G ` k ) e. ZZ )
247	246	3expib 1201	. . . . . . . . . . . . . . . . . . . . . 22 |- ( m e. ZZ -> ( ( m < ( `' G ` k ) /\ ( `' G ` k ) < ( m + 1 ) ) -> -. ( `' G ` k ) e. ZZ ) )
248	247	con2d 619	. . . . . . . . . . . . . . . . . . . . 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 485	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) /\ k e. A ) ) -> G Isom < , < ( ( 1 ... (♯ ` A ) ) , A ) )
251	173	adantrr 476	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) /\ k e. A ) ) -> m e. ( 1 ... (♯ ` A ) ) )
252		isorel 5787	. . . . . . . . . . . . . . . . . . . . . . 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 1231	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) /\ k e. A ) ) -> ( m < ( `' G ` k ) <-> ( G ` m ) < ( G ` ( `' G ` k ) ) ) )
254	33	ad2antrr 485	. . . . . . . . . . . . . . . . . . . . . . . 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 4001	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) /\ k e. A ) ) -> ( ( G ` m ) < ( G ` ( `' G ` k ) ) <-> ( G ` m ) < k ) )
257	193	adantrr 476	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) /\ k e. A ) ) -> ( G ` m ) e. ZZ )
258	30	ad2antrr 485	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) /\ k e. A ) ) -> A C_ ( ZZ>= ` M ) )
259	258, 242	sseldd 3148	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) /\ k e. A ) ) -> k e. ( ZZ>= ` M ) )
260		eluzelz 9496	. . . . . . . . . . . . . . . . . . . . . . . 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 9266	. . . . . . . . . . . . . . . . . . . . . . 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 476	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) /\ k e. A ) ) -> ( m + 1 ) e. ( 1 ... (♯ ` A ) ) )
266		isorel 5787	. . . . . . . . . . . . . . . . . . . . . . 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 1231	. . . . . . . . . . . . . . . . . . . . . 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 3999	. . . . . . . . . . . . . . . . . . . . . 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 476	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ m e. NN ) /\ ( ( m + 1 ) e. ( 1 ... (♯ ` A ) ) /\ k e. A ) ) -> ( G ` ( m + 1 ) ) e. ZZ )
270		zltlem1 9269	. . . . . . . . . . . . . . . . . . . . . . 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 470	. . . . . . . . . . . . . . . . . . . 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 667	. . . . . . . . . . . . . . . . . . 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 619	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( ( ( ( G ` m ) + 1 ) <_ k /\ k <_ ( ( G ` ( m + 1 ) ) - 1 ) ) -> -. k e. A ) )
277		elfzle1 9983	. . . . . . . . . . . . . . . . . 18 |- ( k e. ( ( ( G ` m ) + 1 ) ... ( ( G ` ( m + 1 ) ) - 1 ) ) -> ( ( G ` m ) + 1 ) <_ k )
278		elfzle2 9984	. . . . . . . . . . . . . . . . . 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 3131	. . . . . . . . . . . . . . 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 10465	. . . . . . . . . . . . 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 5868	. . . . . . . . . . . 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 5496	. . . . . . . . . . . . . . . . . 18 |- ( n = ( m + 1 ) -> ( H ` n ) = ( H ` ( m + 1 ) ) )
286		2fveq3 5501	. . . . . . . . . . . . . . . . . 18 |- ( n = ( m + 1 ) -> ( F ` ( G ` n ) ) = ( F ` ( G ` ( m + 1 ) ) ) )
287	285, 286	eqeq12d 2185	. . . . . . . . . . . . . . . . 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 2796	. . . . . . . . . . . . . . 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 474	. . . . . . . . . . . . 13 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( H ` ( m + 1 ) ) = ( F ` ( G ` ( m + 1 ) ) ) )
292	291	oveq2d 5869	. . . . . . . . . . . 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 9335	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( G ` ( m + 1 ) ) e. CC )
294		ax-1cn 7867	. . . . . . . . . . . . . . 15 |- 1 e. CC
295		npcan 8128	. . . . . . . . . . . . . . 15 |- ( ( ( G ` ( m + 1 ) ) e. CC /\ 1 e. CC ) -> ( ( ( G ` ( m + 1 ) ) - 1 ) + 1 ) = ( G ` ( m + 1 ) ) )
296	293, 294, 295	sylancl 411	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( ( ( G ` ( m + 1 ) ) - 1 ) + 1 ) = ( G ` ( m + 1 ) ) )
297		uztrn 9503	. . . . . . . . . . . . . . . 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 9512	. . . . . . . . . . . . . . 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 2248	. . . . . . . . . . . . 13 |- ( ( ( ph /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... (♯ ` A ) ) ) -> ( G ` ( m + 1 ) ) e. ( ZZ>= ` ( M + 1 ) ) )
302	207, 301, 208, 209	seq3m1 10424	. . . . . . . . . . . 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 2214	. . . . . . . . . . 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 10418	. . . . . . . . . . 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 2185	. . . . . . . . . 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 8894	. . 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 973   = wceq 1348   e. wcel 2141   \ cdif 3118   C_ wss 3121   class class class wbr 3989   `'ccnv 4610   |` cres 4613   -->wf 5194   -1-1-onto->wf1o 5197   ` cfv 5198   Isom wiso 5199  (class class class)co 5853   CCcc 7772   RRcr 7773   1c1 7775   + caddc 7777   RR*cxr 7953   < clt 7954   <_ cle 7955   - cmin 8090   NNcn 8878   ZZcz 9212   ZZ>=cuz 9487   ...cfz 9965   seqcseq 10401  ♯chash 10709

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 609  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-13 2143  ax-14 2144  ax-ext 2152  ax-coll 4104  ax-sep 4107  ax-nul 4115  ax-pow 4160  ax-pr 4194  ax-un 4418  ax-setind 4521  ax-iinf 4572  ax-cnex 7865  ax-resscn 7866  ax-1cn 7867  ax-1re 7868  ax-icn 7869  ax-addcl 7870  ax-addrcl 7871  ax-mulcl 7872  ax-addcom 7874  ax-addass 7876  ax-distr 7878  ax-i2m1 7879  ax-0lt1 7880  ax-0id 7882  ax-rnegex 7883  ax-cnre 7885  ax-pre-ltirr 7886  ax-pre-ltwlin 7887  ax-pre-lttrn 7888  ax-pre-ltadd 7890

This theorem depends on definitions:  df-bi 116  df-3or 974  df-3an 975  df-tru 1351  df-fal 1354  df-nf 1454  df-sb 1756  df-eu 2022  df-mo 2023  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ne 2341  df-nel 2436  df-ral 2453  df-rex 2454  df-reu 2455  df-rab 2457  df-v 2732  df-sbc 2956  df-csb 3050  df-dif 3123  df-un 3125  df-in 3127  df-ss 3134  df-nul 3415  df-pw 3568  df-sn 3589  df-pr 3590  df-op 3592  df-uni 3797  df-int 3832  df-iun 3875  df-br 3990  df-opab 4051  df-mpt 4052  df-tr 4088  df-id 4278  df-iord 4351  df-on 4353  df-ilim 4354  df-suc 4356  df-iom 4575  df-xp 4617  df-rel 4618  df-cnv 4619  df-co 4620  df-dm 4621  df-rn 4622  df-res 4623  df-ima 4624  df-iota 5160  df-fun 5200  df-fn 5201  df-f 5202  df-f1 5203  df-fo 5204  df-f1o 5205  df-fv 5206  df-isom 5207  df-riota 5809  df-ov 5856  df-oprab 5857  df-mpo 5858  df-1st 6119  df-2nd 6120  df-recs 6284  df-frec 6370  df-pnf 7956  df-mnf 7957  df-xr 7958  df-ltxr 7959  df-le 7960  df-sub 8092  df-neg 8093  df-inn 8879  df-n0 9136  df-z 9213  df-uz 9488  df-fz 9966  df-fzo 10099  df-seqfrec 10402

This theorem is referenced by:  summodclem2a  11344  prodmodclem2a  11539