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

Theorem fsum3 11111
Description: The value of a sum over a nonempty finite set. (Contributed by Jim Kingdon, 10-Oct-2022.)
Hypotheses
Ref Expression
fsum.1  |-  ( k  =  ( F `  n )  ->  B  =  C )
fsum.2  |-  ( ph  ->  M  e.  NN )
fsum.3  |-  ( ph  ->  F : ( 1 ... M ) -1-1-onto-> A )
fsum.4  |-  ( (
ph  /\  k  e.  A )  ->  B  e.  CC )
fsum.5  |-  ( (
ph  /\  n  e.  ( 1 ... M
) )  ->  ( G `  n )  =  C )
Assertion
Ref Expression
fsum3  |-  ( ph  -> 
sum_ k  e.  A  B  =  (  seq 1 (  +  , 
( n  e.  NN  |->  if ( n  <_  M ,  ( G `  n ) ,  0 ) ) ) `  M ) )
Distinct variable groups:    A, k, n    B, n    C, k    k, F, n    k, G, n   
k, M, n    ph, k, n
Allowed substitution hints:    B( k)    C( n)

Proof of Theorem fsum3
Dummy variables  f  i  j  m  u  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-sumdc 11078 . 2  |-  sum_ k  e.  A  B  =  ( iota x ( E. m  e.  ZZ  ( A  C_  ( ZZ>= `  m
)  /\  A. j  e.  ( ZZ>= `  m )DECID  j  e.  A  /\  seq m
(  +  ,  ( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) ) )  ~~>  x )  \/  E. m  e.  NN  E. f ( f : ( 1 ... m ) -1-1-onto-> A  /\  x  =  (  seq 1 (  +  , 
( n  e.  NN  |->  if ( n  <_  m ,  [_ ( f `  n )  /  k ]_ B ,  0 ) ) ) `  m
) ) ) )
2 nnuz 9317 . . . . 5  |-  NN  =  ( ZZ>= `  1 )
3 1zzd 9039 . . . . 5  |-  ( ph  ->  1  e.  ZZ )
4 elnnuz 9318 . . . . . 6  |-  ( x  e.  NN  <->  x  e.  ( ZZ>= `  1 )
)
52eqimss2i 3124 . . . . . . . . . 10  |-  ( ZZ>= ` 
1 )  C_  NN
65sseli 3063 . . . . . . . . 9  |-  ( x  e.  ( ZZ>= `  1
)  ->  x  e.  NN )
76adantl 275 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( ZZ>= `  1 )
)  ->  x  e.  NN )
8 fveq2 5389 . . . . . . . . . . 11  |-  ( n  =  x  ->  ( G `  n )  =  ( G `  x ) )
98eleq1d 2186 . . . . . . . . . 10  |-  ( n  =  x  ->  (
( G `  n
)  e.  CC  <->  ( G `  x )  e.  CC ) )
10 fsum.1 . . . . . . . . . . . 12  |-  ( k  =  ( F `  n )  ->  B  =  C )
11 fsum.2 . . . . . . . . . . . 12  |-  ( ph  ->  M  e.  NN )
12 fsum.3 . . . . . . . . . . . 12  |-  ( ph  ->  F : ( 1 ... M ) -1-1-onto-> A )
13 fsum.4 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  A )  ->  B  e.  CC )
14 fsum.5 . . . . . . . . . . . 12  |-  ( (
ph  /\  n  e.  ( 1 ... M
) )  ->  ( G `  n )  =  C )
1510, 11, 12, 13, 14fsumgcl 11110 . . . . . . . . . . 11  |-  ( ph  ->  A. n  e.  ( 1 ... M ) ( G `  n
)  e.  CC )
1615ad2antrr 479 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( ZZ>= `  1 )
)  /\  x  <_  M )  ->  A. n  e.  ( 1 ... M
) ( G `  n )  e.  CC )
17 1zzd 9039 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( ZZ>= `  1 )
)  /\  x  <_  M )  ->  1  e.  ZZ )
1811nnzd 9130 . . . . . . . . . . . . 13  |-  ( ph  ->  M  e.  ZZ )
1918ad2antrr 479 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( ZZ>= `  1 )
)  /\  x  <_  M )  ->  M  e.  ZZ )
20 eluzelz 9291 . . . . . . . . . . . . 13  |-  ( x  e.  ( ZZ>= `  1
)  ->  x  e.  ZZ )
2120ad2antlr 480 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( ZZ>= `  1 )
)  /\  x  <_  M )  ->  x  e.  ZZ )
2217, 19, 213jca 1146 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( ZZ>= `  1 )
)  /\  x  <_  M )  ->  ( 1  e.  ZZ  /\  M  e.  ZZ  /\  x  e.  ZZ ) )
23 eluzle 9294 . . . . . . . . . . . . 13  |-  ( x  e.  ( ZZ>= `  1
)  ->  1  <_  x )
2423ad2antlr 480 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( ZZ>= `  1 )
)  /\  x  <_  M )  ->  1  <_  x )
25 simpr 109 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( ZZ>= `  1 )
)  /\  x  <_  M )  ->  x  <_  M )
2624, 25jca 304 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( ZZ>= `  1 )
)  /\  x  <_  M )  ->  ( 1  <_  x  /\  x  <_  M ) )
27 elfz2 9752 . . . . . . . . . . 11  |-  ( x  e.  ( 1 ... M )  <->  ( (
1  e.  ZZ  /\  M  e.  ZZ  /\  x  e.  ZZ )  /\  (
1  <_  x  /\  x  <_  M ) ) )
2822, 26, 27sylanbrc 413 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( ZZ>= `  1 )
)  /\  x  <_  M )  ->  x  e.  ( 1 ... M
) )
299, 16, 28rspcdva 2768 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  ( ZZ>= `  1 )
)  /\  x  <_  M )  ->  ( G `  x )  e.  CC )
30 0cnd 7727 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  ( ZZ>= `  1 )
)  /\  -.  x  <_  M )  ->  0  e.  CC )
317nnzd 9130 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( ZZ>= `  1 )
)  ->  x  e.  ZZ )
3218adantr 274 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( ZZ>= `  1 )
)  ->  M  e.  ZZ )
33 zdcle 9085 . . . . . . . . . 10  |-  ( ( x  e.  ZZ  /\  M  e.  ZZ )  -> DECID  x  <_  M )
3431, 32, 33syl2anc 408 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( ZZ>= `  1 )
)  -> DECID  x  <_  M )
3529, 30, 34ifcldadc 3471 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( ZZ>= `  1 )
)  ->  if (
x  <_  M , 
( G `  x
) ,  0 )  e.  CC )
36 breq1 3902 . . . . . . . . . 10  |-  ( n  =  x  ->  (
n  <_  M  <->  x  <_  M ) )
3736, 8ifbieq1d 3464 . . . . . . . . 9  |-  ( n  =  x  ->  if ( n  <_  M , 
( G `  n
) ,  0 )  =  if ( x  <_  M ,  ( G `  x ) ,  0 ) )
38 eqid 2117 . . . . . . . . 9  |-  ( n  e.  NN  |->  if ( n  <_  M , 
( G `  n
) ,  0 ) )  =  ( n  e.  NN  |->  if ( n  <_  M , 
( G `  n
) ,  0 ) )
3937, 38fvmptg 5465 . . . . . . . 8  |-  ( ( x  e.  NN  /\  if ( x  <_  M ,  ( G `  x ) ,  0 )  e.  CC )  ->  ( ( n  e.  NN  |->  if ( n  <_  M , 
( G `  n
) ,  0 ) ) `  x )  =  if ( x  <_  M ,  ( G `  x ) ,  0 ) )
407, 35, 39syl2anc 408 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( ZZ>= `  1 )
)  ->  ( (
n  e.  NN  |->  if ( n  <_  M ,  ( G `  n ) ,  0 ) ) `  x
)  =  if ( x  <_  M , 
( G `  x
) ,  0 ) )
4140, 35eqeltrd 2194 . . . . . 6  |-  ( (
ph  /\  x  e.  ( ZZ>= `  1 )
)  ->  ( (
n  e.  NN  |->  if ( n  <_  M ,  ( G `  n ) ,  0 ) ) `  x
)  e.  CC )
424, 41sylan2b 285 . . . . 5  |-  ( (
ph  /\  x  e.  NN )  ->  ( ( n  e.  NN  |->  if ( n  <_  M ,  ( G `  n ) ,  0 ) ) `  x
)  e.  CC )
432, 3, 42serf 10202 . . . 4  |-  ( ph  ->  seq 1 (  +  ,  ( n  e.  NN  |->  if ( n  <_  M ,  ( G `  n ) ,  0 ) ) ) : NN --> CC )
4443, 11ffvelrnd 5524 . . 3  |-  ( ph  ->  (  seq 1 (  +  ,  ( n  e.  NN  |->  if ( n  <_  M , 
( G `  n
) ,  0 ) ) ) `  M
)  e.  CC )
4544adantr 274 . . . . . . . 8  |-  ( (
ph  /\  ( E. m  e.  ZZ  ( A  C_  ( ZZ>= `  m
)  /\  A. j  e.  ( ZZ>= `  m )DECID  j  e.  A  /\  seq m
(  +  ,  ( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) ) )  ~~>  x )  \/  E. m  e.  NN  E. f ( f : ( 1 ... m ) -1-1-onto-> A  /\  x  =  (  seq 1 (  +  , 
( n  e.  NN  |->  if ( n  <_  m ,  [_ ( f `  n )  /  k ]_ B ,  0 ) ) ) `  m
) ) ) )  ->  (  seq 1
(  +  ,  ( n  e.  NN  |->  if ( n  <_  M ,  ( G `  n ) ,  0 ) ) ) `  M )  e.  CC )
46 eleq1w 2178 . . . . . . . . . . . . 13  |-  ( n  =  j  ->  (
n  e.  A  <->  j  e.  A ) )
47 csbeq1 2978 . . . . . . . . . . . . 13  |-  ( n  =  j  ->  [_ n  /  k ]_ B  =  [_ j  /  k ]_ B )
4846, 47ifbieq1d 3464 . . . . . . . . . . . 12  |-  ( n  =  j  ->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 )  =  if ( j  e.  A ,  [_ j  /  k ]_ B ,  0 ) )
4948cbvmptv 3994 . . . . . . . . . . 11  |-  ( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) )  =  ( j  e.  ZZ  |->  if ( j  e.  A ,  [_ j  /  k ]_ B ,  0 ) )
5013ralrimiva 2482 . . . . . . . . . . . 12  |-  ( ph  ->  A. k  e.  A  B  e.  CC )
51 nfcsb1v 3005 . . . . . . . . . . . . . 14  |-  F/_ k [_ j  /  k ]_ B
5251nfel1 2269 . . . . . . . . . . . . 13  |-  F/ k
[_ j  /  k ]_ B  e.  CC
53 csbeq1a 2983 . . . . . . . . . . . . . 14  |-  ( k  =  j  ->  B  =  [_ j  /  k ]_ B )
5453eleq1d 2186 . . . . . . . . . . . . 13  |-  ( k  =  j  ->  ( B  e.  CC  <->  [_ j  / 
k ]_ B  e.  CC ) )
5552, 54rspc 2757 . . . . . . . . . . . 12  |-  ( j  e.  A  ->  ( A. k  e.  A  B  e.  CC  ->  [_ j  /  k ]_ B  e.  CC )
)
5650, 55mpan9 279 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  A )  ->  [_ j  /  k ]_ B  e.  CC )
57 breq1 3902 . . . . . . . . . . . . 13  |-  ( n  =  i  ->  (
n  <_  ( `  A
)  <->  i  <_  ( `  A ) ) )
58 fveq2 5389 . . . . . . . . . . . . . . 15  |-  ( n  =  i  ->  (
f `  n )  =  ( f `  i ) )
5958csbeq1d 2981 . . . . . . . . . . . . . 14  |-  ( n  =  i  ->  [_ (
f `  n )  /  k ]_ B  =  [_ ( f `  i )  /  k ]_ B )
60 csbco 2984 . . . . . . . . . . . . . 14  |-  [_ (
f `  i )  /  j ]_ [_ j  /  k ]_ B  =  [_ ( f `  i )  /  k ]_ B
6159, 60syl6eqr 2168 . . . . . . . . . . . . 13  |-  ( n  =  i  ->  [_ (
f `  n )  /  k ]_ B  =  [_ ( f `  i )  /  j ]_ [_ j  /  k ]_ B )
6257, 61ifbieq1d 3464 . . . . . . . . . . . 12  |-  ( n  =  i  ->  if ( n  <_  ( `  A
) ,  [_ (
f `  n )  /  k ]_ B ,  0 )  =  if ( i  <_ 
( `  A ) , 
[_ ( f `  i )  /  j ]_ [_ j  /  k ]_ B ,  0 ) )
6362cbvmptv 3994 . . . . . . . . . . 11  |-  ( n  e.  NN  |->  if ( n  <_  ( `  A
) ,  [_ (
f `  n )  /  k ]_ B ,  0 ) )  =  ( i  e.  NN  |->  if ( i  <_  ( `  A ) ,  [_ ( f `  i )  /  j ]_ [_ j  /  k ]_ B ,  0 ) )
6449, 56, 63, 63summodc 11107 . . . . . . . . . 10  |-  ( ph  ->  E* x ( E. m  e.  ZZ  ( A  C_  ( ZZ>= `  m
)  /\  A. u  e.  ( ZZ>= `  m )DECID  u  e.  A  /\  seq m
(  +  ,  ( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) ) )  ~~>  x )  \/  E. m  e.  NN  E. f ( f : ( 1 ... m ) -1-1-onto-> A  /\  x  =  (  seq 1 (  +  , 
( n  e.  NN  |->  if ( n  <_  ( `  A ) ,  [_ ( f `  n
)  /  k ]_ B ,  0 ) ) ) `  m
) ) ) )
65 eleq1w 2178 . . . . . . . . . . . . . . . 16  |-  ( u  =  j  ->  (
u  e.  A  <->  j  e.  A ) )
6665dcbid 808 . . . . . . . . . . . . . . 15  |-  ( u  =  j  ->  (DECID  u  e.  A  <-> DECID  j  e.  A )
)
6766cbvralv 2631 . . . . . . . . . . . . . 14  |-  ( A. u  e.  ( ZZ>= `  m )DECID  u  e.  A  <->  A. j  e.  ( ZZ>= `  m )DECID  j  e.  A )
68673anbi2i 1158 . . . . . . . . . . . . 13  |-  ( ( A  C_  ( ZZ>= `  m )  /\  A. u  e.  ( ZZ>= `  m )DECID  u  e.  A  /\  seq m (  +  , 
( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) ) )  ~~>  x )  <-> 
( A  C_  ( ZZ>=
`  m )  /\  A. j  e.  ( ZZ>= `  m )DECID  j  e.  A  /\  seq m (  +  , 
( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) ) )  ~~>  x ) )
6968rexbii 2419 . . . . . . . . . . . 12  |-  ( E. m  e.  ZZ  ( A  C_  ( ZZ>= `  m
)  /\  A. u  e.  ( ZZ>= `  m )DECID  u  e.  A  /\  seq m
(  +  ,  ( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) ) )  ~~>  x )  <->  E. m  e.  ZZ  ( A  C_  ( ZZ>= `  m )  /\  A. j  e.  ( ZZ>= `  m )DECID  j  e.  A  /\  seq m (  +  , 
( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) ) )  ~~>  x ) )
70 1zzd 9039 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( m  e.  NN  ->  1  e.  ZZ )
71 nnz 9031 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( m  e.  NN  ->  m  e.  ZZ )
7270, 71fzfigd 10159 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( m  e.  NN  ->  (
1 ... m )  e. 
Fin )
73 fihasheqf1oi 10489 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( 1 ... m
)  e.  Fin  /\  f : ( 1 ... m ) -1-1-onto-> A )  ->  ( `  ( 1 ... m
) )  =  ( `  A ) )
7472, 73sylan 281 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( m  e.  NN  /\  f : ( 1 ... m ) -1-1-onto-> A )  ->  ( `  ( 1 ... m
) )  =  ( `  A ) )
75 nnnn0 8942 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( m  e.  NN  ->  m  e.  NN0 )
7675adantr 274 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( m  e.  NN  /\  f : ( 1 ... m ) -1-1-onto-> A )  ->  m  e.  NN0 )
77 hashfz1 10484 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( m  e.  NN0  ->  ( `  (
1 ... m ) )  =  m )
7876, 77syl 14 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( m  e.  NN  /\  f : ( 1 ... m ) -1-1-onto-> A )  ->  ( `  ( 1 ... m
) )  =  m )
7974, 78eqtr3d 2152 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( m  e.  NN  /\  f : ( 1 ... m ) -1-1-onto-> A )  ->  ( `  A )  =  m )
8079breq2d 3911 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( m  e.  NN  /\  f : ( 1 ... m ) -1-1-onto-> A )  ->  (
n  <_  ( `  A
)  <->  n  <_  m ) )
8180ifbid 3463 . . . . . . . . . . . . . . . . . . 19  |-  ( ( m  e.  NN  /\  f : ( 1 ... m ) -1-1-onto-> A )  ->  if ( n  <_  ( `  A
) ,  [_ (
f `  n )  /  k ]_ B ,  0 )  =  if ( n  <_  m ,  [_ ( f `
 n )  / 
k ]_ B ,  0 ) )
8281mpteq2dv 3989 . . . . . . . . . . . . . . . . . 18  |-  ( ( m  e.  NN  /\  f : ( 1 ... m ) -1-1-onto-> A )  ->  (
n  e.  NN  |->  if ( n  <_  ( `  A ) ,  [_ ( f `  n
)  /  k ]_ B ,  0 ) )  =  ( n  e.  NN  |->  if ( n  <_  m ,  [_ ( f `  n
)  /  k ]_ B ,  0 ) ) )
8382seqeq3d 10181 . . . . . . . . . . . . . . . . 17  |-  ( ( m  e.  NN  /\  f : ( 1 ... m ) -1-1-onto-> A )  ->  seq 1 (  +  , 
( n  e.  NN  |->  if ( n  <_  ( `  A ) ,  [_ ( f `  n
)  /  k ]_ B ,  0 ) ) )  =  seq 1 (  +  , 
( n  e.  NN  |->  if ( n  <_  m ,  [_ ( f `  n )  /  k ]_ B ,  0 ) ) ) )
8483fveq1d 5391 . . . . . . . . . . . . . . . 16  |-  ( ( m  e.  NN  /\  f : ( 1 ... m ) -1-1-onto-> A )  ->  (  seq 1 (  +  , 
( n  e.  NN  |->  if ( n  <_  ( `  A ) ,  [_ ( f `  n
)  /  k ]_ B ,  0 ) ) ) `  m
)  =  (  seq 1 (  +  , 
( n  e.  NN  |->  if ( n  <_  m ,  [_ ( f `  n )  /  k ]_ B ,  0 ) ) ) `  m
) )
8584eqeq2d 2129 . . . . . . . . . . . . . . 15  |-  ( ( m  e.  NN  /\  f : ( 1 ... m ) -1-1-onto-> A )  ->  (
x  =  (  seq 1 (  +  , 
( n  e.  NN  |->  if ( n  <_  ( `  A ) ,  [_ ( f `  n
)  /  k ]_ B ,  0 ) ) ) `  m
)  <->  x  =  (  seq 1 (  +  , 
( n  e.  NN  |->  if ( n  <_  m ,  [_ ( f `  n )  /  k ]_ B ,  0 ) ) ) `  m
) ) )
8685pm5.32da 447 . . . . . . . . . . . . . 14  |-  ( m  e.  NN  ->  (
( f : ( 1 ... m ) -1-1-onto-> A  /\  x  =  (  seq 1 (  +  ,  ( n  e.  NN  |->  if ( n  <_  ( `  A ) ,  [_ ( f `  n )  /  k ]_ B ,  0 ) ) ) `  m
) )  <->  ( f : ( 1 ... m ) -1-1-onto-> A  /\  x  =  (  seq 1 (  +  ,  ( n  e.  NN  |->  if ( n  <_  m ,  [_ ( f `  n
)  /  k ]_ B ,  0 ) ) ) `  m
) ) ) )
8786exbidv 1781 . . . . . . . . . . . . 13  |-  ( m  e.  NN  ->  ( E. f ( f : ( 1 ... m
)
-1-1-onto-> A  /\  x  =  (  seq 1 (  +  ,  ( n  e.  NN  |->  if ( n  <_  ( `  A ) ,  [_ ( f `  n )  /  k ]_ B ,  0 ) ) ) `  m
) )  <->  E. f
( f : ( 1 ... m ) -1-1-onto-> A  /\  x  =  (  seq 1 (  +  ,  ( n  e.  NN  |->  if ( n  <_  m ,  [_ ( f `  n
)  /  k ]_ B ,  0 ) ) ) `  m
) ) ) )
8887rexbiia 2427 . . . . . . . . . . . 12  |-  ( E. m  e.  NN  E. f ( f : ( 1 ... m
)
-1-1-onto-> A  /\  x  =  (  seq 1 (  +  ,  ( n  e.  NN  |->  if ( n  <_  ( `  A ) ,  [_ ( f `  n )  /  k ]_ B ,  0 ) ) ) `  m
) )  <->  E. m  e.  NN  E. f ( f : ( 1 ... m ) -1-1-onto-> A  /\  x  =  (  seq 1 (  +  , 
( n  e.  NN  |->  if ( n  <_  m ,  [_ ( f `  n )  /  k ]_ B ,  0 ) ) ) `  m
) ) )
8969, 88orbi12i 738 . . . . . . . . . . 11  |-  ( ( E. m  e.  ZZ  ( A  C_  ( ZZ>= `  m )  /\  A. u  e.  ( ZZ>= `  m )DECID  u  e.  A  /\  seq m (  +  , 
( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) ) )  ~~>  x )  \/  E. m  e.  NN  E. f ( f : ( 1 ... m ) -1-1-onto-> A  /\  x  =  (  seq 1 (  +  , 
( n  e.  NN  |->  if ( n  <_  ( `  A ) ,  [_ ( f `  n
)  /  k ]_ B ,  0 ) ) ) `  m
) ) )  <->  ( E. m  e.  ZZ  ( A  C_  ( ZZ>= `  m
)  /\  A. j  e.  ( ZZ>= `  m )DECID  j  e.  A  /\  seq m
(  +  ,  ( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) ) )  ~~>  x )  \/  E. m  e.  NN  E. f ( f : ( 1 ... m ) -1-1-onto-> A  /\  x  =  (  seq 1 (  +  , 
( n  e.  NN  |->  if ( n  <_  m ,  [_ ( f `  n )  /  k ]_ B ,  0 ) ) ) `  m
) ) ) )
9089mobii 2014 . . . . . . . . . 10  |-  ( E* x ( E. m  e.  ZZ  ( A  C_  ( ZZ>= `  m )  /\  A. u  e.  (
ZZ>= `  m )DECID  u  e.  A  /\  seq m
(  +  ,  ( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) ) )  ~~>  x )  \/  E. m  e.  NN  E. f ( f : ( 1 ... m ) -1-1-onto-> A  /\  x  =  (  seq 1 (  +  , 
( n  e.  NN  |->  if ( n  <_  ( `  A ) ,  [_ ( f `  n
)  /  k ]_ B ,  0 ) ) ) `  m
) ) )  <->  E* x
( E. m  e.  ZZ  ( A  C_  ( ZZ>= `  m )  /\  A. j  e.  (
ZZ>= `  m )DECID  j  e.  A  /\  seq m
(  +  ,  ( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) ) )  ~~>  x )  \/  E. m  e.  NN  E. f ( f : ( 1 ... m ) -1-1-onto-> A  /\  x  =  (  seq 1 (  +  , 
( n  e.  NN  |->  if ( n  <_  m ,  [_ ( f `  n )  /  k ]_ B ,  0 ) ) ) `  m
) ) ) )
9164, 90sylib 121 . . . . . . . . 9  |-  ( ph  ->  E* x ( E. m  e.  ZZ  ( A  C_  ( ZZ>= `  m
)  /\  A. j  e.  ( ZZ>= `  m )DECID  j  e.  A  /\  seq m
(  +  ,  ( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) ) )  ~~>  x )  \/  E. m  e.  NN  E. f ( f : ( 1 ... m ) -1-1-onto-> A  /\  x  =  (  seq 1 (  +  , 
( n  e.  NN  |->  if ( n  <_  m ,  [_ ( f `  n )  /  k ]_ B ,  0 ) ) ) `  m
) ) ) )
9291adantr 274 . . . . . . . 8  |-  ( (
ph  /\  ( E. m  e.  ZZ  ( A  C_  ( ZZ>= `  m
)  /\  A. j  e.  ( ZZ>= `  m )DECID  j  e.  A  /\  seq m
(  +  ,  ( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) ) )  ~~>  x )  \/  E. m  e.  NN  E. f ( f : ( 1 ... m ) -1-1-onto-> A  /\  x  =  (  seq 1 (  +  , 
( n  e.  NN  |->  if ( n  <_  m ,  [_ ( f `  n )  /  k ]_ B ,  0 ) ) ) `  m
) ) ) )  ->  E* x ( E. m  e.  ZZ  ( A  C_  ( ZZ>= `  m )  /\  A. j  e.  ( ZZ>= `  m )DECID  j  e.  A  /\  seq m (  +  , 
( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) ) )  ~~>  x )  \/  E. m  e.  NN  E. f ( f : ( 1 ... m ) -1-1-onto-> A  /\  x  =  (  seq 1 (  +  , 
( n  e.  NN  |->  if ( n  <_  m ,  [_ ( f `  n )  /  k ]_ B ,  0 ) ) ) `  m
) ) ) )
93 simpr 109 . . . . . . . 8  |-  ( (
ph  /\  ( E. m  e.  ZZ  ( A  C_  ( ZZ>= `  m
)  /\  A. j  e.  ( ZZ>= `  m )DECID  j  e.  A  /\  seq m
(  +  ,  ( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) ) )  ~~>  x )  \/  E. m  e.  NN  E. f ( f : ( 1 ... m ) -1-1-onto-> A  /\  x  =  (  seq 1 (  +  , 
( n  e.  NN  |->  if ( n  <_  m ,  [_ ( f `  n )  /  k ]_ B ,  0 ) ) ) `  m
) ) ) )  ->  ( E. m  e.  ZZ  ( A  C_  ( ZZ>= `  m )  /\  A. j  e.  (
ZZ>= `  m )DECID  j  e.  A  /\  seq m
(  +  ,  ( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) ) )  ~~>  x )  \/  E. m  e.  NN  E. f ( f : ( 1 ... m ) -1-1-onto-> A  /\  x  =  (  seq 1 (  +  , 
( n  e.  NN  |->  if ( n  <_  m ,  [_ ( f `  n )  /  k ]_ B ,  0 ) ) ) `  m
) ) ) )
94 f1of 5335 . . . . . . . . . . . . . 14  |-  ( F : ( 1 ... M ) -1-1-onto-> A  ->  F :
( 1 ... M
) --> A )
9512, 94syl 14 . . . . . . . . . . . . 13  |-  ( ph  ->  F : ( 1 ... M ) --> A )
963, 18fzfigd 10159 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 1 ... M
)  e.  Fin )
97 fex 5615 . . . . . . . . . . . . 13  |-  ( ( F : ( 1 ... M ) --> A  /\  ( 1 ... M )  e.  Fin )  ->  F  e.  _V )
9895, 96, 97syl2anc 408 . . . . . . . . . . . 12  |-  ( ph  ->  F  e.  _V )
9911, 2eleqtrdi 2210 . . . . . . . . . . . . . 14  |-  ( ph  ->  M  e.  ( ZZ>= ` 
1 ) )
10014ralrimiva 2482 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  A. n  e.  ( 1 ... M ) ( G `  n
)  =  C )
101 nfv 1493 . . . . . . . . . . . . . . . . . 18  |-  F/ k ( G `  n
)  =  C
102 nfcsb1v 3005 . . . . . . . . . . . . . . . . . . 19  |-  F/_ n [_ k  /  n ]_ C
103102nfeq2 2270 . . . . . . . . . . . . . . . . . 18  |-  F/ n
( G `  k
)  =  [_ k  /  n ]_ C
104 fveq2 5389 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  k  ->  ( G `  n )  =  ( G `  k ) )
105 csbeq1a 2983 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  k  ->  C  =  [_ k  /  n ]_ C )
106104, 105eqeq12d 2132 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  k  ->  (
( G `  n
)  =  C  <->  ( G `  k )  =  [_ k  /  n ]_ C
) )
107101, 103, 106cbvral 2627 . . . . . . . . . . . . . . . . 17  |-  ( A. n  e.  ( 1 ... M ) ( G `  n )  =  C  <->  A. k  e.  ( 1 ... M
) ( G `  k )  =  [_ k  /  n ]_ C
)
108100, 107sylib 121 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  A. k  e.  ( 1 ... M ) ( G `  k
)  =  [_ k  /  n ]_ C )
109108r19.21bi 2497 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  k  e.  ( 1 ... M
) )  ->  ( G `  k )  =  [_ k  /  n ]_ C )
110 elfznn 9789 . . . . . . . . . . . . . . . . . 18  |-  ( k  e.  ( 1 ... M )  ->  k  e.  NN )
111110adantl 275 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  k  e.  ( 1 ... M
) )  ->  k  e.  NN )
112 elfzle2 9763 . . . . . . . . . . . . . . . . . . . 20  |-  ( k  e.  ( 1 ... M )  ->  k  <_  M )
113112adantl 275 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  k  e.  ( 1 ... M
) )  ->  k  <_  M )
114113iftrued 3451 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  k  e.  ( 1 ... M
) )  ->  if ( k  <_  M ,  ( G `  k ) ,  0 )  =  ( G `
 k ) )
115104eleq1d 2186 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  k  ->  (
( G `  n
)  e.  CC  <->  ( G `  k )  e.  CC ) )
11615adantr 274 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  k  e.  ( 1 ... M
) )  ->  A. n  e.  ( 1 ... M
) ( G `  n )  e.  CC )
117 simpr 109 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  k  e.  ( 1 ... M
) )  ->  k  e.  ( 1 ... M
) )
118115, 116, 117rspcdva 2768 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  k  e.  ( 1 ... M
) )  ->  ( G `  k )  e.  CC )
119114, 118eqeltrd 2194 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  k  e.  ( 1 ... M
) )  ->  if ( k  <_  M ,  ( G `  k ) ,  0 )  e.  CC )
120 breq1 3902 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  k  ->  (
n  <_  M  <->  k  <_  M ) )
121120, 104ifbieq1d 3464 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  k  ->  if ( n  <_  M , 
( G `  n
) ,  0 )  =  if ( k  <_  M ,  ( G `  k ) ,  0 ) )
122121, 38fvmptg 5465 . . . . . . . . . . . . . . . . 17  |-  ( ( k  e.  NN  /\  if ( k  <_  M ,  ( G `  k ) ,  0 )  e.  CC )  ->  ( ( n  e.  NN  |->  if ( n  <_  M , 
( G `  n
) ,  0 ) ) `  k )  =  if ( k  <_  M ,  ( G `  k ) ,  0 ) )
123111, 119, 122syl2anc 408 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  k  e.  ( 1 ... M
) )  ->  (
( n  e.  NN  |->  if ( n  <_  M ,  ( G `  n ) ,  0 ) ) `  k
)  =  if ( k  <_  M , 
( G `  k
) ,  0 ) )
124123, 114eqtrd 2150 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  k  e.  ( 1 ... M
) )  ->  (
( n  e.  NN  |->  if ( n  <_  M ,  ( G `  n ) ,  0 ) ) `  k
)  =  ( G `
 k ) )
