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

Theorem cvgratz 11252
Description: Ratio test for convergence of a complex infinite series. If the ratio  A of the absolute values of successive terms in an infinite sequence  F is less than 1 for all terms, then the infinite sum of the terms of  F converges to a complex number. (Contributed by NM, 26-Apr-2005.) (Revised by Jim Kingdon, 11-Nov-2022.)
Hypotheses
Ref Expression
cvgratz.1  |-  Z  =  ( ZZ>= `  M )
cvgratz.m  |-  ( ph  ->  M  e.  ZZ )
cvgratz.3  |-  ( ph  ->  A  e.  RR )
cvgratz.4  |-  ( ph  ->  A  <  1 )
cvgratz.gt0  |-  ( ph  ->  0  <  A )
cvgratz.6  |-  ( (
ph  /\  k  e.  Z )  ->  ( F `  k )  e.  CC )
cvgratz.7  |-  ( (
ph  /\  k  e.  Z )  ->  ( abs `  ( F `  ( k  +  1 ) ) )  <_ 
( A  x.  ( abs `  ( F `  k ) ) ) )
Assertion
Ref Expression
cvgratz  |-  ( ph  ->  seq M (  +  ,  F )  e. 
dom 
~~>  )
Distinct variable groups:    A, k    k, F    k, M    k, Z    ph, k

Proof of Theorem cvgratz
Dummy variables  i  x  y  a are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cvgratz.m . . . . 5  |-  ( ph  ->  M  e.  ZZ )
21adantr 272 . . . 4  |-  ( (
ph  /\  1  <_  M )  ->  M  e.  ZZ )
3 fveq2 5387 . . . . . 6  |-  ( k  =  x  ->  ( F `  k )  =  ( F `  x ) )
43eleq1d 2184 . . . . 5  |-  ( k  =  x  ->  (
( F `  k
)  e.  CC  <->  ( F `  x )  e.  CC ) )
5 cvgratz.6 . . . . . . 7  |-  ( (
ph  /\  k  e.  Z )  ->  ( F `  k )  e.  CC )
65ralrimiva 2480 . . . . . 6  |-  ( ph  ->  A. k  e.  Z  ( F `  k )  e.  CC )
76ad2antrr 477 . . . . 5  |-  ( ( ( ph  /\  1  <_  M )  /\  x  e.  ( ZZ>= `  M )
)  ->  A. k  e.  Z  ( F `  k )  e.  CC )
8 cvgratz.1 . . . . . . . 8  |-  Z  =  ( ZZ>= `  M )
98eleq2i 2182 . . . . . . 7  |-  ( x  e.  Z  <->  x  e.  ( ZZ>= `  M )
)
109biimpri 132 . . . . . 6  |-  ( x  e.  ( ZZ>= `  M
)  ->  x  e.  Z )
1110adantl 273 . . . . 5  |-  ( ( ( ph  /\  1  <_  M )  /\  x  e.  ( ZZ>= `  M )
)  ->  x  e.  Z )
124, 7, 11rspcdva 2766 . . . 4  |-  ( ( ( ph  /\  1  <_  M )  /\  x  e.  ( ZZ>= `  M )
)  ->  ( F `  x )  e.  CC )
13 eluzelz 9287 . . . . . . . 8  |-  ( k  e.  ( ZZ>= `  M
)  ->  k  e.  ZZ )
1413adantl 273 . . . . . . 7  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= `  M )
)  ->  k  e.  ZZ )
15 1red 7745 . . . . . . . 8  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= `  M )
)  ->  1  e.  RR )
161zred 9127 . . . . . . . . 9  |-  ( ph  ->  M  e.  RR )
1716ad2antrr 477 . . . . . . . 8  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= `  M )
)  ->  M  e.  RR )
1814zred 9127 . . . . . . . 8  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= `  M )
)  ->  k  e.  RR )
19 simplr 502 . . . . . . . 8  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= `  M )
)  ->  1  <_  M )
20 eluzle 9290 . . . . . . . . 9  |-  ( k  e.  ( ZZ>= `  M
)  ->  M  <_  k )
2120adantl 273 . . . . . . . 8  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= `  M )
)  ->  M  <_  k )
2215, 17, 18, 19, 21letrd 7850 . . . . . . 7  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= `  M )
)  ->  1  <_  k )
23 elnnz1 9031 . . . . . . 7  |-  ( k  e.  NN  <->  ( k  e.  ZZ  /\  1  <_ 
k ) )
2414, 22, 23sylanbrc 411 . . . . . 6  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= `  M )
)  ->  k  e.  NN )
25 elnnuz 9314 . . . . . . . 8  |-  ( k  e.  NN  <->  k  e.  ( ZZ>= `  1 )
)
26 fveq2 5387 . . . . . . . . . . . . 13  |-  ( k  =  M  ->  ( F `  k )  =  ( F `  M ) )
2726eleq1d 2184 . . . . . . . . . . . 12  |-  ( k  =  M  ->  (
( F `  k
)  e.  CC  <->  ( F `  M )  e.  CC ) )
28 uzid 9292 . . . . . . . . . . . . . 14  |-  ( M  e.  ZZ  ->  M  e.  ( ZZ>= `  M )
)
291, 28syl 14 . . . . . . . . . . . . 13  |-  ( ph  ->  M  e.  ( ZZ>= `  M ) )
3029, 8syl6eleqr 2209 . . . . . . . . . . . 12  |-  ( ph  ->  M  e.  Z )
3127, 6, 30rspcdva 2766 . . . . . . . . . . 11  |-  ( ph  ->  ( F `  M
)  e.  CC )
3231ad3antrrr 481 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= ` 
1 ) )  /\  k  <  M )  -> 
( F `  M
)  e.  CC )
33 cvgratz.3 . . . . . . . . . . . . . 14  |-  ( ph  ->  A  e.  RR )
34 cvgratz.gt0 . . . . . . . . . . . . . 14  |-  ( ph  ->  0  <  A )
3533, 34elrpd 9432 . . . . . . . . . . . . 13  |-  ( ph  ->  A  e.  RR+ )
3635ad3antrrr 481 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= ` 
1 ) )  /\  k  <  M )  ->  A  e.  RR+ )
372adantr 272 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= `  1 )
)  ->  M  e.  ZZ )
3837adantr 272 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= ` 
1 ) )  /\  k  <  M )  ->  M  e.  ZZ )
3925biimpri 132 . . . . . . . . . . . . . . . 16  |-  ( k  e.  ( ZZ>= `  1
)  ->  k  e.  NN )
4039adantl 273 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= `  1 )
)  ->  k  e.  NN )
4140nnzd 9126 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= `  1 )
)  ->  k  e.  ZZ )
4241adantr 272 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= ` 
1 ) )  /\  k  <  M )  -> 
k  e.  ZZ )
4338, 42zsubcld 9132 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= ` 
1 ) )  /\  k  <  M )  -> 
( M  -  k
)  e.  ZZ )
4436, 43rpexpcld 10399 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= ` 
1 ) )  /\  k  <  M )  -> 
( A ^ ( M  -  k )
)  e.  RR+ )
4544rpcnd 9436 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= ` 
1 ) )  /\  k  <  M )  -> 
( A ^ ( M  -  k )
)  e.  CC )
4644rpap0d 9440 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= ` 
1 ) )  /\  k  <  M )  -> 
( A ^ ( M  -  k )
) #  0 )
4732, 45, 46divclapd 8513 . . . . . . . . 9  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= ` 
1 ) )  /\  k  <  M )  -> 
( ( F `  M )  /  ( A ^ ( M  -  k ) ) )  e.  CC )
48 simplll 505 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= ` 
1 ) )  /\  -.  k  <  M )  ->  ph )
4937adantr 272 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= ` 
1 ) )  /\  -.  k  <  M )  ->  M  e.  ZZ )
5041adantr 272 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= ` 
1 ) )  /\  -.  k  <  M )  ->  k  e.  ZZ )
5116ad3antrrr 481 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= ` 
1 ) )  /\  -.  k  <  M )  ->  M  e.  RR )
5250zred 9127 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= ` 
1 ) )  /\  -.  k  <  M )  ->  k  e.  RR )
53 simpr 109 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= ` 
1 ) )  /\  -.  k  <  M )  ->  -.  k  <  M )
5451, 52, 53nltled 7847 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= ` 
1 ) )  /\  -.  k  <  M )  ->  M  <_  k
)
55 eluz2 9284 . . . . . . . . . . . 12  |-  ( k  e.  ( ZZ>= `  M
)  <->  ( M  e.  ZZ  /\  k  e.  ZZ  /\  M  <_ 
k ) )
5649, 50, 54, 55syl3anbrc 1148 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= ` 
1 ) )  /\  -.  k  <  M )  ->  k  e.  (
ZZ>= `  M ) )
5756, 8syl6eleqr 2209 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= ` 
1 ) )  /\  -.  k  <  M )  ->  k  e.  Z
)
5848, 57, 5syl2anc 406 . . . . . . . . 9  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= ` 
1 ) )  /\  -.  k  <  M )  ->  ( F `  k )  e.  CC )
59 zdclt 9082 . . . . . . . . . 10  |-  ( ( k  e.  ZZ  /\  M  e.  ZZ )  -> DECID  k  <  M )
6041, 37, 59syl2anc 406 . . . . . . . . 9  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= `  1 )
)  -> DECID  k  <  M )
6147, 58, 60ifcldadc 3469 . . . . . . . 8  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= `  1 )
)  ->  if (
k  <  M , 
( ( F `  M )  /  ( A ^ ( M  -  k ) ) ) ,  ( F `  k ) )  e.  CC )
6225, 61sylan2b 283 . . . . . . 7  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  if ( k  <  M ,  ( ( F `
 M )  / 
( A ^ ( M  -  k )
) ) ,  ( F `  k ) )  e.  CC )
6324, 62syldan 278 . . . . . 6  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= `  M )
)  ->  if (
k  <  M , 
( ( F `  M )  /  ( A ^ ( M  -  k ) ) ) ,  ( F `  k ) )  e.  CC )
64 breq1 3900 . . . . . . . 8  |-  ( i  =  k  ->  (
i  <  M  <->  k  <  M ) )
65 oveq2 5748 . . . . . . . . . 10  |-  ( i  =  k  ->  ( M  -  i )  =  ( M  -  k ) )
6665oveq2d 5756 . . . . . . . . 9  |-  ( i  =  k  ->  ( A ^ ( M  -  i ) )  =  ( A ^ ( M  -  k )
) )
6766oveq2d 5756 . . . . . . . 8  |-  ( i  =  k  ->  (
( F `  M
)  /  ( A ^ ( M  -  i ) ) )  =  ( ( F `
 M )  / 
( A ^ ( M  -  k )
) ) )
68 fveq2 5387 . . . . . . . 8  |-  ( i  =  k  ->  ( F `  i )  =  ( F `  k ) )
6964, 67, 68ifbieq12d 3466 . . . . . . 7  |-  ( i  =  k  ->  if ( i  <  M ,  ( ( F `
 M )  / 
( A ^ ( M  -  i )
) ) ,  ( F `  i ) )  =  if ( k  <  M , 
( ( F `  M )  /  ( A ^ ( M  -  k ) ) ) ,  ( F `  k ) ) )
70 eqid 2115 . . . . . . 7  |-  ( i  e.  NN  |->  if ( i  <  M , 
( ( F `  M )  /  ( A ^ ( M  -  i ) ) ) ,  ( F `  i ) ) )  =  ( i  e.  NN  |->  if ( i  <  M ,  ( ( F `  M
)  /  ( A ^ ( M  -  i ) ) ) ,  ( F `  i ) ) )
7169, 70fvmptg 5463 . . . . . 6  |-  ( ( k  e.  NN  /\  if ( k  <  M ,  ( ( F `
 M )  / 
