Users' Mathboxes Mathbox for Steve Rodriguez < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  radcnvrat Structured version   Visualization version   Unicode version

Theorem radcnvrat 36708
Description: Let  L be the limit, if one exists, of the ratio  ( abs `  (
( A `  (
k  +  1 ) )  /  ( A `
 k ) ) ) (as in the ratio test cvgdvgrat 36707) as  k increases. Then the radius of convergence of power series  sum_ n  e.  NN0 ( ( A `  n )  x.  (
x ^ n ) ) is  ( 1  /  L ) if  L is nonzero. Proof "The limit involved in the ratio test..." in https://en.wikipedia.org/wiki/Radius_of_convergence —a few lines that evidently hide quite an involved process to confirm. (Contributed by Steve Rodriguez, 8-Mar-2020.)
Hypotheses
Ref Expression
radcnvrat.g  |-  G  =  ( x  e.  CC  |->  ( n  e.  NN0  |->  ( ( A `  n )  x.  (
x ^ n ) ) ) )
radcnvrat.a  |-  ( ph  ->  A : NN0 --> CC )
radcnvrat.r  |-  R  =  sup ( { r  e.  RR  |  seq 0 (  +  , 
( G `  r
) )  e.  dom  ~~>  } ,  RR* ,  <  )
radcnvrat.rat  |-  D  =  ( k  e.  NN0  |->  ( abs `  ( ( A `  ( k  +  1 ) )  /  ( A `  k ) ) ) )
radcnvrat.z  |-  Z  =  ( ZZ>= `  M )
radcnvrat.m  |-  ( ph  ->  M  e.  NN0 )
radcnvrat.n0  |-  ( (
ph  /\  k  e.  Z )  ->  ( A `  k )  =/=  0 )
radcnvrat.l  |-  ( ph  ->  D  ~~>  L )
radcnvrat.ln0  |-  ( ph  ->  L  =/=  0 )
Assertion
Ref Expression
radcnvrat  |-  ( ph  ->  R  =  ( 1  /  L ) )
Distinct variable groups:    k, n, x, ph    A, n, x    k, G, n, x    k, r, x, G    k, L, x    k, Z, n    D, k    k, M
Allowed substitution hints:    ph( r)    A( k, r)    D( x, n, r)    R( x, k, n, r)    L( n, r)    M( x, n, r)    Z( x, r)

Proof of Theorem radcnvrat
StepHypRef Expression
1 radcnvrat.r . 2  |-  R  =  sup ( { r  e.  RR  |  seq 0 (  +  , 
( G `  r
) )  e.  dom  ~~>  } ,  RR* ,  <  )
2 xrltso 11474 . . . 4  |-  <  Or  RR*
32a1i 11 . . 3  |-  ( ph  ->  <  Or  RR* )
4 radcnvrat.z . . . . . 6  |-  Z  =  ( ZZ>= `  M )
5 radcnvrat.m . . . . . . 7  |-  ( ph  ->  M  e.  NN0 )
65nn0zd 11072 . . . . . 6  |-  ( ph  ->  M  e.  ZZ )
74reseq2i 5124 . . . . . . 7  |-  ( D  |`  Z )  =  ( D  |`  ( ZZ>= `  M ) )
8 radcnvrat.l . . . . . . . 8  |-  ( ph  ->  D  ~~>  L )
9 radcnvrat.rat . . . . . . . . . 10  |-  D  =  ( k  e.  NN0  |->  ( abs `  ( ( A `  ( k  +  1 ) )  /  ( A `  k ) ) ) )
10 nn0ex 10909 . . . . . . . . . . 11  |-  NN0  e.  _V
1110mptex 6166 . . . . . . . . . 10  |-  ( k  e.  NN0  |->  ( abs `  ( ( A `  ( k  +  1 ) )  /  ( A `  k )
) ) )  e. 
_V
129, 11eqeltri 2536 . . . . . . . . 9  |-  D  e. 
_V
13 climres 13694 . . . . . . . . 9  |-  ( ( M  e.  ZZ  /\  D  e.  _V )  ->  ( ( D  |`  ( ZZ>= `  M )
)  ~~>  L  <->  D  ~~>  L ) )
146, 12, 13sylancl 673 . . . . . . . 8  |-  ( ph  ->  ( ( D  |`  ( ZZ>= `  M )
)  ~~>  L  <->  D  ~~>  L ) )
158, 14mpbird 240 . . . . . . 7  |-  ( ph  ->  ( D  |`  ( ZZ>=
`  M ) )  ~~>  L )
167, 15syl5eqbr 4452 . . . . . 6  |-  ( ph  ->  ( D  |`  Z )  ~~>  L )
179reseq1i 5123 . . . . . . . . 9  |-  ( D  |`  Z )  =  ( ( k  e.  NN0  |->  ( abs `  ( ( A `  ( k  +  1 ) )  /  ( A `  k ) ) ) )  |`  Z )
18 eluznn0 11262 . . . . . . . . . . . . . 14  |-  ( ( M  e.  NN0  /\  k  e.  ( ZZ>= `  M ) )  -> 
k  e.  NN0 )
195, 18sylan 478 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  ( ZZ>= `  M )
)  ->  k  e.  NN0 )
2019ex 440 . . . . . . . . . . . 12  |-  ( ph  ->  ( k  e.  (
ZZ>= `  M )  -> 
k  e.  NN0 )
)
2120ssrdv 3450 . . . . . . . . . . 11  |-  ( ph  ->  ( ZZ>= `  M )  C_ 
NN0 )
224, 21syl5eqss 3488 . . . . . . . . . 10  |-  ( ph  ->  Z  C_  NN0 )
2322resmptd 5178 . . . . . . . . 9  |-  ( ph  ->  ( ( k  e. 
NN0  |->  ( abs `  (
( A `  (
k  +  1 ) )  /  ( A `
 k ) ) ) )  |`  Z )  =  ( k  e.  Z  |->  ( abs `  (
( A `  (
k  +  1 ) )  /  ( A `
 k ) ) ) ) )
2417, 23syl5eq 2508 . . . . . . . 8  |-  ( ph  ->  ( D  |`  Z )  =  ( k  e.  Z  |->  ( abs `  (
( A `  (
k  +  1 ) )  /  ( A `
 k ) ) ) ) )
25 fvex 5902 . . . . . . . . 9  |-  ( abs `  ( ( A `  ( k  +  1 ) )  /  ( A `  k )
) )  e.  _V
2625a1i 11 . . . . . . . 8  |-  ( (
ph  /\  k  e.  Z )  ->  ( abs `  ( ( A `
 ( k  +  1 ) )  / 
( A `  k
) ) )  e. 
_V )
2724, 26fvmpt2d 5987 . . . . . . 7  |-  ( (
ph  /\  k  e.  Z )  ->  (
( D  |`  Z ) `
 k )  =  ( abs `  (
( A `  (
k  +  1 ) )  /  ( A `
 k ) ) ) )
284peano2uzs 11247 . . . . . . . . . 10  |-  ( k  e.  Z  ->  (
k  +  1 )  e.  Z )
2922sselda 3444 . . . . . . . . . . 11  |-  ( (
ph  /\  ( k  +  1 )  e.  Z )  ->  (
k  +  1 )  e.  NN0 )
30 radcnvrat.a . . . . . . . . . . . 12  |-  ( ph  ->  A : NN0 --> CC )
3130ffvelrnda 6050 . . . . . . . . . . 11  |-  ( (
ph  /\  ( k  +  1 )  e. 
NN0 )  ->  ( A `  ( k  +  1 ) )  e.  CC )
3229, 31syldan 477 . . . . . . . . . 10  |-  ( (
ph  /\  ( k  +  1 )  e.  Z )  ->  ( A `  ( k  +  1 ) )  e.  CC )
3328, 32sylan2 481 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  Z )  ->  ( A `  ( k  +  1 ) )  e.  CC )
3422sselda 3444 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  Z )  ->  k  e.  NN0 )
3530ffvelrnda 6050 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( A `  k )  e.  CC )
3634, 35syldan 477 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  Z )  ->  ( A `  k )  e.  CC )
37 radcnvrat.n0 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  Z )  ->  ( A `  k )  =/=  0 )
3833, 36, 37divcld 10416 . . . . . . . 8  |-  ( (
ph  /\  k  e.  Z )  ->  (
( A `  (
k  +  1 ) )  /  ( A `
 k ) )  e.  CC )
3938abscld 13553 . . . . . . 7  |-  ( (
ph  /\  k  e.  Z )  ->  ( abs `  ( ( A `
 ( k  +  1 ) )  / 
( A `  k
) ) )  e.  RR )
4027, 39eqeltrd 2540 . . . . . 6  |-  ( (
ph  /\  k  e.  Z )  ->  (
( D  |`  Z ) `
 k )  e.  RR )
414, 6, 16, 40climrecl 13702 . . . . 5  |-  ( ph  ->  L  e.  RR )
42 radcnvrat.ln0 . . . . 5  |-  ( ph  ->  L  =/=  0 )
4341, 42rereccld 10467 . . . 4  |-  ( ph  ->  ( 1  /  L
)  e.  RR )
4443rexrd 9721 . . 3  |-  ( ph  ->  ( 1  /  L
)  e.  RR* )
45 simpr 467 . . . 4  |-  ( (
ph  /\  x  e.  { r  e.  RR  |  seq 0 (  +  , 
( G `  r
) )  e.  dom  ~~>  } )  ->  x  e.  { r  e.  RR  |  seq 0 (  +  , 
( G `  r
) )  e.  dom  ~~>  } )
46 elrabi 3205 . . . . 5  |-  ( x  e.  { r  e.  RR  |  seq 0
(  +  ,  ( G `  r ) )  e.  dom  ~~>  }  ->  x  e.  RR )
4743adantr 471 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  RR )  ->  ( 1  /  L )  e.  RR )
48 recn 9660 . . . . . . . . . . . . 13  |-  ( x  e.  RR  ->  x  e.  CC )
4948abscld 13553 . . . . . . . . . . . 12  |-  ( x  e.  RR  ->  ( abs `  x )  e.  RR )
5049adantl 472 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  RR )  ->  ( abs `  x )  e.  RR )
5147, 50ltlend 9811 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( 1  /  L )  <  ( abs `  x
)  <->  ( ( 1  /  L )  <_ 
( abs `  x
)  /\  ( abs `  x )  =/=  (
1  /  L ) ) ) )
5251simplbda 634 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR )  /\  (
1  /  L )  <  ( abs `  x
) )  ->  ( abs `  x )  =/=  ( 1  /  L
) )
5351adantr 471 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR )  /\  ( abs `  x )  =/=  ( 1  /  L
) )  ->  (
( 1  /  L
)  <  ( abs `  x )  <->  ( (
1  /  L )  <_  ( abs `  x
)  /\  ( abs `  x )  =/=  (
1  /  L ) ) ) )
54 simpr 467 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  RR )  /\  ( abs `  x )  =/=  ( 1  /  L
) )  ->  ( abs `  x )  =/=  ( 1  /  L
) )
5554biantrud 514 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR )  /\  ( abs `  x )  =/=  ( 1  /  L
) )  ->  (
( 1  /  L
)  <_  ( abs `  x )  <->  ( (
1  /  L )  <_  ( abs `  x
)  /\  ( abs `  x )  =/=  (
1  /  L ) ) ) )
5647, 50lenltd 9812 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( 1  /  L )  <_  ( abs `  x
)  <->  -.  ( abs `  x )  <  (
1  /  L ) ) )
5756adantr 471 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR )  /\  ( abs `  x )  =/=  ( 1  /  L
) )  ->  (
( 1  /  L
)  <_  ( abs `  x )  <->  -.  ( abs `  x )  < 
( 1  /  L
) ) )
5853, 55, 573bitr2d 289 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR )  /\  ( abs `  x )  =/=  ( 1  /  L
) )  ->  (
( 1  /  L
)  <  ( abs `  x )  <->  -.  ( abs `  x )  < 
( 1  /  L
) ) )
59 1cnd 9690 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  RR )  ->  1  e.  CC )
6050recnd 9700 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  RR )  ->  ( abs `  x )  e.  CC )
6141recnd 9700 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  L  e.  CC )
6261adantr 471 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  RR )  ->  L  e.  CC )
6342adantr 471 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  RR )  ->  L  =/=  0 )
6459, 60, 62, 63divmul3d 10450 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( 1  /  L )  =  ( abs `  x
)  <->  1  =  ( ( abs `  x
)  x.  L ) ) )
65 eqcom 2469 . . . . . . . . . . . . . . . . 17  |-  ( ( 1  /  L )  =  ( abs `  x
)  <->  ( abs `  x
)  =  ( 1  /  L ) )
66 eqcom 2469 . . . . . . . . . . . . . . . . 17  |-  ( 1  =  ( ( abs `  x )  x.  L
)  <->  ( ( abs `  x )  x.  L
)  =  1 )
6764, 65, 663bitr3g 295 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( abs `  x )  =  ( 1  /  L )  <->  ( ( abs `  x )  x.  L )  =  1 ) )
6867necon3bid 2680 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( abs `  x )  =/=  ( 1  /  L )  <->  ( ( abs `  x )  x.  L )  =/=  1
) )
6968biimpa 491 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  RR )  /\  ( abs `  x )  =/=  ( 1  /  L
) )  ->  (
( abs `  x
)  x.  L )  =/=  1 )
70 1red 9689 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  RR )  ->  1  e.  RR )
71 fvres 5906 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( k  e.  Z  ->  (
( D  |`  Z ) `
 k )  =  ( D `  k
) )
7271adantl 472 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  k  e.  Z )  ->  (
( D  |`  Z ) `
 k )  =  ( D `  k
) )
7372, 40eqeltrrd 2541 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  k  e.  Z )  ->  ( D `  k )  e.  RR )
7438absge0d 13561 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  k  e.  Z )  ->  0  <_  ( abs `  (
( A `  (
k  +  1 ) )  /  ( A `
 k ) ) ) )