125113iftrued 3451 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  k  e.  ( 1 ... M
) )  ->  if ( k  <_  M ,  [_ k  /  n ]_ C ,  0 )  =  [_ k  /  n ]_ C )
12695ffvelrnda 5523 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  n  e.  ( 1 ... M
) )  ->  ( F `  n )  e.  A )
12710adantl 275 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  n  e.  ( 1 ... M
) )  /\  k  =  ( F `  n ) )  ->  B  =  C )
128126, 127csbied 3016 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  n  e.  ( 1 ... M
) )  ->  [_ ( F `  n )  /  k ]_ B  =  C )
12950adantr 274 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  n  e.  ( 1 ... M
) )  ->  A. k  e.  A  B  e.  CC )
130 nfcsb1v 3005 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  F/_ k [_ ( F `  n
)  /  k ]_ B
131130nfel1 2269 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  F/ k
[_ ( F `  n )  /  k ]_ B  e.  CC
132 csbeq1a 2983 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( k  =  ( F `  n )  ->  B  =  [_ ( F `  n )  /  k ]_ B )
133132eleq1d 2186 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( k  =  ( F `  n )  ->  ( B  e.  CC  <->  [_ ( F `
 n )  / 
k ]_ B  e.  CC ) )
134131, 133rspc 2757 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( F `  n )  e.  A  ->  ( A. k  e.  A  B  e.  CC  ->  [_ ( F `  n
)  /  k ]_ B  e.  CC )
)
135126, 129, 134sylc 62 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  n  e.  ( 1 ... M
) )  ->  [_ ( F `  n )  /  k ]_ B  e.  CC )
136128, 135eqeltrrd 2195 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  n  e.  ( 1 ... M
) )  ->  C  e.  CC )
137136ralrimiva 2482 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  A. n  e.  ( 1 ... M ) C  e.  CC )
138 nfv 1493 . . . . . . . . . . . . . . . . . . . . 21  |-  F/ k  C  e.  CC
139102nfel1 2269 . . . . . . . . . . . . . . . . . . . . 21  |-  F/ n [_ k  /  n ]_ C  e.  CC
140105eleq1d 2186 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  =  k  ->  ( C  e.  CC  <->  [_ k  /  n ]_ C  e.  CC ) )
141138, 139, 140cbvral 2627 . . . . . . . . . . . . . . . . . . . 20  |-  ( A. n  e.  ( 1 ... M ) C  e.  CC  <->  A. k  e.  ( 1 ... M
) [_ k  /  n ]_ C  e.  CC )
142137, 141sylib 121 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  A. k  e.  ( 1 ... M )
[_ k  /  n ]_ C  e.  CC )
143142r19.21bi 2497 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  k  e.  ( 1 ... M
) )  ->  [_ k  /  n ]_ C  e.  CC )
144125, 143eqeltrd 2194 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  k  e.  ( 1 ... M
) )  ->  if ( k  <_  M ,  [_ k  /  n ]_ C ,  0 )  e.  CC )
145 nfcv 2258 . . . . . . . . . . . . . . . . . 18  |-  F/_ n
k
146 nfv 1493 . . . . . . . . . . . . . . . . . . 19  |-  F/ n  k  <_  M
147 nfcv 2258 . . . . . . . . . . . . . . . . . . 19  |-  F/_ n
0
148146, 102, 147nfif 3470 . . . . . . . . . . . . . . . . . 18  |-  F/_ n if ( k  <_  M ,  [_ k  /  n ]_ C ,  0 )
149120, 105ifbieq1d 3464 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  k  ->  if ( n  <_  M ,  C ,  0 )  =  if ( k  <_  M ,  [_ k  /  n ]_ C ,  0 ) )
150 eqid 2117 . . . . . . . . . . . . . . . . . 18  |-  ( n  e.  NN  |->  if ( n  <_  M ,  C ,  0 ) )  =  ( n  e.  NN  |->  if ( n  <_  M ,  C ,  0 ) )
151145, 148, 149, 150fvmptf 5481 . . . . . . . . . . . . . . . . 17  |-  ( ( k  e.  NN  /\  if ( k  <_  M ,  [_ k  /  n ]_ C ,  0 )  e.  CC )  -> 
( ( n  e.  NN  |->  if ( n  <_  M ,  C ,  0 ) ) `
 k )  =  if ( k  <_  M ,  [_ k  /  n ]_ C ,  0 ) )
152111, 144, 151syl2anc 408 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  k  e.  ( 1 ... M
) )  ->  (
( n  e.  NN  |->  if ( n  <_  M ,  C ,  0 ) ) `  k )  =  if ( k  <_  M ,  [_ k  /  n ]_ C ,  0 ) )
153152, 125eqtrd 2150 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  k  e.  ( 1 ... M
) )  ->  (
( n  e.  NN  |->  if ( n  <_  M ,  C ,  0 ) ) `  k )  =  [_ k  /  n ]_ C )
154109, 124, 1533eqtr4d 2160 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  ( 1 ... M
) )  ->  (
( n  e.  NN  |->  if ( n  <_  M ,  ( G `  n ) ,  0 ) ) `  k
)  =  ( ( n  e.  NN  |->  if ( n  <_  M ,  C ,  0 ) ) `  k ) )
155137ad2antrr 479 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  ( ZZ>= `  1 )
)  /\  x  <_  M )  ->  A. n  e.  ( 1 ... M
) C  e.  CC )
156 nfcsb1v 3005 . . . . . . . . . . . . . . . . . . . 20  |-  F/_ n [_ x  /  n ]_ C
157156nfel1 2269 . . . . . . . . . . . . . . . . . . 19  |-  F/ n [_ x  /  n ]_ C  e.  CC
158 csbeq1a 2983 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  =  x  ->  C  =  [_ x  /  n ]_ C )
159158eleq1d 2186 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  x  ->  ( C  e.  CC  <->  [_ x  /  n ]_ C  e.  CC ) )
160157, 159rspc 2757 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  ( 1 ... M )  ->  ( A. n  e.  (
1 ... M ) C  e.  CC  ->  [_ x  /  n ]_ C  e.  CC ) )
16128, 155, 160sylc 62 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  ( ZZ>= `  1 )
)  /\  x  <_  M )  ->  [_ x  /  n ]_ C  e.  CC )
162161, 30, 34ifcldadc 3471 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( ZZ>= `  1 )
)  ->  if (
x  <_  M ,  [_ x  /  n ]_ C ,  0 )  e.  CC )
163 nfcv 2258 . . . . . . . . . . . . . . . . 17  |-  F/_ n x
164 nfv 1493 . . . . . . . . . . . . . . . . . 18  |-  F/ n  x  <_  M
165164, 156, 147nfif 3470 . . . . . . . . . . . . . . . . 17  |-  F/_ n if ( x  <_  M ,  [_ x  /  n ]_ C ,  0 )
16636, 158ifbieq1d 3464 . . . . . . . . . . . . . . . . 17  |-  ( n  =  x  ->  if ( n  <_  M ,  C ,  0 )  =  if ( x  <_  M ,  [_ x  /  n ]_ C ,  0 ) )
167163, 165, 166, 150fvmptf 5481 . . . . . . . . . . . . . . . 16  |-  ( ( x  e.  NN  /\  if ( x  <_  M ,  [_ x  /  n ]_ C ,  0 )  e.  CC )  -> 
( ( n  e.  NN  |->  if ( n  <_  M ,  C ,  0 ) ) `
 x )  =  if ( x  <_  M ,  [_ x  /  n ]_ C ,  0 ) )
