ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  seq3coll Unicode version

Theorem seq3coll 10597
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.
StepHypRef Expression
1 seqcoll.3 . 2  |-  ( ph  ->  N  e.  ( 1 ... ( `  A
) ) )
2 elfznn 9846 . . . 4  |-  ( N  e.  ( 1 ... ( `  A )
)  ->  N  e.  NN )
31, 2syl 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
) )
75, 6eqeq12d 2154 . . . . . 6  |-  ( y  =  1  ->  (
(  seq M (  .+  ,  F ) `  ( G `  y )
)  =  (  seq 1 (  .+  ,  H ) `  y
)  <->  (  seq M
(  .+  ,  F
) `  ( G `  1 ) )  =  (  seq 1
(  .+  ,  H
) `  1 )
) )
84, 7imbi12d 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
) ) ) )
98imbi2d 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
) )
1311, 12eqeq12d 2154 . . . . . 6  |-  ( y  =  m  ->  (
(  seq M (  .+  ,  F ) `  ( G `  y )
)  =  (  seq 1 (  .+  ,  H ) `  y
)  <->  (  seq M
(  .+  ,  F
) `  ( G `  m ) )  =  (  seq 1 ( 
.+  ,  H ) `
 m ) ) )
1410, 13imbi12d 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
) ) ) )
1514imbi2d 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 ) ) )
1917, 18eqeq12d 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 ) ) ) )
2016, 19imbi12d 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 ) ) ) ) )
2120imbi2d 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
) )
2523, 24eqeq12d 2154 . . . . . 6  |-  ( y  =  N  ->  (
(  seq M (  .+  ,  F ) `  ( G `  y )
)  =  (  seq 1 (  .+  ,  H ) `  y
)  <->  (  seq M
(  .+  ,  F
) `  ( G `  N ) )  =  (  seq 1 ( 
.+  ,  H ) `
 N ) ) )
2622, 25imbi12d 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
) ) ) )
2726imbi2d 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 )
3331, 32syl 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 )
3533, 34syl 14 . . . . . . . . . . 11  |-  ( ph  ->  G : ( 1 ... ( `  A
) ) --> A )
36 elfzuz2 9821 . . . . . . . . . . . . 13  |-  ( N  e.  ( 1 ... ( `  A )
)  ->  ( `  A
)  e.  ( ZZ>= ` 
1 ) )
371, 36syl 14 . . . . . . . . . . . 12  |-  ( ph  ->  ( `  A )  e.  ( ZZ>= `  1 )
)
38 eluzfz1 9823 . . . . . . . . . . . 12  |-  ( ( `  A )  e.  (
ZZ>= `  1 )  -> 
1  e.  ( 1 ... ( `  A
) ) )
3937, 38syl 14 . . . . . . . . . . 11  |-  ( ph  ->  1  e.  ( 1 ... ( `  A
) ) )
4035, 39ffvelrnd 5556 . . . . . . . . . 10  |-  ( ph  ->  ( G `  1
)  e.  A )
4130, 40sseldd 3098 . . . . . . . . 9  |-  ( ph  ->  ( G `  1
)  e.  ( ZZ>= `  M ) )
42 eluzle 9350 . . . . . . . . . . . . 13  |-  ( ( `  A )  e.  (
ZZ>= `  1 )  -> 
1  <_  ( `  A
) )
4337, 42syl 14 . . . . . . . . . . . 12  |-  ( ph  ->  1  <_  ( `  A
) )
44 elfzelz 9818 . . . . . . . . . . . . . . . . 17  |-  ( k  e.  ( 1 ... ( `  A )
)  ->  k  e.  ZZ )
4544ssriv 3101 . . . . . . . . . . . . . . . 16  |-  ( 1 ... ( `  A
) )  C_  ZZ
46 zssre 9073 . . . . . . . . . . . . . . . 16  |-  ZZ  C_  RR
4745, 46sstri 3106 . . . . . . . . . . . . . . 15  |-  ( 1 ... ( `  A
) )  C_  RR
4847a1i 9 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 1 ... ( `  A ) )  C_  RR )
49 ressxr 7821 . . . . . . . . . . . . . 14  |-  RR  C_  RR*
5048, 49sstrdi 3109 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 1 ... ( `  A ) )  C_  RR* )
51 eluzelre 9348 . . . . . . . . . . . . . . . 16  |-  ( k  e.  ( ZZ>= `  M
)  ->  k  e.  RR )
5251ssriv 3101 . . . . . . . . . . . . . . 15  |-  ( ZZ>= `  M )  C_  RR
5330, 52sstrdi 3109 . . . . . . . . . . . . . 14  |-  ( ph  ->  A  C_  RR )
5453, 49sstrdi 3109 . . . . . . . . . . . . 13  |-  ( ph  ->  A  C_  RR* )
55 eluzfz2 9824 . . . . . . . . . . . . . 14  |-  ( ( `  A )  e.  (
ZZ>= `  1 )  -> 
( `  A )  e.  ( 1 ... ( `  A ) ) )
5637, 55syl 14 . . . . . . . . . . . . 13  |-  ( ph  ->  ( `  A )  e.  ( 1 ... ( `  A ) ) )
57 leisorel 10592 . . . . . . . . . . . . 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 ) ) ) )
5831, 50, 54, 39, 56, 57syl122anc 1225 . . . . . . . . . . . 12  |-  ( ph  ->  ( 1  <_  ( `  A )  <->  ( G `  1 )  <_ 
( G `  ( `  A ) ) ) )
5943, 58mpbid 146 . . . . . . . . . . 11  |-  ( ph  ->  ( G `  1
)  <_  ( G `  ( `  A )
) )
6035, 56ffvelrnd 5556 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( G `  ( `  A ) )  e.  A )
6130, 60sseldd 3098 . . . . . . . . . . . . 13  |-  ( ph  ->  ( G `  ( `  A ) )  e.  ( ZZ>= `  M )
)
62 eluzelz 9347 . . . . . . . . . . . . 13  |-  ( ( G `  ( `  A
) )  e.  (
ZZ>= `  M )  -> 
( G `  ( `  A ) )  e.  ZZ )
6361, 62syl 14 . . . . . . . . . . . 12  |-  ( ph  ->  ( G `  ( `  A ) )  e.  ZZ )
64 elfz5 9810 . . . . . . . . . . . 12  |-  ( ( ( G `  1
)  e.  ( ZZ>= `  M )  /\  ( G `  ( `  A
) )  e.  ZZ )  ->  ( ( G `
 1 )  e.  ( M ... ( G `  ( `  A
) ) )  <->  ( G `  1 )  <_ 
( G `  ( `  A ) ) ) )
6541, 63, 64syl2anc 408 . . . . . . . . . . 11  |-  ( ph  ->  ( ( G ` 
1 )  e.  ( M ... ( G `
 ( `  A
) ) )  <->  ( G `  1 )  <_ 
( G `  ( `  A ) ) ) )
6659, 65mpbird 166 . . . . . . . . . 10  |-  ( ph  ->  ( G `  1
)  e.  ( M ... ( G `  ( `  A ) ) ) )
67 fveq2 5421 . . . . . . . . . . . . 13  |-  ( k  =  ( G ` 
1 )  ->  ( F `  k )  =  ( F `  ( G `  1 ) ) )
6867eleq1d 2208 . . . . . . . . . . . 12  |-  ( k  =  ( G ` 
1 )  ->  (
( F `  k
)  e.  S  <->  ( F `  ( G `  1
) )  e.  S
) )
6968imbi2d 229 . . . . . . . . . . 11  |-  ( k  =  ( G ` 
1 )  ->  (
( ph  ->  ( F `
 k )  e.  S )  <->  ( ph  ->  ( F `  ( G `  1 )
)  e.  S ) ) )
70 elfzuz 9814 . . . . . . . . . . . 12  |-  ( k  e.  ( M ... ( G `  ( `  A
) ) )  -> 
k  e.  ( ZZ>= `  M ) )
71 seqcoll.5 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  ( ZZ>= `  M )
)  ->  ( F `  k )  e.  S
)
7271expcom 115 . . . . . . . . . . . 12  |-  ( k  e.  ( ZZ>= `  M
)  ->  ( ph  ->  ( F `  k
)  e.  S ) )
7370, 72syl 14 . . . . . . . . . . 11  |-  ( k  e.  ( M ... ( G `  ( `  A
) ) )  -> 
( ph  ->  ( F `
 k )  e.  S ) )