7574, 27breqtrrd 4445 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  k  e.  Z )  ->  0  <_  ( ( D  |`  Z ) `  k
) )
7675, 72breqtrd 4443 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  k  e.  Z )  ->  0  <_  ( D `  k
) )
774, 6, 8, 73, 76climge0 13703 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  0  <_  L )
7841, 77, 42ne0gt0d 9803 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  0  <  L )
7941, 78elrpd 11372 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  L  e.  RR+ )
8079adantr 471 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  RR )  ->  L  e.  RR+ )
8150, 70, 80ltmuldivd 11419 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( ( abs `  x
)  x.  L )  <  1  <->  ( abs `  x )  <  (
1  /  L ) ) )
8281adantr 471 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  RR )  /\  (
( abs `  x
)  x.  L )  =/=  1 )  -> 
( ( ( abs `  x )  x.  L
)  <  1  <->  ( abs `  x )  <  (
1  /  L ) ) )
83 elun 3586 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  ( ( RR 
i^i  { 0 } )  u.  ( RR  \  { 0 } ) )  <->  ( x  e.  ( RR  i^i  {
0 } )  \/  x  e.  ( RR 
\  { 0 } ) ) )
84 inundif 3857 . . . . . . . . . . . . . . . . . . 19  |-  ( ( RR  i^i  { 0 } )  u.  ( RR  \  { 0 } ) )  =  RR
8584eleq2i 2532 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  ( ( RR 
i^i  { 0 } )  u.  ( RR  \  { 0 } ) )  <->  x  e.  RR )
8683, 85bitr3i 259 . . . . . . . . . . . . . . . . 17  |-  ( ( x  e.  ( RR 
i^i  { 0 } )  \/  x  e.  ( RR  \  { 0 } ) )  <->  x  e.  RR )
87 elin 3629 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  ( RR  i^i  { 0 } )  <->  ( x  e.  RR  /\  x  e. 
{ 0 } ) )
8887simprbi 470 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  ( RR  i^i  { 0 } )  ->  x  e.  { 0 } )
89 elsni 4005 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  { 0 }  ->  x  =  0 )
9088, 89syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  ( RR  i^i  { 0 } )  ->  x  =  0 )
91 fveq2 5892 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  =  0  ->  ( abs `  x )  =  ( abs `  0
) )
92 abs0 13403 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( abs `  0 )  =  0
9391, 92syl6eq 2512 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  =  0  ->  ( abs `  x )  =  0 )
9493oveq1d 6335 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  0  ->  (
( abs `  x
)  x.  L )  =  ( 0  x.  L ) )
9561mul02d 9862 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( 0  x.  L
)  =  0 )
9694, 95sylan9eqr 2518 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  = 
0 )  ->  (
( abs `  x
)  x.  L )  =  0 )
97 0lt1 10169 . . . . . . . . . . . . . . . . . . . . . 22  |-  0  <  1
9896, 97syl6eqbr 4456 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  = 
0 )  ->  (
( abs `  x
)  x.  L )  <  1 )
99 radcnvrat.g . . . . . . . . . . . . . . . . . . . . . . . 24  |-  G  =  ( x  e.  CC  |->  ( n  e.  NN0  |->  ( ( A `  n )  x.  (
x ^ n ) ) ) )
10099, 30radcnv0 23427 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  0  e.  { r  e.  RR  |  seq 0 (  +  , 
( G `  r
) )  e.  dom  ~~>  } )
101 eleq1 2528 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  0  ->  (
x  e.  { r  e.  RR  |  seq 0 (  +  , 
( G `  r
) )  e.  dom  ~~>  }  <->  0  e.  { r  e.  RR  |  seq 0 (  +  , 
( G `  r
) )  e.  dom  ~~>  } ) )
102100, 101syl5ibrcom 230 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( x  =  0  ->  x  e.  {
r  e.  RR  |  seq 0 (  +  , 
( G `  r
) )  e.  dom  ~~>  } ) )
103102imp 435 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  = 
0 )  ->  x  e.  { r  e.  RR  |  seq 0 (  +  ,  ( G `  r ) )  e. 
dom 
~~>  } )
10498, 1032thd 248 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  = 
0 )  ->  (
( ( abs `  x
)  x.  L )  <  1  <->  x  e.  { r  e.  RR  |  seq 0 (  +  , 
( G `  r
) )  e.  dom  ~~>  } ) )
10590, 104sylan2 481 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  ( RR  i^i  { 0 } ) )  -> 
( ( ( abs `  x )  x.  L
)  <  1  <->  x  e.  { r  e.  RR  |  seq 0 (  +  , 
( G `  r
) )  e.  dom  ~~>  } ) )
106105adantlr 726 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
( abs `  x
)  x.  L )  =/=  1 )  /\  x  e.  ( RR  i^i  { 0 } ) )  ->  ( (
( abs `  x
)  x.  L )  <  1  <->  x  e.  { r  e.  RR  |  seq 0 (  +  , 
( G `  r
) )  e.  dom  ~~>  } ) )
107 ax-resscn 9627 . . . . . . . . . . . . . . . . . . . . . . 23  |-  RR  C_  CC
108 ssdif 3580 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( RR  C_  CC  ->  ( RR  \  { 0 } ) 
C_  ( CC  \  { 0 } ) )
109107, 108ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( RR 
\  { 0 } )  C_  ( CC  \  { 0 } )
110109sseli 3440 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  ( RR  \  { 0 } )  ->  x  e.  ( CC  \  { 0 } ) )
111 nn0uz 11227 . . . . . . . . . . . . . . . . . . . . . 22  |-  NN0  =  ( ZZ>= `  0 )
1125ad2antrr 737 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  ( ( abs `  x )  x.  L
)  =/=  1 )  ->  M  e.  NN0 )
113 fvex 5902 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( G `
 x )  e. 
_V
114113a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  ( ( abs `  x )  x.  L
)  =/=  1 )  ->  ( G `  x )  e.  _V )
115 eldifi 3567 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  e.  ( CC  \  { 0 } )  ->  x  e.  CC )
11699a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  G  =  ( x  e.  CC  |->  ( n  e.  NN0  |->  ( ( A `  n )  x.  ( x ^
n ) ) ) ) )
11710mptex 6166 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( n  e.  NN0  |->  ( ( A `  n )  x.  ( x ^
n ) ) )  e.  _V
118117a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  x  e.  CC )  ->  ( n  e.  NN0  |->  ( ( A `  n )  x.  ( x ^
n ) ) )  e.  _V )
119116, 118fvmpt2d 5987 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  x  e.  CC )  ->  ( G `
 x )  =  ( n  e.  NN0  |->  ( ( A `  n )  x.  (
x ^ n ) ) ) )
120119adantr 471 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  x  e.  CC )  /\  k  e.  NN0 )  ->  ( G `  x )  =  ( n  e. 
NN0  |->  ( ( A `
 n )  x.  ( x ^ n
) ) ) )
121 fveq2 5892 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( n  =  k  ->  ( A `  n )  =  ( A `  k ) )
122 oveq2 6328 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( n  =  k  ->  (
x ^ n )  =  ( x ^
k ) )
123121, 122oveq12d 6338 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( n  =  k  ->  (
( A `  n
)  x.  ( x ^ n ) )  =  ( ( A `
 k )  x.  ( x ^ k
) ) )
124123adantl 472 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  x  e.  CC )  /\  k  e.  NN0 )  /\  n  =  k )  ->  ( ( A `  n )  x.  ( x ^ n
) )  =  ( ( A `  k
)  x.  ( x ^ k ) ) )
125 simpr 467 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  x  e.  CC )  /\  k  e.  NN0 )  ->  k  e.  NN0 )
126 ovex 6348 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( A `  k )  x.  ( x ^
k ) )  e. 
_V
127126a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  x  e.  CC )  /\  k  e.  NN0 )  ->  (
( A `  k
)  x.  ( x ^ k ) )  e.  _V )
128120, 124, 125, 127fvmptd 5982 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  x  e.  CC )  /\  k  e.  NN0 )  ->  (
( G `  x
) `  k )  =  ( ( A `
 k )  x.  ( x ^ k
) ) )
12935adantlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  x  e.  CC )  /\  k  e.  NN0 )  ->  ( A `  k )  e.  CC )
130 simplr 767 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  x  e.  CC )  /\  k  e.  NN0 )  ->  x  e.  CC )
131130, 125expcld 12454 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  x  e.  CC )  /\  k  e.  NN0 )  ->  (
x ^ k )  e.  CC )
132129, 131mulcld 9694 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  x  e.  CC )  /\  k  e.  NN0 )  ->  (
( A `  k
)  x.  ( x ^ k ) )  e.  CC )
133128, 132eqeltrd 2540 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  x  e.  CC )  /\  k  e.  NN0 )  ->  (
( G `  x
) `  k )  e.  CC )
134115, 133sylanl2 661 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  NN0 )  ->  ( ( G `
 x ) `  k )  e.  CC )
135134adantlr 726 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  x  e.  ( CC  \  { 0 } ) )  /\  ( ( abs `  x )  x.  L )  =/=  1 )  /\  k  e.  NN0 )  ->  (
( G `  x
) `  k )  e.  CC )
13634adantlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  x  e.  CC )  /\  k  e.  Z )  ->  k  e.  NN0 )
137136, 128syldan 477 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  x  e.  CC )  /\  k  e.  Z )  ->  (
( G `  x
) `  k )  =  ( ( A `
 k )  x.  ( x ^ k
) ) )
138115, 137sylanl2 661 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( ( G `  x ) `  k )  =  ( ( A `  k
)  x.  ( x ^ k ) ) )
13936adantlr 726 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( A `  k )  e.  CC )
140115adantl 472 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  x  e.  ( CC  \  { 0 } ) )  ->  x  e.  CC )
141140adantr 471 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  x  e.  CC )
14234adantlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  k  e.  NN0 )
143141, 142expcld 12454 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( x ^ k )  e.  CC )
14437adantlr 726 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( A `  k )  =/=  0
)
145 eldifsni 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( x  e.  ( CC  \  { 0 } )  ->  x  =/=  0
)
146145ad2antlr 738 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  x  =/=  0 )
147142nn0zd 11072 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  k  e.  ZZ )
148141, 146, 147expne0d 12460 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( x ^ k )  =/=  0 )
149139, 143, 144, 148mulne0d 10297 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( ( A `  k )  x.  ( x ^ k
) )  =/=  0
)
150138, 149eqnetrd 2703 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( ( G `  x ) `  k )  =/=  0
)
151150adantlr 726 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  x  e.  ( CC  \  { 0 } ) )  /\  ( ( abs `  x )  x.  L )  =/=  1 )  /\  k  e.  Z )  ->  (
( G `  x
) `  k )  =/=  0 )
152 oveq1 6327 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( n  =  k  ->  (
n  +  1 )  =  ( k  +  1 ) )
153152fveq2d 5896 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( n  =  k  ->  (
( G `  x
) `  ( n  +  1 ) )  =  ( ( G `
 x ) `  ( k  +  1 ) ) )
154 fveq2 5892 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( n  =  k  ->  (
( G `  x
) `  n )  =  ( ( G `
 x ) `  k ) )
155153, 154oveq12d 6338 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( n  =  k  ->  (
( ( G `  x ) `  (
n  +  1 ) )  /  ( ( G `  x ) `
 n ) )  =  ( ( ( G `  x ) `
 ( k  +  1 ) )  / 
( ( G `  x ) `  k
) ) )
156155fveq2d 5896 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  =  k  ->  ( abs `  ( ( ( G `  x ) `
 ( n  + 
1 ) )  / 
( ( G `  x ) `  n
) ) )  =  ( abs `  (
( ( G `  x ) `  (
k  +  1 ) )  /  ( ( G `  x ) `
 k ) ) ) )
157156cbvmptv 4511 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( n  e.  Z  |->  ( abs `  ( ( ( G `
 x ) `  ( n  +  1
) )  /  (
( G `  x
) `  n )
) ) )  =  ( k  e.  Z  |->  ( abs `  (
( ( G `  x ) `  (
k  +  1 ) )  /  ( ( G `  x ) `
 k ) ) ) )
1584reseq2i 5124 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( n  e.  NN0  |->  ( abs `  ( ( ( G `
 x ) `  ( n  +  1
) )  /  (
( G `  x
) `  n )
) ) )  |`  Z )  =  ( ( n  e.  NN0  |->  ( abs `  ( ( ( G `  x
) `  ( n  +  1 ) )  /  ( ( G `
 x ) `  n ) ) ) )  |`  ( ZZ>= `  M ) )
15922adantr 471 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  x  e.  ( CC  \  { 0 } ) )  ->  Z  C_  NN0 )
160159resmptd 5178 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  x  e.  ( CC  \  { 0 } ) )  -> 
( ( n  e. 
NN0  |->  ( abs `  (
( ( G `  x ) `  (
n  +  1 ) )  /  ( ( G `  x ) `
 n ) ) ) )  |`  Z )  =  ( n  e.  Z  |->  ( abs `  (
( ( G `  x ) `  (
n  +  1 ) )  /  ( ( G `  x ) `
 n ) ) ) ) )
161158, 160syl5eqr 2510 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  x  e.  ( CC  \  { 0 } ) )  -> 
( ( n  e. 
NN0  |->  ( abs `  (
( ( G `  x ) `  (
n  +  1 ) )  /  ( ( G `  x ) `
 n ) ) ) )  |`  ( ZZ>=
`  M ) )  =  ( n  e.  Z  |->  ( abs `  (
( ( G `  x ) `  (
n  +  1 ) )  /  ( ( G `  x ) `
 n ) ) ) ) )
1626adantr 471 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  x  e.  ( CC  \  { 0 } ) )  ->  M  e.  ZZ )
1638adantr 471 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  x  e.  ( CC  \  { 0 } ) )  ->  D 
~~>  L )
164140abscld 13553 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  x  e.  ( CC  \  { 0 } ) )  -> 
( abs `  x
)  e.  RR )
165164recnd 9700 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  x  e.  ( CC  \  { 0 } ) )  -> 
( abs `  x
)  e.  CC )
16610mptex 6166 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( n  e.  NN0  |->  ( abs `  ( ( ( G `
 x ) `  ( n  +  1
) )  /  (
( G `  x
) `  n )
) ) )  e. 
_V
167166a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  x  e.  ( CC  \  { 0 } ) )  -> 
( n  e.  NN0  |->  ( abs `  ( ( ( G `  x
) `  ( n  +  1 ) )  /  ( ( G `
 x ) `  n ) ) ) )  e.  _V )