1687, 162, 167syl2anc 408 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( ZZ>= `  1 )
)  ->  ( (
n  e.  NN  |->  if ( n  <_  M ,  C ,  0 ) ) `  x )  =  if ( x  <_  M ,  [_ x  /  n ]_ C ,  0 ) )
169168, 162eqeltrd 2194 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( ZZ>= `  1 )
)  ->  ( (
n  e.  NN  |->  if ( n  <_  M ,  C ,  0 ) ) `  x )  e.  CC )
170 addcl 7713 . . . . . . . . . . . . . . 15  |-  ( ( x  e.  CC  /\  y  e.  CC )  ->  ( x  +  y )  e.  CC )
171170adantl 275 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( x  e.  CC  /\  y  e.  CC ) )  -> 
( x  +  y )  e.  CC )
17299, 154, 41, 169, 171seq3fveq 10199 . . . . . . . . . . . . 13  |-  ( ph  ->  (  seq 1 (  +  ,  ( n  e.  NN  |->  if ( n  <_  M , 
( G `  n
) ,  0 ) ) ) `  M
)  =  (  seq 1 (  +  , 
( n  e.  NN  |->  if ( n  <_  M ,  C ,  0 ) ) ) `  M
) )
17312, 172jca 304 . . . . . . . . . . . 12  |-  ( ph  ->  ( F : ( 1 ... M ) -1-1-onto-> A  /\  (  seq 1
(  +  ,  ( n  e.  NN  |->  if ( n  <_  M ,  ( G `  n ) ,  0 ) ) ) `  M )  =  (  seq 1 (  +  ,  ( n  e.  NN  |->  if ( n  <_  M ,  C ,  0 ) ) ) `  M ) ) )
174 f1oeq1 5326 . . . . . . . . . . . . . 14  |-  ( f  =  F  ->  (
f : ( 1 ... M ) -1-1-onto-> A  <->  F :
( 1 ... M
)
-1-1-onto-> A ) )
175 fveq1 5388 . . . . . . . . . . . . . . . . . . . . 21  |-  ( f  =  F  ->  (
f `  n )  =  ( F `  n ) )
176175csbeq1d 2981 . . . . . . . . . . . . . . . . . . . 20  |-  ( f  =  F  ->  [_ (
f `  n )  /  k ]_ B  =  [_ ( F `  n )  /  k ]_ B )
177 vex 2663 . . . . . . . . . . . . . . . . . . . . . . 23  |-  f  e. 
_V
178 vex 2663 . . . . . . . . . . . . . . . . . . . . . . 23  |-  n  e. 
_V
179177, 178fvex 5409 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( f `
 n )  e. 
_V
180175, 179syl6eqelr 2209 . . . . . . . . . . . . . . . . . . . . 21  |-  ( f  =  F  ->  ( F `  n )  e.  _V )
18110adantl 275 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( f  =  F  /\  k  =  ( F `  n ) )  ->  B  =  C )
182180, 181csbied 3016 . . . . . . . . . . . . . . . . . . . 20  |-  ( f  =  F  ->  [_ ( F `  n )  /  k ]_ B  =  C )
183176, 182eqtrd 2150 . . . . . . . . . . . . . . . . . . 19  |-  ( f  =  F  ->  [_ (
f `  n )  /  k ]_ B  =  C )
184183ifeq1d 3459 . . . . . . . . . . . . . . . . . 18  |-  ( f  =  F  ->  if ( n  <_  M ,  [_ ( f `  n
)  /  k ]_ B ,  0 )  =  if ( n  <_  M ,  C ,  0 ) )
185184mpteq2dv 3989 . . . . . . . . . . . . . . . . 17  |-  ( f  =  F  ->  (
n  e.  NN  |->  if ( n  <_  M ,  [_ ( f `  n )  /  k ]_ B ,  0 ) )  =  ( n  e.  NN  |->  if ( n  <_  M ,  C ,  0 ) ) )
186185seqeq3d 10181 . . . . . . . . . . . . . . . 16  |-  ( f  =  F  ->  seq 1 (  +  , 
( n  e.  NN  |->  if ( n  <_  M ,  [_ ( f `  n )  /  k ]_ B ,  0 ) ) )  =  seq 1 (  +  , 
( n  e.  NN  |->  if ( n  <_  M ,  C ,  0 ) ) ) )
187186fveq1d 5391 . . . . . . . . . . . . . . 15  |-  ( f  =  F  ->  (  seq 1 (  +  , 
( n  e.  NN  |->  if ( n  <_  M ,  [_ ( f `  n )  /  k ]_ B ,  0 ) ) ) `  M
)  =  (  seq 1 (  +  , 
( n  e.  NN  |->  if ( n  <_  M ,  C ,  0 ) ) ) `  M
) )
188187eqeq2d 2129 . . . . . . . . . . . . . 14  |-  ( f  =  F  ->  (
(  seq 1 (  +  ,  ( n  e.  NN  |->  if ( n  <_  M ,  ( G `  n ) ,  0 ) ) ) `  M )  =  (  seq 1
(  +  ,  ( n  e.  NN  |->  if ( n  <_  M ,  [_ ( f `  n )  /  k ]_ B ,  0 ) ) ) `  M
)  <->  (  seq 1
(  +  ,  ( n  e.  NN  |->  if ( n  <_  M ,  ( G `  n ) ,  0 ) ) ) `  M )  =  (  seq 1 (  +  ,  ( n  e.  NN  |->  if ( n  <_  M ,  C ,  0 ) ) ) `  M ) ) )
189174, 188anbi12d 464 . . . . . . . . . . . . 13  |-  ( f  =  F  ->  (
( f : ( 1 ... M ) -1-1-onto-> A  /\  (  seq 1
(  +  ,  ( n  e.  NN  |->  if ( n  <_  M ,  ( G `  n ) ,  0 ) ) ) `  M )  =  (  seq 1 (  +  ,  ( n  e.  NN  |->  if ( n  <_  M ,  [_ ( f `  n
)  /  k ]_ B ,  0 ) ) ) `  M
) )  <->  ( F : ( 1 ... M ) -1-1-onto-> A  /\  (  seq 1 (  +  , 
( n  e.  NN  |->  if ( n  <_  M ,  ( G `  n ) ,  0 ) ) ) `  M )  =  (  seq 1 (  +  ,  ( n  e.  NN  |->  if ( n  <_  M ,  C ,  0 ) ) ) `  M ) ) ) )
190189spcegv 2748 . . . . . . . . . . . 12  |-  ( F  e.  _V  ->  (
( F : ( 1 ... M ) -1-1-onto-> A  /\  (  seq 1
(  +  ,  ( n  e.  NN  |->  if ( n  <_  M ,  ( G `  n ) ,  0 ) ) ) `  M )  =  (  seq 1 (  +  ,  ( n  e.  NN  |->  if ( n  <_  M ,  C ,  0 ) ) ) `  M ) )  ->  E. f
( f : ( 1 ... M ) -1-1-onto-> A  /\  (  seq 1
(  +  ,  ( n  e.  NN  |->  if ( n  <_  M ,  ( G `  n ) ,  0 ) ) ) `  M )  =  (  seq 1 (  +  ,  ( n  e.  NN  |->  if ( n  <_  M ,  [_ ( f `  n
)  /  k ]_ B ,  0 ) ) ) `  M
) ) ) )
19198, 173, 190sylc 62 . . . . . . . . . . 11  |-  ( ph  ->  E. f ( f : ( 1 ... M ) -1-1-onto-> A  /\  (  seq 1 (  +  , 
( n  e.  NN  |->  if ( n  <_  M ,  ( G `  n ) ,  0 ) ) ) `  M )  =  (  seq 1 (  +  ,  ( n  e.  NN  |->  if ( n  <_  M ,  [_ ( f `  n
)  /  k ]_ B ,  0 ) ) ) `  M
) ) )
192 oveq2 5750 . . . . . . . . . . . . . . 15  |-  ( m  =  M  ->  (
1 ... m )  =  ( 1 ... M
) )
193 f1oeq2 5327 . . . . . . . . . . . . . . 15  |-  ( ( 1 ... m )  =  ( 1 ... M )  ->  (
f : ( 1 ... m ) -1-1-onto-> A  <->  f :
( 1 ... M
)
-1-1-onto-> A ) )
194192, 193syl 14 . . . . . . . . . . . . . 14  |-  ( m  =  M  ->  (
f : ( 1 ... m ) -1-1-onto-> A  <->  f :
( 1 ... M
)
-1-1-onto-> A ) )
195 breq2 3903 . . . . . . . . . . . . . . . . . . 19  |-  ( m  =  M  ->  (
n  <_  m  <->  n  <_  M ) )
196195ifbid 3463 . . . . . . . . . . . . . . . . . 18  |-  ( m  =  M  ->  if ( n  <_  m , 
[_ ( f `  n )  /  k ]_ B ,  0 )  =  if ( n  <_  M ,  [_ ( f `  n
)  /  k ]_ B ,  0 ) )
197196mpteq2dv 3989 . . . . . . . . . . . . . . . . 17  |-  ( m  =  M  ->  (
n  e.  NN  |->  if ( n  <_  m ,  [_ ( f `  n )  /  k ]_ B ,  0 ) )  =  ( n  e.  NN  |->  if ( n  <_  M ,  [_ ( f `  n
)  /  k ]_ B ,  0 ) ) )
198197seqeq3d 10181 . . . . . . . . . . . . . . . 16  |-  ( m  =  M  ->  seq 1 (  +  , 
( n  e.  NN  |->  if ( n  <_  m ,  [_ ( f `  n )  /  k ]_ B ,  0 ) ) )  =  seq 1 (  +  , 
( n  e.  NN  |->  if ( n  <_  M ,  [_ ( f `  n )  /  k ]_ B ,  0 ) ) ) )
199 id 19 . . . . . . . . . . . . . . . 16  |-  ( m  =  M  ->  m  =  M )
200198, 199fveq12d 5396 . . . . . . . . . . . . . . 15  |-  ( m  =  M  ->  (  seq 1 (  +  , 
( n  e.  NN  |->  if ( n  <_  m ,  [_ ( f `  n )  /  k ]_ B ,  0 ) ) ) `  m
)  =  (  seq 1 (  +  , 
( n  e.  NN  |->  if ( n  <_  M ,  [_ ( f `  n )  /  k ]_ B ,  0 ) ) ) `  M
) )
201200eqeq2d 2129 . . . . . . . . . . . . . 14  |-  ( m  =  M  ->  (
(  seq 1 (  +  ,  ( n  e.  NN  |->  if ( n  <_  M ,  ( G `  n ) ,  0 ) ) ) `  M )  =  (  seq 1
(  +  ,  ( n  e.  NN  |->  if ( n  <_  m ,  [_ ( f `  n )  /  k ]_ B ,  0 ) ) ) `  m
)  <->  (  seq 1
(  +  ,  ( n  e.  NN  |->  if ( n  <_  M ,  ( G `  n ) ,  0 ) ) ) `  M )  =  (  seq 1 (  +  ,  ( n  e.  NN  |->  if ( n  <_  M ,  [_ ( f `  n
)  /  k ]_ B ,  0 ) ) ) `  M
) ) )
202194, 201anbi12d 464 . . . . . . . . . . . . 13  |-  ( m  =  M  ->  (
( f : ( 1 ... m ) -1-1-onto-> A  /\  (  seq 1
(  +  ,  ( n  e.  NN  |->  if ( n  <_  M ,  ( G `  n ) ,  0 ) ) ) `  M )  =  (  seq 1 (  +  ,  ( n  e.  NN  |->  if ( n  <_  m ,  [_ ( f `  n
)  /  k ]_ B ,  0 ) ) ) `  m
) )  <->  ( f : ( 1 ... M ) -1-1-onto-> A  /\  (  seq 1 (  +  , 
( n  e.  NN  |->  if ( n  <_  M ,  ( G `  n ) ,  0 ) ) ) `  M )  =  (  seq 1 (  +  ,  ( n  e.  NN  |->  if ( n  <_  M ,  [_ ( f `  n
)  /  k ]_ B ,  0 ) ) ) `  M
) ) ) )
203202exbidv 1781 . . . . . . . . . . . 12  |-  ( m  =  M  ->  ( E. f ( f : ( 1 ... m
)
-1-1-onto-> A  /\  (  seq 1
(  +  ,  ( n  e.  NN  |->  if ( n  <_  M ,  ( G `  n ) ,  0 ) ) ) `  M )  =  (  seq 1 (  +  ,  ( n  e.  NN  |->  if ( n  <_  m ,  [_ ( f `  n
)  /  k ]_ B ,  0 ) ) ) `  m
) )  <->  E. f
( f : ( 1 ... M ) -1-1-onto-> A  /\  (  seq 1
(  +  ,  ( n  e.  NN  |->  if ( n  <_  M ,  ( G `  n ) ,  0 ) ) ) `  M )  =  (  seq 1 (  +  ,  ( n  e.  NN  |->  if ( n  <_  M ,  [_ ( f `  n
)  /  k ]_ B ,  0 ) ) ) `  M
) ) ) )
204203rspcev 2763 . . . . . . . . . . 11  |-  ( ( M  e.  NN  /\  E. f ( f : ( 1 ... M
)
-1-1-onto-> A  /\  (  seq 1
(  +  ,  ( n  e.  NN  |->  if ( n  <_  M ,  ( G `  n ) ,  0 ) ) ) `  M )  =  (  seq 1 (  +  ,  ( n  e.  NN  |->  if ( n  <_  M ,  [_ ( f `  n
)  /  k ]_ B ,  0 ) ) ) `  M
) ) )  ->  E. m  e.  NN  E. f ( f : ( 1 ... m
)
-1-1-onto-> A  /\  (  seq 1
(  +  ,  ( n  e.  NN  |->  if ( n  <_  M ,  ( G `  n ) ,  0 ) ) ) `  M )  =  (  seq 1 (  +  ,  ( n  e.  NN  |->  if ( n  <_  m ,  [_ ( f `  n
)  /  k ]_ B ,  0 ) ) ) `  m
) ) )
20511, 191, 204syl2anc 408 . . . . . . . . . 10  |-  ( ph  ->  E. m  e.  NN  E. f ( f : ( 1 ... m
)
-1-1-onto-> A  /\  (  seq 1
(  +  ,  ( n  e.  NN  |->  if ( n  <_  M ,  ( G `  n ) ,  0 ) ) ) `  M )  =  (  seq 1 (  +  ,  ( n  e.  NN  |->  if ( n  <_  m ,  [_ ( f `  n
)  /  k ]_ B ,  0 ) ) ) `  m
) ) )
206205olcd 708 . . . . . . . . 9  |-  ( ph  ->  ( E. m  e.  ZZ  ( A  C_  ( ZZ>= `  m )  /\  A. j  e.  (
ZZ>= `  m )DECID  j  e.  A  /\  seq m
(  +  ,  ( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) ) )  ~~>  (  seq 1 (  +  , 
( n  e.  NN  |->  if ( n  <_  M ,  ( G `  n ) ,  0 ) ) ) `  M ) )  \/ 
E. m  e.  NN  E. f ( f : ( 1 ... m
)
-1-1-onto-> A  /\  (  seq 1
(  +  ,  ( n  e.  NN  |->  if ( n  <_  M ,  ( G `  n ) ,  0 ) ) ) `  M )  =  (  seq 1 (  +  ,  ( n  e.  NN  |->  if ( n  <_  m ,  [_ ( f `  n
)  /  k ]_ B ,  0 ) ) ) `  m
) ) ) )
207206adantr 274 . . . . . . . 8  |-  ( (
ph  /\  ( E. m  e.  ZZ  ( A  C_  ( ZZ>= `  m
)  /\  A. j  e.  ( ZZ>= `  m )DECID  j  e.  A  /\  seq m
(  +  ,  ( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) ) )  ~~>  x )  \/  E. m  e.  NN  E. f ( f : ( 1 ... m ) -1-1-onto-> A  /\  x  =  (  seq 1 (  +  , 
( n  e.  NN  |->  if ( n  <_  m ,  [_ ( f `  n )  /  k ]_ B ,  0 ) ) ) `  m
) ) ) )  ->  ( E. m  e.  ZZ  ( A  C_  ( ZZ>= `  m )  /\  A. j  e.  (
ZZ>= `  m )DECID  j  e.  A  /\  seq m
(  +  ,  ( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) ) )  ~~>  (  seq 1 (  +  , 
( n  e.  NN  |->  if ( n  <_  M ,  ( G `  n ) ,  0 ) ) ) `  M ) )  \/ 
E. m  e.  NN  E. f ( f : ( 1 ... m
)
-1-1-onto-> A  /\  (  seq 1
(  +  ,  ( n  e.  NN  |->  if ( n  <_  M ,  ( G `  n ) ,  0 ) ) ) `  M )  =  (  seq 1 (  +  ,  ( n  e.  NN  |->  if ( n  <_  m ,  [_ ( f `  n
)  /  k ]_ B ,  0 ) ) ) `  m
) ) ) )
208 breq2 3903 . . . . . . . . . . . 12  |-  ( x  =  (  seq 1
(  +  ,  ( n  e.  NN  |->  if ( n  <_  M ,  ( G `  n ) ,  0 ) ) ) `  M )  ->  (  seq m (  +  , 
( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) ) )  ~~>  x  <->  seq m
(  +  ,  ( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) ) )  ~~>  (  seq 1 (  +  , 
( n  e.  NN  |->  if ( n  <_  M ,  ( G `  n ) ,  0 ) ) ) `  M ) ) )
2092083anbi3d 1281 . . . . . . . . . . 11  |-  ( x  =  (  seq 1
(  +  ,  ( n  e.  NN  |->  if ( n  <_  M ,  ( G `  n ) ,  0 ) ) ) `  M )  ->  (
( A  C_  ( ZZ>=
`  m )  /\  A. j  e.  ( ZZ>= `  m )DECID  j  e.  A  /\  seq m (  +  , 
( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) ) )  ~~>  x )  <-> 
( A  C_  ( ZZ>=
`  m )  /\  A. j  e.  ( ZZ>= `  m )DECID  j  e.  A  /\  seq m (  +  , 
( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) ) )  ~~>  (  seq 1 (  +  , 
( n  e.  NN  |->  if ( n  <_  M ,  ( G `  n ) ,  0 ) ) ) `  M ) ) ) )
210209rexbidv 2415 . . . . . . . . . 10  |-  ( x  =  (  seq 1
(  +  ,  ( n  e.  NN  |->  if ( n  <_  M ,  ( G `  n ) ,  0 ) ) ) `  M )  ->  ( E. m  e.  ZZ  ( A  C_  ( ZZ>= `  m )  /\  A. j  e.  ( ZZ>= `  m )DECID  j  e.  A  /\  seq m (  +  , 
( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) ) )  ~~>  x )  <->  E. m  e.  ZZ  ( A  C_  ( ZZ>= `  m )  /\  A. j  e.  ( ZZ>= `  m )DECID  j  e.  A  /\  seq m (  +  , 
( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) ) )  ~~>  (  seq 1 (  +  , 
( n  e.  NN  |->  if ( n  <_  M ,  ( G `  n ) ,  0 ) ) ) `  M ) ) ) )
211 eqeq1 2124 . . . . . . . . . . . . 13  |-  ( x  =  (  seq 1
(  +  ,  ( n  e.  NN  |->  if ( n  <_  M ,  ( G `  n ) ,  0 ) ) ) `  M )  ->  (
x  =  (  seq 1 (  +  , 
( n  e.  NN  |->  if ( n  <_  m ,  [_ ( f `  n )  /  k ]_ B ,  0 ) ) ) `  m
)  <->  (  seq 1
(  +  ,  ( n  e.  NN  |->  if ( n  <_  M ,  ( G `  n ) ,  0 ) ) ) `  M )  =  (  seq 1 (  +  ,  ( n  e.  NN  |->  if ( n  <_  m ,  [_ ( f `  n
)  /  k ]_ B ,  0 ) ) ) `  m
) ) )
212211anbi2d 459 . . . . . . . . . . . 12  |-  ( x  =  (  seq 1
(  +  ,  ( n  e.  NN  |->  if ( n  <_  M ,  ( G `  n ) ,  0 ) ) ) `  M )  ->  (
( f : ( 1 ... m ) -1-1-onto-> A  /\  x  =  (  seq 1 (  +  ,  ( n  e.  NN  |->  if ( n  <_  m ,  [_ ( f `  n
)  /  k ]_ B ,  0 ) ) ) `  m
) )  <->  ( f : ( 1 ... m ) -1-1-onto-> A  /\  (  seq 1 (  +  , 
( n  e.  NN  |->  if ( n  <_  M ,  ( G `  n ) ,  0 ) ) ) `  M )  =  (  seq 1 (  +  ,  ( n  e.  NN  |->  if ( n  <_  m ,  [_ ( f `  n
)  /  k ]_ B ,  0 ) ) ) `  m
) ) ) )
213212exbidv 1781 . . . . . . . . . . 11  |-  ( x  =  (  seq 1
(  +  ,  ( n  e.  NN  |->  if ( n  <_  M ,  ( G `  n ) ,  0 ) ) ) `  M )  ->  ( E. f ( f : ( 1 ... m
)
-1-1-onto-> A  /\  x  =  (  seq 1 (  +  ,  ( n  e.  NN  |->  if ( n  <_  m ,  [_ ( f `  n
)  /  k ]_ B ,  0 ) ) ) `  m
) )  <->  E. f
( f : ( 1 ... m ) -1-1-onto-> A  /\  (  seq 1
(  +  ,  ( n  e.  NN  |->  if ( n  <_  M ,  ( G `  n ) ,  0 ) ) ) `  M )  =  (  seq 1 (  +  ,  ( n  e.  NN  |->  if ( n  <_  m ,  [_ ( f `  n
)  /  k ]_ B ,  0 ) ) ) `  m
) ) ) )
214213rexbidv 2415 . . . . . . . . . 10  |-  ( x  =  (  seq 1
(  +  ,  ( n  e.  NN  |->  if ( n  <_  M ,  ( G `  n ) ,  0 ) ) ) `  M )  ->  ( E. m  e.  NN  E. f ( f : ( 1 ... m
)
-1-1-onto-> A  /\  x  =  (  seq 1 (  +  ,  ( n  e.  NN  |->  if ( n  <_  m ,  [_ ( f `  n
)  /  k ]_ B ,  0 ) ) ) `  m
) )  <->  E. m  e.  NN  E. f ( f : ( 1 ... m ) -1-1-onto-> A  /\  (  seq 1 (  +  ,  ( n  e.  NN  |->  if ( n  <_  M ,  ( G `  n ) ,  0 ) ) ) `  M )  =  (  seq 1
(  +  ,  ( n  e.  NN  |->  if ( n  <_  m ,  [_ ( f `  n )  /  k ]_ B ,  0 ) ) ) `  m
) ) ) )
215210, 214orbi12d 767 . . . . . . . . 9  |-  ( x  =  (  seq 1
(  +  ,  ( n  e.  NN  |->  if ( n  <_  M ,  ( G `  n ) ,  0 ) ) ) `  M )  ->  (
( E. m  e.  ZZ  ( A  C_  ( ZZ>= `  m )  /\  A. j  e.  (
ZZ>= `  m )DECID  j  e.  A  /\  seq m
(  +  ,  ( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) ) )  ~~>  x )  \/  E. m  e.  NN  E. f ( f : ( 1 ... m ) -1-1-onto-> A  /\  x  =  (  seq 1 (  +  , 
( n  e.  NN  |->  if ( n  <_  m ,  [_ ( f `  n )  /  k ]_ B ,  0 ) ) ) `  m
) ) )  <->  ( E. m  e.  ZZ  ( A  C_  ( ZZ>= `  m
)  /\  A. j  e.  ( ZZ>= `  m )DECID  j  e.  A  /\  seq m
(  +  ,  ( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) ) )  ~~>  (  seq 1 (  +  , 
( n  e.  NN  |->  if ( n  <_  M ,  ( G `  n ) ,  0 ) ) ) `  M ) )  \/ 
E. m  e.  NN  E. f ( f : ( 1 ... m
)
-1-1-onto-> A  /\  (  seq 1
(  +  ,  ( n  e.  NN  |->  if ( n  <_  M ,  ( G `  n ) ,  0 ) ) ) `  M )  =  (  seq 1 (  +  ,  ( n  e.  NN  |->  if ( n  <_  m ,  [_ ( f `  n
)  /  k ]_ B ,  0 ) ) ) `  m
) ) ) ) )
216215moi2 2838 . . . . . . . 8  |-  ( ( ( (  seq 1
(  +  ,  ( n  e.  NN  |->  if ( n  <_  M ,  ( G `  n ) ,  0 ) ) ) `  M )  e.  CC  /\ 
E* x ( E. m  e.  ZZ  ( A  C_  ( ZZ>= `  m
)  /\  A. j  e.  ( ZZ>= `  m )DECID  j  e.  A  /\  seq m
(  +  ,  ( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) ) )  ~~>  x )  \/  E. m  e.  NN  E. f ( f : ( 1 ... m ) -1-1-onto-> A  /\  x  =  (  seq 1 (  +  , 
( n  e.  NN  |->  if ( n  <_  m ,  [_ ( f `  n )  /  k ]_ B ,  0 ) ) ) `  m
) ) ) )  /\  ( ( E. m  e.  ZZ  ( A  C_  ( ZZ>= `  m
)  /\  A. j  e.  ( ZZ>= `  m )DECID  j  e.  A  /\  seq m
(  +  ,  ( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) ) )  ~~>  x )  \/  E. m  e.  NN  E. f ( f : ( 1 ... m ) -1-1-onto-> A  /\  x  =  (  seq 1 (  +  , 
( n  e.  NN  |->  if ( n  <_  m ,  [_ ( f `  n )  /  k ]_ B ,  0 ) ) ) `  m
) ) )  /\  ( E. m  e.  ZZ  ( A  C_  ( ZZ>= `  m )  /\  A. j  e.  ( ZZ>= `  m )DECID  j  e.  A  /\  seq m (  +  , 
( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) ) )  ~~>  (  seq 1 (  +  , 
( n  e.  NN  |->  if ( n  <_  M ,  ( G `  n ) ,  0 ) ) ) `  M ) )  \/ 
E. m  e.  NN  E. f ( f : ( 1 ... m
)
-1-1-onto-> A  /\  (  seq 1
(  +  ,  ( n  e.  NN  |->  if ( n  <_  M ,  ( G `  n ) ,  0 ) ) ) `  M )  =  (  seq 1 (  +  ,  ( n  e.  NN  |->  if ( n  <_  m ,  [_ ( f `  n
)  /  k ]_ B ,  0 ) ) ) `  m
) ) ) ) )  ->  x  =  (  seq 1 (  +  ,  ( n  e.  NN  |->  if ( n  <_  M ,  ( G `  n ) ,  0 ) ) ) `  M ) )
21745, 92, 93, 207, 216syl22anc 1202 . . . . . . 7  |-  ( (
ph  /\  ( E. m  e.  ZZ  ( A  C_  ( ZZ>= `  m
)  /\  A. j  e.  ( ZZ>= `  m )DECID  j  e.  A  /\  seq m
(  +  ,  ( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) ) )  ~~>  x )  \/  E. m  e.  NN  E. f ( f : ( 1 ... m ) -1-1-onto-> A  /\  x  =  (  seq 1 (  +  , 
( n  e.  NN  |->  if ( n  <_  m ,  [_ ( f `  n )  /  k ]_ B ,  0 ) ) ) `  m
) ) ) )  ->  x  =  (  seq 1 (  +  ,  ( n  e.  NN  |->  if ( n  <_  M ,  ( G `  n ) ,  0 ) ) ) `  M ) )
218217ex 114 . . . . . 6  |-  ( ph  ->  ( ( E. m  e.  ZZ  ( A  C_  ( ZZ>= `  m )  /\  A. j  e.  (
ZZ>= `  m )DECID  j  e.  A  /\  seq m
(  +  ,  ( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) ) )  ~~>  x )  \/  E. m  e.  NN  E. f ( f : ( 1 ... m ) -1-1-onto-> A  /\  x  =  (  seq 1 (  +  , 
( n  e.  NN  |->  if ( n  <_  m ,  [_ ( f `  n )  /  k ]_ B ,  0 ) ) ) `  m
) ) )  ->  x  =  (  seq 1 (  +  , 
( n  e.  NN  |->  if ( n  <_  M ,  ( G `  n ) ,  0 ) ) ) `  M ) ) )
219206, 215syl5ibrcom 156 . . . . . 6  |-  ( ph  ->  ( x  =  (  seq 1 (  +  ,  ( n  e.  NN  |->  if ( n  <_  M ,  ( G `  n ) ,  0 ) ) ) `  M )  ->  ( E. m  e.  ZZ  ( A  C_  ( ZZ>= `  m )  /\  A. j  e.  (
ZZ>= `  m )DECID  j  e.  A  /\  seq m
(  +  ,  ( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) ) )  ~~>  x )  \/  E. m  e.  NN  E. f ( f : ( 1 ... m ) -1-1-onto-> A  /\  x  =  (  seq 1 (  +  , 
( n  e.  NN  |->  if ( n  <_  m ,  [_ ( f `  n )  /  k ]_ B ,  0 ) ) ) `  m
) ) ) ) )
220218, 219impbid 128 . . . . 5  |-  ( ph  ->  ( ( E. m  e.  ZZ  ( A  C_  ( ZZ>= `  m )  /\  A. j  e.  (
ZZ>= `  m )DECID  j  e.  A  /\  seq m
(  +  ,  ( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) ) )  ~~>  x )  \/  E. m  e.  NN  E. f ( f : ( 1 ... m ) -1-1-onto-> A  /\  x  =  (  seq 1 (  +  , 
( n  e.  NN  |->  if ( n  <_  m ,  [_ ( f `  n )  /  k ]_ B ,  0 ) ) ) `  m
) ) )  <->  x  =  (  seq 1 (  +  ,  ( n  e.  NN  |->  if ( n  <_  M ,  ( G `  n ) ,  0 ) ) ) `  M ) ) )
221220adantr 274 . . . 4  |-  ( (
ph  /\  (  seq 1 (  +  , 
( n  e.  NN  |->  if ( n  <_  M ,  ( G `  n ) ,  0 ) ) ) `  M )  e.  CC )  ->  ( ( E. m  e.  ZZ  ( A  C_  ( ZZ>= `  m
)  /\  A. j  e.  ( ZZ>= `  m )DECID  j  e.  A  /\  seq m
(  +  ,  ( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) ) )  ~~>  x )  \/  E. m  e.  NN  E. f ( f : ( 1 ... m ) -1-1-onto-> A  /\  x  =  (  seq 1 (  +  , 
( n  e.  NN  |->  if ( n  <_  m ,  [_ ( f `  n )  /  k ]_ B ,  0 ) ) ) `  m
) ) )  <->  x  =  (  seq 1 (  +  ,  ( n  e.  NN  |->  if ( n  <_  M ,  ( G `  n ) ,  0 ) ) ) `  M ) ) )
222221iota5 5078 . . 3  |-  ( (
ph  /\  (  seq 1 (  +  , 
( n  e.  NN  |->  if ( n  <_  M ,  ( G `  n ) ,  0 ) ) ) `  M )  e.  CC )  ->  ( iota x
( E. m  e.  ZZ  ( A  C_  ( ZZ>= `  m )  /\  A. j  e.  (
ZZ>= `  m )DECID  j  e.  A  /\  seq m
(  +  ,  ( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) ) )  ~~>  x )  \/  E. m  e.  NN  E. f ( f : ( 1 ... m ) -1-1-onto-> A  /\  x  =  (  seq 1 (  +  , 
( n  e.  NN  |->  if ( n  <_  m ,  [_ ( f `  n )  /  k ]_ B ,  0 ) ) ) `  m
) ) ) )  =  (  seq 1
(  +  ,  ( n  e.  NN  |->  if ( n  <_  M ,  ( G `  n ) ,  0 ) ) ) `  M ) )
22344, 222mpdan 417 . 2  |-  ( ph  ->  ( iota x ( E. m  e.  ZZ  ( A  C_  ( ZZ>= `  m )  /\  A. j  e.  ( ZZ>= `  m )DECID  j  e.  A  /\  seq m (  +  , 
( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) ) )  ~~>  x )  \/  E. m  e.  NN  E. f ( f : ( 1 ... m ) -1-1-onto-> A  /\  x  =  (  seq 1 (  +  , 
( n  e.  NN  |->  if ( n  <_  m ,  [_ ( f `  n )  /  k ]_ B ,  0 ) ) ) `  m
) ) ) )  =  (  seq 1
(  +  ,  ( n  e.  NN  |->  if ( n  <_  M ,  ( G `  n ) ,  0 ) ) ) `  M ) )
2241, 223syl5eq 2162 1  |-  ( ph  -> 
sum_ k  e.  A  B  =  (  seq 1 (  +  , 
( n  e.  NN  |->  if ( n  <_  M ,  ( G `  n ) ,  0 ) ) ) `  M ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 103    <-> wb 104    \/ wo 682  DECID wdc 804    /\ w3a 947    = wceq 1316   E.wex 1453    e. wcel 1465   E*wmo 1978   A.wral 2393   E.wrex 2394   _Vcvv 2660   [_csb 2975    C_ wss 3041   ifcif 3444   class class class wbr 3899    |-> cmpt 3959   iotacio 5056   -->wf 5089   -1-1-onto->wf1o 5092   ` cfv 5093  (class class class)co 5742   Fincfn 6602   CCcc 7586   0cc0 7588   1c1 7589    + caddc 7591    <_ cle 7769   NNcn 8684   NN0cn0 8935   ZZcz 9012   ZZ>=cuz 9282   ...cfz 9745    seqcseq 10173  ♯chash 10476    ~~> cli 11002   sum_csu 11077
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-mulrcl 7687  ax-addcom 7688  ax-mulcom 7689  ax-addass 7690  ax-mulass 7691  ax-distr 7692  ax-i2m1 7693  ax-0lt1 7694  ax-1rid 7695  ax-0id 7696  ax-rnegex 7697  ax-precex 7698  ax-cnre 7699  ax-pre-ltirr 7700  ax-pre-ltwlin 7701  ax-pre-lttrn 7702  ax-pre-apti 7703  ax-pre-ltadd 7704  ax-pre-mulgt0 7705  ax-pre-mulext 7706  ax-arch 7707  ax-caucvg 7708
This theorem depends on definitions:  df-bi 116  df-dc 805  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-rmo 2401  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-if 3445  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-po 4188  df-iso 4189  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-irdg 6235  df-frec 6256  df-1o 6281  df-oadd 6285  df-er 6397  df-en 6603  df-dom 6604  df-fin 6605  df-pnf 7770  df-mnf 7771  df-xr 7772  df-ltxr 7773  df-le 7774  df-sub 7903  df-neg 7904  df-reap 8304  df-ap 8311  df-div 8400  df-inn 8685  df-2 8743  df-3 8744  df-4 8745  df-n0 8936  df-z 9013  df-uz 9283  df-q 9368  df-rp 9398  df-fz 9746  df-fzo 9875  df-seqfrec 10174  df-exp 10248  df-ihash 10477  df-cj 10569  df-re 10570  df-im 10571  df-rsqrt 10725  df-abs 10726  df-clim 11003  df-sumdc 11078
This theorem is referenced by:  isumz  11113  fsumf1o  11114  fsumcl2lem  11122  fsumadd  11130  sumsnf  11133  fsummulc2  11172
  Copyright terms: Public domain W3C validator