( A ^ ( M  -  k )
) ) ,  ( F `  k ) )  e.  CC )  ->  ( ( i  e.  NN  |->  if ( i  <  M , 
( ( F `  M )  /  ( A ^ ( M  -  i ) ) ) ,  ( F `  i ) ) ) `
 k )  =  if ( k  < 
M ,  ( ( F `  M )  /  ( A ^
( M  -  k
) ) ) ,  ( F `  k
) ) )
7224, 63, 71syl2anc 406 . . . . 5  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= `  M )
)  ->  ( (
i  e.  NN  |->  if ( i  <  M ,  ( ( F `
 M )  / 
( A ^ ( M  -  i )
) ) ,  ( F `  i ) ) ) `  k
)  =  if ( k  <  M , 
( ( F `  M )  /  ( A ^ ( M  -  k ) ) ) ,  ( F `  k ) ) )
7317, 18, 21lensymd 7848 . . . . . 6  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= `  M )
)  ->  -.  k  <  M )
7473iffalsed 3452 . . . . 5  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= `  M )
)  ->  if (
k  <  M , 
( ( F `  M )  /  ( A ^ ( M  -  k ) ) ) ,  ( F `  k ) )  =  ( F `  k
) )
7572, 74eqtr2d 2149 . . . 4  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= `  M )
)  ->  ( F `  k )  =  ( ( i  e.  NN  |->  if ( i  <  M ,  ( ( F `
 M )  / 