16873recnd 9700 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  k  e.  Z )  ->  ( D `  k )  e.  CC )
169168adantlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( D `  k )  e.  CC )
170 eqidd 2463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( n  e.  NN0  |->  ( abs `  (
( ( G `  x ) `  (
n  +  1 ) )  /  ( ( G `  x ) `
 n ) ) ) )  =  ( n  e.  NN0  |->  ( abs `  ( ( ( G `
 x ) `  ( n  +  1
) )  /  (
( G `  x
) `  n )
) ) ) )
171156adantl 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ph  /\  x  e.  ( CC  \  { 0 } ) )  /\  k  e.  Z )  /\  n  =  k )  -> 
( abs `  (
( ( G `  x ) `  (
n  +  1 ) )  /  ( ( G `  x ) `
 n ) ) )  =  ( abs `  ( ( ( G `
 x ) `  ( k  +  1 ) )  /  (
( G `  x
) `  k )
) ) )
172 fvex 5902 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( abs `  ( ( ( G `
 x ) `  ( k  +  1 ) )  /  (
( G `  x
) `  k )
) )  e.  _V
173172a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( abs `  ( ( ( G `
 x ) `  ( k  +  1 ) )  /  (
( G `  x
) `  k )
) )  e.  _V )
174170, 171, 142, 173fvmptd 5982 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( (
n  e.  NN0  |->  ( abs `  ( ( ( G `
 x ) `  ( n  +  1
) )  /  (
( G `  x
) `  n )
) ) ) `  k )  =  ( abs `  ( ( ( G `  x
) `  ( k  +  1 ) )  /  ( ( G `
 x ) `  k ) ) ) )
175119adantr 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  x  e.  CC )  /\  k  e.  Z )  ->  ( G `  x )  =  ( n  e. 
NN0  |->  ( ( A `
 n )  x.  ( x ^ n
) ) ) )
176 simpr 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ph  /\  x  e.  CC )  /\  k  e.  Z
)  /\  n  =  ( k  +  1 ) )  ->  n  =  ( k  +  1 ) )
177176fveq2d 5896 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ph  /\  x  e.  CC )  /\  k  e.  Z
)  /\  n  =  ( k  +  1 ) )  ->  ( A `  n )  =  ( A `  ( k  +  1 ) ) )
178176oveq2d 6336 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ph  /\  x  e.  CC )  /\  k  e.  Z
)  /\  n  =  ( k  +  1 ) )  ->  (
x ^ n )  =  ( x ^
( k  +  1 ) ) )
179177, 178oveq12d 6338 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ph  /\  x  e.  CC )  /\  k  e.  Z
)  /\  n  =  ( k  +  1 ) )  ->  (
( A `  n
)  x.  ( x ^ n ) )  =  ( ( A `
 ( k  +  1 ) )  x.  ( x ^ (
k  +  1 ) ) ) )
180 1nn0 10919 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  1  e.  NN0
181180a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ph  /\  x  e.  CC )  /\  k  e.  Z )  ->  1  e.  NN0 )
182136, 181nn0addcld 10963 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  x  e.  CC )  /\  k  e.  Z )  ->  (
k  +  1 )  e.  NN0 )
183 ovex 6348 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( A `  ( k  +  1 ) )  x.  ( x ^
( k  +  1 ) ) )  e. 
_V
184183a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  x  e.  CC )  /\  k  e.  Z )  ->  (
( A `  (
k  +  1 ) )  x.  ( x ^ ( k  +  1 ) ) )  e.  _V )
185175, 179, 182, 184fvmptd 5982 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  x  e.  CC )  /\  k  e.  Z )  ->  (
( G `  x
) `  ( k  +  1 ) )  =  ( ( A `
 ( k  +  1 ) )  x.  ( x ^ (
k  +  1 ) ) ) )
186123adantl 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ph  /\  x  e.  CC )  /\  k  e.  Z
)  /\  n  =  k )  ->  (
( A `  n
)  x.  ( x ^ n ) )  =  ( ( A `
 k )  x.  ( x ^ k
) ) )
187126a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  x  e.  CC )  /\  k  e.  Z )  ->  (
( A `  k
)  x.  ( x ^ k ) )  e.  _V )
188175, 186, 136, 187fvmptd 5982 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  x  e.  CC )  /\  k  e.  Z )  ->  (
( G `  x
) `  k )  =  ( ( A `
 k )  x.  ( x ^ k
) ) )
189185, 188oveq12d 6338 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  x  e.  CC )  /\  k  e.  Z )  ->  (
( ( G `  x ) `  (
k  +  1 ) )  /  ( ( G `  x ) `
 k ) )  =  ( ( ( A `  ( k  +  1 ) )  x.  ( x ^
( k  +  1 ) ) )  / 
( ( A `  k )  x.  (
x ^ k ) ) ) )
190115, 189sylanl2 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( (
( G `  x
) `  ( k  +  1 ) )  /  ( ( G `
 x ) `  k ) )  =  ( ( ( A `
 ( k  +  1 ) )  x.  ( x ^ (
k  +  1 ) ) )  /  (
( A `  k
)  x.  ( x ^ k ) ) ) )
19133adantlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( A `  ( k  +  1 ) )  e.  CC )
192115, 182sylanl2 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( k  +  1 )  e. 
NN0 )
193141, 192expcld 12454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( x ^ ( k  +  1 ) )  e.  CC )
194191, 139, 193, 143, 144, 148divmuldivd 10457 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( (
( A `  (
k  +  1 ) )  /  ( A `
 k ) )  x.  ( ( x ^ ( k  +  1 ) )  / 
( x ^ k
) ) )  =  ( ( ( A `
 ( k  +  1 ) )  x.  ( x ^ (
k  +  1 ) ) )  /  (
( A `  k
)  x.  ( x ^ k ) ) ) )
195142nn0cnd 10961 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  k  e.  CC )
196 1cnd 9690 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  1  e.  CC )
197195, 196pncan2d 10019 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( (
k  +  1 )  -  k )  =  1 )
198197oveq2d 6336 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( x ^ ( ( k  +  1 )  -  k ) )  =  ( x ^ 1 ) )
199192nn0zd 11072 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( k  +  1 )  e.  ZZ )
200141, 146, 147, 199expsubd 12465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( x ^ ( ( k  +  1 )  -  k ) )  =  ( ( x ^
( k  +  1 ) )  /  (
x ^ k ) ) )
201141exp1d 12449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( x ^ 1 )  =  x )
202198, 200, 2013eqtr3d 2504 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( (
x ^ ( k  +  1 ) )  /  ( x ^
k ) )  =  x )
203202oveq2d 6336 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( (
( A `  (
k  +  1 ) )  /  ( A `
 k ) )  x.  ( ( x ^ ( k  +  1 ) )  / 
( x ^ k
) ) )  =  ( ( ( A `
 ( k  +  1 ) )  / 
( A `  k
) )  x.  x
) )
204190, 194, 2033eqtr2d 2502 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( (
( G `  x
) `  ( k  +  1 ) )  /  ( ( G `
 x ) `  k ) )  =  ( ( ( A `
 ( k  +  1 ) )  / 
