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

Theorem seq3coll 10540
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 9789 . . . 4  |-  ( N  e.  ( 1 ... ( `  A )
)  ->  N  e.  NN )
31, 2syl 14 . . 3  |-  ( ph  ->  N  e.  NN )
4 eleq1 2180 . . . . . 6  |-  ( y  =  1  ->  (
y  e.  ( 1 ... ( `  A
) )  <->  1  e.  ( 1 ... ( `  A ) ) ) )
5 2fveq3 5394 . . . . . . 7  |-  ( y  =  1  ->  (  seq M (  .+  ,  F ) `  ( G `  y )
)  =  (  seq M (  .+  ,  F ) `  ( G `  1 )
) )
6 fveq2 5389 . . . . . . 7  |-  ( y  =  1  ->  (  seq 1 (  .+  ,  H ) `  y
)  =  (  seq 1 (  .+  ,  H ) `  1
) )
75, 6eqeq12d 2132 . . . . . 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 2180 . . . . . 6  |-  ( y  =  m  ->  (
y  e.  ( 1 ... ( `  A
) )  <->  m  e.  ( 1 ... ( `  A ) ) ) )
11 2fveq3 5394 . . . . . . 7  |-  ( y  =  m  ->  (  seq M (  .+  ,  F ) `  ( G `  y )
)  =  (  seq M (  .+  ,  F ) `  ( G `  m )
) )
12 fveq2 5389 . . . . . . 7  |-  ( y  =  m  ->  (  seq 1 (  .+  ,  H ) `  y
)  =  (  seq 1 (  .+  ,  H ) `  m
) )
1311, 12eqeq12d 2132 . . . . . 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 2180 . . . . . 6  |-  ( y  =  ( m  + 
1 )  ->  (
y  e.  ( 1 ... ( `  A
) )  <->  ( m  +  1 )  e.  ( 1 ... ( `  A ) ) ) )
17 2fveq3 5394 . . . . . . 7  |-  ( y  =  ( m  + 
1 )  ->  (  seq M (  .+  ,  F ) `  ( G `  y )
)  =  (  seq M (  .+  ,  F ) `  ( G `  ( m  +  1 ) ) ) )
18 fveq2 5389 . . . . . . 7  |-  ( y  =  ( m  + 
1 )  ->  (  seq 1 (  .+  ,  H ) `  y
)  =  (  seq 1 (  .+  ,  H ) `  (
m  +  1 ) ) )
1917, 18eqeq12d 2132 . . . . . 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 2180 . . . . . 6  |-  ( y  =  N  ->  (
y  e.  ( 1 ... ( `  A
) )  <->  N  e.  ( 1 ... ( `  A ) ) ) )
23 2fveq3 5394 . . . . . . 7  |-  ( y  =  N  ->  (  seq M (  .+  ,  F ) `  ( G `  y )
)  =  (  seq M (  .+  ,  F ) `  ( G `  N )
) )
24 fveq2 5389 . . . . . . 7  |-  ( y  =  N  ->  (  seq 1 (  .+  ,  H ) `  y
)  =  (  seq 1 (  .+  ,  H ) `  N
) )
2523, 24eqeq12d 2132 . . . . . 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 5676 . . . . . . . . . . . . 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 5335 . . . . . . . . . . . 12  |-  ( G : ( 1 ... ( `  A )
)
-1-1-onto-> A  ->  G : ( 1 ... ( `  A
) ) --> A )
3533, 34syl 14 . . . . . . . . . . 11  |-  ( ph  ->  G : ( 1 ... ( `  A
) ) --> A )
36 elfzuz2 9764 . . . . . . . . . . . . 13  |-  ( N  e.  ( 1 ... ( `  A )
)  ->  ( `  A
)  e.  ( ZZ>= ` 
1 ) )
371, 36syl 14 . . . . . . . . . . . 12  |-  ( ph  ->  ( `  A )  e.  ( ZZ>= `  1 )
)
38 eluzfz1 9766 . . . . . . . . . . . 12  |-  ( ( `  A )  e.  (
ZZ>= `  1 )  -> 
1  e.  ( 1 ... ( `  A
) ) )
3937, 38syl 14 . . . . . . . . . . 11  |-  ( ph  ->  1  e.  ( 1 ... ( `  A
) ) )
4035, 39ffvelrnd 5524 . . . . . . . . . 10  |-  ( ph  ->  ( G `  1
)  e.  A )
4130, 40sseldd 3068 . . . . . . . . 9  |-  ( ph  ->  ( G `  1
)  e.  ( ZZ>= `  M ) )
42 eluzle 9294 . . . . . . . . . . . . 13  |-  ( ( `  A )  e.  (
ZZ>= `  1 )  -> 
1  <_  ( `  A
) )
4337, 42syl 14 . . . . . . . . . . . 12  |-  ( ph  ->  1  <_  ( `  A
) )
44 elfzelz 9761 . . . . . . . . . . . . . . . . 17  |-  ( k  e.  ( 1 ... ( `  A )
)  ->  k  e.  ZZ )
4544ssriv 3071 . . . . . . . . . . . . . . . 16  |-  ( 1 ... ( `  A
) )  C_  ZZ
46 zssre 9019 . . . . . . . . . . . . . . . 16  |-  ZZ  C_  RR
4745, 46sstri 3076 . . . . . . . . . . . . . . 15  |-  ( 1 ... ( `  A
) )  C_  RR
4847a1i 9 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 1 ... ( `  A ) )  C_  RR )
49 ressxr 7777 . . . . . . . . . . . . . 14  |-  RR  C_  RR*
5048, 49sstrdi 3079 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 1 ... ( `  A ) )  C_  RR* )
51 eluzelre 9292 . . . . . . . . . . . . . . . 16  |-  ( k  e.  ( ZZ>= `  M
)  ->  k  e.  RR )
5251ssriv 3071 . . . . . . . . . . . . . . 15  |-  ( ZZ>= `  M )  C_  RR
5330, 52sstrdi 3079 . . . . . . . . . . . . . 14  |-  ( ph  ->  A  C_  RR )
5453, 49sstrdi 3079 . . . . . . . . . . . . 13  |-  ( ph  ->  A  C_  RR* )
55 eluzfz2 9767 . . . . . . . . . . . . . 14  |-  ( ( `  A )  e.  (
ZZ>= `  1 )  -> 
( `  A )  e.  ( 1 ... ( `  A ) ) )
5637, 55syl 14 . . . . . . . . . . . . 13  |-  ( ph  ->  ( `  A )  e.  ( 1 ... ( `  A ) ) )
57 leisorel 10535 . . . . . . . . . . . . 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 1210 . . . . . . . . . . . 12  |-  ( ph  ->  ( 1  <_  ( `  A )  <->  ( G `  1 )  <_ 
( G `  ( `  A ) ) ) )
5943, 58mpbid 146 . . . . . . . . . . 11  |-  ( ph  ->  ( G `  1
)  <_  ( G `  ( `  A )
) )
6035, 56ffvelrnd 5524 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( G `  ( `  A ) )  e.  A )
6130, 60sseldd 3068 . . . . . . . . . . . . 13  |-  ( ph  ->  ( G `  ( `  A ) )  e.  ( ZZ>= `  M )
)
62 eluzelz 9291 . . . . . . . . . . . . 13  |-  ( ( G `  ( `  A
) )  e.  (
ZZ>= `  M )  -> 
( G `  ( `  A ) )  e.  ZZ )
6361, 62syl 14 . . . . . . . . . . . 12  |-  ( ph  ->  ( G `  ( `  A ) )  e.  ZZ )
64 elfz5 9753 . . . . . . . . . . . 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 5389 . . . . . . . . . . . . 13  |-  ( k  =  ( G ` 
1 )  ->  ( F `  k )  =  ( F `  ( G `  1 ) ) )
6867eleq1d 2186 . . . . . . . . . . . 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 9757 . . . . . . . . . . . 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 2726 . . . . . . . . . 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 9291 . . . . . . . . . . . . . . . . . 18  |-  ( ( G `  1 )  e.  ( ZZ>= `  M
)  ->  ( G `  1 )  e.  ZZ )
7741, 76syl 14 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( G `  1
)  e.  ZZ )
78 peano2zm 9050 . . . . . . . . . . . . . . . . 17  |-  ( ( G `  1 )  e.  ZZ  ->  (
( G `  1
)  -  1 )  e.  ZZ )
7977, 78syl 14 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( G ` 
1 )  -  1 )  e.  ZZ )
8079zred 9131 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( G ` 
1 )  -  1 )  e.  RR )
8177zred 9131 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( G `  1
)  e.  RR )
8263zred 9131 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( G `  ( `  A ) )  e.  RR )
8381lem1d 8655 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( G ` 
1 )  -  1 )  <_  ( G `  1 ) )
8480, 81, 82, 83, 59letrd 7854 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( G ` 
1 )  -  1 )  <_  ( G `  ( `  A )
) )
85 eluz 9295 . . . . . . . . . . . . . . 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 9799 . . . . . . . . . . . . 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 3067 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ( M ... ( ( G `  1 )  -  1 ) ) )  ->  k  e.  ( M ... ( G `
 ( `  A
) ) ) )
91 eluzel2 9287 . . . . . . . . . . . . . . 15  |-  ( ( G `  1 )  e.  ( ZZ>= `  M
)  ->  M  e.  ZZ )
9241, 91syl 14 . . . . . . . . . . . . . 14  |-  ( ph  ->  M  e.  ZZ )
93 elfzm11 9826 . . . . . . . . . . . . . 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 968 . . . . . . . . . . . . . 14  |-  ( ( k  e.  ZZ  /\  M  <_  k  /\  k  <  ( G `  1
) )  ->  k  <  ( G `  1
) )
9681adantr 274 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  k  e.  A )  ->  ( G `  1 )  e.  RR )
9753sselda 3067 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  k  e.  A )  ->  k  e.  RR )
98 f1ocnv 5348 . . . . . . . . . . . . . . . . . . . . . . . 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 5335 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( `' G : A -1-1-onto-> ( 1 ... ( `  A
) )  ->  `' G : A --> ( 1 ... ( `  A
) ) )
10199, 100syl 14 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  `' G : A --> ( 1 ... ( `  A
) ) )
102101ffvelrnda 5523 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  k  e.  A )  ->  ( `' G `  k )  e.  ( 1 ... ( `  A )
) )
103 elfznn 9789 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( `' G `  k )  e.  ( 1 ... ( `  A )
)  ->  ( `' G `  k )  e.  NN )
104102, 103syl 14 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  k  e.  A )  ->  ( `' G `  k )  e.  NN )
105104nnge1d 8727 . . . . . . . . . . . . . . . . . . 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 10535 . . . . . . . . . . . . . . . . . . . 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 1210 . . . . . . . . . . . . . . . . . . 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 5647 . . . . . . . . . . . . . . . . . . 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 3924 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  k  e.  A )  ->  ( G `  1 )  <_  k )
11696, 97, 115lensymd 7852 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  k  e.  A )  ->  -.  k  <  ( G ` 
1 ) )
117116ex 114 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( k  e.  A  ->  -.  k  <  ( G `  1 )
) )
118117con2d 598 . . . . . . . . . . . . . 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 3051 . . . . . . . . . 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 10236 . . . . . . . 8  |-  ( ph  ->  (  seq M ( 
.+  ,  F )  |`  ( ZZ>= `  ( G `  1 ) ) )  =  seq ( G `  1 )
(  .+  ,  F
) )
127126fveq1d 5391 . . . . . . 7  |-  ( ph  ->  ( (  seq M
(  .+  ,  F
)  |`  ( ZZ>= `  ( G `  1 )
) ) `  ( G `  1 )
)  =  (  seq ( G `  1
) (  .+  ,  F ) `  ( G `  1 )
) )
128 uzid 9296 . . . . . . . . 9  |-  ( ( G `  1 )  e.  ZZ  ->  ( G `  1 )  e.  ( ZZ>= `  ( G `  1 ) ) )
12977, 128syl 14 . . . . . . . 8  |-  ( ph  ->  ( G `  1
)  e.  ( ZZ>= `  ( G `  1 ) ) )
130 fvres 5413 . . . . . . . 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 9291 . . . . . . . . . . . 12  |-  ( k  e.  ( ZZ>= `  ( G `  1 )
)  ->  k  e.  ZZ )
134133adantl 275 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ( ZZ>= `  ( G `  1 ) ) )  ->  k  e.  ZZ )
135132zred 9131 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  ( ZZ>= `  ( G `  1 ) ) )  ->  M  e.  RR )
13681adantr 274 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  ( ZZ>= `  ( G `  1 ) ) )  ->  ( G `  1 )  e.  RR )
137134zred 9131 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  ( ZZ>= `  ( G `  1 ) ) )  ->  k  e.  RR )
138 eluzle 9294 . . . . . . . . . . . . . 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 9294 . . . . . . . . . . . . 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 7854 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ( ZZ>= `  ( G `  1 ) ) )  ->  M  <_  k )
144 eluz2 9288 . . . . . . . . . . 11  |-  ( k  e.  ( ZZ>= `  M
)  <->  ( M  e.  ZZ  /\  k  e.  ZZ  /\  M  <_ 
k ) )
145132, 134, 143, 144syl3anbrc 1150 . . . . . . . . . 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 10188 . . . . . . . 8  |-  ( ph  ->  (  seq ( G `
 1 ) ( 
.+  ,  F ) `
 ( G ` 
1 ) )  =  ( F `  ( G `  1 )
) )
148 fveq2 5389 . . . . . . . . . . . 12  |-  ( n  =  1  ->  ( H `  n )  =  ( H ` 
1 ) )
149 2fveq3 5394 . . . . . . . . . . . 12  |-  ( n  =  1  ->  ( F `  ( G `  n ) )  =  ( F `  ( G `  1 )
) )
150148, 149eqeq12d 2132 . . . . . . . . . . 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 2726 . . . . . . . . 9  |-  ( 1  e.  ( 1 ... ( `  A )
)  ->  ( ph  ->  ( H `  1
)  =  ( F `
 ( G ` 
1 ) ) ) )
15539, 154mpcom 36 . . . . . . . 8  |-  ( ph  ->  ( H `  1
)  =  ( F `
 ( G ` 
1 ) ) )
156147, 155eqtr4d 2153 . . . . . . 7  |-  ( ph  ->  (  seq ( G `
 1 ) ( 
.+  ,  F ) `
 ( G ` 
1 ) )  =  ( H `  1
) )
157127, 131, 1563eqtr3d 2158 . . . . . 6  |-  ( ph  ->  (  seq M ( 
.+  ,  F ) `
 ( G ` 
1 ) )  =  ( H `  1
) )
158 1zzd 9039 . . . . . . 7  |-  ( ph  ->  1  e.  ZZ )
159 seqcoll.hcl . . . . . . 7  |-  ( (
ph  /\  k  e.  ( ZZ>= `  1 )
)  ->  ( H `  k )  e.  S
)
160158, 159, 125seq3-1 10188 . . . . . 6  |-  ( ph  ->  (  seq 1 ( 
.+  ,  H ) `
 1 )  =  ( H `  1
) )
161157, 160eqtr4d 2153 . . . . 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 504 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
m  +  1 )  e.  ( 1 ... ( `  A )
) )  ->  m  e.  NN )
164 nnuz 9317 . . . . . . . . . . 11  |-  NN  =  ( ZZ>= `  1 )
165163, 164eleqtrdi 2210 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
m  +  1 )  e.  ( 1 ... ( `  A )
) )  ->  m  e.  ( ZZ>= `  1 )
)
166 nnz 9031 . . . . . . . . . . . 12  |-  ( m  e.  NN  ->  m  e.  ZZ )
167166ad2antlr 480 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
m  +  1 )  e.  ( 1 ... ( `  A )
) )  ->  m  e.  ZZ )
168 elfzuz3 9758 . . . . . . . . . . . 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 9336 . . . . . . . . . . 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 9755 . . . . . . . . . 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 5749 . . . . . . . . . 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 503 . . . . . . . . . . . . . . 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 5524 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
m  +  1 )  e.  ( 1 ... ( `  A )
) )  ->  ( G `  m )  e.  A )
183180, 182sseldd 3068 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
m  +  1 )  e.  ( 1 ... ( `  A )
) )  ->  ( G `  m )  e.  ( ZZ>= `  M )
)
184 nnre 8691 . . . . . . . . . . . . . . . . . . 19  |-  ( m  e.  NN  ->  m  e.  RR )
185184ad2antlr 480 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
m  +  1 )  e.  ( 1 ... ( `  A )
) )  ->  m  e.  RR )
186185ltp1d 8652 . . . . . . . . . . . . . . . . 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 5677 . . . . . . . . . . . . . . . . . 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 1199 . . . . . . . . . . . . . . . . 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 9291 . . . . . . . . . . . . . . . . . 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 5524 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
m  +  1 )  e.  ( 1 ... ( `  A )
) )  ->  ( G `  ( m  +  1 ) )  e.  A )
195180, 194sseldd 3068 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
m  +  1 )  e.  ( 1 ... ( `  A )
) )  ->  ( G `  ( m  +  1 ) )  e.  ( ZZ>= `  M
) )
196 eluzelz 9291 . . . . . . . . . . . . . . . . . 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 9069 . . . . . . . . . . . . . . . . 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 9050 . . . . . . . . . . . . . . . . 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 9295 . . . . . . . . . . . . . . . 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 2117 . . . . . . . . . . . . . . . 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 10189 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
m  +  1 )  e.  ( 1 ... ( `  A )
) )  ->  seq M (  .+  ,  F ) : (
ZZ>= `  M ) --> S )
211210, 183ffvelrnd 5524 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
m  +  1 )  e.  ( 1 ... ( `  A )
) )  ->  (  seq M (  .+  ,  F ) `  ( G `  m )
)  e.  S )
212 simplll 507 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  m  e.  NN )  /\  ( m  +  1 )  e.  ( 1 ... ( `  A
) ) )  /\  k  e.  ( (
( G `  m
)  +  1 ) ... ( ( G `
 ( m  + 
1 ) )  - 
1 ) ) )  ->  ph )
213 elfzuz 9757 . . . . . . . . . . . . . . . . . 18  |-  ( k  e.  ( ( ( G `  m )  +  1 ) ... ( ( G `  ( m  +  1
) )  -  1 ) )  ->  k  e.  ( ZZ>= `  ( ( G `  m )  +  1 ) ) )
214 peano2uz 9334 . . . . . . . . . . . . . . . . . . 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 9298 . . . . . . . . . . . . . . . . . 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 9131 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
m  +  1 )  e.  ( 1 ... ( `  A )
) )  ->  (
( G `  (
m  +  1 ) )  -  1 )  e.  RR )
219197zred 9131 . . . . . . . . . . . . . . . . . . . 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 8655 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
m  +  1 )  e.  ( 1 ... ( `  A )
) )  ->  (
( G `  (
m  +  1 ) )  -  1 )  <_  ( G `  ( m  +  1
) ) )
222 elfzle2 9763 . . . . . . . . . . . . . . . . . . . . . 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 10535 . . . . . . . . . . . . . . . . . . . . . 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 1210 . . . . . . . . . . . . . . . . . . . . 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 7854 . . . . . . . . . . . . . . . . . . 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 9295 . . . . . . . . . . . . . . . . . . . 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 9758 . . . . . . . . . . . . . . . . . 18  |-  ( k  e.  ( ( ( G `  m )  +  1 ) ... ( ( G `  ( m  +  1
) )  -  1 ) )  ->  (
( G `  (
m  +  1 ) )  -  1 )  e.  ( ZZ>= `  k
) )
236 uztrn 9298 . . . . . . . . . . . . . . . . . 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 9755 . . . . . . . . . . . . . . . . 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 506 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
( m  +  1 )  e.  ( 1 ... ( `  A
) )  /\  k  e.  A ) )  -> 
k  e.  A )
243241, 242ffvelrnd 5524 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
( m  +  1 )  e.  ( 1 ... ( `  A
) )  /\  k  e.  A ) )  -> 
( `' G `  k )  e.  ( 1 ... ( `  A
) ) )
244 elfzelz 9761 . . . . . . . . . . . . . . . . . . . . . 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 9103 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( m  e.  ZZ  /\  m  <  ( `' G `  k )  /\  ( `' G `  k )  <  ( m  + 
1 ) )  ->  -.  ( `' G `  k )  e.  ZZ )
2472463expib 1169 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( m  e.  ZZ  ->  (
( m  <  ( `' G `  k )  /\  ( `' G `  k )  <  (
m  +  1 ) )  ->  -.  ( `' G `  k )  e.  ZZ ) )
248247con2d 598 . . . . . . . . . . . . . . . . . . . . 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 5677 . . . . . . . . . . . . . . . . . . . . . . 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 1199 . . . . . . . . . . . . . . . . . . . . . 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 3911 . . . . . . . . . . . . . . . . . . . . . 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 3068 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
( m  +  1 )  e.  ( 1 ... ( `  A
) )  /\  k  e.  A ) )  -> 
k  e.  ( ZZ>= `  M ) )
260 eluzelz 9291 . . . . . . . . . . . . . . . . . . . . . . . 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 9066 . . . . . . . . . . . . . . . . . . . . . . 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 5677 . . . . . . . . . . . . . . . . . . . . . . 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 1199 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
( m  +  1 )  e.  ( 1 ... ( `  A
) )  /\  k  e.  A ) )  -> 
( ( `' G `  k )  <  (
m  +  1 )  <-> 
( G `  ( `' G `  k ) )  <  ( G `
 ( m  + 
1 ) ) ) )
268255breq1d 3909 . . . . . . . . . . . . . . . . . . . . . 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 9069 . . . . . . . . . . . . . . . . . . . . . . 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 646 . . . . . . . . . . . . . . . . . . 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 598 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
m  +  1 )  e.  ( 1 ... ( `  A )
) )  ->  (
( ( ( G `
 m )  +  1 )  <_  k  /\  k  <_  ( ( G `  ( m  +  1 ) )  -  1 ) )  ->  -.  k  e.  A ) )
277 elfzle1 9762 . . . . . . . . . . . . . . . . . 18  |-  ( k  e.  ( ( ( G `  m )  +  1 ) ... ( ( G `  ( m  +  1
) )  -  1 ) )  ->  (
( G `  m
)  +  1 )  <_  k )
278 elfzle2 9763 . . . . . . . . . . . . . . . . . 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 3051 . . . . . . . . . . . . . . 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 10237 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
m  +  1 )  e.  ( 1 ... ( `  A )
) )  ->  (  seq M (  .+  ,  F ) `  ( G `  m )
)  =  (  seq M (  .+  ,  F ) `  (
( G `  (
m  +  1 ) )  -  1 ) ) )
284283oveq1d 5757 . . . . . . . . . . . 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 5389 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  ( m  + 
1 )  ->  ( H `  n )  =  ( H `  ( m  +  1
) ) )
286 2fveq3 5394 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  ( m  + 
1 )  ->  ( F `  ( G `  n ) )  =  ( F `  ( G `  ( m  +  1 ) ) ) )
287285, 286eqeq12d 2132 . . . . . . . . . . . . . . . . 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 2726 . . . . . . . . . . . . . . 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 5758 . . . . . . . . . . . 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 9132 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
m  +  1 )  e.  ( 1 ... ( `  A )
) )  ->  ( G `  ( m  +  1 ) )  e.  CC )
294 ax-1cn 7681 . . . . . . . . . . . . . . 15  |-  1  e.  CC
295 npcan 7939 . . . . . . . . . . . . . . 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 9298 . . . . . . . . . . . . . . . 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 9307 . . . . . . . . . . . . . . 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 2195 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
m  +  1 )  e.  ( 1 ... ( `  A )
) )  ->  ( G `  ( m  +  1 ) )  e.  ( ZZ>= `  ( M  +  1 ) ) )
302207, 301, 208, 209seq3m1 10196 . . . . . . . . . . . 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 2161 . . . . . . . . . . 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 10190 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
m  +  1 )  e.  ( 1 ... ( `  A )
) )  ->  (  seq 1 (  .+  ,  H ) `  (
m  +  1 ) )  =  ( (  seq 1 (  .+  ,  H ) `  m
)  .+  ( H `  ( m  +  1 ) ) ) )
306303, 305eqeq12d 2132 . . . . . . . . . 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 8700 . . 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 947    = wceq 1316    e. wcel 1465    \ cdif 3038    C_ wss 3041   class class class wbr 3899   `'ccnv 4508    |` cres 4511   -->wf 5089   -1-1-onto->wf1o 5092   ` cfv 5093    Isom wiso 5094  (class class class)co 5742   CCcc 7586   RRcr 7587   1c1 7589    + caddc 7591   RR*cxr 7767    < clt 7768    <_ cle 7769    - cmin 7901   NNcn 8684   ZZcz 9012   ZZ>=cuz 9282   ...cfz 9745    seqcseq 10173  ♯chash 10476
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 588  ax-in2 589  ax-io 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-10 1468  ax-11 1469  ax-i12 1470  ax-bndl 1471  ax-4 1472  ax-13 1476  ax-14 1477  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099  ax-coll 4013  ax-sep 4016  ax-nul 4024  ax-pow 4068  ax-pr 4101  ax-un 4325  ax-setind 4422  ax-iinf 4472  ax-cnex 7679  ax-resscn 7680  ax-1cn 7681  ax-1re 7682  ax-icn 7683  ax-addcl 7684  ax-addrcl 7685  ax-mulcl 7686  ax-addcom 7688  ax-addass 7690  ax-distr 7692  ax-i2m1 7693  ax-0lt1 7694  ax-0id 7696  ax-rnegex 7697  ax-cnre 7699  ax-pre-ltirr 7700  ax-pre-ltwlin 7701  ax-pre-lttrn 7702  ax-pre-ltadd 7704
This theorem depends on definitions:  df-bi 116  df-3or 948  df-3an 949  df-tru 1319  df-fal 1322  df-nf 1422  df-sb 1721  df-eu 1980  df-mo 1981  df-clab 2104  df-cleq 2110  df-clel 2113  df-nfc 2247  df-ne 2286  df-nel 2381  df-ral 2398  df-rex 2399  df-reu 2400  df-rab 2402  df-v 2662  df-sbc 2883  df-csb 2976  df-dif 3043  df-un 3045  df-in 3047  df-ss 3054  df-nul 3334  df-pw 3482  df-sn 3503  df-pr 3504  df-op 3506  df-uni 3707  df-int 3742  df-iun 3785  df-br 3900  df-opab 3960  df-mpt 3961  df-tr 3997  df-id 4185  df-iord 4258  df-on 4260  df-ilim 4261  df-suc 4263  df-iom 4475  df-xp 4515  df-rel 4516  df-cnv 4517  df-co 4518  df-dm 4519  df-rn 4520  df-res 4521  df-ima 4522  df-iota 5058  df-fun 5095  df-fn 5096  df-f 5097  df-f1 5098  df-fo 5099  df-f1o 5100  df-fv 5101  df-isom 5102  df-riota 5698  df-ov 5745  df-oprab 5746  df-mpo 5747  df-1st 6006  df-2nd 6007  df-recs 6170  df-frec 6256  df-pnf 7770  df-mnf 7771  df-xr 7772  df-ltxr 7773  df-le 7774  df-sub 7903  df-neg 7904  df-inn 8685  df-n0 8936  df-z 9013  df-uz 9283  df-fz 9746  df-fzo 9875  df-seqfrec 10174
This theorem is referenced by:  summodclem2a  11105
  Copyright terms: Public domain W3C validator