( A ^ ( M  -  i )
) ) ,  ( F `  i ) ) ) `  k
) )
76 addcl 7709 . . . . 5  |-  ( ( x  e.  CC  /\  y  e.  CC )  ->  ( x  +  y )  e.  CC )
7776adantl 273 . . . 4  |-  ( ( ( ph  /\  1  <_  M )  /\  (
x  e.  CC  /\  y  e.  CC )
)  ->  ( x  +  y )  e.  CC )
782, 12, 75, 77seq3feq 10196 . . 3  |-  ( (
ph  /\  1  <_  M )  ->  seq M (  +  ,  F )  =  seq M (  +  ,  ( i  e.  NN  |->  if ( i  <  M , 
( ( F `  M )  /  ( A ^ ( M  -  i ) ) ) ,  ( F `  i ) ) ) ) )
7933adantr 272 . . . . 5  |-  ( (
ph  /\  1  <_  M )  ->  A  e.  RR )
80 cvgratz.4 . . . . . 6  |-  ( ph  ->  A  <  1 )
8180adantr 272 . . . . 5  |-  ( (
ph  /\  1  <_  M )  ->  A  <  1 )
8234adantr 272 . . . . 5  |-  ( (
ph  /\  1  <_  M )  ->  0  <  A )
8371eleq1d 2184 . . . . . . . 8  |-  ( ( k  e.  NN  /\  if ( k  <  M ,  ( ( F `
 M )  / 
( A ^ ( M  -  k )
) ) ,  ( F `  k ) )  e.  CC )  ->  ( ( ( i  e.  NN  |->  if ( i  <  M ,  ( ( F `
 M )  / 
( A ^ ( M  -  i )
) ) ,  ( F `  i ) ) ) `  k
)  e.  CC  <->  if (
k  <  M , 
( ( F `  M )  /  ( A ^ ( M  -  k ) ) ) ,  ( F `  k ) )  e.  CC ) )
8440, 61, 83syl2anc 406 . . . . . . 7  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= `  1 )
)  ->  ( (
( i  e.  NN  |->  if ( i  <  M ,  ( ( F `
 M )  / 
( A ^ ( M  -  i )
) ) ,  ( F `  i ) ) ) `  k
)  e.  CC  <->  if (
k  <  M , 
( ( F `  M )  /  ( A ^ ( M  -  k ) ) ) ,  ( F `  k ) )  e.  CC ) )
8561, 84mpbird 166 . . . . . 6  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= `  1 )
)  ->  ( (
i  e.  NN  |->  if ( i  <  M ,  ( ( F `
 M )  / 
( A ^ ( M  -  i )
) ) ,  ( F `  i ) ) ) `  k
)  e.  CC )
8625, 85sylan2b 283 . . . . 5  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  (
( i  e.  NN  |->  if ( i  <  M ,  ( ( F `
 M )  / 
( A ^ ( M  -  i )
) ) ,  ( F `  i ) ) ) `  k
)  e.  CC )
8731ad3antrrr 481 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  <  M )  ->  ( F `  M )  e.  CC )
8835ad3antrrr 481 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  <  M )  ->  A  e.  RR+ )
892ad2antrr 477 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  <  M )  ->  M  e.  ZZ )
9025, 41sylan2b 283 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  k  e.  ZZ )
9190adantr 272 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  <  M )  ->  k  e.  ZZ )
9291peano2zd 9130 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  <  M )  ->  ( k  +  1 )  e.  ZZ )
9389, 92zsubcld 9132 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  <  M )  ->  ( M  -  ( k  +  1 ) )  e.  ZZ )
9488, 93rpexpcld 10399 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  <  M )  ->  ( A ^
( M  -  (
k  +  1 ) ) )  e.  RR+ )
9594rpcnd 9436 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  <  M )  ->  ( A ^
( M  -  (
k  +  1 ) ) )  e.  CC )
9694rpap0d 9440 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  <  M )  ->  ( A ^
( M  -  (
k  +  1 ) ) ) #  0 )
9787, 95, 96divclapd 8513 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  <  M )  ->  ( ( F `
 M )  / 
( A ^ ( M  -  ( k  +  1 ) ) ) )  e.  CC )
98 fveq2 5387 . . . . . . . . . . . 12  |-  ( a  =  ( k  +  1 )  ->  ( F `  a )  =  ( F `  ( k  +  1 ) ) )
9998eleq1d 2184 . . . . . . . . . . 11  |-  ( a  =  ( k  +  1 )  ->  (
( F `  a
)  e.  CC  <->  ( F `  ( k  +  1 ) )  e.  CC ) )
100 fveq2 5387 . . . . . . . . . . . . . . 15  |-  ( k  =  a  ->  ( F `  k )  =  ( F `  a ) )
101100eleq1d 2184 . . . . . . . . . . . . . 14  |-  ( k  =  a  ->  (
( F `  k
)  e.  CC  <->  ( F `  a )  e.  CC ) )
102101cbvralv 2629 . . . . . . . . . . . . 13  |-  ( A. k  e.  Z  ( F `  k )  e.  CC  <->  A. a  e.  Z  ( F `  a )  e.  CC )
1036, 102sylib 121 . . . . . . . . . . . 12  |-  ( ph  ->  A. a  e.  Z  ( F `  a )  e.  CC )
104103ad3antrrr 481 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  -.  ( k  +  1 )  <  M
)  ->  A. a  e.  Z  ( F `  a )  e.  CC )
1052ad2antrr 477 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  -.  ( k  +  1 )  <  M
)  ->  M  e.  ZZ )
106 peano2nn 8692 . . . . . . . . . . . . . . . 16  |-  ( k  e.  NN  ->  (
k  +  1 )  e.  NN )
107106adantl 273 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  (
k  +  1 )  e.  NN )
108107nnzd 9126 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  (
k  +  1 )  e.  ZZ )
109108adantr 272 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  -.  ( k  +  1 )  <  M
)  ->  ( k  +  1 )  e.  ZZ )
11016ad3antrrr 481 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  -.  ( k  +  1 )  <  M
)  ->  M  e.  RR )
111107nnred 8693 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  (
k  +  1 )  e.  RR )
112111adantr 272 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  -.  ( k  +  1 )  <  M
)  ->  ( k  +  1 )  e.  RR )
113 simpr 109 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  -.  ( k  +  1 )  <  M
)  ->  -.  (
k  +  1 )  <  M )
114110, 112, 113nltled 7847 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  -.  ( k  +  1 )  <  M
)  ->  M  <_  ( k  +  1 ) )
115 eluz2 9284 . . . . . . . . . . . . 13  |-  ( ( k  +  1 )  e.  ( ZZ>= `  M
)  <->  ( M  e.  ZZ  /\  ( k  +  1 )  e.  ZZ  /\  M  <_ 
( k  +  1 ) ) )
116105, 109, 114, 115syl3anbrc 1148 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  -.  ( k  +  1 )  <  M
)  ->  ( k  +  1 )  e.  ( ZZ>= `  M )
)
117116, 8syl6eleqr 2209 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  -.  ( k  +  1 )  <  M
)  ->  ( k  +  1 )  e.  Z )
11899, 104, 117rspcdva 2766 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  -.  ( k  +  1 )  <  M
)  ->  ( F `  ( k  +  1 ) )  e.  CC )
1192adantr 272 . . . . . . . . . . 11  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  M  e.  ZZ )
120 zdclt 9082 . . . . . . . . . . 11  |-  ( ( ( k  +  1 )  e.  ZZ  /\  M  e.  ZZ )  -> DECID  ( k  +  1 )  <  M )
121108, 119, 120syl2anc 406 . . . . . . . . . 10  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  -> DECID  ( k  +  1 )  <  M )
12297, 118, 121ifcldadc 3469 . . . . . . . . 9  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  if ( ( k  +  1 )  <  M ,  ( ( F `
 M )  / 