( A `  k
) )  x.  x
) )
205204fveq2d 5896 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( abs `  ( ( ( G `
 x ) `  ( k  +  1 ) )  /  (
( G `  x
) `  k )
) )  =  ( abs `  ( ( ( A `  (
k  +  1 ) )  /  ( A `
 k ) )  x.  x ) ) )
20638adantlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( ( A `  ( k  +  1 ) )  /  ( A `  k ) )  e.  CC )
207206, 141absmuld 13571 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( abs `  ( ( ( A `
 ( k  +  1 ) )  / 
( A `  k
) )  x.  x
) )  =  ( ( abs `  (
( A `  (
k  +  1 ) )  /  ( A `
 k ) ) )  x.  ( abs `  x ) ) )
208174, 205, 2073eqtrd 2500 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( (
n  e.  NN0  |->  ( abs `  ( ( ( G `
 x ) `  ( n  +  1
) )  /  (
( G `  x
) `  n )
) ) ) `  k )  =  ( ( abs `  (
( A `  (
k  +  1 ) )  /  ( A `
 k ) ) )  x.  ( abs `  x ) ) )
20972, 27eqtr3d 2498 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  k  e.  Z )  ->  ( D `  k )  =  ( abs `  (
( A `  (
k  +  1 ) )  /  ( A `
 k ) ) ) )
