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

Theorem cvgratz 11495
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 5496 . . . . . 6  |-  ( k  =  x  ->  ( F `  k )  =  ( F `  x ) )
43eleq1d 2239 . . . . 5  |-  ( k  =  x  ->  (
( F `  k
)  e.  CC  <->  ( F `  x )  e.  CC ) )
5 cvgratz.6 . . . . . . 7  |-  ( (
ph  /\  k  e.  Z )  ->  ( F `  k )  e.  CC )
65ralrimiva 2543 . . . . . 6  |-  ( ph  ->  A. k  e.  Z  ( F `  k )  e.  CC )
76ad2antrr 485 . . . . 5  |-  ( ( ( ph  /\  1  <_  M )  /\  x  e.  ( ZZ>= `  M )
)  ->  A. k  e.  Z  ( F `  k )  e.  CC )
8 cvgratz.1 . . . . . . . 8  |-  Z  =  ( ZZ>= `  M )
98eleq2i 2237 . . . . . . 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 2839 . . . 4  |-  ( ( ( ph  /\  1  <_  M )  /\  x  e.  ( ZZ>= `  M )
)  ->  ( F `  x )  e.  CC )
13 eluzelz 9496 . . . . . . . 8  |-  ( k  e.  ( ZZ>= `  M
)  ->  k  e.  ZZ )
1413adantl 275 . . . . . . 7  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= `  M )
)  ->  k  e.  ZZ )
15 1red 7935 . . . . . . . 8  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= `  M )
)  ->  1  e.  RR )
161zred 9334 . . . . . . . . 9  |-  ( ph  ->  M  e.  RR )
1716ad2antrr 485 . . . . . . . 8  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= `  M )
)  ->  M  e.  RR )
1814zred 9334 . . . . . . . 8  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= `  M )
)  ->  k  e.  RR )
19 simplr 525 . . . . . . . 8  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= `  M )
)  ->  1  <_  M )
20 eluzle 9499 . . . . . . . . 9  |-  ( k  e.  ( ZZ>= `  M
)  ->  M  <_  k )
2120adantl 275 . . . . . . . 8  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= `  M )
)  ->  M  <_  k )
2215, 17, 18, 19, 21letrd 8043 . . . . . . 7  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= `  M )
)  ->  1  <_  k )
23 elnnz1 9235 . . . . . . 7  |-  ( k  e.  NN  <->  ( k  e.  ZZ  /\  1  <_ 
k ) )
2414, 22, 23sylanbrc 415 . . . . . 6  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= `  M )
)  ->  k  e.  NN )
25 elnnuz 9523 . . . . . . . 8  |-  ( k  e.  NN  <->  k  e.  ( ZZ>= `  1 )
)
26 fveq2 5496 . . . . . . . . . . . . 13  |-  ( k  =  M  ->  ( F `  k )  =  ( F `  M ) )
2726eleq1d 2239 . . . . . . . . . . . 12  |-  ( k  =  M  ->  (
( F `  k
)  e.  CC  <->  ( F `  M )  e.  CC ) )
28 uzid 9501 . . . . . . . . . . . . . 14  |-  ( M  e.  ZZ  ->  M  e.  ( ZZ>= `  M )
)
291, 28syl 14 . . . . . . . . . . . . 13  |-  ( ph  ->  M  e.  ( ZZ>= `  M ) )
3029, 8eleqtrrdi 2264 . . . . . . . . . . . 12  |-  ( ph  ->  M  e.  Z )
3127, 6, 30rspcdva 2839 . . . . . . . . . . 11  |-  ( ph  ->  ( F `  M
)  e.  CC )
3231ad3antrrr 489 . . . . . . . . . 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 9650 . . . . . . . . . . . . 13  |-  ( ph  ->  A  e.  RR+ )
3635ad3antrrr 489 . . . . . . . . . . . 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 9333 . . . . . . . . . . . . . 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 9339 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= ` 
1 ) )  /\  k  <  M )  -> 
( M  -  k
)  e.  ZZ )
4436, 43rpexpcld 10633 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= ` 
1 ) )  /\  k  <  M )  -> 
( A ^ ( M  -  k )
)  e.  RR+ )
4544rpcnd 9655 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= ` 
1 ) )  /\  k  <  M )  -> 
( A ^ ( M  -  k )
)  e.  CC )
4644rpap0d 9659 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= ` 
1 ) )  /\  k  <  M )  -> 
( A ^ ( M  -  k )
) #  0 )
4732, 45, 46divclapd 8707 . . . . . . . . 9  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= ` 
1 ) )  /\  k  <  M )  -> 
( ( F `  M )  /  ( A ^ ( M  -  k ) ) )  e.  CC )
48 simplll 528 . . . . . . . . . 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 489 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= ` 
1 ) )  /\  -.  k  <  M )  ->  M  e.  RR )
5250zred 9334 . . . . . . . . . . . . 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 8040 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= ` 
1 ) )  /\  -.  k  <  M )  ->  M  <_  k
)
55 eluz2 9493 . . . . . . . . . . . 12  |-  ( k  e.  ( ZZ>= `  M
)  <->  ( M  e.  ZZ  /\  k  e.  ZZ  /\  M  <_ 
k ) )
5649, 50, 54, 55syl3anbrc 1176 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= ` 
1 ) )  /\  -.  k  <  M )  ->  k  e.  (
ZZ>= `  M ) )
5756, 8eleqtrrdi 2264 . . . . . . . . . 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 9289 . . . . . . . . . 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 3555 . . . . . . . 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 3992 . . . . . . . 8  |-  ( i  =  k  ->  (
i  <  M  <->  k  <  M ) )
65 oveq2 5861 . . . . . . . . . 10  |-  ( i  =  k  ->  ( M  -  i )  =  ( M  -  k ) )
6665oveq2d 5869 . . . . . . . . 9  |-  ( i  =  k  ->  ( A ^ ( M  -  i ) )  =  ( A ^ ( M  -  k )
) )
6766oveq2d 5869 . . . . . . . 8  |-  ( i  =  k  ->  (
( F `  M
)  /  ( A ^ ( M  -  i ) ) )  =  ( ( F `
 M )  / 
( A ^ ( M  -  k )
) ) )
68 fveq2 5496 . . . . . . . 8  |-  ( i  =  k  ->  ( F `  i )  =  ( F `  k ) )
6964, 67, 68ifbieq12d 3552 . . . . . . 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 2170 . . . . . . 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 5572 . . . . . 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 8041 . . . . . 6  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= `  M )
)  ->  -.  k  <  M )
7473iffalsed 3536 . . . . 5  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  ( ZZ>= `  M )
)  ->  if (
k  <  M , 
( ( F `  M )  /  ( A ^ ( M  -  k ) ) ) ,  ( F `  k ) )  =  ( F `  k
) )
7572, 74eqtr2d 2204 . . . 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 7899 . . . . 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 10428 . . 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 2239 . . . . . . . 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 489 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  <  M )  ->  ( F `  M )  e.  CC )
8835ad3antrrr 489 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  <  M )  ->  A  e.  RR+ )
892ad2antrr 485 . . . . . . . . . . . . . 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 9337 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  <  M )  ->  ( k  +  1 )  e.  ZZ )
9389, 92zsubcld 9339 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  <  M )  ->  ( M  -  ( k  +  1 ) )  e.  ZZ )
9488, 93rpexpcld 10633 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  <  M )  ->  ( A ^
( M  -  (
k  +  1 ) ) )  e.  RR+ )
9594rpcnd 9655 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  <  M )  ->  ( A ^
( M  -  (
k  +  1 ) ) )  e.  CC )
9694rpap0d 9659 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  <  M )  ->  ( A ^
( M  -  (
k  +  1 ) ) ) #  0 )
9787, 95, 96divclapd 8707 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  <  M )  ->  ( ( F `
 M )  / 
( A ^ ( M  -  ( k  +  1 ) ) ) )  e.  CC )
98 fveq2 5496 . . . . . . . . . . . 12  |-  ( a  =  ( k  +  1 )  ->  ( F `  a )  =  ( F `  ( k  +  1 ) ) )
9998eleq1d 2239 . . . . . . . . . . 11  |-  ( a  =  ( k  +  1 )  ->  (
( F `  a
)  e.  CC  <->  ( F `  ( k  +  1 ) )  e.  CC ) )
100 fveq2 5496 . . . . . . . . . . . . . . 15  |-  ( k  =  a  ->  ( F `  k )  =  ( F `  a ) )
101100eleq1d 2239 . . . . . . . . . . . . . 14  |-  ( k  =  a  ->  (
( F `  k
)  e.  CC  <->  ( F `  a )  e.  CC ) )
102101cbvralv 2696 . . . . . . . . . . . . 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 489 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  -.  ( k  +  1 )  <  M
)  ->  A. a  e.  Z  ( F `  a )  e.  CC )
1052ad2antrr 485 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  -.  ( k  +  1 )  <  M
)  ->  M  e.  ZZ )
106 peano2nn 8890 . . . . . . . . . . . . . . . 16  |-  ( k  e.  NN  ->  (
k  +  1 )  e.  NN )
107106adantl 275 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  (
k  +  1 )  e.  NN )
108107nnzd 9333 . . . . . . . . . . . . . 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 489 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  -.  ( k  +  1 )  <  M
)  ->  M  e.  RR )
111107nnred 8891 . . . . . . . . . . . . . . 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 8040 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  -.  ( k  +  1 )  <  M
)  ->  M  <_  ( k  +  1 ) )
115 eluz2 9493 . . . . . . . . . . . . 13  |-  ( ( k  +  1 )  e.  ( ZZ>= `  M
)  <->  ( M  e.  ZZ  /\  ( k  +  1 )  e.  ZZ  /\  M  <_ 
( k  +  1 ) ) )
116105, 109, 114, 115syl3anbrc 1176 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  -.  ( k  +  1 )  <  M
)  ->  ( k  +  1 )  e.  ( ZZ>= `  M )
)
117116, 8eleqtrrdi 2264 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  -.  ( k  +  1 )  <  M
)  ->  ( k  +  1 )  e.  Z )
11899, 104, 117rspcdva 2839 . . . . . . . . . 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 9289 . . . . . . . . . . 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 3555 . . . . . . . . 9  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  if ( ( k  +  1 )  <  M ,  ( ( F `
 M )  / 
( A ^ ( M  -  ( k  +  1 ) ) ) ) ,  ( F `  ( k  +  1 ) ) )  e.  CC )
123122abscld 11145 . . . . . . . 8  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  ( abs `  if ( ( k  +  1 )  <  M ,  ( ( F `  M
)  /  ( A ^ ( M  -  ( k  +  1 ) ) ) ) ,  ( F `  ( k  +  1 ) ) ) )  e.  RR )
12416recnd 7948 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  M  e.  CC )
125124ad2antrr 485 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  M  e.  CC )
126 simpr 109 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  k  e.  NN )
127126nncnd 8892 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  k  e.  CC )
128 1cnd 7936 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  1  e.  CC )
129125, 127, 128subsub4d 8261 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  (
( M  -  k
)  -  1 )  =  ( M  -  ( k  +  1 ) ) )
130129oveq2d 5869 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  ( A ^ ( ( M  -  k )  - 
1 ) )  =  ( A ^ ( M  -  ( k  +  1 ) ) ) )
13133recnd 7948 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  A  e.  CC )
132131ad2antrr 485 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  A  e.  CC )
13333, 34gt0ap0d 8548 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  A #  0 )
134133ad2antrr 485 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  A #  0 )
135119, 90zsubcld 9339 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  ( M  -  k )  e.  ZZ )
136132, 134, 135expm1apd 10619 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  ( A ^ ( ( M  -  k )  - 
1 ) )  =  ( ( A ^
( M  -  k
) )  /  A
) )
137130, 136eqtr3d 2205 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  ( A ^ ( M  -  ( k  +  1 ) ) )  =  ( ( A ^
( M  -  k
) )  /  A
) )
138137oveq2d 5869 . . . . . . . . . . . 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 3533 . . . . . . . . . . 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 8891 . . . . . . . . . . . . . . . 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 8055 . . . . . . . . . . . . . . . 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 489 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  <  M )  ->  M  e.  RR )
147143ltp1d 8846 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  <  M )  ->  k  <  (
k  +  1 ) )
148143, 145, 146, 147, 140lttrd 8045 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  <  M )  ->  k  <  M
)
149148iftrued 3533 . . . . . . . . . . . . 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 5869 . . . . . . . . . . . 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 485 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  ( F `  M )  e.  CC )
152132, 134, 135expclzapd 10614 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  ( A ^ ( M  -  k ) )  e.  CC )
153132, 134, 135expap0d 10615 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  ( A ^ ( M  -  k ) ) #  0 )
154151, 152, 132, 153, 134divdivap2d 8740 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  (
( F `  M
)  /  ( ( A ^ ( M  -  k ) )  /  A ) )  =  ( ( ( F `  M )  x.  A )  / 
( A ^ ( M  -  k )
) ) )
155151, 132mulcomd 7941 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  (
( F `  M
)  x.  A )  =  ( A  x.  ( F `  M ) ) )
156155oveq1d 5868 . . . . . . . . . . . . . 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 8743 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  (
( A  x.  ( F `  M )
)  /  ( A ^ ( M  -  k ) ) )  =  ( A  x.  ( ( F `  M )  /  ( A ^ ( M  -  k ) ) ) ) )
158154, 156, 1573eqtrd 2207 . . . . . . . . . . . . 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 2206 . . . . . . . . . . 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 2213 . . . . . . . . . 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 5500 . . . . . . . . 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 11158 . . . . . . . . . 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 9657 . . . . . . . . . . . 12  |-  ( ph  ->  0  <_  A )
16633, 165absidd 11131 . . . . . . . . . . 11  |-  ( ph  ->  ( abs `  A
)  =  A )
167166oveq1d 5868 . . . . . . . . . 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 489 . . . . . . . . 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 2207 . . . . . . . 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 8011 . . . . . . . 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 590 . . . . . . 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 485 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  ->  M  e.  RR )
173111, 172lttri3d 8034 . . . . . . . . . . . . 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 3536 . . . . . . . . . . 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 5500 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  =  M )  ->  ( F `  ( k  +  1 ) )  =  ( F `  M ) )
178175, 177eqtrd 2203 . . . . . . . . . 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 5500 . . . . . . . . 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 8846 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  =  M )  ->  k  <  (
k  +  1 ) )
182 breq2 3993 . . . . . . . . . . . . . . . 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 3533 . . . . . . . . . . . . 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 5868 . . . . . . . . . . . . . . . . 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 7936 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  =  M )  ->  1  e.  CC )
189187, 188pncan2d 8232 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  =  M )  ->  ( ( k  +  1 )  -  k )  =  1 )
190186, 189eqtr3d 2205 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  =  M )  ->  ( M  -  k )  =  1 )
191190oveq2d 5869 . . . . . . . . . . . . . . 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 10604 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  =  M )  ->  ( A ^
1 )  =  A )
194191, 193eqtrd 2203 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  =  M )  ->  ( A ^
( M  -  k
) )  =  A )
195194oveq2d 5869 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  =  M )  ->  ( ( F `
 M )  / 
( A ^ ( M  -  k )
) )  =  ( ( F `  M
)  /  A ) )
196185, 195eqtrd 2203 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  =  M )  ->  if ( k  <  M ,  ( ( F `  M
)  /  ( A ^ ( M  -  k ) ) ) ,  ( F `  k ) )  =  ( ( F `  M )  /  A
) )
197196oveq2d 5869 . . . . . . . . . . 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 8709 . . . . . . . . . . . 12  |-  ( ph  ->  ( A  x.  (
( F `  M
)  /  A ) )  =  ( F `
 M ) )
199198ad3antrrr 489 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  ( k  +  1 )  =  M )  ->  ( A  x.  ( ( F `  M )  /  A
) )  =  ( F `  M ) )
200197, 199eqtrd 2203 . . . . . . . . . 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 5500 . . . . . . . . 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 485 . . . . . . . . . . 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 2203 . . . . . . . . . 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 2209 . . . . . . . 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 590 . . . . . . 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 528 . . . . . . . . 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 9267 . . . . . . . . . . . . 13  |-  ( ( M  e.  ZZ  /\  k  e.  ZZ )  ->  ( M  <_  k  <->  M  <  ( k  +  1 ) ) )
212119, 209, 211syl2an2r 590 . . . . . . . . . . . 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 1176 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  M  <  ( k  +  1 ) )  ->  k  e.  (
ZZ>= `  M ) )
215214, 8eleqtrrdi 2264 . . . . . . . . 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 8039 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  M  <  ( k  +  1 ) )  ->  -.  ( k  +  1 )  < 
M )
221220iffalsed 3536 . . . . . . . . 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 5500 . . . . . . . 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 8041 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  M  <  ( k  +  1 ) )  ->  -.  k  <  M )
225224iffalsed 3536 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  1  <_  M )  /\  k  e.  NN )  /\  M  <  ( k  +  1 ) )  ->  if ( k  <  M ,  ( ( F `  M
)  /  ( A ^ ( M  -  k ) ) ) ,  ( F `  k ) )  =  ( F `  k
) )
226225fveq2d 5500 . . . . . . . . 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 5869 . . . . . . . 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 4021 . . . . . . 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 9255 . . . . . . . 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 1302 . . . . . 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 3992 . . . . . . . . . 10  |-  ( i  =  ( k  +  1 )  ->  (
i  <  M  <->  ( k  +  1 )  < 
M ) )
233 oveq2 5861 . . . . . . . . . . . 12  |-  ( i  =  ( k  +  1 )  ->  ( M  -  i )  =  ( M  -  ( k  +  1 ) ) )
234233oveq2d 5869 . . . . . . . . . . 11  |-  ( i  =  ( k  +  1 )  ->  ( A ^ ( M  -  i ) )  =  ( A ^ ( M  -  ( k  +  1 ) ) ) )
235234oveq2d 5869 . . . . . . . . . 10  |-  ( i  =  ( k  +  1 )  ->  (
( F `  M
)  /  ( A ^ ( M  -  i ) ) )  =  ( ( F `
 M )  / 
( A ^ ( M  -  ( k  +  1 ) ) ) ) )
236 fveq2 5496 . . . . . . . . . 10  |-  ( i  =  ( k  +  1 )  ->  ( F `  i )  =  ( F `  ( k  +  1 ) ) )
237232, 235, 236ifbieq12d 3552 . . . . . . . . 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 5572 . . . . . . . 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 5500 . . . . . 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 5500 . . . . . . 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 5869 . . . . . 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 4021 . . . . 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 11494 . . . 4  |-  ( (
ph  /\  1  <_  M )  ->  seq 1
(  +  ,  ( i  e.  NN  |->  if ( i  <  M ,  ( ( F `
 M )  / 
( A ^ ( M  -  i )
) ) ,  ( F `  i ) ) ) )  e. 
dom 
~~>  )
246 eqid 2170 . . . . 5  |-  ( ZZ>= ` 
1 )  =  (
ZZ>= `  1 )
247 1zzd 9239 . . . . . 6  |-  ( (
ph  /\  1  <_  M )  ->  1  e.  ZZ )
248 simpr 109 . . . . . 6  |-  ( (
ph  /\  1  <_  M )  ->  1  <_  M )
249 eluz2 9493 . . . . . 6  |-  ( M  e.  ( ZZ>= `  1
)  <->  ( 1  e.  ZZ  /\  M  e.  ZZ  /\  1  <_  M ) )
250247, 2, 248, 249syl3anbrc 1176 . . . . 5  |-  ( (
ph  /\  1  <_  M )  ->  M  e.  ( ZZ>= `  1 )
)
251246, 250, 85iserex 11302 . . . 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 2247 . 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 9231 . . . . . . 7  |-  ( k  e.  NN  ->  k  e.  ZZ )
260259adantl 275 . . . . . 6  |-  ( ( ( ph  /\  M  <_  1 )  /\  k  e.  NN )  ->  k  e.  ZZ )
261258zred 9334 . . . . . . 7  |-  ( ( ( ph  /\  M  <_  1 )  /\  k  e.  NN )  ->  M  e.  RR )
262 1red 7935 . . . . . . 7  |-  ( ( ( ph  /\  M  <_  1 )  /\  k  e.  NN )  ->  1  e.  RR )
263260zred 9334 . . . . . . 7  |-  ( ( ( ph  /\  M  <_  1 )  /\  k  e.  NN )  ->  k  e.  RR )
264 simplr 525 . . . . . . 7  |-  ( ( ( ph  /\  M  <_  1 )  /\  k  e.  NN )  ->  M  <_  1 )
265 nnge1 8901 . . . . . . . 8  |-  ( k  e.  NN  ->  1  <_  k )
266265adantl 275 . . . . . . 7  |-  ( ( ( ph  /\  M  <_  1 )  /\  k  e.  NN )  ->  1  <_  k )
267261, 262, 263, 264, 266letrd 8043 . . . . . 6  |-  ( ( ( ph  /\  M  <_  1 )  /\  k  e.  NN )  ->  M  <_  k )
268258, 260, 267, 55syl3anbrc 1176 . . . . 5  |-  ( ( ( ph  /\  M  <_  1 )  /\  k  e.  NN )  ->  k  e.  ( ZZ>= `  M )
)
2698eleq2i 2237 . . . . . . 7  |-  ( k  e.  Z  <->  k  e.  ( ZZ>= `  M )
)
270269, 5sylan2br 286 . . . . . 6  |-  ( (
ph  /\  k  e.  ( ZZ>= `  M )
)  ->  ( F `  k )  e.  CC )
271270adantlr 474 . . . . 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 474 . . . . 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 11494 . . 3  |-  ( (
ph  /\  M  <_  1 )  ->  seq 1
(  +  ,  F
)  e.  dom  ~~>  )
277 eqid 2170 . . . 4  |-  ( ZZ>= `  M )  =  (
ZZ>= `  M )
278 1zzd 9239 . . . . 5  |-  ( (
ph  /\  M  <_  1 )  ->  1  e.  ZZ )
279 simpr 109 . . . . 5  |-  ( (
ph  /\  M  <_  1 )  ->  M  <_  1 )
280 eluz2 9493 . . . . 5  |-  ( 1  e.  ( ZZ>= `  M
)  <->  ( M  e.  ZZ  /\  1  e.  ZZ  /\  M  <_ 
1 ) )
281257, 278, 279, 280syl3anbrc 1176 . . . 4  |-  ( (
ph  /\  M  <_  1 )  ->  1  e.  ( ZZ>= `  M )
)
282277, 281, 271iserex 11302 . . 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 9238 . . 3  |-  1  e.  ZZ
285 zletric 9256 . . 3  |-  ( ( 1  e.  ZZ  /\  M  e.  ZZ )  ->  ( 1  <_  M  \/  M  <_  1 ) )
286284, 1, 285sylancr 412 . 2  |-  ( ph  ->  ( 1  <_  M  \/  M  <_  1 ) )
287253, 283, 286mpjaodan 793 1  |-  ( ph  ->  seq M (  +  ,  F )  e. 
dom 
~~>  )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 103    <-> wb 104    \/ wo 703  DECID wdc 829    \/ w3o 972    = wceq 1348    e. wcel 2141   A.wral 2448   ifcif 3526   class class class wbr 3989    |-> cmpt 4050   dom cdm 4611   ` cfv 5198  (class class class)co 5853   CCcc 7772   RRcr 7773   0cc0 7774   1c1 7775    + caddc 7777    x. cmul 7779    < clt 7954    <_ cle 7955    - cmin 8090   # cap 8500    / cdiv 8589   NNcn 8878   ZZcz 9212   ZZ>=cuz 9487   RR+crp 9610    seqcseq 10401   ^cexp 10475   abscabs 10961    ~~> cli 11241
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 609  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-13 2143  ax-14 2144  ax-ext 2152  ax-coll 4104  ax-sep 4107  ax-nul 4115  ax-pow 4160  ax-pr 4194  ax-un 4418  ax-setind 4521  ax-iinf 4572  ax-cnex 7865  ax-resscn 7866  ax-1cn 7867  ax-1re 7868  ax-icn 7869  ax-addcl 7870  ax-addrcl 7871  ax-mulcl 7872  ax-mulrcl 7873  ax-addcom 7874  ax-mulcom 7875  ax-addass 7876  ax-mulass 7877  ax-distr 7878  ax-i2m1 7879  ax-0lt1 7880  ax-1rid 7881  ax-0id 7882  ax-rnegex 7883  ax-precex 7884  ax-cnre 7885  ax-pre-ltirr 7886  ax-pre-ltwlin 7887  ax-pre-lttrn 7888  ax-pre-apti 7889  ax-pre-ltadd 7890  ax-pre-mulgt0 7891  ax-pre-mulext 7892  ax-arch 7893  ax-caucvg 7894
This theorem depends on definitions:  df-bi 116  df-dc 830  df-3or 974  df-3an 975  df-tru 1351  df-fal 1354  df-nf 1454  df-sb 1756  df-eu 2022  df-mo 2023  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ne 2341  df-nel 2436  df-ral 2453  df-rex 2454  df-reu 2455  df-rmo 2456  df-rab 2457  df-v 2732  df-sbc 2956  df-csb 3050  df-dif 3123  df-un 3125  df-in 3127  df-ss 3134  df-nul 3415  df-if 3527  df-pw 3568  df-sn 3589  df-pr 3590  df-op 3592  df-uni 3797  df-int 3832  df-iun 3875  df-br 3990  df-opab 4051  df-mpt 4052  df-tr 4088  df-id 4278  df-po 4281  df-iso 4282  df-iord 4351  df-on 4353  df-ilim 4354  df-suc 4356  df-iom 4575  df-xp 4617  df-rel 4618  df-cnv 4619  df-co 4620  df-dm 4621  df-rn 4622  df-res 4623  df-ima 4624  df-iota 5160  df-fun 5200  df-fn 5201  df-f 5202  df-f1 5203  df-fo 5204  df-f1o 5205  df-fv 5206  df-isom 5207  df-riota 5809  df-ov 5856  df-oprab 5857  df-mpo 5858  df-1st 6119  df-2nd 6120  df-recs 6284  df-irdg 6349  df-frec 6370  df-1o 6395  df-oadd 6399  df-er 6513  df-en 6719  df-dom 6720  df-fin 6721  df-pnf 7956  df-mnf 7957  df-xr 7958  df-ltxr 7959  df-le 7960  df-sub 8092  df-neg 8093  df-reap 8494  df-ap 8501  df-div 8590  df-inn 8879  df-2 8937  df-3 8938  df-4 8939  df-n0 9136  df-z 9213  df-uz 9488  df-q 9579  df-rp 9611  df-ico 9851  df-fz 9966  df-fzo 10099  df-seqfrec 10402  df-exp 10476  df-ihash 10710  df-cj 10806  df-re 10807  df-im 10808  df-rsqrt 10962  df-abs 10963  df-clim 11242  df-sumdc 11317
This theorem is referenced by:  cvgratgt0  11496
  Copyright terms: Public domain W3C validator