( A ^ ( M  -  ( k  +  1 ) ) ) ) ,  ( F `  ( k  +  1 ) ) )  e.  CC )
123122abscld 10904 . . . . . . . 8  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  ( abs `  if ( ( k  +  1 )  <  M ,  ( ( F `  M
)  /  ( A ^ ( M  -  ( k  +  1 ) ) ) ) ,  ( F `  ( k  +  1 ) ) ) )  e.  RR )
12416recnd 7758 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  M  e.  CC )
125124ad2antrr 477 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  M  e.  CC )
126 simpr 109 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  k  e.  NN )
127126nncnd 8694 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  k  e.  CC )
128 1cnd 7746 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  1  e.  CC )
129125, 127, 128subsub4d 8068 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  (
( M  -  k
)  -  1 )  =  ( M  -  ( k  +  1 ) ) )
130129oveq2d 5756 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  ( A ^ ( ( M  -  k )  - 
1 ) )  =  ( A ^ ( M  -  ( k  +  1 ) ) ) )
13133recnd 7758 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  A  e.  CC )
132131ad2antrr 477 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  A  e.  CC )
13333, 34gt0ap0d 8354 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  A #  0 )
134133ad2antrr 477 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  A #  0 )
135119, 90zsubcld 9132 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  ( M  -  k )  e.  ZZ )
136132, 134, 135expm1apd 10385 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  ( A ^ ( ( M  -  k )  - 
1 ) )  =  ( ( A ^
( M  -  k
) )  /  A
) )
137130, 136eqtr3d 2150 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  ( A ^ ( M  -  ( k  +  1 ) ) )  =  ( ( A ^
( M  -  k
) )  /  A
) )
138137oveq2d 5756 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  (
( F `  M
)  /  ( A ^ ( M  -  ( k  +  1 ) ) ) )  =  ( ( F `
 M )  / 
( ( A ^
( M  -  k
) )  /  A
) ) )
139138adantr 272 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  <  M )  ->  ( ( F `
 M )  / 
( A ^ ( M  -  ( k  +  1 ) ) ) )  =  ( ( F `  M
)  /  ( ( A ^ ( M  -  k ) )  /  A ) ) )
140 simpr 109 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  <  M )  ->  ( k  +  1 )  <  M
)
141140iftrued 3449 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  <  M )  ->  if ( ( k  +  1 )  <  M ,  ( ( F `  M
)  /  ( A ^ ( M  -  ( k  +  1 ) ) ) ) ,  ( F `  ( k  +  1 ) ) )  =  ( ( F `  M )  /  ( A ^ ( M  -  ( k  +  1 ) ) ) ) )
142126nnred 8693 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  k  e.  RR )
143142adantr 272 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  <  M )  ->  k  e.  RR )
144 peano2re 7862 . . . . . . . . . . . . . . . 16  |-  ( k  e.  RR  ->  (
k  +  1 )  e.  RR )
145143, 144syl 14 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  <  M )  ->  ( k  +  1 )  e.  RR )
14616ad3antrrr 481 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  <  M )  ->  M  e.  RR )
147143ltp1d 8648 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  <  M )  ->  k  <  (
k  +  1 ) )
148143, 145, 146, 147, 140lttrd 7852 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  <  M )  ->  k  <  M
)
149148iftrued 3449 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  <  M )  ->  if ( k  <  M ,  ( ( F `  M
)  /  ( A ^ ( M  -  k ) ) ) ,  ( F `  k ) )  =  ( ( F `  M )  /  ( A ^ ( M  -  k ) ) ) )
150149oveq2d 5756 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  <  M )  ->  ( A  x.  if ( k  <  M ,  ( ( F `
 M )  / 
( A ^ ( M  -  k )
) ) ,  ( F `  k ) ) )  =  ( A  x.  ( ( F `  M )  /  ( A ^
( M  -  k
) ) ) ) )
15131ad2antrr 477 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  ( F `  M )  e.  CC )
152132, 134, 135expclzapd 10380 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  ( A ^ ( M  -  k ) )  e.  CC )
153132, 134, 135expap0d 10381 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  ( A ^ ( M  -  k ) ) #  0 )
154151, 152, 132, 153, 134divdivap2d 8546 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  (
( F `  M
)  /  ( ( A ^ ( M  -  k ) )  /  A ) )  =  ( ( ( F `  M )  x.  A )  / 
( A ^ ( M  -  k )
) ) )
155151, 132mulcomd 7751 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  (
( F `  M
)  x.  A )  =  ( A  x.  ( F `  M ) ) )
156155oveq1d 5755 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  (
( ( F `  M )  x.  A
)  /  ( A ^ ( M  -  k ) ) )  =  ( ( A  x.  ( F `  M ) )  / 
( A ^ ( M  -  k )
) ) )
157132, 151, 152, 153divassapd 8549 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  (
( A  x.  ( F `  M )
)  /  ( A ^ ( M  -  k ) ) )  =  ( A  x.  ( ( F `  M )  /  ( A ^ ( M  -  k ) ) ) ) )
158154, 156, 1573eqtrd 2152 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  (
( F `  M
)  /  ( ( A ^ ( M  -  k ) )  /  A ) )  =  ( A  x.  ( ( F `  M )  /  ( A ^ ( M  -  k ) ) ) ) )
159158adantr 272 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  <  M )  ->  ( ( F `
 M )  / 
( ( A ^
( M  -  k
) )  /  A
) )  =  ( A  x.  ( ( F `  M )  /  ( A ^
( M  -  k
) ) ) ) )
160150, 159eqtr4d 2151 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  <  M )  ->  ( A  x.  if ( k  <  M ,  ( ( F `
 M )  / 
( A ^ ( M  -  k )
) ) ,  ( F `  k ) ) )  =  ( ( F `  M
)  /  ( ( A ^ ( M  -  k ) )  /  A ) ) )
161139, 141, 1603eqtr4d 2158 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  <  M )  ->  if ( ( k  +  1 )  <  M ,  ( ( F `  M
)  /  ( A ^ ( M  -  ( k  +  1 ) ) ) ) ,  ( F `  ( k  +  1 ) ) )  =  ( A  x.  if ( k  <  M ,  ( ( F `
 M )  / 
( A ^ ( M  -  k )
) ) ,  ( F `  k ) ) ) )
162161fveq2d 5391 . . . . . . . . 9  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  <  M )  ->  ( abs `  if ( ( k  +  1 )  <  M ,  ( ( F `
 M )  / 
( A ^ ( M  -  ( k  +  1 ) ) ) ) ,  ( F `  ( k  +  1 ) ) ) )  =  ( abs `  ( A  x.  if ( k  <  M ,  ( ( F `  M
)  /  ( A ^ ( M  -  k ) ) ) ,  ( F `  k ) ) ) ) )
163132, 62absmuld 10917 . . . . . . . . . 10  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  ( abs `  ( A  x.  if ( k  <  M ,  ( ( F `
 M )  / 
( A ^ ( M  -  k )
) ) ,  ( F `  k ) ) ) )  =  ( ( abs `  A
)  x.  ( abs `  if ( k  < 
M ,  ( ( F `  M )  /  ( A ^
( M  -  k
) ) ) ,  ( F `  k
) ) ) ) )
164163adantr 272 . . . . . . . . 9  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  <  M )  ->  ( abs `  ( A  x.  if (
k  <  M , 
( ( F `  M )  /  ( A ^ ( M  -  k ) ) ) ,  ( F `  k ) ) ) )  =  ( ( abs `  A )  x.  ( abs `  if ( k  <  M ,  ( ( F `
 M )  / 
( A ^ ( M  -  k )
) ) ,  ( F `  k ) ) ) ) )
16535rpge0d 9438 . . . . . . . . . . . 12  |-  ( ph  ->  0  <_  A )
16633, 165absidd 10890 . . . . . . . . . . 11  |-  ( ph  ->  ( abs `  A
)  =  A )
167166oveq1d 5755 . . . . . . . . . 10  |-  ( ph  ->  ( ( abs `  A
)  x.  ( abs `  if ( k  < 
M ,  ( ( F `  M )  /  ( A ^
( M  -  k
) ) ) ,  ( F `  k
) ) ) )  =  ( A  x.  ( abs `  if ( k  <  M , 
( ( F `  M )  /  ( A ^ ( M  -  k ) ) ) ,  ( F `  k ) ) ) ) )
168167ad3antrrr 481 . . . . . . . . 9  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  <  M )  ->  ( ( abs `  A )  x.  ( abs `  if ( k  <  M ,  ( ( F `  M
)  /  ( A ^ ( M  -  k ) ) ) ,  ( F `  k ) ) ) )  =  ( A  x.  ( abs `  if ( k  <  M ,  ( ( F `
 M )  / 
( A ^ ( M  -  k )
) ) ,  ( F `  k ) ) ) ) )
169162, 164, 1683eqtrd 2152 . . . . . . . 8  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  <  M )  ->  ( abs `  if ( ( k  +  1 )  <  M ,  ( ( F `
 M )  / 