210209adantlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( D `  k )  =  ( abs `  ( ( A `  ( k  +  1 ) )  /  ( A `  k ) ) ) )
211210eqcomd 2468 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( abs `  ( ( A `  ( k  +  1 ) )  /  ( A `  k )
) )  =  ( D `  k ) )
212211oveq1d 6335 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( ( abs `  ( ( A `
 ( k  +  1 ) )  / 
( A `  k
) ) )  x.  ( abs `  x
) )  =  ( ( D `  k
)  x.  ( abs `  x ) ) )
213165adantr 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( abs `  x )  e.  CC )
214169, 213mulcomd 9695 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( ( D `  k )  x.  ( abs `  x
) )  =  ( ( abs `  x
)  x.  ( D `
 k ) ) )
215208, 212, 2143eqtrd 2500 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( (
n  e.  NN0  |->  ( abs `  ( ( ( G `
 x ) `  ( n  +  1
) )  /  (
( G `  x
) `  n )
) ) ) `  k )  =  ( ( abs `  x
)  x.  ( D `
 k ) ) )
2164, 162, 163, 165, 167, 169, 215climmulc2 13755 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  x  e.  ( CC  \  { 0 } ) )  -> 
( n  e.  NN0  |->  ( abs `  ( ( ( G `  x
) `  ( n  +  1 ) )  /  ( ( G `
 x ) `  n ) ) ) )  ~~>  ( ( abs `  x )  x.  L
) )
217 climres 13694 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( M  e.  ZZ  /\  ( n  e.  NN0  |->  ( abs `  ( ( ( G `  x
) `  ( n  +  1 ) )  /  ( ( G `
 x ) `  n ) ) ) )  e.  _V )  ->  ( ( ( n  e.  NN0  |->  ( abs `  ( ( ( G `
 x ) `  ( n  +  1
) )  /  (
( G `  x
) `  n )
) ) )  |`  ( ZZ>= `  M )
)  ~~>  ( ( abs `  x )  x.  L
)  <->  ( n  e. 
NN0  |->  ( abs `  (
( ( G `  x ) `  (
n  +  1 ) )  /  ( ( G `  x ) `
 n ) ) ) )  ~~>  ( ( abs `  x )  x.  L ) ) )
218162, 166, 217sylancl 673 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  x  e.  ( CC  \  { 0 } ) )  -> 
( ( ( n  e.  NN0  |->  ( abs `  ( ( ( G `
 x ) `  ( n  +  1
) )  /  (
( G `  x
) `  n )
) ) )  |`  ( ZZ>= `  M )
)  ~~>  ( ( abs `  x )  x.  L
)  <->  ( n  e. 
NN0  |->  ( abs `  (
( ( G `  x ) `  (
n  +  1 ) )  /  ( ( G `  x ) `
 n ) ) ) )  ~~>  ( ( abs `  x )  x.  L ) ) )
219216, 218mpbird 240 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  x  e.  ( CC  \  { 0 } ) )  -> 
( ( n  e. 
NN0  |->  ( abs `  (
( ( G `  x ) `  (
n  +  1 ) )  /  ( ( G `  x ) `
 n ) ) ) )  |`  ( ZZ>=
`  M ) )  ~~>  ( ( abs `  x
)  x.  L ) )
220161, 219eqbrtrrd 4441 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  x  e.  ( CC  \  { 0 } ) )  -> 
( n  e.  Z  |->  ( abs `  (
( ( G `  x ) `  (
n  +  1 ) )  /  ( ( G `  x ) `
 n ) ) ) )  ~~>  ( ( abs `  x )  x.  L ) )
