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

Theorem fsum3 11096
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 11063 . 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 9310 . . . . 5  |-  NN  =  ( ZZ>= `  1 )
3 1zzd 9032 . . . . 5  |-  ( ph  ->  1  e.  ZZ )
4 elnnuz 9311 . . . . . 6  |-  ( x  e.  NN  <->  x  e.  ( ZZ>= `  1 )
)
52eqimss2i 3122 . . . . . . . . . 10  |-  ( ZZ>= ` 
1 )  C_  NN
65sseli 3061 . . . . . . . . 9  |-  ( x  e.  ( ZZ>= `  1
)  ->  x  e.  NN )
76adantl 273 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( ZZ>= `  1 )
)  ->  x  e.  NN )
8 fveq2 5387 . . . . . . . . . . 11  |-  ( n  =  x  ->  ( G `  n )  =  ( G `  x ) )
98eleq1d 2184 . . . . . . . . . 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 11095 . . . . . . . . . . 11  |-  ( ph  ->  A. n  e.  ( 1 ... M ) ( G `  n
)  e.  CC )
1615ad2antrr 477 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( ZZ>= `  1 )
)  /\  x  <_  M )  ->  A. n  e.  ( 1 ... M
) ( G `  n )  e.  CC )
17 1zzd 9032 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( ZZ>= `  1 )
)  /\  x  <_  M )  ->  1  e.  ZZ )
1811nnzd 9123 . . . . . . . . . . . . 13  |-  ( ph  ->  M  e.  ZZ )
1918ad2antrr 477 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( ZZ>= `  1 )
)  /\  x  <_  M )  ->  M  e.  ZZ )
20 eluzelz 9284 . . . . . . . . . . . . 13  |-  ( x  e.  ( ZZ>= `  1
)  ->  x  e.  ZZ )
2120ad2antlr 478 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( ZZ>= `  1 )
)  /\  x  <_  M )  ->  x  e.  ZZ )
2217, 19, 213jca 1144 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( ZZ>= `  1 )
)  /\  x  <_  M )  ->  ( 1  e.  ZZ  /\  M  e.  ZZ  /\  x  e.  ZZ ) )
23 eluzle 9287 . . . . . . . . . . . . 13  |-  ( x  e.  ( ZZ>= `  1
)  ->  1  <_  x )
2423ad2antlr 478 . . . . . . . . . . . 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 302 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( ZZ>= `  1 )
)  /\  x  <_  M )  ->  ( 1  <_  x  /\  x  <_  M ) )
27 elfz2 9737 . . . . . . . . . . 11  |-  ( x  e.  ( 1 ... M )  <->  ( (
1  e.  ZZ  /\  M  e.  ZZ  /\  x  e.  ZZ )  /\  (
1  <_  x  /\  x  <_  M ) ) )
2822, 26, 27sylanbrc 411 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( ZZ>= `  1 )
)  /\  x  <_  M )  ->  x  e.  ( 1 ... M
) )
299, 16, 28rspcdva 2766 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  ( ZZ>= `  1 )
)  /\  x  <_  M )  ->  ( G `  x )  e.  CC )
30 0cnd 7723 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  ( ZZ>= `  1 )
)  /\  -.  x  <_  M )  ->  0  e.  CC )
317nnzd 9123 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( ZZ>= `  1 )
)  ->  x  e.  ZZ )
3218adantr 272 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( ZZ>= `  1 )
)  ->  M  e.  ZZ )
33 zdcle 9078 . . . . . . . . . 10  |-  ( ( x  e.  ZZ  /\  M  e.  ZZ )  -> DECID  x  <_  M )
3431, 32, 33syl2anc 406 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( ZZ>= `  1 )
)  -> DECID  x  <_  M )
3529, 30, 34ifcldadc 3469 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( ZZ>= `  1 )
)  ->  if (
x  <_  M , 
( G `  x
) ,  0 )  e.  CC )
36 breq1 3900 . . . . . . . . . 10  |-  ( n  =  x  ->  (
n  <_  M  <->  x  <_  M ) )
3736, 8ifbieq1d 3462 . . . . . . . . 9  |-  ( n  =  x  ->  if ( n  <_  M , 
( G `  n
) ,  0 )  =  if ( x  <_  M ,  ( G `  x ) ,  0 ) )
38 eqid 2115 . . . . . . . . 9  |-  ( n  e.  NN  |->  if ( n  <_  M , 
( G `  n
) ,  0 ) )  =  ( n  e.  NN  |->  if ( n  <_  M , 
( G `  n
) ,  0 ) )
3937, 38fvmptg 5463 . . . . . . . 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 406 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( ZZ>= `  1 )
)  ->  ( (
n  e.  NN  |->  if ( n  <_  M ,  ( G `  n ) ,  0 ) ) `  x
)  =  if ( x  <_  M , 
( G `  x
) ,  0 ) )
4140, 35eqeltrd 2192 . . . . . 6  |-  ( (
ph  /\  x  e.  ( ZZ>= `  1 )
)  ->  ( (
n  e.  NN  |->  if ( n  <_  M ,  ( G `  n ) ,  0 ) ) `  x
)  e.  CC )
424, 41sylan2b 283 . . . . 5  |-  ( (
ph  /\  x  e.  NN )  ->  ( ( n  e.  NN  |->  if ( n  <_  M ,  ( G `  n ) ,  0 ) ) `  x
)  e.  CC )
432, 3, 42serf 10187 . . . 4  |-  ( ph  ->  seq 1 (  +  ,  ( n  e.  NN  |->  if ( n  <_  M ,  ( G `  n ) ,  0 ) ) ) : NN --> CC )
4443, 11ffvelrnd 5522 . . 3  |-  ( ph  ->  (  seq 1 (  +  ,  ( n  e.  NN  |->  if ( n  <_  M , 
( G `  n
) ,  0 ) ) ) `  M
)  e.  CC )
4544adantr 272 . . . . . . . 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 2176 . . . . . . . . . . . . 13  |-  ( n  =  j  ->  (
n  e.  A  <->  j  e.  A ) )
47 csbeq1 2976 . . . . . . . . . . . . 13  |-  ( n  =  j  ->  [_ n  /  k ]_ B  =  [_ j  /  k ]_ B )
4846, 47ifbieq1d 3462 . . . . . . . . . . . 12  |-  ( n  =  j  ->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 )  =  if ( j  e.  A ,  [_ j  /  k ]_ B ,  0 ) )
4948cbvmptv 3992 . . . . . . . . . . 11  |-  ( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) )  =  ( j  e.  ZZ  |->  if ( j  e.  A ,  [_ j  /  k ]_ B ,  0 ) )
5013ralrimiva 2480 . . . . . . . . . . . 12  |-  ( ph  ->  A. k  e.  A  B  e.  CC )
51 nfcsb1v 3003 . . . . . . . . . . . . . 14  |-  F/_ k [_ j  /  k ]_ B
5251nfel1 2267 . . . . . . . . . . . . 13  |-  F/ k
[_ j  /  k ]_ B  e.  CC
53 csbeq1a 2981 . . . . . . . . . . . . . 14  |-  ( k  =  j  ->  B  =  [_ j  /  k ]_ B )
5453eleq1d 2184 . . . . . . . . . . . . 13  |-  ( k  =  j  ->  ( B  e.  CC  <->  [_ j  / 
k ]_ B  e.  CC ) )
5552, 54rspc 2755 . . . . . . . . . . . 12  |-  ( j  e.  A  ->  ( A. k  e.  A  B  e.  CC  ->  [_ j  /  k ]_ B  e.  CC )
)
5650, 55mpan9 277 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  A )  ->  [_ j  /  k ]_ B  e.  CC )
57 breq1 3900 . . . . . . . . . . . . 13  |-  ( n  =  i  ->  (
n  <_  ( `  A
)  <->  i  <_  ( `  A ) ) )
58 fveq2 5387 . . . . . . . . . . . . . . 15  |-  ( n  =  i  ->  (
f `  n )  =  ( f `  i ) )
5958csbeq1d 2979 . . . . . . . . . . . . . 14  |-  ( n  =  i  ->  [_ (
f `  n )  /  k ]_ B  =  [_ ( f `  i )  /  k ]_ B )
60 csbco 2982 . . . . . . . . . . . . . 14  |-  [_ (
f `  i )  /  j ]_ [_ j  /  k ]_ B  =  [_ ( f `  i )  /  k ]_ B
6159, 60syl6eqr 2166 . . . . . . . . . . . . 13  |-  ( n  =  i  ->  [_ (
f `  n )  /  k ]_ B  =  [_ ( f `  i )  /  j ]_ [_ j  /  k ]_ B )
6257, 61ifbieq1d 3462 . . . . . . . . . . . 12  |-  ( n  =  i  ->  if ( n  <_  ( `  A
) ,  [_ (
f `  n )  /  k ]_ B ,  0 )  =  if ( i  <_ 
( `  A ) , 
[_ ( f `  i )  /  j ]_ [_ j  /  k ]_ B ,  0 ) )
6362cbvmptv 3992 . . . . . . . . . . 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 11092 . . . . . . . . . 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 2176 . . . . . . . . . . . . . . . 16  |-  ( u  =  j  ->  (
u  e.  A  <->  j  e.  A ) )
6665dcbid 806 . . . . . . . . . . . . . . 15  |-  ( u  =  j  ->  (DECID  u  e.  A  <-> DECID  j  e.  A )
)
6766cbvralv 2629 . . . . . . . . . . . . . 14  |-  ( A. u  e.  ( ZZ>= `  m )DECID  u  e.  A  <->  A. j  e.  ( ZZ>= `  m )DECID  j  e.  A )
68673anbi2i 1156 . . . . . . . . . . . . 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 2417 . . . . . . . . . . . 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 9032 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( m  e.  NN  ->  1  e.  ZZ )
71 nnz 9024 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( m  e.  NN  ->  m  e.  ZZ )
7270, 71fzfigd 10144 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( m  e.  NN  ->  (
1 ... m )  e. 
Fin )
73 fihasheqf1oi 10474 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( 1 ... m
)  e.  Fin  /\  f : ( 1 ... m ) -1-1-onto-> A )  ->  ( `  ( 1 ... m
) )  =  ( `  A ) )
7472, 73sylan 279 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( m  e.  NN  /\  f : ( 1 ... m ) -1-1-onto-> A )  ->  ( `  ( 1 ... m
) )  =  ( `  A ) )
75 nnnn0 8935 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( m  e.  NN  ->  m  e.  NN0 )
7675adantr 272 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( m  e.  NN  /\  f : ( 1 ... m ) -1-1-onto-> A )  ->  m  e.  NN0 )
77 hashfz1 10469 . . . . . . . . . . . . . . . . . . . . . . 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 2150 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( m  e.  NN  /\  f : ( 1 ... m ) -1-1-onto-> A )  ->  ( `  A )  =  m )
8079breq2d 3909 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( m  e.  NN  /\  f : ( 1 ... m ) -1-1-onto-> A )  ->  (
n  <_  ( `  A
)  <->  n  <_  m ) )
8180ifbid 3461 . . . . . . . . . . . . . . . . . . 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 3987 . . . . . . . . . . . . . . . . . 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 10166 . . . . . . . . . . . . . . . . 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 5389 . . . . . . . . . . . . . . . 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 2127 . . . . . . . . . . . . . . 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 445 . . . . . . . . . . . . . 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 1779 . . . . . . . . . . . . 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 2425 . . . . . . . . . . . 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 736 . . . . . . . . . . 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 2012 . . . . . . . . . 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 272 . . . . . . . 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 5333 . . . . . . . . . . . . . 14  |-  ( F : ( 1 ... M ) -1-1-onto-> A  ->  F :
( 1 ... M
) --> A )
9512, 94syl 14 . . . . . . . . . . . . 13  |-  ( ph  ->  F : ( 1 ... M ) --> A )
963, 18fzfigd 10144 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 1 ... M
)  e.  Fin )
97 fex 5613 . . . . . . . . . . . . 13  |-  ( ( F : ( 1 ... M ) --> A  /\  ( 1 ... M )  e.  Fin )  ->  F  e.  _V )
9895, 96, 97syl2anc 406 . . . . . . . . . . . 12  |-  ( ph  ->  F  e.  _V )
9911, 2syl6eleq 2208 . . . . . . . . . . . . . 14  |-  ( ph  ->  M  e.  ( ZZ>= ` 
1 ) )
10014ralrimiva 2480 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  A. n  e.  ( 1 ... M ) ( G `  n
)  =  C )
101 nfv 1491 . . . . . . . . . . . . . . . . . 18  |-  F/ k ( G `  n
)  =  C
102 nfcsb1v 3003 . . . . . . . . . . . . . . . . . . 19  |-  F/_ n [_ k  /  n ]_ C
103102nfeq2 2268 . . . . . . . . . . . . . . . . . 18  |-  F/ n
( G `  k
)  =  [_ k  /  n ]_ C
104 fveq2 5387 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  k  ->  ( G `  n )  =  ( G `  k ) )
105 csbeq1a 2981 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  k  ->  C  =  [_ k  /  n ]_ C )
106104, 105eqeq12d 2130 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  k  ->  (
( G `  n
)  =  C  <->  ( G `  k )  =  [_ k  /  n ]_ C
) )
107101, 103, 106cbvral 2625 . . . . . . . . . . . . . . . . 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 2495 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  k  e.  ( 1 ... M
) )  ->  ( G `  k )  =  [_ k  /  n ]_ C )
110 elfznn 9774 . . . . . . . . . . . . . . . . . 18  |-  ( k  e.  ( 1 ... M )  ->  k  e.  NN )
111110adantl 273 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  k  e.  ( 1 ... M
) )  ->  k  e.  NN )
112 elfzle2 9748 . . . . . . . . . . . . . . . . . . . 20  |-  ( k  e.  ( 1 ... M )  ->  k  <_  M )
113112adantl 273 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  k  e.  ( 1 ... M
) )  ->  k  <_  M )
114113iftrued 3449 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  k  e.  ( 1 ... M
) )  ->  if ( k  <_  M ,  ( G `  k ) ,  0 )  =  ( G `
 k ) )
115104eleq1d 2184 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  k  ->  (
( G `  n
)  e.  CC  <->  ( G `  k )  e.  CC ) )
11615adantr 272 . . . . . . . . . . . . . . . . . . 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 2766 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  k  e.  ( 1 ... M
) )  ->  ( G `  k )  e.  CC )
119114, 118eqeltrd 2192 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  k  e.  ( 1 ... M
) )  ->  if ( k  <_  M ,  ( G `  k ) ,  0 )  e.  CC )
120 breq1 3900 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  k  ->  (
n  <_  M  <->  k  <_  M ) )
121120, 104ifbieq1d 3462 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  k  ->  if ( n  <_  M , 
( G `  n
) ,  0 )  =  if ( k  <_  M ,  ( G `  k ) ,  0 ) )
122121, 38fvmptg 5463 . . . . . . . . . . . . . . . . 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 406 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  k  e.  ( 1 ... M
) )  ->  (
( n  e.  NN  |->  if ( n  <_  M ,  ( G `  n ) ,  0 ) ) `  k
)  =  if ( k  <_  M , 
( G `  k
) ,  0 ) )
124123, 114eqtrd 2148 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  k  e.  ( 1 ... M
) )  ->  (
( n  e.  NN  |->  if ( n  <_  M ,  ( G `  n ) ,  0 ) ) `  k
)  =  ( G `
 k ) )
125113iftrued 3449 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  k  e.  ( 1 ... M
) )  ->  if ( k  <_  M ,  [_ k  /  n ]_ C ,  0 )  =  [_ k  /  n ]_ C )
12695ffvelrnda 5521 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  n  e.  ( 1 ... M
) )  ->  ( F `  n )  e.  A )
12710adantl 273 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  n  e.  ( 1 ... M
) )  /\  k  =  ( F `  n ) )  ->  B  =  C )
128126, 127csbied 3014 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  n  e.  ( 1 ... M
) )  ->  [_ ( F `  n )  /  k ]_ B  =  C )
12950adantr 272 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  n  e.  ( 1 ... M
) )  ->  A. k  e.  A  B  e.  CC )
130 nfcsb1v 3003 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  F/_ k [_ ( F `  n
)  /  k ]_ B
131130nfel1 2267 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  F/ k
[_ ( F `  n )  /  k ]_ B  e.  CC
132 csbeq1a 2981 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( k  =  ( F `  n )  ->  B  =  [_ ( F `  n )  /  k ]_ B )
133132eleq1d 2184 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( k  =  ( F `  n )  ->  ( B  e.  CC  <->  [_ ( F `
 n )  / 
k ]_ B  e.  CC ) )
134131, 133rspc 2755 . . . . . . . . . . . . . . . . . . . . . . 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 2193 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  n  e.  ( 1 ... M
) )  ->  C  e.  CC )
137136ralrimiva 2480 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  A. n  e.  ( 1 ... M ) C  e.  CC )
138 nfv 1491 . . . . . . . . . . . . . . . . . . . . 21  |-  F/ k  C  e.  CC
139102nfel1 2267 . . . . . . . . . . . . . . . . . . . . 21  |-  F/ n [_ k  /  n ]_ C  e.  CC
140105eleq1d 2184 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  =  k  ->  ( C  e.  CC  <->  [_ k  /  n ]_ C  e.  CC ) )
141138, 139, 140cbvral 2625 . . . . . . . . . . . . . . . . . . . 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 2495 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  k  e.  ( 1 ... M
) )  ->  [_ k  /  n ]_ C  e.  CC )
144125, 143eqeltrd 2192 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  k  e.  ( 1 ... M
) )  ->  if ( k  <_  M ,  [_ k  /  n ]_ C ,  0 )  e.  CC )
145 nfcv 2256 . . . . . . . . . . . . . . . . . 18  |-  F/_ n
k
146 nfv 1491 . . . . . . . . . . . . . . . . . . 19  |-  F/ n  k  <_  M
147 nfcv 2256 . . . . . . . . . . . . . . . . . . 19  |-  F/_ n
0
148146, 102, 147nfif 3468 . . . . . . . . . . . . . . . . . 18  |-  F/_ n if ( k  <_  M ,  [_ k  /  n ]_ C ,  0 )
149120, 105ifbieq1d 3462 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  k  ->  if ( n  <_  M ,  C ,  0 )  =  if ( k  <_  M ,  [_ k  /  n ]_ C ,  0 ) )
150 eqid 2115 . . . . . . . . . . . . . . . . . 18  |-  ( n  e.  NN  |->  if ( n  <_  M ,  C ,  0 ) )  =  ( n  e.  NN  |->  if ( n  <_  M ,  C ,  0 ) )
151145, 148, 149, 150fvmptf 5479 . . . . . . . . . . . . . . . . 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 406 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  k  e.  ( 1 ... M
) )  ->  (
( n  e.  NN  |->  if ( n  <_  M ,  C ,  0 ) ) `  k )  =  if ( k  <_  M ,  [_ k  /  n ]_ C ,  0 ) )
153152, 125eqtrd 2148 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  k  e.  ( 1 ... M
) )  ->  (
( n  e.  NN  |->  if ( n  <_  M ,  C ,  0 ) ) `  k )  =  [_ k  /  n ]_ C )
154109, 124, 1533eqtr4d 2158 . . . . . . . . . . . . . 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 477 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  ( ZZ>= `  1 )
)  /\  x  <_  M )  ->  A. n  e.  ( 1 ... M
) C  e.  CC )
156 nfcsb1v 3003 . . . . . . . . . . . . . . . . . . . 20  |-  F/_ n [_ x  /  n ]_ C
157156nfel1 2267 . . . . . . . . . . . . . . . . . . 19  |-  F/ n [_ x  /  n ]_ C  e.  CC
158 csbeq1a 2981 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  =  x  ->  C  =  [_ x  /  n ]_ C )
159158eleq1d 2184 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  x  ->  ( C  e.  CC  <->  [_ x  /  n ]_ C  e.  CC ) )
160157, 159rspc 2755 . . . . . . . . . . . . . . . . . 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 3469 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( ZZ>= `  1 )
)  ->  if (
x  <_  M ,  [_ x  /  n ]_ C ,  0 )  e.  CC )
163 nfcv 2256 . . . . . . . . . . . . . . . . 17  |-  F/_ n x
164 nfv 1491 . . . . . . . . . . . . . . . . . 18  |-  F/ n  x  <_  M
165164, 156, 147nfif 3468 . . . . . . . . . . . . . . . . 17  |-  F/_ n if ( x  <_  M ,  [_ x  /  n ]_ C ,  0 )
16636, 158ifbieq1d 3462 . . . . . . . . . . . . . . . . 17  |-  ( n  =  x  ->  if ( n  <_  M ,  C ,  0 )  =  if ( x  <_  M ,  [_ x  /  n ]_ C ,  0 ) )
167163, 165, 166, 150fvmptf 5479 . . . . . . . . . . . . . . . 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 406 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( ZZ>= `  1 )
)  ->  ( (
n  e.  NN  |->  if ( n  <_  M ,  C ,  0 ) ) `  x )  =  if ( x  <_  M ,  [_ x  /  n ]_ C ,  0 ) )
169168, 162eqeltrd 2192 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( ZZ>= `  1 )
)  ->  ( (
n  e.  NN  |->  if ( n  <_  M ,  C ,  0 ) ) `  x )  e.  CC )
170 addcl 7709 . . . . . . . . . . . . . . 15  |-  ( ( x  e.  CC  /\  y  e.  CC )  ->  ( x  +  y )  e.  CC )
171170adantl 273 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( x  e.  CC  /\  y  e.  CC ) )  -> 
( x  +  y )  e.  CC )
17299, 154, 41, 169, 171seq3fveq 10184 . . . . . . . . . . . . 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 302 . . . . . . . . . . . 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 5324 . . . . . . . . . . . . . 14  |-  ( f  =  F  ->  (
f : ( 1 ... M ) -1-1-onto-> A  <->  F :
( 1 ... M
)
-1-1-onto-> A ) )
175 fveq1 5386 . . . . . . . . . . . . . . . . . . . . 21  |-  ( f  =  F  ->  (
f `  n )  =  ( F `  n ) )
176175csbeq1d 2979 . . . . . . . . . . . . . . . . . . . 20  |-  ( f  =  F  ->  [_ (
f `  n )  /  k ]_ B  =  [_ ( F `  n )  /  k ]_ B )
177 vex 2661 . . . . . . . . . . . . . . . . . . . . . . 23  |-  f  e. 
_V
178 vex 2661 . . . . . . . . . . . . . . . . . . . . . . 23  |-  n  e. 
_V
179177, 178fvex 5407 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( f `
 n )  e. 
_V
180175, 179syl6eqelr 2207 . . . . . . . . . . . . . . . . . . . . 21  |-  ( f  =  F  ->  ( F `  n )  e.  _V )
18110adantl 273 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( f  =  F  /\  k  =  ( F `  n ) )  ->  B  =  C )
182180, 181csbied 3014 . . . . . . . . . . . . . . . . . . . 20  |-  ( f  =  F  ->  [_ ( F `  n )  /  k ]_ B  =  C )
183176, 182eqtrd 2148 . . . . . . . . . . . . . . . . . . 19  |-  ( f  =  F  ->  [_ (
f `  n )  /  k ]_ B  =  C )
184183ifeq1d 3457 . . . . . . . . . . . . . . . . . 18  |-  ( f  =  F  ->  if ( n  <_  M ,  [_ ( f `  n
)  /  k ]_ B ,  0 )  =  if ( n  <_  M ,  C ,  0 ) )
185184mpteq2dv 3987 . . . . . . . . . . . . . . . . 17  |-  ( f  =  F  ->  (
n  e.  NN  |->  if ( n  <_  M ,  [_ ( f `  n )  /  k ]_ B ,  0 ) )  =  ( n  e.  NN  |->  if ( n  <_  M ,  C ,  0 ) ) )
186185seqeq3d 10166 . . . . . . . . . . . . . . . 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 5389 . . . . . . . . . . . . . . 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 2127 . . . . . . . . . . . . . 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 462 . . . . . . . . . . . . 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 2746 . . . . . . . . . . . 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 5748 . . . . . . . . . . . . . . 15  |-  ( m  =  M  ->  (
1 ... m )  =  ( 1 ... M
) )
193 f1oeq2 5325 . . . . . . . . . . . . . . 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 3901 . . . . . . . . . . . . . . . . . . 19  |-  ( m  =  M  ->  (
n  <_  m  <->  n  <_  M ) )
196195ifbid 3461 . . . . . . . . . . . . . . . . . 18  |-  ( m  =  M  ->  if ( n  <_  m , 
[_ ( f `  n )  /  k ]_ B ,  0 )  =  if ( n  <_  M ,  [_ ( f `  n
)  /  k ]_ B ,  0 ) )
197196mpteq2dv 3987 . . . . . . . . . . . . . . . . 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 10166 . . . . . . . . . . . . . . . 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 5394 . . . . . . . . . . . . . . 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 2127 . . . . . . . . . . . . . 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 462 . . . . . . . . . . . . 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 1779 . . . . . . . . . . . 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 2761 . . . . . . . . . . 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 406 . . . . . . . . . 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 706 . . . . . . . . 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 272 . . . . . . . 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 3901 . . . . . . . . . . . 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 1279 . . . . . . . . . . 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 2413 . . . . . . . . . 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 2122 . . . . . . . . . . . . 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 457 . . . . . . . . . . . 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 1779 . . . . . . . . . . 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 2413 . . . . . . . . . 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 765 . . . . . . . . 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 2836 . . . . . . . 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 1200 . . . . . . 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 272 . . . 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 5076 . . 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 415 . 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 2160 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 680  DECID wdc 802    /\ w3a 945    = wceq 1314   E.wex 1451    e. wcel 1463   E*wmo 1976   A.wral 2391   E.wrex 2392   _Vcvv 2658   [_csb 2973    C_ wss 3039   ifcif 3442   class class class wbr 3897    |-> cmpt 3957   iotacio 5054   -->wf 5087   -1-1-onto->wf1o 5090   ` cfv 5091  (class class class)co 5740   Fincfn 6600   CCcc 7582   0cc0 7584   1c1 7585    + caddc 7587    <_ cle 7765   NNcn 8677   NN0cn0 8928   ZZcz 9005   ZZ>=cuz 9275   ...cfz 9730    seqcseq 10158  ♯chash 10461    ~~> cli 10987   sum_csu 11062
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 586  ax-in2 587  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-13 1474  ax-14 1475  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097  ax-coll 4011  ax-sep 4014  ax-nul 4022  ax-pow 4066  ax-pr 4099  ax-un 4323  ax-setind 4420  ax-iinf 4470  ax-cnex 7675  ax-resscn 7676  ax-1cn 7677  ax-1re 7678  ax-icn 7679  ax-addcl 7680  ax-addrcl 7681  ax-mulcl 7682  ax-mulrcl 7683  ax-addcom 7684  ax-mulcom 7685  ax-addass 7686  ax-mulass 7687  ax-distr 7688  ax-i2m1 7689  ax-0lt1 7690  ax-1rid 7691  ax-0id 7692  ax-rnegex 7693  ax-precex 7694  ax-cnre 7695  ax-pre-ltirr 7696  ax-pre-ltwlin 7697  ax-pre-lttrn 7698  ax-pre-apti 7699  ax-pre-ltadd 7700  ax-pre-mulgt0 7701  ax-pre-mulext 7702  ax-arch 7703  ax-caucvg 7704
This theorem depends on definitions:  df-bi 116  df-dc 803  df-3or 946  df-3an 947  df-tru 1317  df-fal 1320  df-nf 1420  df-sb 1719  df-eu 1978  df-mo 1979  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2245  df-ne 2284  df-nel 2379  df-ral 2396  df-rex 2397  df-reu 2398  df-rmo 2399  df-rab 2400  df-v 2660  df-sbc 2881  df-csb 2974  df-dif 3041  df-un 3043  df-in 3045  df-ss 3052  df-nul 3332  df-if 3443  df-pw 3480  df-sn 3501  df-pr 3502  df-op 3504  df-uni 3705  df-int 3740  df-iun 3783  df-br 3898  df-opab 3958  df-mpt 3959  df-tr 3995  df-id 4183  df-po 4186  df-iso 4187  df-iord 4256  df-on 4258  df-ilim 4259  df-suc 4261  df-iom 4473  df-xp 4513  df-rel 4514  df-cnv 4515  df-co 4516  df-dm 4517  df-rn 4518  df-res 4519  df-ima 4520  df-iota 5056  df-fun 5093  df-fn 5094  df-f 5095  df-f1 5096  df-fo 5097  df-f1o 5098  df-fv 5099  df-isom 5100  df-riota 5696  df-ov 5743  df-oprab 5744  df-mpo 5745  df-1st 6004  df-2nd 6005  df-recs 6168  df-irdg 6233  df-frec 6254  df-1o 6279  df-oadd 6283  df-er 6395  df-en 6601  df-dom 6602  df-fin 6603  df-pnf 7766  df-mnf 7767  df-xr 7768  df-ltxr 7769  df-le 7770  df-sub 7899  df-neg 7900  df-reap 8300  df-ap 8307  df-div 8393  df-inn 8678  df-2 8736  df-3 8737  df-4 8738  df-n0 8929  df-z 9006  df-uz 9276  df-q 9361  df-rp 9391  df-fz 9731  df-fzo 9860  df-seqfrec 10159  df-exp 10233  df-ihash 10462  df-cj 10554  df-re 10555  df-im 10556  df-rsqrt 10710  df-abs 10711  df-clim 10988  df-sumdc 11063
This theorem is referenced by:  isumz  11098  fsumf1o  11099  fsumcl2lem  11107  fsumadd  11115  sumsnf  11118  fsummulc2  11157
  Copyright terms: Public domain W3C validator