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

Theorem cvgratz 11256
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 274 . . . 4  |-  ( (
ph  /\  1  <_  M )  ->  M  e.  ZZ )
3 fveq2 5389 . . . . . 6  |-  ( k  =  x  ->  ( F `  k )  =  ( F `  x ) )
43eleq1d 2186 . . . . 5  |-  ( k  =  x  ->  (
( F `  k
)  e.  CC  <->  ( F `  x )  e.  CC ) )
5 cvgratz.6 . . . . . . 7  |-  ( (
ph  /\  k  e.  Z )  ->  ( F `  k )  e.  CC )
65ralrimiva 2482 . . . . . 6  |-  ( ph  ->  A. k  e.  Z  ( F `  k )  e.  CC )
76ad2antrr 479 . . . . 5  |-  ( ( ( ph  /\  1  <_  M )  /\  x  e.  ( ZZ>= `  M )
)  ->  A. k  e.  Z  ( F `  k )  e.  CC )
8 cvgratz.1 . . . . . . . 8  |-  Z  =  ( ZZ>= `  M )
98eleq2i 2184 . . . . . . 7  |-  ( x  e.  Z  <->  x  e.  ( ZZ>= `  M )
)
109biimpri 132 . . . . . 6  |-  ( x  e.  ( ZZ>= `  M
)  ->  x  e.  Z )
1110adantl 275 . . . . 5  |-  ( ( ( ph  /\  1  <_  M )  /\  x  e.  ( ZZ>= `  M )
)  ->  x  e.  Z )
124, 7, 11rspcdva 2768 . . . 4  |-  ( ( ( ph  /\  1  <_  M )  /\  x  e.  ( ZZ>= `  M )
)  ->  ( F `  x )  e.  CC )
13 eluzelz 9291 . . . . . . . 8  |-  ( k  e.  ( ZZ>= `  M
)  ->  k  e.  ZZ )
1413adantl 275 . . . . . . 7  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= `  M )
)  ->  k  e.  ZZ )
15 1red 7749 . . . . . . . 8  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= `  M )
)  ->  1  e.  RR )
161zred 9131 . . . . . . . . 9  |-  ( ph  ->  M  e.  RR )
1716ad2antrr 479 . . . . . . . 8  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= `  M )
)  ->  M  e.  RR )
1814zred 9131 . . . . . . . 8  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= `  M )
)  ->  k  e.  RR )
19 simplr 504 . . . . . . . 8  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= `  M )
)  ->  1  <_  M )
20 eluzle 9294 . . . . . . . . 9  |-  ( k  e.  ( ZZ>= `  M
)  ->  M  <_  k )
2120adantl 275 . . . . . . . 8  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= `  M )
)  ->  M  <_  k )
2215, 17, 18, 19, 21letrd 7854 . . . . . . 7  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= `  M )
)  ->  1  <_  k )
23 elnnz1 9035 . . . . . . 7  |-  ( k  e.  NN  <->  ( k  e.  ZZ  /\  1  <_ 
k ) )
2414, 22, 23sylanbrc 413 . . . . . 6  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= `  M )
)  ->  k  e.  NN )
25 elnnuz 9318 . . . . . . . 8  |-  ( k  e.  NN  <->  k  e.  ( ZZ>= `  1 )
)
26 fveq2 5389 . . . . . . . . . . . . 13  |-  ( k  =  M  ->  ( F `  k )  =  ( F `  M ) )
2726eleq1d 2186 . . . . . . . . . . . 12  |-  ( k  =  M  ->  (
( F `  k
)  e.  CC  <->  ( F `  M )  e.  CC ) )
28 uzid 9296 . . . . . . . . . . . . . 14  |-  ( M  e.  ZZ  ->  M  e.  ( ZZ>= `  M )
)
291, 28syl 14 . . . . . . . . . . . . 13  |-  ( ph  ->  M  e.  ( ZZ>= `  M ) )
3029, 8eleqtrrdi 2211 . . . . . . . . . . . 12  |-  ( ph  ->  M  e.  Z )
3127, 6, 30rspcdva 2768 . . . . . . . . . . 11  |-  ( ph  ->  ( F `  M
)  e.  CC )
3231ad3antrrr 483 . . . . . . . . . 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 9436 . . . . . . . . . . . . 13  |-  ( ph  ->  A  e.  RR+ )
3635ad3antrrr 483 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= ` 
1 ) )  /\  k  <  M )  ->  A  e.  RR+ )
372adantr 274 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= `  1 )
)  ->  M  e.  ZZ )
3837adantr 274 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= ` 
1 ) )  /\  k  <  M )  ->  M  e.  ZZ )
3925biimpri 132 . . . . . . . . . . . . . . . 16  |-  ( k  e.  ( ZZ>= `  1
)  ->  k  e.  NN )
4039adantl 275 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= `  1 )
)  ->  k  e.  NN )
4140nnzd 9130 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= `  1 )
)  ->  k  e.  ZZ )
4241adantr 274 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= ` 
1 ) )  /\  k  <  M )  -> 
k  e.  ZZ )
4338, 42zsubcld 9136 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= ` 
1 ) )  /\  k  <  M )  -> 
( M  -  k
)  e.  ZZ )
4436, 43rpexpcld 10403 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= ` 
1 ) )  /\  k  <  M )  -> 
( A ^ ( M  -  k )
)  e.  RR+ )
4544rpcnd 9440 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= ` 
1 ) )  /\  k  <  M )  -> 
( A ^ ( M  -  k )
)  e.  CC )
4644rpap0d 9444 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= ` 
1 ) )  /\  k  <  M )  -> 
( A ^ ( M  -  k )
) #  0 )
4732, 45, 46divclapd 8517 . . . . . . . . 9  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= ` 
1 ) )  /\  k  <  M )  -> 
( ( F `  M )  /  ( A ^ ( M  -  k ) ) )  e.  CC )
48 simplll 507 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= ` 
1 ) )  /\  -.  k  <  M )  ->  ph )
4937adantr 274 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= ` 
1 ) )  /\  -.  k  <  M )  ->  M  e.  ZZ )
5041adantr 274 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= ` 
1 ) )  /\  -.  k  <  M )  ->  k  e.  ZZ )
5116ad3antrrr 483 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= ` 
1 ) )  /\  -.  k  <  M )  ->  M  e.  RR )
5250zred 9131 . . . . . . . . . . . . 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 7851 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= ` 
1 ) )  /\  -.  k  <  M )  ->  M  <_  k
)
55 eluz2 9288 . . . . . . . . . . . 12  |-  ( k  e.  ( ZZ>= `  M
)  <->  ( M  e.  ZZ  /\  k  e.  ZZ  /\  M  <_ 
k ) )
5649, 50, 54, 55syl3anbrc 1150 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= ` 
1 ) )  /\  -.  k  <  M )  ->  k  e.  (
ZZ>= `  M ) )
5756, 8eleqtrrdi 2211 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= ` 
1 ) )  /\  -.  k  <  M )  ->  k  e.  Z
)
5848, 57, 5syl2anc 408 . . . . . . . . 9  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= ` 
1 ) )  /\  -.  k  <  M )  ->  ( F `  k )  e.  CC )
59 zdclt 9086 . . . . . . . . . 10  |-  ( ( k  e.  ZZ  /\  M  e.  ZZ )  -> DECID  k  <  M )
6041, 37, 59syl2anc 408 . . . . . . . . 9  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= `  1 )
)  -> DECID  k  <  M )
6147, 58, 60ifcldadc 3471 . . . . . . . 8  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= `  1 )
)  ->  if (
k  <  M , 
( ( F `  M )  /  ( A ^ ( M  -  k ) ) ) ,  ( F `  k ) )  e.  CC )
6225, 61sylan2b 285 . . . . . . 7  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  if ( k  <  M ,  ( ( F `
 M )  / 
( A ^ ( M  -  k )
) ) ,  ( F `  k ) )  e.  CC )
6324, 62syldan 280 . . . . . 6  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= `  M )
)  ->  if (
k  <  M , 
( ( F `  M )  /  ( A ^ ( M  -  k ) ) ) ,  ( F `  k ) )  e.  CC )
64 breq1 3902 . . . . . . . 8  |-  ( i  =  k  ->  (
i  <  M  <->  k  <  M ) )
65 oveq2 5750 . . . . . . . . . 10  |-  ( i  =  k  ->  ( M  -  i )  =  ( M  -  k ) )
6665oveq2d 5758 . . . . . . . . 9  |-  ( i  =  k  ->  ( A ^ ( M  -  i ) )  =  ( A ^ ( M  -  k )
) )
6766oveq2d 5758 . . . . . . . 8  |-  ( i  =  k  ->  (
( F `  M
)  /  ( A ^ ( M  -  i ) ) )  =  ( ( F `
 M )  / 
( A ^ ( M  -  k )
) ) )
68 fveq2 5389 . . . . . . . 8  |-  ( i  =  k  ->  ( F `  i )  =  ( F `  k ) )
6964, 67, 68ifbieq12d 3468 . . . . . . 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 2117 . . . . . . 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 5465 . . . . . 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 408 . . . . 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 7852 . . . . . 6  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= `  M )
)  ->  -.  k  <  M )
7473iffalsed 3454 . . . . 5  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= `  M )
)  ->  if (
k  <  M , 
( ( F `  M )  /  ( A ^ ( M  -  k ) ) ) ,  ( F `  k ) )  =  ( F `  k
) )
7572, 74eqtr2d 2151 . . . 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 7713 . . . . 5  |-  ( ( x  e.  CC  /\  y  e.  CC )  ->  ( x  +  y )  e.  CC )
7776adantl 275 . . . 4  |-  ( ( ( ph  /\  1  <_  M )  /\  (
x  e.  CC  /\  y  e.  CC )
)  ->  ( x  +  y )  e.  CC )
782, 12, 75, 77seq3feq 10200 . . 3  |-  ( (
ph  /\  1  <_  M )  ->  seq M (  +  ,  F )  =  seq M (  +  ,  ( i  e.  NN  |->  if ( i  <  M , 
( ( F `  M )  /  ( A ^ ( M  -  i ) ) ) ,  ( F `  i ) ) ) ) )
7933adantr 274 . . . . 5  |-  ( (
ph  /\  1  <_  M )  ->  A  e.  RR )
80 cvgratz.4 . . . . . 6  |-  ( ph  ->  A  <  1 )
8180adantr 274 . . . . 5  |-  ( (
ph  /\  1  <_  M )  ->  A  <  1 )
8234adantr 274 . . . . 5  |-  ( (
ph  /\  1  <_  M )  ->  0  <  A )
8371eleq1d 2186 . . . . . . . 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 408 . . . . . . 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 285 . . . . 5  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  (
( i  e.  NN  |->  if ( i  <  M ,  ( ( F `
 M )  / 
( A ^ ( M  -  i )
) ) ,  ( F `  i ) ) ) `  k
)  e.  CC )
8731ad3antrrr 483 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  <  M )  ->  ( F `  M )  e.  CC )
8835ad3antrrr 483 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  <  M )  ->  A  e.  RR+ )
892ad2antrr 479 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  <  M )  ->  M  e.  ZZ )
9025, 41sylan2b 285 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  k  e.  ZZ )
9190adantr 274 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  <  M )  ->  k  e.  ZZ )
9291peano2zd 9134 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  <  M )  ->  ( k  +  1 )  e.  ZZ )
9389, 92zsubcld 9136 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  <  M )  ->  ( M  -  ( k  +  1 ) )  e.  ZZ )
9488, 93rpexpcld 10403 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  <  M )  ->  ( A ^
( M  -  (
k  +  1 ) ) )  e.  RR+ )
9594rpcnd 9440 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  <  M )  ->  ( A ^
( M  -  (
k  +  1 ) ) )  e.  CC )
9694rpap0d 9444 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  <  M )  ->  ( A ^
( M  -  (
k  +  1 ) ) ) #  0 )
9787, 95, 96divclapd 8517 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  <  M )  ->  ( ( F `
 M )  / 
( A ^ ( M  -  ( k  +  1 ) ) ) )  e.  CC )
98 fveq2 5389 . . . . . . . . . . . 12  |-  ( a  =  ( k  +  1 )  ->  ( F `  a )  =  ( F `  ( k  +  1 ) ) )
9998eleq1d 2186 . . . . . . . . . . 11  |-  ( a  =  ( k  +  1 )  ->  (
( F `  a
)  e.  CC  <->  ( F `  ( k  +  1 ) )  e.  CC ) )
100 fveq2 5389 . . . . . . . . . . . . . . 15  |-  ( k  =  a  ->  ( F `  k )  =  ( F `  a ) )
101100eleq1d 2186 . . . . . . . . . . . . . 14  |-  ( k  =  a  ->  (
( F `  k
)  e.  CC  <->  ( F `  a )  e.  CC ) )
102101cbvralv 2631 . . . . . . . . . . . . 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 483 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  -.  ( k  +  1 )  <  M
)  ->  A. a  e.  Z  ( F `  a )  e.  CC )
1052ad2antrr 479 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  -.  ( k  +  1 )  <  M
)  ->  M  e.  ZZ )
106 peano2nn 8696 . . . . . . . . . . . . . . . 16  |-  ( k  e.  NN  ->  (
k  +  1 )  e.  NN )
107106adantl 275 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  (
k  +  1 )  e.  NN )
108107nnzd 9130 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  (
k  +  1 )  e.  ZZ )
109108adantr 274 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  -.  ( k  +  1 )  <  M
)  ->  ( k  +  1 )  e.  ZZ )
11016ad3antrrr 483 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  -.  ( k  +  1 )  <  M
)  ->  M  e.  RR )
111107nnred 8697 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  (
k  +  1 )  e.  RR )
112111adantr 274 . . . . . . . . . . . . . 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 7851 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  -.  ( k  +  1 )  <  M
)  ->  M  <_  ( k  +  1 ) )
115 eluz2 9288 . . . . . . . . . . . . 13  |-  ( ( k  +  1 )  e.  ( ZZ>= `  M
)  <->  ( M  e.  ZZ  /\  ( k  +  1 )  e.  ZZ  /\  M  <_ 
( k  +  1 ) ) )
116105, 109, 114, 115syl3anbrc 1150 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  -.  ( k  +  1 )  <  M
)  ->  ( k  +  1 )  e.  ( ZZ>= `  M )
)
117116, 8eleqtrrdi 2211 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  -.  ( k  +  1 )  <  M
)  ->  ( k  +  1 )  e.  Z )
11899, 104, 117rspcdva 2768 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  -.  ( k  +  1 )  <  M
)  ->  ( F `  ( k  +  1 ) )  e.  CC )
1192adantr 274 . . . . . . . . . . 11  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  M  e.  ZZ )
120 zdclt 9086 . . . . . . . . . . 11  |-  ( ( ( k  +  1 )  e.  ZZ  /\  M  e.  ZZ )  -> DECID  ( k  +  1 )  <  M )
121108, 119, 120syl2anc 408 . . . . . . . . . 10  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  -> DECID  ( k  +  1 )  <  M )
12297, 118, 121ifcldadc 3471 . . . . . . . . 9  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  if ( ( k  +  1 )  <  M ,  ( ( F `
 M )  / 