221220adantr 471 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  ( ( abs `  x )  x.  L
)  =/=  1 )  ->  ( n  e.  Z  |->  ( abs `  (
( ( G `  x ) `  (
n  +  1 ) )  /  ( ( G `  x ) `
 n ) ) ) )  ~~>  ( ( abs `  x )  x.  L ) )
222 simpr 467 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  ( ( abs `  x )  x.  L
)  =/=  1 )  ->  ( ( abs `  x )  x.  L
)  =/=  1 )
223111, 4, 112, 114, 135, 151, 157, 221, 222cvgdvgrat 36707 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  ( ( abs `  x )  x.  L
)  =/=  1 )  ->  ( ( ( abs `  x )  x.  L )  <  1  <->  seq 0 (  +  ,  ( G `  x ) )  e. 
dom 
~~>  ) )
224110, 223sylanl2 661 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  x  e.  ( RR  \  {
0 } ) )  /\  ( ( abs `  x )  x.  L
)  =/=  1 )  ->  ( ( ( abs `  x )  x.  L )  <  1  <->  seq 0 (  +  ,  ( G `  x ) )  e. 
dom 
~~>  ) )
225 eldifi 3567 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  ( RR  \  { 0 } )  ->  x  e.  RR )
226 fveq2 5892 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( r  =  x  ->  ( G `  r )  =  ( G `  x ) )
227226seqeq3d 12259 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( r  =  x  ->  seq 0 (  +  , 
( G `  r
) )  =  seq 0 (  +  , 
( G `  x
) ) )
228227eleq1d 2524 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( r  =  x  ->  (  seq 0 (  +  , 
( G `  r
) )  e.  dom  ~~>  <->  seq 0 (  +  , 
( G `  x
) )  e.  dom  ~~>  ) )
229228elrab3 3209 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  RR  ->  (
x  e.  { r  e.  RR  |  seq 0 (  +  , 
( G `  r
) )  e.  dom  ~~>  }  <->  seq 0 (  +  , 
( G `  x
) )  e.  dom  ~~>  ) )
230225, 229syl 17 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  ( RR  \  { 0 } )  ->  ( x  e. 
{ r  e.  RR  |  seq 0 (  +  ,  ( G `  r ) )  e. 
dom 
~~>  }  <->  seq 0 (  +  ,  ( G `  x ) )  e. 
dom 
~~>  ) )
231230ad2antlr 738 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  x  e.  ( RR  \  {
0 } ) )  /\  ( ( abs `  x )  x.  L
)  =/=  1 )  ->  ( x  e. 
{ r  e.  RR  |  seq 0 (  +  ,  ( G `  r ) )  e. 
dom 
~~>  }  <->  seq 0 (  +  ,  ( G `  x ) )  e. 
dom 
~~>  ) )
232224, 231bitr4d 264 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  x  e.  ( RR  \  {
0 } ) )  /\  ( ( abs `  x )  x.  L
)  =/=  1 )  ->  ( ( ( abs `  x )  x.  L )  <  1  <->  x  e.  { r  e.  RR  |  seq 0 (  +  , 
( G `  r
) )  e.  dom  ~~>  } ) )
233232an32s 818 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
( abs `  x
)  x.  L )  =/=  1 )  /\  x  e.  ( RR  \  { 0 } ) )  ->  ( (
( abs `  x
)  x.  L )  <  1  <->  x  e.  { r  e.  RR  |  seq 0 (  +  , 
( G `  r
) )  e.  dom  ~~>  } ) )
234106, 233jaodan 799 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
( abs `  x
)  x.  L )  =/=  1 )  /\  ( x  e.  ( RR  i^i  { 0 } )  \/  x  e.  ( RR  \  {
0 } ) ) )  ->  ( (
( abs `  x
)  x.  L )  <  1  <->  x  e.  { r  e.  RR  |  seq 0 (  +  , 
( G `  r
) )  e.  dom  ~~>  } ) )
23586, 234sylan2br 483 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
( abs `  x
)  x.  L )  =/=  1 )  /\  x  e.  RR )  ->  ( ( ( abs `  x )  x.  L
)  <  1  <->  x  e.  { r  e.  RR  |  seq 0 (  +  , 
( G `  r
) )  e.  dom  ~~>  } ) )
236235an32s 818 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  RR )  /\  (
( abs `  x
)  x.  L )  =/=  1 )  -> 
( ( ( abs `  x )  x.  L
)  <  1  <->  x  e.  { r  e.  RR  |  seq 0 (  +  , 
( G `  r
) )  e.  dom  ~~>  } ) )
23782, 236bitr3d 263 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  RR )  /\  (
( abs `  x
)  x.  L )  =/=  1 )  -> 
( ( abs `  x
)  <  ( 1  /  L )  <->  x  e.  { r  e.  RR  |  seq 0 (  +  , 
( G `  r
) )  e.  dom  ~~>  } ) )
23869, 237syldan 477 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR )  /\  ( abs `  x )  =/=  ( 1  /  L
) )  ->  (
( abs `  x
)  <  ( 1  /  L )  <->  x  e.  { r  e.  RR  |  seq 0 (  +  , 
( G `  r
) )  e.  dom  ~~>  } ) )
239238notbid 300 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR )  /\  ( abs `  x )  =/=  ( 1  /  L
) )  ->  ( -.  ( abs `  x
)  <  ( 1  /  L )  <->  -.  x  e.  { r  e.  RR  |  seq 0 (  +  ,  ( G `  r ) )  e. 
dom 
~~>  } ) )
24058, 239bitrd 261 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR )  /\  ( abs `  x )  =/=  ( 1  /  L
) )  ->  (
( 1  /  L
)  <  ( abs `  x )  <->  -.  x  e.  { r  e.  RR  |  seq 0 (  +  ,  ( G `  r ) )  e. 
dom 
~~>  } ) )
241240biimpd 212 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR )  /\  ( abs `  x )  =/=  ( 1  /  L
) )  ->  (
( 1  /  L
)  <  ( abs `  x )  ->  -.  x  e.  { r  e.  RR  |  seq 0
(  +  ,  ( G `  r ) )  e.  dom  ~~>  } ) )
242241impancom 446 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR )  /\  (
1  /  L )  <  ( abs `  x
) )  ->  (
( abs `  x
)  =/=  ( 1  /  L )  ->  -.  x  e.  { r  e.  RR  |  seq 0 (  +  , 
( G `  r
) )  e.  dom  ~~>  } ) )
24352, 242mpd 15 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR )  /\  (
1  /  L )  <  ( abs `  x
) )  ->  -.  x  e.  { r  e.  RR  |  seq 0
(  +  ,  ( G `  r ) )  e.  dom  ~~>  } )
244243ex 440 . . . . . . 7  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( 1  /  L )  <  ( abs `  x
)  ->  -.  x  e.  { r  e.  RR  |  seq 0 (  +  ,  ( G `  r ) )  e. 
dom 
~~>  } ) )
245244con2d 120 . . . . . 6  |-  ( (
ph  /\  x  e.  RR )  ->  ( x  e.  { r  e.  RR  |  seq 0
(  +  ,  ( G `  r ) )  e.  dom  ~~>  }  ->  -.  ( 1  /  L
)  <  ( abs `  x ) ) )
24647adantr 471 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR )  /\  (
1  /  L )  <  x )  -> 
( 1  /  L
)  e.  RR )
247 simplr 767 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR )  /\  (
1  /  L )  <  x )  ->  x  e.  RR )
24850adantr 471 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR )  /\  (
1  /  L )  <  x )  -> 
( abs `  x
)  e.  RR )
249 simpr 467 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR )  /\  (
1  /  L )  <  x )  -> 
( 1  /  L
)  <  x )
250247leabsd 13531 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR )  /\  (
1  /  L )  <  x )  ->  x  <_  ( abs `  x
) )
251246, 247, 248, 249, 250ltletrd 9826 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR )  /\  (
1  /  L )  <  x )  -> 
( 1  /  L
)  <  ( abs `  x ) )
252251ex 440 . . . . . 6  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( 1  /  L )  <  x  ->  (
1  /  L )  <  ( abs `  x
) ) )
253245, 252nsyld 147 . . . . 5  |-  ( (
ph  /\  x  e.  RR )  ->  ( x  e.  { r  e.  RR  |  seq 0
(  +  ,  ( G `  r ) )  e.  dom  ~~>  }  ->  -.  ( 1  /  L
)  <  x )
)
25446, 253sylan2 481 . . . 4  |-  ( (
ph  /\  x  e.  { r  e.  RR  |  seq 0 (  +  , 
( G `  r
) )  e.  dom  ~~>  } )  ->  ( x  e.  { r  e.  RR  |  seq 0 (  +  ,  ( G `  r ) )  e. 
dom 
~~>  }  ->  -.  (
1  /  L )  <  x ) )
25545, 254mpd 15 . . 3  |-  ( (
ph  /\  x  e.  { r  e.  RR  |  seq 0 (  +  , 
( G `  r
) )  e.  dom  ~~>  } )  ->  -.  (
1  /  L )  <  x )
25643renegcld 10079 . . . . . . . . 9  |-  ( ph  -> 
-u ( 1  /  L )  e.  RR )
257256rexrd 9721 . . . . . . . 8  |-  ( ph  -> 
-u ( 1  /  L )  e.  RR* )
258 iooss1 11705 . . . . . . . 8  |-  ( (
-u ( 1  /  L )  e.  RR*  /\  -u ( 1  /  L
)  <_  x )  ->  ( x (,) (
1  /  L ) )  C_  ( -u (
1  /  L ) (,) ( 1  /  L ) ) )
259257, 258sylan 478 . . . . . . 7  |-  ( (
ph  /\  -u ( 1  /  L )  <_  x )  ->  (
x (,) ( 1  /  L ) ) 
C_  ( -u (
1  /  L ) (,) ( 1  /  L ) ) )
260259adantlr 726 . . . . . 6  |-  ( ( ( ph  /\  (
x  e.  RR*  /\  x  <  ( 1  /  L
) ) )  /\  -u ( 1  /  L
)  <_  x )  ->  ( x (,) (
1  /  L ) )  C_  ( -u (
1  /  L ) (,) ( 1  /  L ) ) )
261 eliooord 11728 . . . . . . . . . . 11  |-  ( k  e.  ( x (,) ( 1  /  L
) )  ->  (
x  <  k  /\  k  <  ( 1  /  L ) ) )
262261simpld 465 . . . . . . . . . 10  |-  ( k  e.  ( x (,) ( 1  /  L
) )  ->  x  <  k )
263262rgen 2759 . . . . . . . . 9  |-  A. k  e.  ( x (,) (
1  /  L ) ) x  <  k
264 ioon0 11696 . . . . . . . . . . . . 13  |-  ( ( x  e.  RR*  /\  (
1  /  L )  e.  RR* )  ->  (
( x (,) (
1  /  L ) )  =/=  (/)  <->  x  <  ( 1  /  L ) ) )
26544, 264sylan2 481 . . . . . . . . . . . 12  |-  ( ( x  e.  RR*  /\  ph )  ->  ( ( x (,) ( 1  /  L ) )  =/=  (/) 
<->  x  <  ( 1  /  L ) ) )
266265ancoms 459 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  RR* )  ->  ( (
x (,) ( 1  /  L ) )  =/=  (/)  <->  x  <  ( 1  /  L ) ) )
267266biimpar 492 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR* )  /\  x  <  ( 1  /  L
) )  ->  (
x (,) ( 1  /  L ) )  =/=  (/) )
268 r19.2zb 3871 . . . . . . . . . 10  |-  ( ( x (,) ( 1  /  L ) )  =/=  (/)  <->  ( A. k  e.  ( x (,) (
1  /  L ) ) x  <  k  ->  E. k  e.  ( x (,) ( 1  /  L ) ) x  <  k ) )
269267, 268sylib 201 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR* )  /\  x  <  ( 1  /  L
) )  ->  ( A. k  e.  (
x (,) ( 1  /  L ) ) x  <  k  ->  E. k  e.  (
x (,) ( 1  /  L ) ) x  <  k ) )
270263, 269mpi 20 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR* )  /\  x  <  ( 1  /  L
) )  ->  E. k  e.  ( x (,) (
1  /  L ) ) x  <  k
)
271270anasss 657 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  RR*  /\  x  < 
( 1  /  L
) ) )  ->  E. k  e.  (
x (,) ( 1  /  L ) ) x  <  k )
272271adantr 471 . . . . . 6  |-  ( ( ( ph  /\  (
x  e.  RR*  /\  x  <  ( 1  /  L
) ) )  /\  -u ( 1  /  L
)  <_  x )  ->  E. k  e.  ( x (,) ( 1  /  L ) ) x  <  k )
273 ssrexv 3506 . . . . . 6  |-  ( ( x (,) ( 1  /  L ) ) 
C_  ( -u (
1  /  L ) (,) ( 1  /  L ) )  -> 
( E. k  e.  ( x (,) (
1  /  L ) ) x  <  k  ->  E. k  e.  (
-u ( 1  /  L ) (,) (
1  /  L ) ) x  <  k
) )
274260, 272, 273sylc 62 . . . . 5  |-  ( ( ( ph  /\  (
x  e.  RR*  /\  x  <  ( 1  /  L
) ) )  /\  -u ( 1  /  L
)  <_  x )  ->  E. k  e.  (
-u ( 1  /  L ) (,) (
1  /  L ) ) x  <  k
)
275 simplr 767 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR* )  /\  -.  -u ( 1  /  L
)  <_  x )  ->  x  e.  RR* )
276 xrltnle 9732 . . . . . . . . . . . . . . 15  |-  ( ( x  e.  RR*  /\  -u (
1  /  L )  e.  RR* )  ->  (
x  <  -u ( 1  /  L )  <->  -.  -u (
1  /  L )  <_  x ) )
277 xrltle 11482 . . . . . . . . . . . . . . 15  |-  ( ( x  e.  RR*  /\  -u (
1  /  L )  e.  RR* )  ->  (
x  <  -u ( 1  /  L )  ->  x  <_  -u ( 1  /  L ) ) )
278276, 277sylbird 243 . . . . . . . . . . . . . 14  |-  ( ( x  e.  RR*  /\  -u (
1  /  L )  e.  RR* )  ->  ( -.  -u ( 1  /  L )  <_  x  ->  x  <_  -u ( 1  /  L ) ) )
279257, 278sylan2 481 . . . . . . . . . . . . 13  |-  ( ( x  e.  RR*  /\  ph )  ->  ( -.  -u (
1  /  L )  <_  x  ->  x  <_ 
-u ( 1  /  L ) ) )
280279ancoms 459 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  RR* )  ->  ( -.  -u ( 1  /  L
)  <_  x  ->  x  <_  -u ( 1  /  L ) ) )
281280imp 435 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR* )  /\  -.  -u ( 1  /  L
)  <_  x )  ->  x  <_  -u ( 1  /  L ) )
282 iooss1 11705 . . . . . . . . . . 11  |-  ( ( x  e.  RR*  /\  x  <_ 
-u ( 1  /  L ) )  -> 
( -u ( 1  /  L ) (,) (
1  /  L ) )  C_  ( x (,) ( 1  /  L
) ) )
283275, 281, 282syl2anc 671 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR* )  /\  -.  -u ( 1  /  L
)  <_  x )  ->  ( -u ( 1  /  L ) (,) ( 1  /  L
) )  C_  (
x (,) ( 1  /  L ) ) )
284283sselda 3444 . . . . . . . . 9  |-  ( ( ( ( ph  /\  x  e.  RR* )  /\  -.  -u ( 1  /  L )  <_  x
)  /\  k  e.  ( -u ( 1  /  L ) (,) (
1  /  L ) ) )  ->  k  e.  ( x (,) (
1  /  L ) ) )
285284, 262syl 17 . . . . . . . 8  |-  ( ( ( ( ph  /\  x  e.  RR* )  /\  -.  -u ( 1  /  L )  <_  x
)  /\  k  e.  ( -u ( 1  /  L ) (,) (
1  /  L ) ) )  ->  x  <  k )
286285ralrimiva 2814 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR* )  /\  -.  -u ( 1  /  L
)  <_  x )  ->  A. k  e.  (
-u ( 1  /  L ) (,) (
1  /  L ) ) x  <  k
)
28741, 78recgt0d 10574 . . . . . . . . . . . . 13  |-  ( ph  ->  0  <  ( 1  /  L ) )
28843, 43, 287, 287addgt0d 10221 . . . . . . . . . . . 12  |-  ( ph  ->  0  <  ( ( 1  /  L )  +  ( 1  /  L ) ) )
28943recnd 9700 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 1  /  L
)  e.  CC )
290289, 289subnegd 10024 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( 1  /  L )  -  -u (
1  /  L ) )  =  ( ( 1  /  L )  +  ( 1  /  L ) ) )
291288, 290breqtrrd 4445 . . . . . . . . . . 11  |-  ( ph  ->  0  <  ( ( 1  /  L )  -  -u ( 1  /  L ) ) )
292256, 43posdifd 10233 . . . . . . . . . . 11  |-  ( ph  ->  ( -u ( 1  /  L )  < 
( 1  /  L
)  <->  0  <  (
( 1  /  L
)  -  -u (
1  /  L ) ) ) )
293291, 292mpbird 240 . . . . . . . . . 10  |-  ( ph  -> 
-u ( 1  /  L )  <  (
1  /  L ) )
294 ioon0 11696 . . . . . . . . . . 11  |-  ( (
-u ( 1  /  L )  e.  RR*  /\  ( 1  /  L
)  e.  RR* )  ->  ( ( -u (
1  /  L ) (,) ( 1  /  L ) )  =/=  (/) 
<-> 
-u ( 1  /  L )  <  (
1  /  L ) ) )
295257, 44, 294syl2anc 671 . . . . . . . . . 10  |-  ( ph  ->  ( ( -u (
1  /  L ) (,) ( 1  /  L ) )  =/=  (/) 
<-> 
-u ( 1  /  L )  <  (
1  /  L ) ) )
296293, 295mpbird 240 . . . . . . . . 9  |-  ( ph  ->  ( -u ( 1  /  L ) (,) ( 1  /  L
) )  =/=  (/) )
297 r19.2zb 3871 . . . . . . . . 9  |-  ( (
-u ( 1  /  L ) (,) (
1  /  L ) )  =/=  (/)  <->  ( A. k  e.  ( -u (
1  /  L ) (,) ( 1  /  L ) ) x  <  k  ->  E. k  e.  ( -u ( 1  /  L ) (,) ( 1  /  L
) ) x  < 
k ) )
298296, 297sylib 201 . . . . . . . 8  |-  ( ph  ->  ( A. k  e.  ( -u ( 1  /  L ) (,) ( 1  /  L
) ) x  < 
k  ->  E. k  e.  ( -u ( 1  /  L ) (,) ( 1  /  L
) ) x  < 
k ) )
299298ad2antrr 737 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR* )  /\  -.  -u ( 1  /  L
)  <_  x )  ->  ( A. k  e.  ( -u ( 1  /  L ) (,) ( 1  /  L
) ) x  < 
k  ->  E. k  e.  ( -u ( 1  /  L ) (,) ( 1  /  L
) ) x  < 
k ) )
300286, 299mpd 15 . . . . . 6  |-  ( ( ( ph  /\  x  e.  RR* )  /\  -.  -u ( 1  /  L
)  <_  x )  ->  E. k  e.  (
-u ( 1  /  L ) (,) (
1  /  L ) ) x  <  k
)
301300adantlrr 732 . . . . 5  |-  ( ( ( ph  /\  (
x  e.  RR*  /\  x  <  ( 1  /  L
) ) )  /\  -.  -u ( 1  /  L )  <_  x
)  ->  E. k  e.  ( -u ( 1  /  L ) (,) ( 1  /  L
) ) x  < 
k )
302274, 301pm2.61dan 805 . . . 4  |-  ( (
ph  /\  ( x  e.  RR*  /\  x  < 
( 1  /  L
) ) )  ->  E. k  e.  ( -u ( 1  /  L
) (,) ( 1  /  L ) ) x  <  k )
303 elioo2 11711 . . . . . . . . . . 11  |-  ( (
-u ( 1  /  L )  e.  RR*  /\  ( 1  /  L
)  e.  RR* )  ->  ( x  e.  (
-u ( 1  /  L ) (,) (
1  /  L ) )  <->  ( x  e.  RR  /\  -u (
1  /  L )  <  x  /\  x  <  ( 1  /  L
) ) ) )
304257, 44, 303syl2anc 671 . . . . . . . . . 10  |-  ( ph  ->  ( x  e.  (
-u ( 1  /  L ) (,) (
1  /  L ) )  <->  ( x  e.  RR  /\  -u (
1  /  L )  <  x  /\  x  <  ( 1  /  L
) ) ) )
305304biimpa 491 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( -u ( 1  /  L ) (,) (
1  /  L ) ) )  ->  (
x  e.  RR  /\  -u ( 1  /  L
)  <  x  /\  x  <  ( 1  /  L ) ) )
306 simpr 467 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  RR )  ->  x  e.  RR )
307306, 47absltd 13546 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( abs `  x )  <  ( 1  /  L )  <->  ( -u (
1  /  L )  <  x  /\  x  <  ( 1  /  L
) ) ) )
30850adantr 471 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  RR )  /\  ( abs `  x )  < 
( 1  /  L
) )  ->  ( abs `  x )  e.  RR )
309 simpr 467 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  RR )  /\  ( abs `  x )  < 
( 1  /  L
) )  ->  ( abs `  x )  < 
( 1  /  L
) )
310308, 309ltned 9802 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  RR )  /\  ( abs `  x )  < 
( 1  /  L
) )  ->  ( abs `  x )  =/=  ( 1  /  L
) )
311238biimpd 212 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  RR )  /\  ( abs `  x )  =/=  ( 1  /  L
) )  ->  (
( abs `  x
)  <  ( 1  /  L )  ->  x  e.  { r  e.  RR  |  seq 0
(  +  ,  ( G `  r ) )  e.  dom  ~~>  } ) )
312311impancom 446 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  RR )  /\  ( abs `  x )  < 
( 1  /  L
) )  ->  (
( abs `  x
)  =/=  ( 1  /  L )  ->  x  e.  { r  e.  RR  |  seq 0
(  +  ,  ( G `  r ) )  e.  dom  ~~>  } ) )
313310, 312mpd 15 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  RR )  /\  ( abs `  x )  < 
( 1  /  L
) )  ->  x  e.  { r  e.  RR  |  seq 0 (  +  ,  ( G `  r ) )  e. 
dom 
~~>  } )
314313ex 440 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( abs `  x )  <  ( 1  /  L )  ->  x  e.  { r  e.  RR  |  seq 0 (  +  ,  ( G `  r ) )  e. 
dom 
~~>  } ) )
315307, 314sylbird 243 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  RR )  ->  ( (
-u ( 1  /  L )  <  x  /\  x  <  ( 1  /  L ) )  ->  x  e.  {
r  e.  RR  |  seq 0 (  +  , 
( G `  r
) )  e.  dom  ~~>  } ) )
316315impr 629 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( x  e.  RR  /\  ( -u ( 1  /  L
)  <  x  /\  x  <  ( 1  /  L ) ) ) )  ->  x  e.  { r  e.  RR  |  seq 0 (  +  , 
( G `  r
) )  e.  dom  ~~>  } )
317316expcom 441 . . . . . . . . . . 11  |-  ( ( x  e.  RR  /\  ( -u ( 1  /  L )  <  x  /\  x  <  ( 1  /  L ) ) )  ->  ( ph  ->  x  e.  { r  e.  RR  |  seq 0 (  +  , 
( G `  r
) )  e.  dom  ~~>  } ) )
3183173impb 1211 . . . . . . . . . 10  |-  ( ( x  e.  RR  /\  -u ( 1  /  L
)  <  x  /\  x  <  ( 1  /  L ) )  -> 
( ph  ->  x  e. 
{ r  e.  RR  |  seq 0 (  +  ,  ( G `  r ) )  e. 
dom 
~~>  } ) )
319318impcom 436 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  RR  /\  -u (
1  /  L )  <  x  /\  x  <  ( 1  /  L
) ) )  ->  x  e.  { r  e.  RR  |  seq 0
(  +  ,  ( G `  r ) )  e.  dom  ~~>  } )
320305, 319syldan 477 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( -u ( 1  /  L ) (,) (
1  /  L ) ) )  ->  x  e.  { r  e.  RR  |  seq 0 (  +  ,  ( G `  r ) )  e. 
dom 
~~>  } )
321320ex 440 . . . . . . 7  |-  ( ph  ->  ( x  e.  (
-u ( 1  /  L ) (,) (
1  /  L ) )  ->  x  e.  { r  e.  RR  |  seq 0 (  +  , 
( G `  r
) )  e.  dom  ~~>  } ) )
322321ssrdv 3450 . . . . . 6  |-  ( ph  ->  ( -u ( 1  /  L ) (,) ( 1  /  L
) )  C_  { r  e.  RR  |  seq 0 (  +  , 
( G `  r
) )  e.  dom  ~~>  } )
323 ssrexv 3506 . . . . . 6  |-  ( (
-u ( 1  /  L ) (,) (
1  /  L ) )  C_  { r  e.  RR  |  seq 0
(  +  ,  ( G `  r ) )  e.  dom  ~~>  }  ->  ( E. k  e.  (
-u ( 1  /  L ) (,) (
1  /  L ) ) x  <  k  ->  E. k  e.  {
r  e.  RR  |  seq 0 (  +  , 
( G `  r
) )  e.  dom  ~~>  } x  <  k ) )
324322, 323syl 17 . . . . 5  |-  ( ph  ->  ( E. k  e.  ( -u ( 1  /  L ) (,) ( 1  /  L
) ) x  < 
k  ->  E. k  e.  { r  e.  RR  |  seq 0 (  +  ,  ( G `  r ) )  e. 
dom 
~~>  } x  <  k
) )
325324adantr 471 . . . 4  |-  ( (
ph  /\  ( x  e.  RR*  /\  x  < 
( 1  /  L
) ) )  -> 
( E. k  e.  ( -u ( 1  /  L ) (,) ( 1  /  L
) ) x  < 
k  ->  E. k  e.  { r  e.  RR  |  seq 0 (  +  ,  ( G `  r ) )  e. 
dom 
~~>  } x  <  k
) )
326302, 325mpd 15 . . 3  |-  ( (
ph  /\  ( x  e.  RR*  /\  x  < 
( 1  /  L
) ) )  ->  E. k  e.  { r  e.  RR  |  seq 0 (  +  , 
( G `  r
) )  e.  dom  ~~>  } x  <  k )
3273, 44, 255, 326eqsupd 8002 . 2  |-  ( ph  ->  sup ( { r  e.  RR  |  seq 0 (  +  , 
( G `  r
) )  e.  dom  ~~>  } ,  RR* ,  <  )  =  ( 1  /  L ) )
3281, 327syl5eq 2508 1  |-  ( ph  ->  R  =  ( 1  /  L ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 189    \/ wo 374    /\ wa 375    /\ w3a 991    = wceq 1455    e. wcel 1898    =/= wne 2633   A.wral 2749   E.wrex 2750   {crab 2753   _Vcvv 3057    \ cdif 3413    u. cun 3414    i^i cin 3415    C_ wss 3416   (/)c0 3743   {csn 3980   class class class wbr 4418    |-> cmpt 4477    Or wor 4776   dom cdm 4856    |` cres 4858   -->wf 5601   ` cfv 5605  (class class class)co 6320   supcsup 7985   CCcc 9568   RRcr 9569   0cc0 9570   1c1 9571    + caddc 9573    x. cmul 9575   RR*cxr 9705    < clt 9706    <_ cle 9707    - cmin 9891   -ucneg 9892    / cdiv 10302   NN0cn0 10903   ZZcz 10971   ZZ>=cuz 11193   RR+crp 11336   (,)cioo 11669    seqcseq 12251   ^cexp 12310   abscabs 13352    ~~> cli 13603
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-rep 4531  ax-sep 4541  ax-nul 4550  ax-pow 4598  ax-pr 4656  ax-un 6615  ax-inf2 8177  ax-cnex 9626  ax-resscn 9627  ax-1cn 9628  ax-icn 9629  ax-addcl 9630  ax-addrcl 9631  ax-mulcl 9632  ax-mulrcl 9633  ax-mulcom 9634  ax-addass 9635  ax-mulass 9636  ax-distr 9637  ax-i2m1 9638  ax-1ne0 9639  ax-1rid 9640  ax-rnegex 9641  ax-rrecex 9642  ax-cnre 9643  ax-pre-lttri 9644  ax-pre-lttrn 9645  ax-pre-ltadd 9646  ax-pre-mulgt0 9647  ax-pre-sup 9648  ax-addf 9649  ax-mulf 9650
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-fal 1461  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-nel 2636  df-ral 2754  df-rex 2755  df-reu 2756  df-rmo 2757  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-tp 3985  df-op 3987  df-uni 4213  df-int 4249  df-iun 4294  df-br 4419  df-opab 4478  df-mpt 4479  df-tr 4514  df-eprel 4767  df-id 4771  df-po 4777  df-so 4778  df-fr 4815  df-se 4816  df-we 4817  df-xp 4862  df-rel 4863  df-cnv 4864  df-co 4865  df-dm 4866  df-rn 4867  df-res 4868  df-ima 4869  df-pred 5403  df-ord 5449  df-on 5450  df-lim 5451  df-suc 5452  df-iota 5569  df-fun 5607  df-fn 5608  df-f 5609  df-f1 5610  df-fo 5611  df-f1o 5612  df-fv 5613  df-isom 5614  df-riota 6282  df-ov 6323  df-oprab 6324  df-mpt2 6325  df-om 6725  df-1st 6825  df-2nd 6826  df-wrecs 7059  df-recs 7121  df-rdg 7159  df-1o 7213  df-oadd 7217  df-er 7394  df-pm 7506  df-en 7601  df-dom 7602  df-sdom 7603  df-fin 7604  df-sup 7987  df-inf 7988  df-oi 8056  df-card 8404  df-pnf 9708  df-mnf 9709  df-xr 9710  df-ltxr 9711  df-le 9712  df-sub 9893  df-neg 9894  df-div 10303  df-nn 10643  df-2 10701  df-3 10702  df-n0 10904  df-z 10972  df-uz 11194  df-q 11299  df-rp 11337  df-ioo 11673  df-ico 11675  df-fz 11820  df-fzo 11953  df-fl 12066  df-seq 12252  df-exp 12311  df-hash 12554  df-shft 13185  df-cj 13217  df-re 13218  df-im 13219  df-sqrt 13353  df-abs 13354  df-limsup 13581  df-clim 13607  df-rlim 13608  df-sum 13808
This theorem is referenced by:  binomcxplemradcnv  36746
  Copyright terms: Public domain W3C validator