7469, 73vtoclga 2752 . . . . . . . . . 10  |-  ( ( G `  1 )  e.  ( M ... ( G `  ( `  A
) ) )  -> 
( ph  ->  ( F `
 ( G ` 
1 ) )  e.  S ) )
7566, 74mpcom 36 . . . . . . . . 9  |-  ( ph  ->  ( F `  ( G `  1 )
)  e.  S )
76 eluzelz 9347 . . . . . . . . . . . . . . . . . 18  |-  ( ( G `  1 )  e.  ( ZZ>= `  M
)  ->  ( G `  1 )  e.  ZZ )
7741, 76syl 14 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( G `  1
)  e.  ZZ )
78 peano2zm 9104 . . . . . . . . . . . . . . . . 17  |-  ( ( G `  1 )  e.  ZZ  ->  (
( G `  1
)  -  1 )  e.  ZZ )
7977, 78syl 14 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( G ` 
1 )  -  1 )  e.  ZZ )
8079zred 9185 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( G ` 
1 )  -  1 )  e.  RR )
8177zred 9185 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( G `  1
)  e.  RR )
8263zred 9185 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( G `  ( `  A ) )  e.  RR )
8381lem1d 8703 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( G ` 
1 )  -  1 )  <_  ( G `  1 ) )
8480, 81, 82, 83, 59letrd 7898 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( G ` 
1 )  -  1 )  <_  ( G `  ( `  A )
) )
85 eluz 9351 . . . . . . . . . . . . . . 15  |-  ( ( ( ( G ` 
1 )  -  1 )  e.  ZZ  /\  ( G `  ( `  A
) )  e.  ZZ )  ->  ( ( G `
 ( `  A
) )  e.  (
ZZ>= `  ( ( G `
 1 )  - 
1 ) )  <->  ( ( G `  1 )  -  1 )  <_ 
( G `  ( `  A ) ) ) )
8679, 63, 85syl2anc 408 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( G `  ( `  A ) )  e.  ( ZZ>= `  (
( G `  1
)  -  1 ) )  <->  ( ( G `
 1 )  - 
1 )  <_  ( G `  ( `  A
) ) ) )
8784, 86mpbird 166 . . . . . . . . . . . . 13  |-  ( ph  ->  ( G `  ( `  A ) )  e.  ( ZZ>= `  ( ( G `  1 )  -  1 ) ) )
88 fzss2 9856 . . . . . . . . . . . . 13  |-  ( ( G `  ( `  A
) )  e.  (
ZZ>= `  ( ( G `
 1 )  - 
