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

Theorem cvgratz 11424
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 5467 . . . . . 6  |-  ( k  =  x  ->  ( F `  k )  =  ( F `  x ) )
43eleq1d 2226 . . . . 5  |-  ( k  =  x  ->  (
( F `  k
)  e.  CC  <->  ( F `  x )  e.  CC ) )
5 cvgratz.6 . . . . . . 7  |-  ( (
ph  /\  k  e.  Z )  ->  ( F `  k )  e.  CC )
65ralrimiva 2530 . . . . . 6  |-  ( ph  ->  A. k  e.  Z  ( F `  k )  e.  CC )
76ad2antrr 480 . . . . 5  |-  ( ( ( ph  /\  1  <_  M )  /\  x  e.  ( ZZ>= `  M )
)  ->  A. k  e.  Z  ( F `  k )  e.  CC )
8 cvgratz.1 . . . . . . . 8  |-  Z  =  ( ZZ>= `  M )
98eleq2i 2224 . . . . . . 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 2821 . . . 4  |-  ( ( ( ph  /\  1  <_  M )  /\  x  e.  ( ZZ>= `  M )
)  ->  ( F `  x )  e.  CC )
13 eluzelz 9443 . . . . . . . 8  |-  ( k  e.  ( ZZ>= `  M
)  ->  k  e.  ZZ )
1413adantl 275 . . . . . . 7  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= `  M )
)  ->  k  e.  ZZ )
15 1red 7888 . . . . . . . 8  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= `  M )
)  ->  1  e.  RR )
161zred 9281 . . . . . . . . 9  |-  ( ph  ->  M  e.  RR )
1716ad2antrr 480 . . . . . . . 8  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= `  M )
)  ->  M  e.  RR )
1814zred 9281 . . . . . . . 8  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= `  M )
)  ->  k  e.  RR )
19 simplr 520 . . . . . . . 8  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= `  M )
)  ->  1  <_  M )
20 eluzle 9446 . . . . . . . . 9  |-  ( k  e.  ( ZZ>= `  M
)  ->  M  <_  k )
2120adantl 275 . . . . . . . 8  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= `  M )
)  ->  M  <_  k )
2215, 17, 18, 19, 21letrd 7994 . . . . . . 7  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= `  M )
)  ->  1  <_  k )
23 elnnz1 9185 . . . . . . 7  |-  ( k  e.  NN  <->  ( k  e.  ZZ  /\  1  <_ 
k ) )
2414, 22, 23sylanbrc 414 . . . . . 6  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= `  M )
)  ->  k  e.  NN )
25 elnnuz 9470 . . . . . . . 8  |-  ( k  e.  NN  <->  k  e.  ( ZZ>= `  1 )
)
26 fveq2 5467 . . . . . . . . . . . . 13  |-  ( k  =  M  ->  ( F `  k )  =  ( F `  M ) )
2726eleq1d 2226 . . . . . . . . . . . 12  |-  ( k  =  M  ->  (
( F `  k
)  e.  CC  <->  ( F `  M )  e.  CC ) )
28 uzid 9448 . . . . . . . . . . . . . 14  |-  ( M  e.  ZZ  ->  M  e.  ( ZZ>= `  M )
)
291, 28syl 14 . . . . . . . . . . . . 13  |-  ( ph  ->  M  e.  ( ZZ>= `  M ) )
3029, 8eleqtrrdi 2251 . . . . . . . . . . . 12  |-  ( ph  ->  M  e.  Z )
3127, 6, 30rspcdva 2821 . . . . . . . . . . 11  |-  ( ph  ->  ( F `  M
)  e.  CC )
3231ad3antrrr 484 . . . . . . . . . 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 9595 . . . . . . . . . . . . 13  |-  ( ph  ->  A  e.  RR+ )
3635ad3antrrr 484 . . . . . . . . . . . 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 9280 . . . . . . . . . . . . . 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 9286 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= ` 
1 ) )  /\  k  <  M )  -> 
( M  -  k
)  e.  ZZ )
4436, 43rpexpcld 10570 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= ` 
1 ) )  /\  k  <  M )  -> 
( A ^ ( M  -  k )
)  e.  RR+ )
4544rpcnd 9600 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= ` 
1 ) )  /\  k  <  M )  -> 
( A ^ ( M  -  k )
)  e.  CC )
4644rpap0d 9604 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= ` 
1 ) )  /\  k  <  M )  -> 
( A ^ ( M  -  k )
) #  0 )
4732, 45, 46divclapd 8658 . . . . . . . . 9  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= ` 
1 ) )  /\  k  <  M )  -> 
( ( F `  M )  /  ( A ^ ( M  -  k ) ) )  e.  CC )
48 simplll 523 . . . . . . . . . 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 484 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= ` 
1 ) )  /\  -.  k  <  M )  ->  M  e.  RR )
5250zred 9281 . . . . . . . . . . . . 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 7991 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= ` 
1 ) )  /\  -.  k  <  M )  ->  M  <_  k
)
55 eluz2 9440 . . . . . . . . . . . 12  |-  ( k  e.  ( ZZ>= `  M
)  <->  ( M  e.  ZZ  /\  k  e.  ZZ  /\  M  <_ 
k ) )
5649, 50, 54, 55syl3anbrc 1166 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= ` 
1 ) )  /\  -.  k  <  M )  ->  k  e.  (
ZZ>= `  M ) )
5756, 8eleqtrrdi 2251 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= ` 
1 ) )  /\  -.  k  <  M )  ->  k  e.  Z
)
5848, 57, 5syl2anc 409 . . . . . . . . 9  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= ` 
1 ) )  /\  -.  k  <  M )  ->  ( F `  k )  e.  CC )
59 zdclt 9236 . . . . . . . . . 10  |-  ( ( k  e.  ZZ  /\  M  e.  ZZ )  -> DECID  k  <  M )
6041, 37, 59syl2anc 409 . . . . . . . . 9  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= `  1 )
)  -> DECID  k  <  M )
6147, 58, 60ifcldadc 3534 . . . . . . . 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 3968 . . . . . . . 8  |-  ( i  =  k  ->  (
i  <  M  <->  k  <  M ) )
65 oveq2 5829 . . . . . . . . . 10  |-  ( i  =  k  ->  ( M  -  i )  =  ( M  -  k ) )
6665oveq2d 5837 . . . . . . . . 9  |-  ( i  =  k  ->  ( A ^ ( M  -  i ) )  =  ( A ^ ( M  -  k )
) )
6766oveq2d 5837 . . . . . . . 8  |-  ( i  =  k  ->  (
( F `  M
)  /  ( A ^ ( M  -  i ) ) )  =  ( ( F `
 M )  / 
( A ^ ( M  -  k )
) ) )
68 fveq2 5467 . . . . . . . 8  |-  ( i  =  k  ->  ( F `  i )  =  ( F `  k ) )
6964, 67, 68ifbieq12d 3531 . . . . . . 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 2157 . . . . . . 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 5543 . . . . . 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 409 . . . . 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 7992 . . . . . 6  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= `  M )
)  ->  -.  k  <  M )
7473iffalsed 3515 . . . . 5  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= `  M )
)  ->  if (
k  <  M , 
( ( F `  M )  /  ( A ^ ( M  -  k ) ) ) ,  ( F `  k ) )  =  ( F `  k
) )
7572, 74eqtr2d 2191 . . . 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 7852 . . . . 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 10366 . . 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 2226 . . . . . . . 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 409 . . . . . . 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 484 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  <  M )  ->  ( F `  M )  e.  CC )
8835ad3antrrr 484 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  <  M )  ->  A  e.  RR+ )
892ad2antrr 480 . . . . . . . . . . . . . 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 9284 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  <  M )  ->  ( k  +  1 )  e.  ZZ )
9389, 92zsubcld 9286 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  <  M )  ->  ( M  -  ( k  +  1 ) )  e.  ZZ )
9488, 93rpexpcld 10570 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  <  M )  ->  ( A ^
( M  -  (
k  +  1 ) ) )  e.  RR+ )
9594rpcnd 9600 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  <  M )  ->  ( A ^
( M  -  (
k  +  1 ) ) )  e.  CC )
9694rpap0d 9604 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  <  M )  ->  ( A ^
( M  -  (
k  +  1 ) ) ) #  0 )
9787, 95, 96divclapd 8658 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  <  M )  ->  ( ( F `
 M )  / 
( A ^ ( M  -  ( k  +  1 ) ) ) )  e.  CC )
98 fveq2 5467 . . . . . . . . . . . 12  |-  ( a  =  ( k  +  1 )  ->  ( F `  a )  =  ( F `  ( k  +  1 ) ) )
9998eleq1d 2226 . . . . . . . . . . 11  |-  ( a  =  ( k  +  1 )  ->  (
( F `  a
)  e.  CC  <->  ( F `  ( k  +  1 ) )  e.  CC ) )
100 fveq2 5467 . . . . . . . . . . . . . . 15  |-  ( k  =  a  ->  ( F `  k )  =  ( F `  a ) )
101100eleq1d 2226 . . . . . . . . . . . . . 14  |-  ( k  =  a  ->  (
( F `  k
)  e.  CC  <->  ( F `  a )  e.  CC ) )
102101cbvralv 2680 . . . . . . . . . . . . 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 484 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  -.  ( k  +  1 )  <  M
)  ->  A. a  e.  Z  ( F `  a )  e.  CC )
1052ad2antrr 480 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  -.  ( k  +  1 )  <  M
)  ->  M  e.  ZZ )
106 peano2nn 8840 . . . . . . . . . . . . . . . 16  |-  ( k  e.  NN  ->  (
k  +  1 )  e.  NN )
107106adantl 275 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  (
k  +  1 )  e.  NN )
108107nnzd 9280 . . . . . . . . . . . . . 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 484 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  -.  ( k  +  1 )  <  M
)  ->  M  e.  RR )
111107nnred 8841 . . . . . . . . . . . . . . 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 7991 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  -.  ( k  +  1 )  <  M
)  ->  M  <_  ( k  +  1 ) )
115 eluz2 9440 . . . . . . . . . . . . 13  |-  ( ( k  +  1 )  e.  ( ZZ>= `  M
)  <->  ( M  e.  ZZ  /\  ( k  +  1 )  e.  ZZ  /\  M  <_ 
( k  +  1 ) ) )
116105, 109, 114, 115syl3anbrc 1166 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  -.  ( k  +  1 )  <  M
)  ->  ( k  +  1 )  e.  ( ZZ>= `  M )
)
117116, 8eleqtrrdi 2251 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  -.  ( k  +  1 )  <  M
)  ->  ( k  +  1 )  e.  Z )
11899, 104, 117rspcdva 2821 . . . . . . . . . 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 9236 . . . . . . . . . . 11  |-  ( ( ( k  +  1 )  e.  ZZ  /\  M  e.  ZZ )  -> DECID  ( k  +  1 )  <  M )
121108, 119, 120syl2anc 409 . . . . . . . . . 10  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  -> DECID  ( k  +  1 )  <  M )
12297, 118, 121ifcldadc 3534 . . . . . . . . 9  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  if ( ( k  +  1 )  <  M ,  ( ( F `
 M )  / 
( A ^ ( M  -  ( k  +  1 ) ) ) ) ,  ( F `  ( k  +  1 ) ) )  e.  CC )
123122abscld 11076 . . . . . . . 8  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  ( abs `  if ( ( k  +  1 )  <  M ,  ( ( F `  M
)  /  ( A ^ ( M  -  ( k  +  1 ) ) ) ) ,  ( F `  ( k  +  1 ) ) ) )  e.  RR )
12416recnd 7901 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  M  e.  CC )
125124ad2antrr 480 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  M  e.  CC )
126 simpr 109 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  k  e.  NN )
127126nncnd 8842 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  k  e.  CC )
128 1cnd 7889 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  1  e.  CC )
129125, 127, 128subsub4d 8212 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  (
( M  -  k
)  -  1 )  =  ( M  -  ( k  +  1 ) ) )
130129oveq2d 5837 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  ( A ^ ( ( M  -  k )  - 
1 ) )  =  ( A ^ ( M  -  ( k  +  1 ) ) ) )
13133recnd 7901 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  A  e.  CC )
132131ad2antrr 480 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  A  e.  CC )
13333, 34gt0ap0d 8499 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  A #  0 )
134133ad2antrr 480 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  A #  0 )
135119, 90zsubcld 9286 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  ( M  -  k )  e.  ZZ )
136132, 134, 135expm1apd 10556 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  ( A ^ ( ( M  -  k )  - 
1 ) )  =  ( ( A ^
( M  -  k
) )  /  A
) )
137130, 136eqtr3d 2192 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  ( A ^ ( M  -  ( k  +  1 ) ) )  =  ( ( A ^
( M  -  k
) )  /  A
) )
138137oveq2d 5837 . . . . . . . . . . . 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 3512 . . . . . . . . . . 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 8841 . . . . . . . . . . . . . . . 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 8006 . . . . . . . . . . . . . . . 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 484 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  <  M )  ->  M  e.  RR )
147143ltp1d 8796 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  <  M )  ->  k  <  (
k  +  1 ) )
148143, 145, 146, 147, 140lttrd 7996 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  <  M )  ->  k  <  M
)
149148iftrued 3512 . . . . . . . . . . . . 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 5837 . . . . . . . . . . . 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 480 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  ( F `  M )  e.  CC )
152132, 134, 135expclzapd 10551 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  ( A ^ ( M  -  k ) )  e.  CC )
153132, 134, 135expap0d 10552 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  ( A ^ ( M  -  k ) ) #  0 )
154151, 152, 132, 153, 134divdivap2d 8691 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  (
( F `  M
)  /  ( ( A ^ ( M  -  k ) )  /  A ) )  =  ( ( ( F `  M )  x.  A )  / 
( A ^ ( M  -  k )
) ) )
155151, 132mulcomd 7894 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  (
( F `  M
)  x.  A )  =  ( A  x.  ( F `  M ) ) )
156155oveq1d 5836 . . . . . . . . . . . . . 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 8694 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  (
( A  x.  ( F `  M )
)  /  ( A ^ ( M  -  k ) ) )  =  ( A  x.  ( ( F `  M )  /  ( A ^ ( M  -  k ) ) ) ) )
158154, 156, 1573eqtrd 2194 . . . . . . . . . . . . 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 2193 . . . . . . . . . . 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 2200 . . . . . . . . . 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 5471 . . . . . . . . 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 11089 . . . . . . . . . 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 9602 . . . . . . . . . . . 12  |-  ( ph  ->  0  <_  A )
16633, 165absidd 11062 . . . . . . . . . . 11  |-  ( ph  ->  ( abs `  A
)  =  A )
167166oveq1d 5836 . . . . . . . . . 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 484 . . . . . . . . 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 2194 . . . . . . . 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 7963 . . . . . . . 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 585 . . . . . . 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 480 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  M  e.  RR )
173111, 172lttri3d 7986 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  (
( k  +  1 )  =  M  <->  ( -.  ( k  +  1 )  <  M  /\  -.  M  <  ( k  +  1 ) ) ) )
174173simprbda 381 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  =  M )  ->  -.  ( k  +  1 )  < 
M )
175174iffalsed 3515 . . . . . . . . . . 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 5471 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  =  M )  ->  ( F `  ( k  +  1 ) )  =  ( F `  M ) )
178175, 177eqtrd 2190 . . . . . . . . . 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 5471 . . . . . . . . 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 8796 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  =  M )  ->  k  <  (
k  +  1 ) )
182 breq2 3969 . . . . . . . . . . . . . . . 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 3512 . . . . . . . . . . . . 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 5836 . . . . . . . . . . . . . . . . 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 7889 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  =  M )  ->  1  e.  CC )
189187, 188pncan2d 8183 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  =  M )  ->  ( ( k  +  1 )  -  k )  =  1 )
190186, 189eqtr3d 2192 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  =  M )  ->  ( M  -  k )  =  1 )
191190oveq2d 5837 . . . . . . . . . . . . . . 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 10541 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  =  M )  ->  ( A ^
1 )  =  A )
194191, 193eqtrd 2190 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  =  M )  ->  ( A ^
( M  -  k
) )  =  A )
195194oveq2d 5837 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  =  M )  ->  ( ( F `
 M )  / 
( A ^ ( M  -  k )
) )  =  ( ( F `  M
)  /  A ) )
196185, 195eqtrd 2190 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  =  M )  ->  if ( k  <  M ,  ( ( F `  M
)  /  ( A ^ ( M  -  k ) ) ) ,  ( F `  k ) )  =  ( ( F `  M )  /  A
) )
197196oveq2d 5837 . . . . . . . . . . 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 8660 . . . . . . . . . . . 12  |-  ( ph  ->  ( A  x.  (
( F `  M
)  /  A ) )  =  ( F `
 M ) )
199198ad3antrrr 484 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  =  M )  ->  ( A  x.  ( ( F `  M )  /  A
) )  =  ( F `  M ) )
200197, 199eqtrd 2190 . . . . . . . . . 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 5471 . . . . . . . . 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 480 . . . . . . . . . . 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 2190 . . . . . . . . . 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 2196 . . . . . . . 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 585 . . . . . . 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 523 . . . . . . . . 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 9217 . . . . . . . . . . . . 13  |-  ( ( M  e.  ZZ  /\  k  e.  ZZ )  ->  ( M  <_  k  <->  M  <  ( k  +  1 ) ) )
212119, 209, 211syl2an2r 585 . . . . . . . . . . . 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 1166 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  M  <  ( k  +  1 ) )  ->  k  e.  (
ZZ>= `  M ) )
215214, 8eleqtrrdi 2251 . . . . . . . . 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 409 . . . . . . . 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 7990 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  M  <  ( k  +  1 ) )  ->  -.  ( k  +  1 )  < 
M )
221220iffalsed 3515 . . . . . . . . 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 5471 . . . . . . . 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 7992 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  M  <  ( k  +  1 ) )  ->  -.  k  <  M )
225224iffalsed 3515 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  M  <  ( k  +  1 ) )  ->  if ( k  <  M ,  ( ( F `  M
)  /  ( A ^ ( M  -  k ) ) ) ,  ( F `  k ) )  =  ( F `  k
) )
226225fveq2d 5471 . . . . . . . . 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 5837 . . . . . . . 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 3996 . . . . . . 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 9205 . . . . . . . 8  |-  ( ( ( k  +  1 )  e.  ZZ  /\  M  e.  ZZ )  ->  ( ( k  +  1 )  <  M  \/  ( k  +  1 )  =  M  \/  M  <  ( k  +  1 ) ) )
230108, 119, 229syl2anc 409 . . . . . . 7  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  (
( k  +  1 )  <  M  \/  ( k  +  1 )  =  M  \/  M  <  ( k  +  1 ) ) )
231171, 206, 228, 230mpjao3dan 1289 . . . . . 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 3968 . . . . . . . . . 10  |-  ( i  =  ( k  +  1 )  ->  (
i  <  M  <->  ( k  +  1 )  < 
M ) )
233 oveq2 5829 . . . . . . . . . . . 12  |-  ( i  =  ( k  +  1 )  ->  ( M  -  i )  =  ( M  -  ( k  +  1 ) ) )
234233oveq2d 5837 . . . . . . . . . . 11  |-  ( i  =  ( k  +  1 )  ->  ( A ^ ( M  -  i ) )  =  ( A ^ ( M  -  ( k  +  1 ) ) ) )
235234oveq2d 5837 . . . . . . . . . 10  |-  ( i  =  ( k  +  1 )  ->  (
( F `  M
)  /  ( A ^ ( M  -  i ) ) )  =  ( ( F `
 M )  / 
( A ^ ( M  -  ( k  +  1 ) ) ) ) )
236 fveq2 5467 . . . . . . . . . 10  |-  ( i  =  ( k  +  1 )  ->  ( F `  i )  =  ( F `  ( k  +  1 ) ) )
237232, 235, 236ifbieq12d 3531 . . . . . . . . 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 5543 . . . . . . . 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 409 . . . . . . 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 5471 . . . . . 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 409 . . . . . . . 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 5471 . . . . . . 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 5837 . . . . . 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 3996 . . . . 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 11423 . . . 4  |-  ( (
ph  /\  1  <_  M )  ->  seq 1
(  +  ,  ( i  e.  NN  |->  if ( i  <  M ,  ( ( F `
 M )  / 
( A ^ ( M  -  i )
) ) ,  ( F `  i ) ) ) )  e. 
dom 
~~>  )
246 eqid 2157 . . . . 5  |-  ( ZZ>= ` 
1 )  =  (
ZZ>= `  1 )
247 1zzd 9189 . . . . . 6  |-  ( (
ph  /\  1  <_  M )  ->  1  e.  ZZ )
248 simpr 109 . . . . . 6  |-  ( (
ph  /\  1  <_  M )  ->  1  <_  M )
249 eluz2 9440 . . . . . 6  |-  ( M  e.  ( ZZ>= `  1
)  <->  ( 1  e.  ZZ  /\  M  e.  ZZ  /\  1  <_  M ) )
250247, 2, 248, 249syl3anbrc 1166 . . . . 5  |-  ( (
ph  /\  1  <_  M )  ->  M  e.  ( ZZ>= `  1 )
)
251246, 250, 85iserex 11231 . . . 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 2234 . 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 9181 . . . . . . 7  |-  ( k  e.  NN  ->  k  e.  ZZ )
260259adantl 275 . . . . . 6  |-  ( ( ( ph  /\  M  <_  1 )  /\  k  e.  NN )  ->  k  e.  ZZ )
261258zred 9281 . . . . . . 7  |-  ( ( ( ph  /\  M  <_  1 )  /\  k  e.  NN )  ->  M  e.  RR )
262 1red 7888 . . . . . . 7  |-  ( ( ( ph  /\  M  <_  1 )  /\  k  e.  NN )  ->  1  e.  RR )
263260zred 9281 . . . . . . 7  |-  ( ( ( ph  /\  M  <_  1 )  /\  k  e.  NN )  ->  k  e.  RR )
264 simplr 520 . . . . . . 7  |-  ( ( ( ph  /\  M  <_  1 )  /\  k  e.  NN )  ->  M  <_  1 )
265 nnge1 8851 . . . . . . . 8  |-  ( k  e.  NN  ->  1  <_  k )
266265adantl 275 . . . . . . 7  |-  ( ( ( ph  /\  M  <_  1 )  /\  k  e.  NN )  ->  1  <_  k )
267261, 262, 263, 264, 266letrd 7994 . . . . . 6  |-  ( ( ( ph  /\  M  <_  1 )  /\  k  e.  NN )  ->  M  <_  k )
268258, 260, 267, 55syl3anbrc 1166 . . . . 5  |-  ( ( ( ph  /\  M  <_  1 )  /\  k  e.  NN )  ->  k  e.  ( ZZ>= `  M )
)
2698eleq2i 2224 . . . . . . 7  |-  ( k  e.  Z  <->  k  e.  ( ZZ>= `  M )
)
270269, 5sylan2br 286 . . . . . 6  |-  ( (
ph  /\  k  e.  ( ZZ>= `  M )
)  ->  ( F `  k )  e.  CC )
271270adantlr 469 . . . . 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 469 . . . . 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 11423 . . 3  |-  ( (
ph  /\  M  <_  1 )  ->  seq 1
(  +  ,  F
)  e.  dom  ~~>  )
277 eqid 2157 . . . 4  |-  ( ZZ>= `  M )  =  (
ZZ>= `  M )
278 1zzd 9189 . . . . 5  |-  ( (
ph  /\  M  <_  1 )  ->  1  e.  ZZ )
279 simpr 109 . . . . 5  |-  ( (
ph  /\  M  <_  1 )  ->  M  <_  1 )
280 eluz2 9440 . . . . 5  |-  ( 1  e.  ( ZZ>= `  M
)  <->  ( M  e.  ZZ  /\  1  e.  ZZ  /\  M  <_ 
1 ) )
281257, 278, 279, 280syl3anbrc 1166 . . . 4  |-  ( (
ph  /\  M  <_  1 )  ->  1  e.  ( ZZ>= `  M )
)
282277, 281, 271iserex 11231 . . 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 9188 . . 3  |-  1  e.  ZZ
285 zletric 9206 . . 3  |-  ( ( 1  e.  ZZ  /\  M  e.  ZZ )  ->  ( 1  <_  M  \/  M  <_  1 ) )
286284, 1, 285sylancr 411 . 2  |-  ( ph  ->  ( 1  <_  M  \/  M  <_  1 ) )
287253, 283, 286mpjaodan 788 1  |-  ( ph  ->  seq M (  +  ,  F )  e. 
dom 
~~>  )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 103    <-> wb 104    \/ wo 698  DECID wdc 820    \/ w3o 962    = wceq 1335    e. wcel 2128   A.wral 2435   ifcif 3505   class class class wbr 3965    |-> cmpt 4025   dom cdm 4585   ` cfv 5169  (class class class)co 5821   CCcc 7725   RRcr 7726   0cc0 7727   1c1 7728    + caddc 7730    x. cmul 7732    < clt 7907    <_ cle 7908    - cmin 8041   # cap 8451    / cdiv 8540   NNcn 8828   ZZcz 9162   ZZ>=cuz 9434   RR+crp 9555    seqcseq 10339   ^cexp 10413   abscabs 10892    ~~> cli 11170
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 604  ax-in2 605  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-13 2130  ax-14 2131  ax-ext 2139  ax-coll 4079  ax-sep 4082  ax-nul 4090  ax-pow 4135  ax-pr 4169  ax-un 4393  ax-setind 4495  ax-iinf 4546  ax-cnex 7818  ax-resscn 7819  ax-1cn 7820  ax-1re 7821  ax-icn 7822  ax-addcl 7823  ax-addrcl 7824  ax-mulcl 7825  ax-mulrcl 7826  ax-addcom 7827  ax-mulcom 7828  ax-addass 7829  ax-mulass 7830  ax-distr 7831  ax-i2m1 7832  ax-0lt1 7833  ax-1rid 7834  ax-0id 7835  ax-rnegex 7836  ax-precex 7837  ax-cnre 7838  ax-pre-ltirr 7839  ax-pre-ltwlin 7840  ax-pre-lttrn 7841  ax-pre-apti 7842  ax-pre-ltadd 7843  ax-pre-mulgt0 7844  ax-pre-mulext 7845  ax-arch 7846  ax-caucvg 7847
This theorem depends on definitions:  df-bi 116  df-dc 821  df-3or 964  df-3an 965  df-tru 1338  df-fal 1341  df-nf 1441  df-sb 1743  df-eu 2009  df-mo 2010  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ne 2328  df-nel 2423  df-ral 2440  df-rex 2441  df-reu 2442  df-rmo 2443  df-rab 2444  df-v 2714  df-sbc 2938  df-csb 3032  df-dif 3104  df-un 3106  df-in 3108  df-ss 3115  df-nul 3395  df-if 3506  df-pw 3545  df-sn 3566  df-pr 3567  df-op 3569  df-uni 3773  df-int 3808  df-iun 3851  df-br 3966  df-opab 4026  df-mpt 4027  df-tr 4063  df-id 4253  df-po 4256  df-iso 4257  df-iord 4326  df-on 4328  df-ilim 4329  df-suc 4331  df-iom 4549  df-xp 4591  df-rel 4592  df-cnv 4593  df-co 4594  df-dm 4595  df-rn 4596  df-res 4597  df-ima 4598  df-iota 5134  df-fun 5171  df-fn 5172  df-f 5173  df-f1 5174  df-fo 5175  df-f1o 5176  df-fv 5177  df-isom 5178  df-riota 5777  df-ov 5824  df-oprab 5825  df-mpo 5826  df-1st 6085  df-2nd 6086  df-recs 6249  df-irdg 6314  df-frec 6335  df-1o 6360  df-oadd 6364  df-er 6477  df-en 6683  df-dom 6684  df-fin 6685  df-pnf 7909  df-mnf 7910  df-xr 7911  df-ltxr 7912  df-le 7913  df-sub 8043  df-neg 8044  df-reap 8445  df-ap 8452  df-div 8541  df-inn 8829  df-2 8887  df-3 8888  df-4 8889  df-n0 9086  df-z 9163  df-uz 9435  df-q 9524  df-rp 9556  df-ico 9793  df-fz 9908  df-fzo 10037  df-seqfrec 10340  df-exp 10414  df-ihash 10645  df-cj 10737  df-re 10738  df-im 10739  df-rsqrt 10893  df-abs 10894  df-clim 11171  df-sumdc 11246
This theorem is referenced by:  cvgratgt0  11425
  Copyright terms: Public domain W3C validator