( A ^ ( M  -  ( k  +  1 ) ) ) ) ,  ( F `  ( k  +  1 ) ) ) )  =  ( A  x.  ( abs `  if ( k  < 
M ,  ( ( F `  M )  /  ( A ^
( M  -  k
) ) ) ,  ( F `  k
) ) ) ) )
170 eqle 7819 . . . . . . . 8  |-  ( ( ( abs `  if ( ( k  +  1 )  <  M ,  ( ( F `
 M )  / 
( A ^ ( M  -  ( k  +  1 ) ) ) ) ,  ( F `  ( k  +  1 ) ) ) )  e.  RR  /\  ( abs `  if ( ( k  +  1 )  <  M ,  ( ( F `
 M )  / 
( A ^ ( M  -  ( k  +  1 ) ) ) ) ,  ( F `  ( k  +  1 ) ) ) )  =  ( A  x.  ( abs `  if ( k  < 
M ,  ( ( F `  M )  /  ( A ^
( M  -  k
) ) ) ,  ( F `  k
) ) ) ) )  ->  ( abs `  if ( ( k  +  1 )  < 
M ,  ( ( F `  M )  /  ( A ^
( M  -  (
k  +  1 ) ) ) ) ,  ( F `  (
k  +  1 ) ) ) )  <_ 
( A  x.  ( abs `  if ( k  <  M ,  ( ( F `  M
)  /  ( A ^ ( M  -  k ) ) ) ,  ( F `  k ) ) ) ) )
171123, 169, 170syl2an2r 567 . . . . . . 7  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  <  M )  ->  ( abs `  if ( ( k  +  1 )  <  M ,  ( ( F `
 M )  / 
( A ^ ( M  -  ( k  +  1 ) ) ) ) ,  ( F `  ( k  +  1 ) ) ) )  <_  ( A  x.  ( abs `  if ( k  < 
M ,  ( ( F `  M )  /  ( A ^
( M  -  k
) ) ) ,  ( F `  k
) ) ) ) )
17216ad2antrr 477 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  M  e.  RR )
173111, 172lttri3d 7842 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  (
( k  +  1 )  =  M  <->  ( -.  ( k  +  1 )  <  M  /\  -.  M  <  ( k  +  1 ) ) ) )
174173simprbda 378 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  =  M )  ->  -.  ( k  +  1 )  < 
M )
175174iffalsed 3452 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  =  M )  ->  if ( ( k  +  1 )  <  M ,  ( ( F `  M
)  /  ( A ^ ( M  -  ( k  +  1 ) ) ) ) ,  ( F `  ( k  +  1 ) ) )  =  ( F `  (
k  +  1 ) ) )
176 simpr 109 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  =  M )  ->  ( k  +  1 )  =  M )
177176fveq2d 5391 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  =  M )  ->  ( F `  ( k  +  1 ) )  =  ( F `  M ) )
178175, 177eqtrd 2148 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  =  M )  ->  if ( ( k  +  1 )  <  M ,  ( ( F `  M
)  /  ( A ^ ( M  -  ( k  +  1 ) ) ) ) ,  ( F `  ( k  +  1 ) ) )  =  ( F `  M
) )
179178fveq2d 5391 . . . . . . . . 9  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  =  M )  ->  ( abs `  if ( ( k  +  1 )  <  M ,  ( ( F `
 M )  / 
( A ^ ( M  -  ( k  +  1 ) ) ) ) ,  ( F `  ( k  +  1 ) ) ) )  =  ( abs `  ( F `
 M ) ) )
180142adantr 272 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  =  M )  ->  k  e.  RR )
181180ltp1d 8648 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  =  M )  ->  k  <  (
k  +  1 ) )
182 breq2 3901 . . . . . . . . . . . . . . . 16  |-  ( ( k  +  1 )  =  M  ->  (
k  <  ( k  +  1 )  <->  k  <  M ) )
183182adantl 273 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  =  M )  ->  ( k  < 
( k  +  1 )  <->  k  <  M
) )
184181, 183mpbid 146 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  =  M )  ->  k  <  M
)
185184iftrued 3449 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  =  M )  ->  if ( k  <  M ,  ( ( F `  M
)  /  ( A ^ ( M  -  k ) ) ) ,  ( F `  k ) )  =  ( ( F `  M )  /  ( A ^ ( M  -  k ) ) ) )
186176oveq1d 5755 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  =  M )  ->  ( ( k  +  1 )  -  k )  =  ( M  -  k ) )
187127adantr 272 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  =  M )  ->  k  e.  CC )
188 1cnd 7746 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  =  M )  ->  1  e.  CC )
189187, 188pncan2d 8039 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  =  M )  ->  ( ( k  +  1 )  -  k )  =  1 )
190186, 189eqtr3d 2150 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  =  M )  ->  ( M  -  k )  =  1 )
191190oveq2d 5756 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  =  M )  ->  ( A ^
( M  -  k
) )  =  ( A ^ 1 ) )
192132adantr 272 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  =  M )  ->  A  e.  CC )
193192exp1d 10370 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  =  M )  ->  ( A ^
1 )  =  A )
194191, 193eqtrd 2148 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  =  M )  ->  ( A ^
( M  -  k
) )  =  A )
195194oveq2d 5756 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  =  M )  ->  ( ( F `
 M )  / 
( A ^ ( M  -  k )
) )  =  ( ( F `  M
)  /  A ) )
196185, 195eqtrd 2148 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  =  M )  ->  if ( k  <  M ,  ( ( F `  M
)  /  ( A ^ ( M  -  k ) ) ) ,  ( F `  k ) )  =  ( ( F `  M )  /  A
) )
197196oveq2d 5756 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  =  M )  ->  ( A  x.  if ( k  <  M ,  ( ( F `
 M )  / 
( A ^ ( M  -  k )
) ) ,  ( F `  k ) ) )  =  ( A  x.  ( ( F `  M )  /  A ) ) )
19831, 131, 133divcanap2d 8515 . . . . . . . . . . . 12  |-  ( ph  ->  ( A  x.  (
( F `  M
)  /  A ) )  =  ( F `
 M ) )
199198ad3antrrr 481 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  =  M )  ->  ( A  x.  ( ( F `  M )  /  A
) )  =  ( F `  M ) )
200197, 199eqtrd 2148 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  =  M )  ->  ( A  x.  if ( k  <  M ,  ( ( F `
 M )  / 