1 ) )  -> 
( M ... (
( G `  1
)  -  1 ) )  C_  ( M ... ( G `  ( `  A ) ) ) )
8987, 88syl 14 . . . . . . . . . . . 12  |-  ( ph  ->  ( M ... (
( G `  1
)  -  1 ) )  C_  ( M ... ( G `  ( `  A ) ) ) )
9089sselda 3097 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ( M ... ( ( G `  1 )  -  1 ) ) )  ->  k  e.  ( M ... ( G `
 ( `  A
) ) ) )
91 eluzel2 9343 . . . . . . . . . . . . . . 15  |-  ( ( G `  1 )  e.  ( ZZ>= `  M
)  ->  M  e.  ZZ )
9241, 91syl 14 . . . . . . . . . . . . . 14  |-  ( ph  ->  M  e.  ZZ )
93 elfzm11 9883 . . . . . . . . . . . . . 14  |-  ( ( M  e.  ZZ  /\  ( G `  1 )  e.  ZZ )  -> 
( k  e.  ( M ... ( ( G `  1 )  -  1 ) )  <-> 
( k  e.  ZZ  /\  M  <_  k  /\  k  <  ( G ` 
1 ) ) ) )
9492, 77, 93syl2anc 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
) )
9681adantr 274 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  k  e.  A )  ->  ( G `  1 )  e.  RR )
9753sselda 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 ) ) )
9933, 98syl 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
) ) )
10199, 100syl 14 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  `' G : A --> ( 1 ... ( `  A
) ) )
102101ffvelrnda 5555 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  k  e.  A )  ->  ( `' G `  k )  e.  ( 1 ... ( `  A )
) )
103 elfznn 9846 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( `' G `  k )  e.  ( 1 ... ( `  A )
)  ->  ( `' G `  k )  e.  NN )
104102, 103syl 14 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  k  e.  A )  ->  ( `' G `  k )  e.  NN )
105104nnge1d 8775 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  k  e.  A )  ->  1  <_  ( `' G `  k ) )
10631adantr 274 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  k  e.  A )  ->  G  Isom  <  ,  <  (
( 1 ... ( `  A ) ) ,  A ) )
10750adantr 274 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  k  e.  A )  ->  (
1 ... ( `  A
) )  C_  RR* )
10854adantr 274 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  k  e.  A )  ->  A  C_ 
RR* )
10939adantr 274 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  k  e.  A )  ->  1  e.  ( 1 ... ( `  A ) ) )
110 leisorel 10592 . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
111106, 107, 108, 109, 102, 110syl122anc 1225 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  k  e.  A )  ->  (
1  <_  ( `' G `  k )  <->  ( G `  1 )  <_  ( G `  ( `' G `  k ) ) ) )
112105, 111mpbid 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 )
11433, 113sylan 281 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  k  e.  A )  ->  ( G `  ( `' G `  k )
)  =  k )
115112, 114breqtrd 3954 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  k  e.  A )  ->  ( G `  1 )  <_  k )
11696, 97, 115lensymd 7896 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  k  e.  A )  ->  -.  k  <  ( G ` 
1 ) )
117116ex 114 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( k  e.  A  ->  -.  k  <  ( G `  1 )
) )
118117con2d 613 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( k  <  ( G `  1 )  ->  -.  k  e.  A
) )
11995, 118syl5 32 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( k  e.  ZZ  /\  M  <_ 
k  /\  k  <  ( G `  1 ) )  ->  -.  k  e.  A ) )
12094, 119sylbid 149 . . . . . . . . . . . 12  |-  ( ph  ->  ( k  e.  ( M ... ( ( G `  1 )  -  1 ) )  ->  -.  k  e.  A ) )
121120imp 123 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ( M ... ( ( G `  1 )  -  1 ) ) )  ->  -.  k  e.  A )
12290, 121eldifd 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 )
124122, 123syldan 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 )
12628, 29, 41, 75, 124, 71, 125seq3id 10293 . . . . . . . 8  |-  ( ph  ->  (  seq M ( 
.+  ,  F )  |`  ( ZZ>= `  ( G `  1 ) ) )  =  seq ( G `  1 )
(  .+  ,  F
) )
127126fveq1d 5423 . . . . . . 7  |-  ( ph  ->  ( (  seq M
(  .+  ,  F
)  |`  ( ZZ>= `  ( G `  1 )
) ) `  ( G `  1 )
)  =  (  seq ( G `  1
) (  .+  ,  F ) `  ( G `  1 )
) )
128 uzid 9352 . . . . . . . . 9  |-  ( ( G `  1 )  e.  ZZ  ->  ( G `  1 )  e.  ( ZZ>= `  ( G `  1 ) ) )
12977, 128syl 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 ) ) )
131129, 130syl 14 . . . . . . 7  |-  ( ph  ->  ( (  seq M
(  .+  ,  F
)  |`  ( ZZ>= `  ( G `  1 )
) ) `  ( G `  1 )
)  =  (  seq M (  .+  ,  F ) `  ( G `  1 )
) )
13292adantr 274 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ( ZZ>= `  ( G `  1 ) ) )  ->  M  e.  ZZ )
133 eluzelz 9347 . . . . . . . . . . . 12  |-  ( k  e.  ( ZZ>= `  ( G `  1 )
)  ->  k  e.  ZZ )
134133adantl 275 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ( ZZ>= `  ( G `  1 ) ) )  ->  k  e.  ZZ )
135132zred 9185 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  ( ZZ>= `  ( G `  1 ) ) )  ->  M  e.  RR )
13681adantr 274 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  ( ZZ>= `  ( G `  1 ) ) )  ->  ( G `  1 )  e.  RR )
137134zred 9185 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  ( ZZ>= `  ( G `  1 ) ) )  ->  k  e.  RR )
138 eluzle 9350 . . . . . . . . . . . . . 14  |-  ( ( G `  1 )  e.  ( ZZ>= `  M
)  ->  M  <_  ( G `  1 ) )
13941, 138syl 14 . . . . . . . . . . . . 13  |-  ( ph  ->  M  <_  ( G `  1 ) )
140139adantr 274 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  ( ZZ>= `  ( G `  1 ) ) )  ->  M  <_  ( G `  1 ) )
141 eluzle 9350 . . . . . . . . . . . . 13  |-  ( k  e.  ( ZZ>= `  ( G `  1 )
)  ->  ( G `  1 )  <_ 
k )
142141adantl 275 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  ( ZZ>= `  ( G `  1 ) ) )  ->  ( G `  1 )  <_ 
k )
143135, 136, 137, 140, 142letrd 7898 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ( ZZ>= `  ( G `  1 ) ) )  ->  M  <_  k )
144 eluz2 9344 . . . . . . . . . . 11  |-  ( k  e.  ( ZZ>= `  M
)  <->  ( M  e.  ZZ  /\  k  e.  ZZ  /\  M  <_ 
k ) )
145132, 134, 143, 144syl3anbrc 1165 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  ( ZZ>= `  ( G `  1 ) ) )  ->  k  e.  ( ZZ>= `  M )
)
146145, 71syldan 280 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( ZZ>= `  ( G `  1 ) ) )  ->  ( F `  k )  e.  S
)
14777, 146, 125seq3-1 10245 . . . . . . . 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 )
) )
150148, 149eqeq12d 2154 . . . . . . . . . . 11  |-  ( n  =  1  ->  (
( H `  n
)  =  ( F `
 ( G `  n ) )  <->  ( H `  1 )  =  ( F `  ( G `  1 )
) ) )
151150imbi2d 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 ) ) )
153152expcom 115 . . . . . . . . . 10  |-  ( n  e.  ( 1 ... ( `  A )
)  ->  ( ph  ->  ( H `  n
)  =  ( F `
 ( G `  n ) ) ) )
154151, 153vtoclga 2752 . . . . . . . . 9  |-  ( 1  e.  ( 1 ... ( `  A )
)  ->  ( ph  ->  ( H `  1
)  =  ( F `
 ( G ` 
1 ) ) ) )
15539, 154mpcom 36 . . . . . . . 8  |-  ( ph  ->  ( H `  1
)  =  ( F `
 ( G ` 
1 ) ) )
156147, 155eqtr4d 2175 . . . . . . 7  |-  ( ph  ->  (  seq ( G `
 1 ) ( 
.+  ,  F ) `
 ( G ` 
1 ) )  =  ( H `  1
) )
157127, 131, 1563eqtr3d 2180 . . . . . 6  |-  ( ph  ->  (  seq M ( 
.+  ,  F ) `
 ( G ` 
1 ) )  =  ( H `  1
) )
158 1zzd 9093 . . . . . . 7  |-  ( ph  ->  1  e.  ZZ )
159 seqcoll.hcl . . . . . . 7  |-  ( (
ph  /\  k  e.  ( ZZ>= `  1 )
)  ->  ( H `  k )  e.  S
)
160158, 159, 125seq3-1 10245 . . . . . 6  |-  ( ph  ->  (  seq 1 ( 
.+  ,  H ) `
 1 )  =  ( H `  1
) )
161157, 160eqtr4d 2175 . . . . 5  |-  ( ph  ->  (  seq M ( 
.+  ,  F ) `
 ( G ` 
1 ) )  =  (  seq 1 ( 
.+  ,  H ) `
 1 ) )
162161a1d 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 9373 . . . . . . . . . . 11  |-  NN  =  ( ZZ>= `  1 )
165163, 164eleqtrdi 2232 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
m  +  1 )  e.  ( 1 ... ( `  A )
) )  ->  m  e.  ( ZZ>= `  1 )
)
166 nnz 9085 . . . . . . . . . . . 12  |-  ( m  e.  NN  ->  m  e.  ZZ )
167166ad2antlr 480 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
m  +  1 )  e.  ( 1 ... ( `  A )
) )  ->  m  e.  ZZ )
168 elfzuz3 9815 . . . . . . . . . . . 12  |-  ( ( m  +  1 )  e.  ( 1 ... ( `  A )
)  ->  ( `  A
)  e.  ( ZZ>= `  ( m  +  1
) ) )
169168adantl 275 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
m  +  1 )  e.  ( 1 ... ( `  A )
) )  ->  ( `  A )  e.  (
ZZ>= `  ( m  + 
1 ) ) )
170 peano2uzr 9392 . . . . . . . . . . 11  |-  ( ( m  e.  ZZ  /\  ( `  A )  e.  ( ZZ>= `  ( m  +  1 ) ) )  ->  ( `  A
)  e.  ( ZZ>= `  m ) )
171167, 169, 170syl2anc 408 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
m  +  1 )  e.  ( 1 ... ( `  A )
) )  ->  ( `  A )  e.  (
ZZ>= `  m ) )
172 elfzuzb 9812 . . . . . . . . . 10  |-  ( m  e.  ( 1 ... ( `  A )
)  <->  ( m  e.  ( ZZ>= `  1 )  /\  ( `  A )  e.  ( ZZ>= `  m )
) )
173165, 171, 172sylanbrc 413 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
m  +  1 )  e.  ( 1 ... ( `  A )
) )  ->  m  e.  ( 1 ... ( `  A ) ) )
174173ex 114 . . . . . . . 8  |-  ( (
ph  /\  m  e.  NN )  ->  ( ( m  +  1 )  e.  ( 1 ... ( `  A )
)  ->  m  e.  ( 1 ... ( `  A ) ) ) )
175174imim1d 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 )
179177, 178sylan 281 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  m  e.  NN )  /\  ( m  +  1 )  e.  ( 1 ... ( `  A
) ) )  /\  k  e.  S )  ->  ( k  .+  Z
)  =  k )
18030ad2antrr 479 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
m  +  1 )  e.  ( 1 ... ( `  A )
) )  ->  A  C_  ( ZZ>= `  M )
)
18135ad2antrr 479 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
m  +  1 )  e.  ( 1 ... ( `  A )
) )  ->  G : ( 1 ... ( `  A )
) --> A )
182181, 173ffvelrnd 5556 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
m  +  1 )  e.  ( 1 ... ( `  A )
) )  ->  ( G `  m )  e.  A )
183180, 182sseldd 3098 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
m  +  1 )  e.  ( 1 ... ( `  A )
) )  ->  ( G `  m )  e.  ( ZZ>= `  M )
)
184 nnre 8739 . . . . . . . . . . . . . . . . . . 19  |-  ( m  e.  NN  ->  m  e.  RR )
185184ad2antlr 480 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
m  +  1 )  e.  ( 1 ... ( `  A )
) )  ->  m  e.  RR )
186185ltp1d 8700 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
m  +  1 )  e.  ( 1 ... ( `  A )
) )  ->  m  <  ( m  +  1 ) )
18731ad2antrr 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 ) ) ) )
190187, 173, 188, 189syl12anc 1214 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
m  +  1 )  e.  ( 1 ... ( `  A )
) )  ->  (
m  <  ( m  +  1 )  <->  ( G `  m )  <  ( G `  ( m  +  1 ) ) ) )
191186, 190mpbid 146 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
m  +  1 )  e.  ( 1 ... ( `  A )
) )  ->  ( G `  m )  <  ( G `  (
m  +  1 ) ) )
192 eluzelz 9347 . . . . . . . . . . . . . . . . . 18  |-  ( ( G `  m )  e.  ( ZZ>= `  M
)  ->  ( G `  m )  e.  ZZ )
193183, 192syl 14 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
m  +  1 )  e.  ( 1 ... ( `  A )
) )  ->  ( G `  m )  e.  ZZ )
194181, 188ffvelrnd 5556 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
m  +  1 )  e.  ( 1 ... ( `  A )
) )  ->  ( G `  ( m  +  1 ) )  e.  A )
195180, 194sseldd 3098 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
m  +  1 )  e.  ( 1 ... ( `  A )
) )  ->  ( G `  ( m  +  1 ) )  e.  ( ZZ>= `  M
) )
196 eluzelz 9347 . . . . . . . . . . . . . . . . . 18  |-  ( ( G `  ( m  +  1 ) )  e.  ( ZZ>= `  M
)  ->  ( G `  ( m  +  1 ) )  e.  ZZ )
197195, 196syl 14 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
m  +  1 )  e.  ( 1 ... ( `  A )
) )  ->  ( G `  ( m  +  1 ) )  e.  ZZ )
198 zltlem1 9123 . . . . . . . . . . . . . . . . 17  |-  ( ( ( G `  m
)  e.  ZZ  /\  ( G `  ( m  +  1 ) )  e.  ZZ )  -> 
( ( G `  m )  <  ( G `  ( m  +  1 ) )  <-> 
( G `  m
)  <_  ( ( G `  ( m  +  1 ) )  -  1 ) ) )
199193, 197, 198syl2anc 408 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
m  +  1 )  e.  ( 1 ... ( `  A )
) )  ->  (
( G `  m
)  <  ( G `  ( m  +  1 ) )  <->  ( G `  m )  <_  (
( G `  (
m  +  1 ) )  -  1 ) ) )
200191, 199mpbid 146 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
m  +  1 )  e.  ( 1 ... ( `  A )
) )  ->  ( G `  m )  <_  ( ( G `  ( m  +  1
) )  -  1 ) )
201 peano2zm 9104 . . . . . . . . . . . . . . . . 17  |-  ( ( G `  ( m  +  1 ) )  e.  ZZ  ->  (
( G `  (
m  +  1 ) )  -  1 )  e.  ZZ )
202197, 201syl 14 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
m  +  1 )  e.  ( 1 ... ( `  A )
) )  ->  (
( G `  (
m  +  1 ) )  -  1 )  e.  ZZ )
203 eluz 9351 . . . . . . . . . . . . . . . 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 ) ) )
204193, 202, 203syl2anc 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 ) ) )
205200, 204mpbird 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 )
20792ad2antrr 479 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
m  +  1 )  e.  ( 1 ... ( `  A )
) )  ->  M  e.  ZZ )
208177, 71sylan 281 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  m  e.  NN )  /\  ( m  +  1 )  e.  ( 1 ... ( `  A
) ) )  /\  k  e.  ( ZZ>= `  M ) )  -> 
( F `  k
)  e.  S )
209177, 125sylan 281 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  m  e.  NN )  /\  ( m  +  1 )  e.  ( 1 ... ( `  A
) ) )  /\  ( k  e.  S  /\  n  e.  S
) )  ->  (
k  .+  n )  e.  S )
210206, 207, 208, 209seqf 10246 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
m  +  1 )  e.  ( 1 ... ( `  A )
) )  ->  seq M (  .+  ,  F ) : (
ZZ>= `  M ) --> S )
211210, 183ffvelrnd 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 9814 . . . . . . . . . . . . . . . . . 18  |-  ( k  e.  ( ( ( G `  m )  +  1 ) ... ( ( G `  ( m  +  1
) )  -  1 ) )  ->  k  e.  ( ZZ>= `  ( ( G `  m )  +  1 ) ) )
214 peano2uz 9390 . . . . . . . . . . . . . . . . . . 19  |-  ( ( G `  m )  e.  ( ZZ>= `  M
)  ->  ( ( G `  m )  +  1 )  e.  ( ZZ>= `  M )
)
215183, 214syl 14 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
m  +  1 )  e.  ( 1 ... ( `  A )
) )  ->  (
( G `  m
)  +  1 )  e.  ( ZZ>= `  M
) )
216 uztrn 9354 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  e.  ( ZZ>= `  ( ( G `  m )  +  1 ) )  /\  (
( G `  m
)  +  1 )  e.  ( ZZ>= `  M
) )  ->  k  e.  ( ZZ>= `  M )
)
217213, 215, 216syl2anr 288 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  m  e.  NN )  /\  ( m  +  1 )  e.  ( 1 ... ( `  A
) ) )  /\  k  e.  ( (
( G `  m
)  +  1 ) ... ( ( G `
 ( m  + 
1 ) )  - 
1 ) ) )  ->  k  e.  (
ZZ>= `  M ) )
218202zred 9185 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
m  +  1 )  e.  ( 1 ... ( `  A )
) )  ->  (
( G `  (
m  +  1 ) )  -  1 )  e.  RR )
219197zred 9185 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
m  +  1 )  e.  ( 1 ... ( `  A )
) )  ->  ( G `  ( m  +  1 ) )  e.  RR )
22082ad2antrr 479 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
m  +  1 )  e.  ( 1 ... ( `  A )
) )  ->  ( G `  ( `  A
) )  e.  RR )
221219lem1d 8703 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
m  +  1 )  e.  ( 1 ... ( `  A )
) )  ->  (
( G `  (
m  +  1 ) )  -  1 )  <_  ( G `  ( m  +  1
) ) )
222 elfzle2 9820 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( m  +  1 )  e.  ( 1 ... ( `  A )
)  ->  ( m  +  1 )  <_ 
( `  A ) )
223222adantl 275 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
m  +  1 )  e.  ( 1 ... ( `  A )
) )  ->  (
m  +  1 )  <_  ( `  A )
)
22450ad2antrr 479 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
m  +  1 )  e.  ( 1 ... ( `  A )
) )  ->  (
1 ... ( `  A
) )  C_  RR* )
22554ad2antrr 479 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
m  +  1 )  e.  ( 1 ... ( `  A )
) )  ->  A  C_ 
RR* )
22656ad2antrr 479 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
m  +  1 )  e.  ( 1 ... ( `  A )
) )  ->  ( `  A )  e.  ( 1 ... ( `  A
) ) )
227 leisorel 10592 . . . . . . . . . . . . . . . . . . . . . 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
) ) ) )
228187, 224, 225, 188, 226, 227syl122anc 1225 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
m  +  1 )  e.  ( 1 ... ( `  A )
) )  ->  (
( m  +  1 )  <_  ( `  A
)  <->  ( G `  ( m  +  1
) )  <_  ( G `  ( `  A
) ) ) )
229223, 228mpbid 146 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
m  +  1 )  e.  ( 1 ... ( `  A )
) )  ->  ( G `  ( m  +  1 ) )  <_  ( G `  ( `  A ) ) )
230218, 219, 220, 221, 229letrd 7898 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
m  +  1 )  e.  ( 1 ... ( `  A )
) )  ->  (
( G `  (
m  +  1 ) )  -  1 )  <_  ( G `  ( `  A ) ) )
23163ad2antrr 479 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
m  +  1 )  e.  ( 1 ... ( `  A )
) )  ->  ( G `  ( `  A
) )  e.  ZZ )
232 eluz 9351 . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
233202, 231, 232syl2anc 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 )
) ) )
234230, 233mpbird 166 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
m  +  1 )  e.  ( 1 ... ( `  A )
) )  ->  ( G `  ( `  A
) )  e.  (
ZZ>= `  ( ( G `
 ( m  + 
1 ) )  - 
1 ) ) )
235 elfzuz3 9815 . . . . . . . . . . . . . . . . . 18  |-  ( k  e.  ( ( ( G `  m )  +  1 ) ... ( ( G `  ( m  +  1
) )  -  1 ) )  ->  (
( G `  (
m  +  1 ) )  -  1 )  e.  ( ZZ>= `  k
) )
236 uztrn 9354 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( G `  ( `  A ) )  e.  ( ZZ>= `  ( ( G `  ( m  +  1 ) )  -  1 ) )  /\  ( ( G `
 ( m  + 
1 ) )  - 
1 )  e.  (
ZZ>= `  k ) )  ->  ( G `  ( `  A ) )  e.  ( ZZ>= `  k
) )
237234, 235, 236syl2an 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 9812 . . . . . . . . . . . . . . . . 17  |-  ( k  e.  ( M ... ( G `  ( `  A
) ) )  <->  ( k  e.  ( ZZ>= `  M )  /\  ( G `  ( `  A ) )  e.  ( ZZ>= `  k )
) )
239217, 237, 238sylanbrc 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
) ) ) )
240166ad2antlr 480 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
( m  +  1 )  e.  ( 1 ... ( `  A
) )  /\  k  e.  A ) )  ->  m  e.  ZZ )
241101ad2antrr 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 )
243241, 242ffvelrnd 5556 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
( m  +  1 )  e.  ( 1 ... ( `  A
) )  /\  k  e.  A ) )  -> 
( `' G `  k )  e.  ( 1 ... ( `  A
) ) )
244 elfzelz 9818 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( `' G `  k )  e.  ( 1 ... ( `  A )
)  ->  ( `' G `  k )  e.  ZZ )
245243, 244syl 14 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
( m  +  1 )  e.  ( 1 ... ( `  A
) )  /\  k  e.  A ) )  -> 
( `' G `  k )  e.  ZZ )
246 btwnnz 9157 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( m  e.  ZZ  /\  m  <  ( `' G `  k )  /\  ( `' G `  k )  <  ( m  + 
1 ) )  ->  -.  ( `' G `  k )  e.  ZZ )
2472463expib 1184 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( m  e.  ZZ  ->  (
( m  <  ( `' G `  k )  /\  ( `' G `  k )  <  (
m  +  1 ) )  ->  -.  ( `' G `  k )  e.  ZZ ) )
248247con2d 613 . . . . . . . . . . . . . . . . . . . . 21  |-  ( m  e.  ZZ  ->  (
( `' G `  k )  e.  ZZ  ->  -.  ( m  < 
( `' G `  k )  /\  ( `' G `  k )  <  ( m  + 
1 ) ) ) )
249240, 245, 248sylc 62 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
( m  +  1 )  e.  ( 1 ... ( `  A
) )  /\  k  e.  A ) )  ->  -.  ( m  <  ( `' G `  k )  /\  ( `' G `  k )  <  (
m  +  1 ) ) )
25031ad2antrr 479 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
( m  +  1 )  e.  ( 1 ... ( `  A
) )  /\  k  e.  A ) )  ->  G  Isom  <  ,  <  ( ( 1 ... ( `  A ) ) ,  A ) )
251173adantrr 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 ) ) ) )
253250, 251, 243, 252syl12anc 1214 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
( m  +  1 )  e.  ( 1 ... ( `  A
) )  /\  k  e.  A ) )  -> 
( m  <  ( `' G `  k )  <-> 
( G `  m
)  <  ( G `  ( `' G `  k ) ) ) )
25433ad2antrr 479 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
( m  +  1 )  e.  ( 1 ... ( `  A
) )  /\  k  e.  A ) )  ->  G : ( 1 ... ( `  A )
)
-1-1-onto-> A )
255254, 242, 113syl2anc 408 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
( m  +  1 )  e.  ( 1 ... ( `  A
) )  /\  k  e.  A ) )  -> 
( G `  ( `' G `  k ) )  =  k )
256255breq2d 3941 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
( m  +  1 )  e.  ( 1 ... ( `  A
) )  /\  k  e.  A ) )  -> 
( ( G `  m )  <  ( G `  ( `' G `  k )
)  <->  ( G `  m )  <  k
) )
257193adantrr 470 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
( m  +  1 )  e.  ( 1 ... ( `  A
) )  /\  k  e.  A ) )  -> 
( G `  m
)  e.  ZZ )
25830ad2antrr 479 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
( m  +  1 )  e.  ( 1 ... ( `  A
) )  /\  k  e.  A ) )  ->  A  C_  ( ZZ>= `  M
) )
259258, 242sseldd 3098 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
( m  +  1 )  e.  ( 1 ... ( `  A
) )  /\  k  e.  A ) )  -> 
k  e.  ( ZZ>= `  M ) )
260 eluzelz 9347 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( k  e.  ( ZZ>= `  M
)  ->  k  e.  ZZ )
261259, 260syl 14 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
( m  +  1 )  e.  ( 1 ... ( `  A
) )  /\  k  e.  A ) )  -> 
k  e.  ZZ )
262 zltp1le 9120 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( G `  m
)  e.  ZZ  /\  k  e.  ZZ )  ->  ( ( G `  m )  <  k  <->  ( ( G `  m
)  +  1 )  <_  k ) )
263257, 261, 262syl2anc 408 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
( m  +  1 )  e.  ( 1 ... ( `  A
) )  /\  k  e.  A ) )  -> 
( ( G `  m )  <  k  <->  ( ( G `  m
)  +  1 )  <_  k ) )
264253, 256, 2633bitrd 213 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
( m  +  1 )  e.  ( 1 ... ( `  A
) )  /\  k  e.  A ) )  -> 
( m  <  ( `' G `  k )  <-> 
( ( G `  m )  +  1 )  <_  k )
)
265188adantrr 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 ) ) ) )
267250, 243, 265, 266syl12anc 1214 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
( m  +  1 )  e.  ( 1 ... ( `  A
) )  /\  k  e.  A ) )  -> 
( ( `' G `  k )  <  (
m  +  1 )  <-> 
( G `  ( `' G `  k ) )  <  ( G `
 ( m  + 
1 ) ) ) )
268255breq1d 3939 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
( m  +  1 )  e.  ( 1 ... ( `  A
) )  /\  k  e.  A ) )  -> 
( ( G `  ( `' G `  k ) )  <  ( G `
 ( m  + 
1 ) )  <->  k  <  ( G `  ( m  +  1 ) ) ) )
269197adantrr 470 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
( m  +  1 )  e.  ( 1 ... ( `  A
) )  /\  k  e.  A ) )  -> 
( G `  (
m  +  1 ) )  e.  ZZ )
270 zltlem1 9123 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( k  e.  ZZ  /\  ( G `  ( m  +  1 ) )  e.  ZZ )  -> 
( k  <  ( G `  ( m  +  1 ) )  <-> 
k  <_  ( ( G `  ( m  +  1 ) )  -  1 ) ) )
271261, 269, 270syl2anc 408 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
( m  +  1 )  e.  ( 1 ... ( `  A
) )  /\  k  e.  A ) )  -> 
( k  <  ( G `  ( m  +  1 ) )  <-> 
k  <_  ( ( G `  ( m  +  1 ) )  -  1 ) ) )
272267, 268, 2713bitrd 213 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
( m  +  1 )  e.  ( 1 ... ( `  A
) )  /\  k  e.  A ) )  -> 
( ( `' G `  k )  <  (
m  +  1 )  <-> 
k  <_  ( ( G `  ( m  +  1 ) )  -  1 ) ) )
273264, 272anbi12d 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 ) ) ) )
274249, 273mtbid 661 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
( m  +  1 )  e.  ( 1 ... ( `  A
) )  /\  k  e.  A ) )  ->  -.  ( ( ( G `
 m )  +  1 )  <_  k  /\  k  <_  ( ( G `  ( m  +  1 ) )  -  1 ) ) )