( A ^ ( M  -  ( k  +  1 ) ) ) ) ,  ( F `  ( k  +  1 ) ) )  e.  CC )
123122abscld 10908 . . . . . . . 8  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  ( abs `  if ( ( k  +  1 )  <  M ,  ( ( F `  M
)  /  ( A ^ ( M  -  ( k  +  1 ) ) ) ) ,  ( F `  ( k  +  1 ) ) ) )  e.  RR )
12416recnd 7762 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  M  e.  CC )
125124ad2antrr 479 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  M  e.  CC )
126 simpr 109 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  k  e.  NN )
127126nncnd 8698 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  k  e.  CC )
128 1cnd 7750 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  1  e.  CC )
129125, 127, 128subsub4d 8072 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  (
( M  -  k
)  -  1 )  =  ( M  -  ( k  +  1 ) ) )
130129oveq2d 5758 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  ( A ^ ( ( M  -  k )  - 
1 ) )  =  ( A ^ ( M  -  ( k  +  1 ) ) ) )
13133recnd 7762 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  A  e.  CC )
132131ad2antrr 479 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  A  e.  CC )
13333, 34gt0ap0d 8358 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  A #  0 )
134133ad2antrr 479 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  A #  0 )
135119, 90zsubcld 9136 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  ( M  -  k )  e.  ZZ )
136132, 134, 135expm1apd 10389 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  ( A ^ ( ( M  -  k )  - 
1 ) )  =  ( ( A ^
( M  -  k
) )  /  A
) )
137130, 136eqtr3d 2152 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  ( A ^ ( M  -  ( k  +  1 ) ) )  =  ( ( A ^
( M  -  k
) )  /  A
) )
138137oveq2d 5758 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  (
( F `  M
)  /  ( A ^ ( M  -  ( k  +  1 ) ) ) )  =  ( ( F `
 M )  / 
( ( A ^
( M  -  k
) )  /  A
) ) )
139138adantr 274 . . . . . . . . . . 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 3451 . . . . . . . . . . 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 8697 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  k  e.  RR )
143142adantr 274 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  <  M )  ->  k  e.  RR )
144 peano2re 7866 . . . . . . . . . . . . . . . 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 483 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  <  M )  ->  M  e.  RR )
147143ltp1d 8652 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  <  M )  ->  k  <  (
k  +  1 ) )
148143, 145, 146, 147, 140lttrd 7856 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  <  M )  ->  k  <  M
)
149148iftrued 3451 . . . . . . . . . . . . 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 5758 . . . . . . . . . . . 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 479 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  ( F `  M )  e.  CC )
152132, 134, 135expclzapd 10384 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  ( A ^ ( M  -  k ) )  e.  CC )
153132, 134, 135expap0d 10385 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  ( A ^ ( M  -  k ) ) #  0 )
154151, 152, 132, 153, 134divdivap2d 8550 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  (
( F `  M
)  /  ( ( A ^ ( M  -  k ) )  /  A ) )  =  ( ( ( F `  M )  x.  A )  / 
( A ^ ( M  -  k )
) ) )
155151, 132mulcomd 7755 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  (
( F `  M
)  x.  A )  =  ( A  x.  ( F `  M ) ) )
156155oveq1d 5757 . . . . . . . . . . . . . 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 8553 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  (
( A  x.  ( F `  M )
)  /  ( A ^ ( M  -  k ) ) )  =  ( A  x.  ( ( F `  M )  /  ( A ^ ( M  -  k ) ) ) ) )
158154, 156, 1573eqtrd 2154 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  (
( F `  M
)  /  ( ( A ^ ( M  -  k ) )  /  A ) )  =  ( A  x.  ( ( F `  M )  /  ( A ^ ( M  -  k ) ) ) ) )
159158adantr 274 . . . . . . . . . . . 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 2153 . . . . . . . . . . 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 2160 . . . . . . . . . 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 5393 . . . . . . . . 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 10921 . . . . . . . . . 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 274 . . . . . . . . 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 9442 . . . . . . . . . . . 12  |-  ( ph  ->  0  <_  A )
16633, 165absidd 10894 . . . . . . . . . . 11  |-  ( ph  ->  ( abs `  A
)  =  A )
167166oveq1d 5757 . . . . . . . . . 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 483 . . . . . . . . 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 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
) ) ) ) )
170 eqle 7823 . . . . . . . 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 569 . . . . . . 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 479 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  M  e.  RR )
173111, 172lttri3d 7846 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  (
( k  +  1 )  =  M  <->  ( -.  ( k  +  1 )  <  M  /\  -.  M  <  ( k  +  1 ) ) ) )
174173simprbda 380 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  =  M )  ->  -.  ( k  +  1 )  < 
M )
175174iffalsed 3454 . . . . . . . . . . 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 5393 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  =  M )  ->  ( F `  ( k  +  1 ) )  =  ( F `  M ) )
178175, 177eqtrd 2150 . . . . . . . . . 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 5393 . . . . . . . . 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 274 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  =  M )  ->  k  e.  RR )
181180ltp1d 8652 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  =  M )  ->  k  <  (
k  +  1 ) )
182 breq2 3903 . . . . . . . . . . . . . . . 16  |-  ( ( k  +  1 )  =  M  ->  (
k  <  ( k  +  1 )  <->  k  <  M ) )
183182adantl 275 . . . . . . . . . . . . . . 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 3451 . . . . . . . . . . . . 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 5757 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  =  M )  ->  ( ( k  +  1 )  -  k )  =  ( M  -  k ) )
187127adantr 274 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  =  M )  ->  k  e.  CC )
188 1cnd 7750 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  =  M )  ->  1  e.  CC )
189187, 188pncan2d 8043 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  =  M )  ->  ( ( k  +  1 )  -  k )  =  1 )
190186, 189eqtr3d 2152 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  =  M )  ->  ( M  -  k )  =  1 )
191190oveq2d 5758 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  =  M )  ->  ( A ^
( M  -  k
) )  =  ( A ^ 1 ) )
192132adantr 274 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  =  M )  ->  A  e.  CC )
193192exp1d 10374 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  =  M )  ->  ( A ^
1 )  =  A )
194191, 193eqtrd 2150 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  =  M )  ->  ( A ^
( M  -  k
) )  =  A )
195194oveq2d 5758 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  =  M )  ->  ( ( F `
 M )  / 
( A ^ ( M  -  k )
) )  =  ( ( F `  M
)  /  A ) )
196185, 195eqtrd 2150 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  =  M )  ->  if ( k  <  M ,  ( ( F `  M
)  /  ( A ^ ( M  -  k ) ) ) ,  ( F `  k ) )  =  ( ( F `  M )  /  A
) )
197196oveq2d 5758 . . . . . . . . . . 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 8519 . . . . . . . . . . . 12  |-  ( ph  ->  ( A  x.  (
( F `  M
)  /  A ) )  =  ( F `
 M ) )
199198ad3antrrr 483 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  =  M )  ->  ( A  x.  ( ( F `  M )  /  A
) )  =  ( F `  M ) )
200197, 199eqtrd 2150 . . . . . . . . . 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 5393 . . . . . . . . 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 479 . . . . . . . . . . 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 2150 . . . . . . . . . 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 274 . . . . . . . . 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 2156 . . . . . . . 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 569 . . . . . . 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 507 . . . . . . . . 9  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  M  <  ( k  +  1 ) )  ->  ph )
208119adantr 274 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  M  <  ( k  +  1 ) )  ->  M  e.  ZZ )
20990adantr 274 . . . . . . . . . . 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 9067 . . . . . . . . . . . . 13  |-  ( ( M  e.  ZZ  /\  k  e.  ZZ )  ->  ( M  <_  k  <->  M  <  ( k  +  1 ) ) )
212119, 209, 211syl2an2r 569 . . . . . . . . . . . 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 1150 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  M  <  ( k  +  1 ) )  ->  k  e.  (
ZZ>= `  M ) )
215214, 8eleqtrrdi 2211 . . . . . . . . 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 408 . . . . . . . 8  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  M  <  ( k  +  1 ) )  ->  ( abs `  ( F `  ( k  +  1 ) ) )  <_  ( A  x.  ( abs `  ( F `  k )
) ) )
218172adantr 274 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  M  <  ( k  +  1 ) )  ->  M  e.  RR )
219111adantr 274 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  M  <  ( k  +  1 ) )  ->  ( k  +  1 )  e.  RR )
220218, 219, 210ltnsymd 7850 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  M  <  ( k  +  1 ) )  ->  -.  ( k  +  1 )  < 
M )
221220iffalsed 3454 . . . . . . . . 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 5393 . . . . . . . 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 274 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  M  <  ( k  +  1 ) )  ->  k  e.  RR )
224218, 223, 213lensymd 7852 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  M  <  ( k  +  1 ) )  ->  -.  k  <  M )
225224iffalsed 3454 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  M  <  ( k  +  1 ) )  ->  if ( k  <  M ,  ( ( F `  M
)  /  ( A ^ ( M  -  k ) ) ) ,  ( F `  k ) )  =  ( F `  k
) )
226225fveq2d 5393 . . . . . . . . 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 5758 . . . . . . . 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 3930 . . . . . . 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 9055 . . . . . . . 8  |-  ( ( ( k  +  1 )  e.  ZZ  /\  M  e.  ZZ )  ->  ( ( k  +  1 )  <  M  \/  ( k  +  1 )  =  M  \/  M  <  ( k  +  1 ) ) )
230108, 119, 229syl2anc 408 . . . . . . 7  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  (
( k  +  1 )  <  M  \/  ( k  +  1 )  =  M  \/  M  <  ( k  +  1 ) ) )
231171, 206, 228, 230mpjao3dan 1270 . . . . . 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 3902 . . . . . . . . . 10  |-  ( i  =  ( k  +  1 )  ->  (
i  <  M  <->  ( k  +  1 )  < 
M ) )
233 oveq2 5750 . . . . . . . . . . . 12  |-  ( i  =  ( k  +  1 )  ->  ( M  -  i )  =  ( M  -  ( k  +  1 ) ) )
234233oveq2d 5758 . . . . . . . . . . 11  |-  ( i  =  ( k  +  1 )  ->  ( A ^ ( M  -  i ) )  =  ( A ^ ( M  -  ( k  +  1 ) ) ) )
235234oveq2d 5758 . . . . . . . . . 10  |-  ( i  =  ( k  +  1 )  ->  (
( F `  M
)  /  ( A ^ ( M  -  i ) ) )  =  ( ( F `
 M )  / 
( A ^ ( M  -  ( k  +  1 ) ) ) ) )
236 fveq2 5389 . . . . . . . . . 10  |-  ( i  =  ( k  +  1 )  ->  ( F `  i )  =  ( F `  ( k  +  1 ) ) )
237232, 235, 236ifbieq12d 3468 . . . . . . . . 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 5465 . . . . . . . 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 408 . . . . . . 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 5393 . . . . . 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 408 . . . . . . . 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 5393 . . . . . . 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 5758 . . . . . 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 3930 . . . . 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 11255 . . . 4  |-  ( (
ph  /\  1  <_  M )  ->  seq 1
(  +  ,  ( i  e.  NN  |->  if ( i  <  M ,  ( ( F `
 M )  / 
( A ^ ( M  -  i )
) ) ,  ( F `  i ) ) ) )  e. 
dom 
~~>  )
246 eqid 2117 . . . . 5  |-  ( ZZ>= ` 
1 )  =  (
ZZ>= `  1 )
247 1zzd 9039 . . . . . 6  |-  ( (
ph  /\  1  <_  M )  ->  1  e.  ZZ )
248 simpr 109 . . . . . 6  |-  ( (
ph  /\  1  <_  M )  ->  1  <_  M )
249 eluz2 9288 . . . . . 6  |-  ( M  e.  ( ZZ>= `  1
)  <->  ( 1  e.  ZZ  /\  M  e.  ZZ  /\  1  <_  M ) )
250247, 2, 248, 249syl3anbrc 1150 . . . . 5  |-  ( (
ph  /\  1  <_  M )  ->  M  e.  ( ZZ>= `  1 )
)
251246, 250, 85iserex 11063 . . . 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 2194 . 2  |-  ( (
ph  /\  1  <_  M )  ->  seq M (  +  ,  F )  e.  dom  ~~>  )
25433adantr 274 . . . 4  |-  ( (
ph  /\  M  <_  1 )  ->  A  e.  RR )
25580adantr 274 . . . 4  |-  ( (
ph  /\  M  <_  1 )  ->  A  <  1 )
25634adantr 274 . . . 4  |-  ( (
ph  /\  M  <_  1 )  ->  0  <  A )
2571adantr 274 . . . . . . 7  |-  ( (
ph  /\  M  <_  1 )  ->  M  e.  ZZ )
258257adantr 274 . . . . . 6  |-  ( ( ( ph  /\  M  <_  1 )  /\  k  e.  NN )  ->  M  e.  ZZ )
259 nnz 9031 . . . . . . 7  |-  ( k  e.  NN  ->  k  e.  ZZ )
260259adantl 275 . . . . . 6  |-  ( ( ( ph  /\  M  <_  1 )  /\  k  e.  NN )  ->  k  e.  ZZ )
261258zred 9131 . . . . . . 7  |-  ( ( ( ph  /\  M  <_  1 )  /\  k  e.  NN )  ->  M  e.  RR )
262 1red 7749 . . . . . . 7  |-  ( ( ( ph  /\  M  <_  1 )  /\  k  e.  NN )  ->  1  e.  RR )
263260zred 9131 . . . . . . 7  |-  ( ( ( ph  /\  M  <_  1 )  /\  k  e.  NN )  ->  k  e.  RR )
264 simplr 504 . . . . . . 7  |-  ( ( ( ph  /\  M  <_  1 )  /\  k  e.  NN )  ->  M  <_  1 )
265 nnge1 8707 . . . . . . . 8  |-  ( k  e.  NN  ->  1  <_  k )
266265adantl 275 . . . . . . 7  |-  ( ( ( ph  /\  M  <_  1 )  /\  k  e.  NN )  ->  1  <_  k )
267261, 262, 263, 264, 266letrd 7854 . . . . . 6  |-  ( ( ( ph  /\  M  <_  1 )  /\  k  e.  NN )  ->  M  <_  k )
268258, 260, 267, 55syl3anbrc 1150 . . . . 5  |-  ( ( ( ph  /\  M  <_  1 )  /\  k  e.  NN )  ->  k  e.  ( ZZ>= `  M )
)
2698eleq2i 2184 . . . . . . 7  |-  ( k  e.  Z  <->  k  e.  ( ZZ>= `  M )
)
270269, 5sylan2br 286 . . . . . 6  |-  ( (
ph  /\  k  e.  ( ZZ>= `  M )
)  ->  ( F `  k )  e.  CC )
271270adantlr 468 . . . . 5  |-  ( ( ( ph  /\  M  <_  1 )  /\  k  e.  ( ZZ>= `  M )
)  ->  ( F `  k )  e.  CC )
272268, 271syldan 280 . . . 4  |-  ( ( ( ph  /\  M  <_  1 )  /\  k  e.  NN )  ->  ( F `  k )  e.  CC )
273269, 216sylan2br 286 . . . . . 6  |-  ( (
ph  /\  k  e.  ( ZZ>= `  M )
)  ->  ( abs `  ( F `  (
k  +  1 ) ) )  <_  ( A  x.  ( abs `  ( F `  k
) ) ) )
274273adantlr 468 . . . . 5  |-  ( ( ( ph  /\  M  <_  1 )  /\  k  e.  ( ZZ>= `  M )
)  ->  ( abs `  ( F `  (
k  +  1 ) ) )  <_  ( A  x.  ( abs `  ( F `  k
) ) ) )
275268, 274syldan 280 . . . 4  |-  ( ( ( ph  /\  M  <_  1 )  /\  k  e.  NN )  ->  ( abs `  ( F `  ( k  +  1 ) ) )  <_ 
( A  x.  ( abs `  ( F `  k ) ) ) )
276254, 255, 256, 272, 275cvgratnn 11255 . . 3  |-  ( (
ph  /\  M  <_  1 )  ->  seq 1
(  +  ,  F
)  e.  dom  ~~>  )
277 eqid 2117 . . . 4  |-  ( ZZ>= `  M )  =  (
ZZ>= `  M )
278 1zzd 9039 . . . . 5  |-  ( (
ph  /\  M  <_  1 )  ->  1  e.  ZZ )
279 simpr 109 . . . . 5  |-  ( (
ph  /\  M  <_  1 )  ->  M  <_  1 )
280 eluz2 9288 . . . . 5  |-  ( 1  e.  ( ZZ>= `  M
)  <->  ( M  e.  ZZ  /\  1  e.  ZZ  /\  M  <_ 
1 ) )
281257, 278, 279, 280syl3anbrc 1150 . . . 4  |-  ( (
ph  /\  M  <_  1 )  ->  1  e.  ( ZZ>= `  M )
)
282277, 281, 271iserex 11063 . . 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 9038 . . 3  |-  1  e.  ZZ
285 zletric 9056 . . 3  |-  ( ( 1  e.  ZZ  /\  M  e.  ZZ )  ->  ( 1  <_  M  \/  M  <_  1 ) )
286284, 1, 285sylancr 410 . 2  |-  ( ph  ->  ( 1  <_  M  \/  M  <_  1 ) )
287253, 283, 286mpjaodan 772 1  |-  ( ph  ->  seq M (  +  ,  F )  e. 
dom 
~~>  )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 103    <-> wb 104    \/ wo 682  DECID wdc 804    \/ w3o 946    = wceq 1316    e. wcel 1465   A.wral 2393   ifcif 3444   class class class wbr 3899    |-> cmpt 3959   dom cdm 4509   ` cfv 5093  (class class class)co 5742   CCcc 7586   RRcr 7587   0cc0 7588   1c1 7589    + caddc 7591    x. cmul 7593    < clt 7768    <_ cle 7769    - cmin 7901   # cap 8310    / cdiv 8399   NNcn 8684   ZZcz 9012   ZZ>=cuz 9282   RR+crp 9397    seqcseq 10173   ^cexp 10247   abscabs 10724    ~~> cli 11002
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 588  ax-in2 589  ax-io 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-10 1468  ax-11 1469  ax-i12 1470  ax-bndl 1471  ax-4 1472  ax-13 1476  ax-14 1477  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099  ax-coll 4013  ax-sep 4016  ax-nul 4024  ax-pow 4068  ax-pr 4101  ax-un 4325  ax-setind 4422  ax-iinf 4472  ax-cnex 7679  ax-resscn 7680  ax-1cn 7681  ax-1re 7682  ax-icn 7683  ax-addcl 7684  ax-addrcl 7685  ax-mulcl 7686  ax-mulrcl 7687  ax-addcom 7688  ax-mulcom 7689  ax-addass 7690  ax-mulass 7691  ax-distr 7692  ax-i2m1 7693  ax-0lt1 7694  ax-1rid 7695  ax-0id 7696  ax-rnegex 7697  ax-precex 7698  ax-cnre 7699  ax-pre-ltirr 7700  ax-pre-ltwlin 7701  ax-pre-lttrn 7702  ax-pre-apti 7703  ax-pre-ltadd 7704  ax-pre-mulgt0 7705  ax-pre-mulext 7706  ax-arch 7707  ax-caucvg 7708
This theorem depends on definitions:  df-bi 116  df-dc 805  df-3or 948  df-3an 949  df-tru 1319  df-fal 1322  df-nf 1422  df-sb 1721  df-eu 1980  df-mo 1981  df-clab 2104  df-cleq 2110  df-clel 2113  df-nfc 2247  df-ne 2286  df-nel 2381  df-ral 2398  df-rex 2399  df-reu 2400  df-rmo 2401  df-rab 2402  df-v 2662  df-sbc 2883  df-csb 2976  df-dif 3043  df-un 3045  df-in 3047  df-ss 3054  df-nul 3334  df-if 3445  df-pw 3482  df-sn 3503  df-pr 3504  df-op 3506  df-uni 3707  df-int 3742  df-iun 3785  df-br 3900  df-opab 3960  df-mpt 3961  df-tr 3997  df-id 4185  df-po 4188  df-iso 4189  df-iord 4258  df-on 4260  df-ilim 4261  df-suc 4263  df-iom 4475  df-xp 4515  df-rel 4516  df-cnv 4517  df-co 4518  df-dm 4519  df-rn 4520  df-res 4521  df-ima 4522  df-iota 5058  df-fun 5095  df-fn 5096  df-f 5097  df-f1 5098  df-fo 5099  df-f1o 5100  df-fv 5101  df-isom 5102  df-riota 5698  df-ov 5745  df-oprab 5746  df-mpo 5747  df-1st 6006  df-2nd 6007  df-recs 6170  df-irdg 6235  df-frec 6256  df-1o 6281  df-oadd 6285  df-er 6397  df-en 6603  df-dom 6604  df-fin 6605  df-pnf 7770  df-mnf 7771  df-xr 7772  df-ltxr 7773  df-le 7774  df-sub 7903  df-neg 7904  df-reap 8304  df-ap 8311  df-div 8400  df-inn 8685  df-2 8743  df-3 8744  df-4 8745  df-n0 8936  df-z 9013  df-uz 9283  df-q 9368  df-rp 9398  df-ico 9632  df-fz 9746  df-fzo 9875  df-seqfrec 10174  df-exp 10248  df-ihash 10477  df-cj 10569  df-re 10570  df-im 10571  df-rsqrt 10725  df-abs 10726  df-clim 11003  df-sumdc 11078
This theorem is referenced by:  cvgratgt0  11257
  Copyright terms: Public domain W3C validator