( A ^ ( M  -  k )
) ) ,  ( F `  k ) ) )  =  ( F `  M ) )
201200fveq2d 5391 . . . . . . . . 9  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  =  M )  ->  ( abs `  ( A  x.  if (
k  <  M , 
( ( F `  M )  /  ( A ^ ( M  -  k ) ) ) ,  ( F `  k ) ) ) )  =  ( abs `  ( F `  M
) ) )
202167ad2antrr 477 . . . . . . . . . . 11  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  (
( abs `  A
)  x.  ( abs `  if ( k  < 
M ,  ( ( F `  M )  /  ( A ^
( M  -  k
) ) ) ,  ( F `  k
) ) ) )  =  ( A  x.  ( abs `  if ( k  <  M , 
( ( F `  M )  /  ( A ^ ( M  -  k ) ) ) ,  ( F `  k ) ) ) ) )
203163, 202eqtrd 2148 . . . . . . . . . 10  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  ( abs `  ( A  x.  if ( k  <  M ,  ( ( F `
 M )  / 
( A ^ ( M  -  k )
) ) ,  ( F `  k ) ) ) )  =  ( A  x.  ( abs `  if ( k  <  M ,  ( ( F `  M
)  /  ( A ^ ( M  -  k ) ) ) ,  ( F `  k ) ) ) ) )
204203adantr 272 . . . . . . . . 9  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  =  M )  ->  ( abs `  ( A  x.  if (
k  <  M , 
( ( F `  M )  /  ( A ^ ( M  -  k ) ) ) ,  ( F `  k ) ) ) )  =  ( A  x.  ( abs `  if ( k  <  M ,  ( ( F `
 M )  / 
( A ^ ( M  -  k )
) ) ,  ( F `  k ) ) ) ) )
205179, 201, 2043eqtr2d 2154 . . . . . . . 8  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  =  M )  ->  ( abs `  if ( ( k  +  1 )  <  M ,  ( ( F `
 M )  / 
( A ^ ( M  -  ( k  +  1 ) ) ) ) ,  ( F `  ( k  +  1 ) ) ) )  =  ( A  x.  ( abs `  if ( k  < 
M ,  ( ( F `  M )  /  ( A ^
( M  -  k
) ) ) ,  ( F `  k
) ) ) ) )
206123, 205, 170syl2an2r 567 . . . . . . 7  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  =  M )  ->  ( abs `  if ( ( k  +  1 )  <  M ,  ( ( F `
 M )  / 
( A ^ ( M  -  ( k  +  1 ) ) ) ) ,  ( F `  ( k  +  1 ) ) ) )  <_  ( A  x.  ( abs `  if ( k  < 
M ,  ( ( F `  M )  /  ( A ^
( M  -  k
) ) ) ,  ( F `  k
) ) ) ) )
207 simplll 505 . . . . . . . . 9  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  M  <  ( k  +  1 ) )  ->  ph )
208119adantr 272 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  M  <  ( k  +  1 ) )  ->  M  e.  ZZ )
20990adantr 272 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  M  <  ( k  +  1 ) )  ->  k  e.  ZZ )
210 simpr 109 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  M  <  ( k  +  1 ) )  ->  M  <  (
k  +  1 ) )
211 zleltp1 9063 . . . . . . . . . . . . 13  |-  ( ( M  e.  ZZ  /\  k  e.  ZZ )  ->  ( M  <_  k  <->  M  <  ( k  +  1 ) ) )
212119, 209, 211syl2an2r 567 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  M  <  ( k  +  1 ) )  ->  ( M  <_ 
k  <->  M  <  ( k  +  1 ) ) )
213210, 212mpbird 166 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  M  <  ( k  +  1 ) )  ->  M  <_  k
)
214208, 209, 213, 55syl3anbrc 1148 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  M  <  ( k  +  1 ) )  ->  k  e.  (
ZZ>= `  M ) )
215214, 8syl6eleqr 2209 . . . . . . . . 9  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  M  <  ( k  +  1 ) )  ->  k  e.  Z
)
216 cvgratz.7 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  Z )  ->  ( abs `  ( F `  ( k  +  1 ) ) )  <_ 
( A  x.  ( abs `  ( F `  k ) ) ) )
217207, 215, 216syl2anc 406 . . . . . . . 8  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  M  <  ( k  +  1 ) )  ->  ( abs `  ( F `  ( k  +  1 ) ) )  <_  ( A  x.  ( abs `  ( F `  k )
) ) )
218172adantr 272 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  M  <  ( k  +  1 ) )  ->  M  e.  RR )
219111adantr 272 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  M  <  ( k  +  1 ) )  ->  ( k  +  1 )  e.  RR )
220218, 219, 210ltnsymd 7846 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  M  <  ( k  +  1 ) )  ->  -.  ( k  +  1 )  < 
M )
221220iffalsed 3452 . . . . . . . . 9  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  M  <  ( k  +  1 ) )  ->  if ( ( k  +  1 )  <  M ,  ( ( F `  M
)  /  ( A ^ ( M  -  ( k  +  1 ) ) ) ) ,  ( F `  ( k  +  1 ) ) )  =  ( F `  (
k  +  1 ) ) )
222221fveq2d 5391 . . . . . . . 8  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  M  <  ( k  +  1 ) )  ->  ( abs `  if ( ( k  +  1 )  <  M ,  ( ( F `
 M )  / 
( A ^ ( M  -  ( k  +  1 ) ) ) ) ,  ( F `  ( k  +  1 ) ) ) )  =  ( abs `  ( F `
 ( k  +  1 ) ) ) )
223142adantr 272 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  M  <  ( k  +  1 ) )  ->  k  e.  RR )
224218, 223, 213lensymd 7848 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  M  <  ( k  +  1 ) )  ->  -.  k  <  M )
225224iffalsed 3452 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  M  <  ( k  +  1 ) )  ->  if ( k  <  M ,  ( ( F `  M
)  /  ( A ^ ( M  -  k ) ) ) ,  ( F `  k ) )  =  ( F `  k
) )
226225fveq2d 5391 . . . . . . . . 9  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  M  <  ( k  +  1 ) )  ->  ( abs `  if ( k  <  M ,  ( ( F `
 M )  / 
( A ^ ( M  -  k )
) ) ,  ( F `  k ) ) )  =  ( abs `  ( F `
 k ) ) )
227226oveq2d 5756 . . . . . . . 8  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  M  <  ( k  +  1 ) )  ->  ( A  x.  ( abs `  if ( k  <  M , 
( ( F `  M )  /  ( A ^ ( M  -  k ) ) ) ,  ( F `  k ) ) ) )  =  ( A  x.  ( abs `  ( F `  k )
) ) )
228217, 222, 2273brtr4d 3928 . . . . . . 7  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  M  <  ( k  +  1 ) )  ->  ( abs `  if ( ( k  +  1 )  <  M ,  ( ( F `
 M )  / 