275274expr 372 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
m  +  1 )  e.  ( 1 ... ( `  A )
) )  ->  (
k  e.  A  ->  -.  ( ( ( G `
 m )  +  1 )  <_  k  /\  k  <_  ( ( G `  ( m  +  1 ) )  -  1 ) ) ) )
276275con2d 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 9819 . . . . . . . . . . . . . . . . . 18  |-  ( k  e.  ( ( ( G `  m )  +  1 ) ... ( ( G `  ( m  +  1
) )  -  1 ) )  ->  (
( G `  m
)  +  1 )  <_  k )
278 elfzle2 9820 . . . . . . . . . . . . . . . . . 18  |-  ( k  e.  ( ( ( G `  m )  +  1 ) ... ( ( G `  ( m  +  1
) )  -  1 ) )  ->  k  <_  ( ( G `  ( m  +  1
) )  -  1 ) )
279277, 278jca 304 . . . . . . . . . . . . . . . . 17  |-  ( k  e.  ( ( ( G `  m )  +  1 ) ... ( ( G `  ( m  +  1
) )  -  1 ) )  ->  (
( ( G `  m )  +  1 )  <_  k  /\  k  <_  ( ( G `
 ( m  + 
1 ) )  - 
1 ) ) )
280276, 279impel 278 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  m  e.  NN )  /\  ( m  +  1 )  e.  ( 1 ... ( `  A
) ) )  /\  k  e.  ( (
( G `  m
)  +  1 ) ... ( ( G `
 ( m  + 
1 ) )  - 
1 ) ) )  ->  -.  k  e.  A )
281239, 280eldifd 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 ) )
282212, 281, 123syl2anc 408 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  m  e.  NN )  /\  ( m  +  1 )  e.  ( 1 ... ( `  A
) ) )  /\  k  e.  ( (
( G `  m
)  +  1 ) ... ( ( G `
 ( m  + 
1 ) )  - 
1 ) ) )  ->  ( F `  k )  =  Z )
283179, 183, 205, 211, 282, 208, 209seq3id2 10294 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
m  +  1 )  e.  ( 1 ... ( `  A )
) )  ->  (  seq M (  .+  ,  F ) `  ( G `  m )
)  =  (  seq M (  .+  ,  F ) `  (
( G `  (
m  +  1 ) )  -  1 ) ) )
284283oveq1d 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 ) ) ) )
287285, 286eqeq12d 2154 . . . . . . . . . . . . . . . . 17  |-  ( n  =  ( m  + 
1 )  ->  (
( H `  n
)  =  ( F `
 ( G `  n ) )  <->  ( H `  ( m  +  1 ) )  =  ( F `  ( G `
 ( m  + 
1 ) ) ) ) )
288287imbi2d 229 . . . . . . . . . . . . . . . 16  |-  ( n  =  ( m  + 
1 )  ->  (
( ph  ->  ( H `
 n )  =  ( F `  ( G `  n )
) )  <->  ( ph  ->  ( H `  (
m  +  1 ) )  =  ( F `
 ( G `  ( m  +  1
) ) ) ) ) )
289288, 153vtoclga 2752 . . . . . . . . . . . . . . 15  |-  ( ( m  +  1 )  e.  ( 1 ... ( `  A )
)  ->  ( ph  ->  ( H `  (
m  +  1 ) )  =  ( F `
 ( G `  ( m  +  1
) ) ) ) )
290289impcom 124 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( m  +  1 )  e.  ( 1 ... ( `  A ) ) )  ->  ( H `  ( m  +  1
) )  =  ( F `  ( G `
 ( m  + 
1 ) ) ) )
291290adantlr 468 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
m  +  1 )  e.  ( 1 ... ( `  A )
) )  ->  ( H `  ( m  +  1 ) )  =  ( F `  ( G `  ( m  +  1 ) ) ) )
292291oveq2d 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 ) ) ) ) )
293197zcnd 9186 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
m  +  1 )  e.  ( 1 ... ( `  A )
) )  ->  ( G `  ( m  +  1 ) )  e.  CC )
294 ax-1cn 7725 . . . . . . . . . . . . . . 15  |-  1  e.  CC
295 npcan 7983 . . . . . . . . . . . . . . 15  |-  ( ( ( G `  (
m  +  1 ) )  e.  CC  /\  1  e.  CC )  ->  ( ( ( G `
 ( m  + 
1 ) )  - 
1 )  +  1 )  =  ( G `
 ( m  + 
1 ) ) )
296293, 294, 295sylancl 409 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
m  +  1 )  e.  ( 1 ... ( `  A )
) )  ->  (
( ( G `  ( m  +  1
) )  -  1 )  +  1 )  =  ( G `  ( m  +  1
) ) )
297 uztrn 9354 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( G `  ( m  +  1
) )  -  1 )  e.  ( ZZ>= `  ( G `  m ) )  /\  ( G `
 m )  e.  ( ZZ>= `  M )
)  ->  ( ( G `  ( m  +  1 ) )  -  1 )  e.  ( ZZ>= `  M )
)
298205, 183, 297syl2anc 408 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
m  +  1 )  e.  ( 1 ... ( `  A )
) )  ->  (
( G `  (
m  +  1 ) )  -  1 )  e.  ( ZZ>= `  M
) )
299 eluzp1p1 9363 . . . . . . . . . . . . . . 15  |-  ( ( ( G `  (
m  +  1 ) )  -  1 )  e.  ( ZZ>= `  M
)  ->  ( (
( G `  (
m  +  1 ) )  -  1 )  +  1 )  e.  ( ZZ>= `  ( M  +  1 ) ) )
300298, 299syl 14 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
m  +  1 )  e.  ( 1 ... ( `  A )
) )  ->  (
( ( G `  ( m  +  1
) )  -  1 )  +  1 )  e.  ( ZZ>= `  ( M  +  1 ) ) )
301296, 300eqeltrrd 2217 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
m  +  1 )  e.  ( 1 ... ( `  A )
) )  ->  ( G `  ( m  +  1 ) )  e.  ( ZZ>= `  ( M  +  1 ) ) )
302207, 301, 208, 209seq3m1 10253 . . . . . . . . . . . 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
) ) ) ) )
303284, 292, 3023eqtr4rd 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 ) ) ) )
304177, 159sylan 281 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  m  e.  NN )  /\  ( m  +  1 )  e.  ( 1 ... ( `  A
) ) )  /\  k  e.  ( ZZ>= ` 
1 ) )  -> 
( H `  k
)  e.  S )
305165, 304, 209seq3p1 10247 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
m  +  1 )  e.  ( 1 ... ( `  A )
) )  ->  (  seq 1 (  .+  ,  H ) `  (
m  +  1 ) )  =  ( (  seq 1 (  .+  ,  H ) `  m
)  .+  ( H `  ( m  +  1 ) ) ) )
306303, 305eqeq12d 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 ) ) ) ) )
307176, 306syl5ibr 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 ) ) ) )
308307ex 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 ) ) ) ) )
309308a2d 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 ) ) ) ) )
310175, 309syld 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 ) ) ) ) )
311310expcom 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 ) ) ) ) ) )
312311a2d 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 ) ) ) ) ) )
3139, 15, 21, 27, 162, 312nnind 8748 . . 3  |-  ( N  e.  NN  ->  ( ph  ->  ( N  e.  ( 1 ... ( `  A ) )  -> 
(  seq M (  .+  ,  F ) `  ( G `  N )
)  =  (  seq 1 (  .+  ,  H ) `  N
) ) ) )
3143, 313mpcom 36 . 2  |-  ( ph  ->  ( N  e.  ( 1 ... ( `  A
) )  ->  (  seq M (  .+  ,  F ) `  ( G `  N )
)  =  (  seq 1 (  .+  ,  H ) `  N
) ) )
3151, 314mpd 13 1  |-  ( ph  ->  (  seq M ( 
.+  ,  F ) `
 ( G `  N ) )  =  (  seq 1 ( 
.+  ,  H ) `
 N ) )
Colors of variables: wff set class
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 7630   RRcr 7631   1c1 7633    + caddc 7635   RR*cxr 7811    < clt 7812    <_ cle 7813    - cmin 7945   NNcn 8732   ZZcz 9066   ZZ>=cuz 9338   ...cfz 9802    seqcseq 10230  ♯chash 10533
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 7723  ax-resscn 7724  ax-1cn 7725  ax-1re 7726  ax-icn 7727  ax-addcl 7728  ax-addrcl 7729  ax-mulcl 7730  ax-addcom 7732  ax-addass 7734  ax-distr 7736  ax-i2m1 7737  ax-0lt1 7738  ax-0id 7740  ax-rnegex 7741  ax-cnre 7743  ax-pre-ltirr 7744  ax-pre-ltwlin 7745  ax-pre-lttrn 7746  ax-pre-ltadd 7748
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 7814  df-mnf 7815  df-xr 7816  df-ltxr 7817  df-le 7818  df-sub 7947  df-neg 7948  df-inn 8733  df-n0 8990  df-z 9067  df-uz 9339  df-fz 9803  df-fzo 9932  df-seqfrec 10231
This theorem is referenced by:  summodclem2a  11162  prodmodclem2a  11357
  Copyright terms: Public domain W3C validator