( A ^ ( M  -  ( k  +  1 ) ) ) ) ,  ( F `  ( k  +  1 ) ) ) )  <_  ( A  x.  ( abs `  if ( k  < 
M ,  ( ( F `  M )  /  ( A ^
( M  -  k
) ) ) ,  ( F `  k
) ) ) ) )
229 ztri3or 9051 . . . . . . . 8  |-  ( ( ( k  +  1 )  e.  ZZ  /\  M  e.  ZZ )  ->  ( ( k  +  1 )  <  M  \/  ( k  +  1 )  =  M  \/  M  <  ( k  +  1 ) ) )
230108, 119, 229syl2anc 406 . . . . . . 7  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  (
( k  +  1 )  <  M  \/  ( k  +  1 )  =  M  \/  M  <  ( k  +  1 ) ) )
231171, 206, 228, 230mpjao3dan 1268 . . . . . 6  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  ( abs `  if ( ( k  +  1 )  <  M ,  ( ( F `  M
)  /  ( A ^ ( M  -  ( k  +  1 ) ) ) ) ,  ( F `  ( k  +  1 ) ) ) )  <_  ( A  x.  ( abs `  if ( k  <  M , 
( ( F `  M )  /  ( A ^ ( M  -  k ) ) ) ,  ( F `  k ) ) ) ) )
232 breq1 3900 . . . . . . . . . 10  |-  ( i  =  ( k  +  1 )  ->  (
i  <  M  <->  ( k  +  1 )  < 
M ) )
233 oveq2 5748 . . . . . . . . . . . 12  |-  ( i  =  ( k  +  1 )  ->  ( M  -  i )  =  ( M  -  ( k  +  1 ) ) )
234233oveq2d 5756 . . . . . . . . . . 11  |-  ( i  =  ( k  +  1 )  ->  ( A ^ ( M  -  i ) )  =  ( A ^ ( M  -  ( k  +  1 ) ) ) )
235234oveq2d 5756 . . . . . . . . . 10  |-  ( i  =  ( k  +  1 )  ->  (
( F `  M
)  /  ( A ^ ( M  -  i ) ) )  =  ( ( F `
 M )  / 
( A ^ ( M  -  ( k  +  1 ) ) ) ) )
236 fveq2 5387 . . . . . . . . . 10  |-  ( i  =  ( k  +  1 )  ->  ( F `  i )  =  ( F `  ( k  +  1 ) ) )
237232, 235, 236ifbieq12d 3466 . . . . . . . . 9  |-  ( i  =  ( k  +  1 )  ->  if ( i  <  M ,  ( ( F `
 M )  / 
( A ^ ( M  -  i )
) ) ,  ( F `  i ) )  =  if ( ( k  +  1 )  <  M , 
( ( F `  M )  /  ( A ^ ( M  -  ( k  +  1 ) ) ) ) ,  ( F `  ( k  +  1 ) ) ) )
238237, 70fvmptg 5463 . . . . . . . 8  |-  ( ( ( k  +  1 )  e.  NN  /\  if ( ( k  +  1 )  <  M ,  ( ( F `
 M )  / 
( A ^ ( M  -  ( k  +  1 ) ) ) ) ,  ( F `  ( k  +  1 ) ) )  e.  CC )  ->  ( ( i  e.  NN  |->  if ( i  <  M , 
( ( F `  M )  /  ( A ^ ( M  -  i ) ) ) ,  ( F `  i ) ) ) `
 ( k  +  1 ) )  =  if ( ( k  +  1 )  < 
M ,  ( ( F `  M )  /  ( A ^
( M  -  (
k  +  1 ) ) ) ) ,  ( F `  (
k  +  1 ) ) ) )
239107, 122, 238syl2anc 406 . . . . . . 7  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  (
( i  e.  NN  |->  if ( i  <  M ,  ( ( F `
 M )  / 
( A ^ ( M  -  i )
) ) ,  ( F `  i ) ) ) `  (
k  +  1 ) )  =  if ( ( k  +  1 )  <  M , 
( ( F `  M )  /  ( A ^ ( M  -  ( k  +  1 ) ) ) ) ,  ( F `  ( k  +  1 ) ) ) )
240239fveq2d 5391 . . . . . 6  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  ( abs `  ( ( i  e.  NN  |->  if ( i  <  M , 
( ( F `  M )  /  ( A ^ ( M  -  i ) ) ) ,  ( F `  i ) ) ) `
 ( k  +  1 ) ) )  =  ( abs `  if ( ( k  +  1 )  <  M ,  ( ( F `
 M )  / 
( A ^ ( M  -  ( k  +  1 ) ) ) ) ,  ( F `  ( k  +  1 ) ) ) ) )
241126, 62, 71syl2anc 406 . . . . . . . 8  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  (
( i  e.  NN  |->  if ( i  <  M ,  ( ( F `
 M )  / 
( A ^ ( M  -  i )
) ) ,  ( F `  i ) ) ) `  k
)  =  if ( k  <  M , 
( ( F `  M )  /  ( A ^ ( M  -  k ) ) ) ,  ( F `  k ) ) )
242241fveq2d 5391 . . . . . . 7  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  ( abs `  ( ( i  e.  NN  |->  if ( i  <  M , 
( ( F `  M )  /  ( A ^ ( M  -  i ) ) ) ,  ( F `  i ) ) ) `
 k ) )  =  ( abs `  if ( k  <  M ,  ( ( F `
 M )  / 
( A ^ ( M  -  k )
) ) ,  ( F `  k ) ) ) )
243242oveq2d 5756 . . . . . 6  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  ( A  x.  ( abs `  ( ( i  e.  NN  |->  if ( i  <  M ,  ( ( F `  M
)  /  ( A ^ ( M  -  i ) ) ) ,  ( F `  i ) ) ) `
 k ) ) )  =  ( A  x.  ( abs `  if ( k  <  M ,  ( ( F `
 M )  / 
( A ^ ( M  -  k )
) ) ,  ( F `  k ) ) ) ) )
244231, 240, 2433brtr4d 3928 . . . . 5  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  ( abs `  ( ( i  e.  NN  |->  if ( i  <  M , 
( ( F `  M )  /  ( A ^ ( M  -  i ) ) ) ,  ( F `  i ) ) ) `
 ( k  +  1 ) ) )  <_  ( A  x.  ( abs `  ( ( i  e.  NN  |->  if ( i  <  M ,  ( ( F `
 M )  / 
( A ^ ( M  -  i )
) ) ,  ( F `  i ) ) ) `  k
) ) ) )
24579, 81, 82, 86, 244cvgratnn 11251 . . . 4  |-  ( (
ph  /\  1  <_  M )  ->  seq 1
(  +  ,  ( i  e.  NN  |->  if ( i  <  M ,  ( ( F `
 M )  / 
( A ^ ( M  -  i )
) ) ,  ( F `  i ) ) ) )  e. 
dom 
~~>  )
246 eqid 2115 . . . . 5  |-  ( ZZ>= ` 
1 )  =  (
ZZ>= `  1 )
247 1zzd 9035 . . . . . 6  |-  ( (
ph  /\  1  <_  M )  ->  1  e.  ZZ )
248 simpr 109 . . . . . 6  |-  ( (
ph  /\  1  <_  M )  ->  1  <_  M )
249 eluz2 9284 . . . . . 6  |-  ( M  e.  ( ZZ>= `  1
)  <->  ( 1  e.  ZZ  /\  M  e.  ZZ  /\  1  <_  M ) )
250247, 2, 248, 249syl3anbrc 1148 . . . . 5  |-  ( (
ph  /\  1  <_  M )  ->  M  e.  ( ZZ>= `  1 )
)
251246, 250, 85iserex 11059 . . . 4  |-  ( (
ph  /\  1  <_  M )  ->  (  seq 1 (  +  , 
( i  e.  NN  |->  if ( i  <  M ,  ( ( F `
 M )  / 
( A ^ ( M  -  i )
) ) ,  ( F `  i ) ) ) )  e. 
dom 
~~> 
<->  seq M (  +  ,  ( i  e.  NN  |->  if ( i  <  M ,  ( ( F `  M
)  /  ( A ^ ( M  -  i ) ) ) ,  ( F `  i ) ) ) )  e.  dom  ~~>  ) )
252245, 251mpbid 146 . . 3  |-  ( (
ph  /\  1  <_  M )  ->  seq M (  +  ,  ( i  e.  NN  |->  if ( i  <  M , 
( ( F `  M )  /  ( A ^ ( M  -  i ) ) ) ,  ( F `  i ) ) ) )  e.  dom  ~~>  )
25378, 252eqeltrd 2192 . 2  |-  ( (
ph  /\  1  <_  M )  ->  seq M (  +  ,  F )  e.  dom  ~~>  )
25433adantr 272 . . . 4  |-  ( (
ph  /\  M  <_  1 )  ->  A  e.  RR )
25580adantr 272 . . . 4  |-  ( (
ph  /\  M  <_  1 )  ->  A  <  1 )
25634adantr 272 . . . 4  |-  ( (
ph  /\  M  <_  1 )  ->  0  <  A )
2571adantr 272 . . . . . . 7  |-  ( (
ph  /\  M  <_  1 )  ->  M  e.  ZZ )
258257adantr 272 . . . . . 6  |-  ( ( ( ph  /\  M  <_  1 )  /\  k  e.  NN )  ->  M  e.  ZZ )
259 nnz 9027 . . . . . . 7  |-  ( k  e.  NN  ->  k  e.  ZZ )
260259adantl 273 . . . . . 6  |-  ( ( ( ph  /\  M  <_  1 )  /\  k  e.  NN )  ->  k  e.  ZZ )
261258zred 9127 . . . . . . 7  |-  ( ( ( ph  /\  M  <_  1 )  /\  k  e.  NN )  ->  M  e.  RR )
262 1red 7745 . . . . . . 7  |-  ( ( ( ph  /\  M  <_  1 )  /\  k  e.  NN )  ->  1  e.  RR )
263260zred 9127 . . . . . . 7  |-  ( ( ( ph  /\  M  <_  1 )  /\  k  e.  NN )  ->  k  e.  RR )
264 simplr 502 . . . . . . 7  |-  ( ( ( ph  /\  M  <_  1 )  /\  k  e.  NN )  ->  M  <_  1 )
265 nnge1 8703 . . . . . . . 8  |-  ( k  e.  NN  ->  1  <_  k )
266265adantl 273 . . . . . . 7  |-  ( ( ( ph  /\  M  <_  1 )  /\  k  e.  NN )  ->  1  <_  k )
267261, 262, 263, 264, 266letrd 7850 . . . . . 6  |-  ( ( ( ph  /\  M  <_  1 )  /\  k  e.  NN )  ->  M  <_  k )
268258, 260, 267, 55syl3anbrc 1148 . . . . 5  |-  ( ( ( ph  /\  M  <_  1 )  /\  k  e.  NN )  ->  k  e.  ( ZZ>= `  M )
)
2698eleq2i 2182 . . . . . . 7  |-  ( k  e.  Z  <->  k  e.  ( ZZ>= `  M )
)
270269, 5sylan2br 284 . . . . . 6  |-  ( (
ph  /\  k  e.  ( ZZ>= `  M )
)  ->  ( F `  k )  e.  CC )
271270adantlr 466 . . . . 5  |-  ( ( ( ph  /\  M  <_  1 )  /\  k  e.  ( ZZ>= `  M )
)  ->  ( F `  k )  e.  CC )
272268, 271syldan 278 . . . 4  |-  ( ( ( ph  /\  M  <_  1 )  /\  k  e.  NN )  ->  ( F `  k )  e.  CC )
273269, 216sylan2br 284 . . . . . 6  |-  ( (
ph  /\  k  e.  ( ZZ>= `  M )
)  ->  ( abs `  ( F `  (
k  +  1 ) ) )  <_  ( A  x.  ( abs `  ( F `  k
) ) ) )
274273adantlr 466 . . . . 5  |-  ( ( ( ph  /\  M  <_  1 )  /\  k  e.  ( ZZ>= `  M )
)  ->  ( abs `  ( F `  (
k  +  1 ) ) )  <_  ( A  x.  ( abs `  ( F `  k
) ) ) )
275268, 274syldan 278 . . . 4  |-  ( ( ( ph  /\  M  <_  1 )  /\  k  e.  NN )  ->  ( abs `  ( F `  ( k  +  1 ) ) )  <_ 
( A  x.  ( abs `  ( F `  k ) ) ) )
276254, 255, 256, 272, 275cvgratnn 11251 . . 3  |-  ( (
ph  /\  M  <_  1 )  ->  seq 1
(  +  ,  F
)  e.  dom  ~~>  )
277 eqid 2115 . . . 4  |-  ( ZZ>= `  M )  =  (
ZZ>= `  M )
278 1zzd 9035 . . . . 5  |-  ( (
ph  /\  M  <_  1 )  ->  1  e.  ZZ )
279 simpr 109 . . . . 5  |-  ( (
ph  /\  M  <_  1 )  ->  M  <_  1 )
280 eluz2 9284 . . . . 5  |-  ( 1  e.  ( ZZ>= `  M
)  <->  ( M  e.  ZZ  /\  1  e.  ZZ  /\  M  <_ 
1 ) )
281257, 278, 279, 280syl3anbrc 1148 . . . 4  |-  ( (
ph  /\  M  <_  1 )  ->  1  e.  ( ZZ>= `  M )
)
282277, 281, 271iserex 11059 . . 3  |-  ( (
ph  /\  M  <_  1 )  ->  (  seq M (  +  ,  F )  e.  dom  ~~>  <->  seq 1 (  +  ,  F )  e.  dom  ~~>  ) )
283276, 282mpbird 166 . 2  |-  ( (
ph  /\  M  <_  1 )  ->  seq M (  +  ,  F )  e.  dom  ~~>  )
284 1z 9034 . . 3  |-  1  e.  ZZ
285 zletric 9052 . . 3  |-  ( ( 1  e.  ZZ  /\  M  e.  ZZ )  ->  ( 1  <_  M  \/  M  <_  1 ) )
286284, 1, 285sylancr 408 . 2  |-  ( ph  ->  ( 1  <_  M  \/  M  <_  1 ) )
287253, 283, 286mpjaodan 770 1  |-  ( ph  ->  seq M (  +  ,  F )  e. 
dom 
~~>  )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 103    <-> wb 104    \/ wo 680  DECID wdc 802    \/ w3o 944    = wceq 1314    e. wcel 1463   A.wral 2391   ifcif 3442   class class class wbr 3897    |-> cmpt 3957   dom cdm 4507   ` cfv 5091  (class class class)co 5740   CCcc 7582   RRcr 7583   0cc0 7584   1c1 7585    + caddc 7587    x. cmul 7589    < clt 7764    <_ cle 7765    - cmin 7897   # cap 8306    / cdiv 8395   NNcn 8680   ZZcz 9008   ZZ>=cuz 9278   RR+crp 9393    seqcseq 10169   ^cexp 10243   abscabs 10720    ~~> cli 10998
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 8396  df-inn 8681  df-2 8739  df-3 8740  df-4 8741  df-n0 8932  df-z 9009  df-uz 9279  df-q 9364  df-rp 9394  df-ico 9628  df-fz 9742  df-fzo 9871  df-seqfrec 10170  df-exp 10244  df-ihash 10473  df-cj 10565  df-re 10566  df-im 10567  df-rsqrt 10721  df-abs 10722  df-clim 10999  df-sumdc 11074
This theorem is referenced by:  cvgratgt0  11253
  Copyright terms: Public domain W3C validator