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

Theorem radcnvrat 31436
Description: Let  L be the limit, if one exists, of the ratio  ( abs `  (
( A `  (
k  +  1 ) )  /  ( A `
 k ) ) ) (as in the ratio test cvgdvgrat 31435) 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 11350 . . . 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 10963 . . . . . 6  |-  ( ph  ->  M  e.  ZZ )
74reseq2i 5259 . . . . . . 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 10797 . . . . . . . . . . 11  |-  NN0  e.  _V
1110mptex 6118 . . . . . . . . . 10  |-  ( k  e.  NN0  |->  ( abs `  ( ( A `  ( k  +  1 ) )  /  ( A `  k )
) ) )  e. 
_V
129, 11eqeltri 2538 . . . . . . . . 9  |-  D  e. 
_V
13 climres 13480 . . . . . . . . 9  |-  ( ( M  e.  ZZ  /\  D  e.  _V )  ->  ( ( D  |`  ( ZZ>= `  M )
)  ~~>  L  <->  D  ~~>  L ) )
146, 12, 13sylancl 660 . . . . . . . 8  |-  ( ph  ->  ( ( D  |`  ( ZZ>= `  M )
)  ~~>  L  <->  D  ~~>  L ) )
158, 14mpbird 232 . . . . . . 7  |-  ( ph  ->  ( D  |`  ( ZZ>=
`  M ) )  ~~>  L )
167, 15syl5eqbr 4472 . . . . . 6  |-  ( ph  ->  ( D  |`  Z )  ~~>  L )
179reseq1i 5258 . . . . . . . . 9  |-  ( D  |`  Z )  =  ( ( k  e.  NN0  |->  ( abs `  ( ( A `  ( k  +  1 ) )  /  ( A `  k ) ) ) )  |`  Z )
18 eluznn0 11152 . . . . . . . . . . . . . 14  |-  ( ( M  e.  NN0  /\  k  e.  ( ZZ>= `  M ) )  -> 
k  e.  NN0 )
195, 18sylan 469 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  ( ZZ>= `  M )
)  ->  k  e.  NN0 )
2019ex 432 . . . . . . . . . . . 12  |-  ( ph  ->  ( k  e.  (
ZZ>= `  M )  -> 
k  e.  NN0 )
)
2120ssrdv 3495 . . . . . . . . . . 11  |-  ( ph  ->  ( ZZ>= `  M )  C_ 
NN0 )
224, 21syl5eqss 3533 . . . . . . . . . 10  |-  ( ph  ->  Z  C_  NN0 )
2322resmptd 5313 . . . . . . . . 9  |-  ( ph  ->  ( ( k  e. 
NN0  |->  ( abs `  (
( A `  (
k  +  1 ) )  /  ( A `
 k ) ) ) )  |`  Z )  =  ( k  e.  Z  |->  ( abs `  (
( A `  (
k  +  1 ) )  /  ( A `
 k ) ) ) ) )
2417, 23syl5eq 2507 . . . . . . . 8  |-  ( ph  ->  ( D  |`  Z )  =  ( k  e.  Z  |->  ( abs `  (
( A `  (
k  +  1 ) )  /  ( A `
 k ) ) ) ) )
25 fvex 5858 . . . . . . . . 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 5941 . . . . . . 7  |-  ( (
ph  /\  k  e.  Z )  ->  (
( D  |`  Z ) `
 k )  =  ( abs `  (
( A `  (
k  +  1 ) )  /  ( A `
 k ) ) ) )
284peano2uzs 11136 . . . . . . . . . 10  |-  ( k  e.  Z  ->  (
k  +  1 )  e.  Z )
2922sselda 3489 . . . . . . . . . . 11  |-  ( (
ph  /\  ( k  +  1 )  e.  Z )  ->  (
k  +  1 )  e.  NN0 )
30 radcnvrat.a . . . . . . . . . . . 12  |-  ( ph  ->  A : NN0 --> CC )
3130ffvelrnda 6007 . . . . . . . . . . 11  |-  ( (
ph  /\  ( k  +  1 )  e. 
NN0 )  ->  ( A `  ( k  +  1 ) )  e.  CC )
3229, 31syldan 468 . . . . . . . . . 10  |-  ( (
ph  /\  ( k  +  1 )  e.  Z )  ->  ( A `  ( k  +  1 ) )  e.  CC )
3328, 32sylan2 472 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  Z )  ->  ( A `  ( k  +  1 ) )  e.  CC )
3422sselda 3489 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  Z )  ->  k  e.  NN0 )
3530ffvelrnda 6007 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( A `  k )  e.  CC )
3634, 35syldan 468 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  Z )  ->  ( A `  k )  e.  CC )
37 radcnvrat.n0 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  Z )  ->  ( A `  k )  =/=  0 )
3833, 36, 37divcld 10316 . . . . . . . 8  |-  ( (
ph  /\  k  e.  Z )  ->  (
( A `  (
k  +  1 ) )  /  ( A `
 k ) )  e.  CC )
3938abscld 13349 . . . . . . 7  |-  ( (
ph  /\  k  e.  Z )  ->  ( abs `  ( ( A `
 ( k  +  1 ) )  / 
( A `  k
) ) )  e.  RR )
4027, 39eqeltrd 2542 . . . . . 6  |-  ( (
ph  /\  k  e.  Z )  ->  (
( D  |`  Z ) `
 k )  e.  RR )
414, 6, 16, 40climrecl 13488 . . . . 5  |-  ( ph  ->  L  e.  RR )
42 radcnvrat.ln0 . . . . 5  |-  ( ph  ->  L  =/=  0 )
4341, 42rereccld 10367 . . . 4  |-  ( ph  ->  ( 1  /  L
)  e.  RR )
4443rexrd 9632 . . 3  |-  ( ph  ->  ( 1  /  L
)  e.  RR* )
45 simpr 459 . . . 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 3251 . . . . 5  |-  ( x  e.  { r  e.  RR  |  seq 0
(  +  ,  ( G `  r ) )  e.  dom  ~~>  }  ->  x  e.  RR )
4743adantr 463 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  RR )  ->  ( 1  /  L )  e.  RR )
48 recn 9571 . . . . . . . . . . . . 13  |-  ( x  e.  RR  ->  x  e.  CC )
4948abscld 13349 . . . . . . . . . . . 12  |-  ( x  e.  RR  ->  ( abs `  x )  e.  RR )
5049adantl 464 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  RR )  ->  ( abs `  x )  e.  RR )
5147, 50ltlend 9719 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( 1  /  L )  <  ( abs `  x
)  <->  ( ( 1  /  L )  <_ 
( abs `  x
)  /\  ( abs `  x )  =/=  (
1  /  L ) ) ) )
5251simplbda 622 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR )  /\  (
1  /  L )  <  ( abs `  x
) )  ->  ( abs `  x )  =/=  ( 1  /  L
) )
5351adantr 463 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR )  /\  ( abs `  x )  =/=  ( 1  /  L
) )  ->  (
( 1  /  L
)  <  ( abs `  x )  <->  ( (
1  /  L )  <_  ( abs `  x
)  /\  ( abs `  x )  =/=  (
1  /  L ) ) ) )
54 simpr 459 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  RR )  /\  ( abs `  x )  =/=  ( 1  /  L
) )  ->  ( abs `  x )  =/=  ( 1  /  L
) )
5554biantrud 505 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR )  /\  ( abs `  x )  =/=  ( 1  /  L
) )  ->  (
( 1  /  L
)  <_  ( abs `  x )  <->  ( (
1  /  L )  <_  ( abs `  x
)  /\  ( abs `  x )  =/=  (
1  /  L ) ) ) )
5647, 50lenltd 9720 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( 1  /  L )  <_  ( abs `  x
)  <->  -.  ( abs `  x )  <  (
1  /  L ) ) )
5756adantr 463 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR )  /\  ( abs `  x )  =/=  ( 1  /  L
) )  ->  (
( 1  /  L
)  <_  ( abs `  x )  <->  -.  ( abs `  x )  < 
( 1  /  L
) ) )
5853, 55, 573bitr2d 281 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR )  /\  ( abs `  x )  =/=  ( 1  /  L
) )  ->  (
( 1  /  L
)  <  ( abs `  x )  <->  -.  ( abs `  x )  < 
( 1  /  L
) ) )
59 1cnd 9601 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  RR )  ->  1  e.  CC )
6050recnd 9611 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  RR )  ->  ( abs `  x )  e.  CC )
6141recnd 9611 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  L  e.  CC )
6261adantr 463 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  RR )  ->  L  e.  CC )
6342adantr 463 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  RR )  ->  L  =/=  0 )
6459, 60, 62, 63divmul3d 10350 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( 1  /  L )  =  ( abs `  x
)  <->  1  =  ( ( abs `  x
)  x.  L ) ) )
65 eqcom 2463 . . . . . . . . . . . . . . . . 17  |-  ( ( 1  /  L )  =  ( abs `  x
)  <->  ( abs `  x
)  =  ( 1  /  L ) )
66 eqcom 2463 . . . . . . . . . . . . . . . . 17  |-  ( 1  =  ( ( abs `  x )  x.  L
)  <->  ( ( abs `  x )  x.  L
)  =  1 )
6764, 65, 663bitr3g 287 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( abs `  x )  =  ( 1  /  L )  <->  ( ( abs `  x )  x.  L )  =  1 ) )
6867necon3bid 2712 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( abs `  x )  =/=  ( 1  /  L )  <->  ( ( abs `  x )  x.  L )  =/=  1
) )
6968biimpa 482 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  RR )  /\  ( abs `  x )  =/=  ( 1  /  L
) )  ->  (
( abs `  x
)  x.  L )  =/=  1 )
70 1red 9600 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  RR )  ->  1  e.  RR )
71 fvres 5862 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( k  e.  Z  ->  (
( D  |`  Z ) `
 k )  =  ( D `  k
) )
7271adantl 464 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  k  e.  Z )  ->  (
( D  |`  Z ) `
 k )  =  ( D `  k
) )
7372, 40eqeltrrd 2543 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  k  e.  Z )  ->  ( D `  k )  e.  RR )
7438absge0d 13357 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  k  e.  Z )  ->  0  <_  ( abs `  (
( A `  (
k  +  1 ) )  /  ( A `
 k ) ) ) )
7574, 27breqtrrd 4465 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  k  e.  Z )  ->  0  <_  ( ( D  |`  Z ) `  k
) )
7675, 72breqtrd 4463 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  k  e.  Z )  ->  0  <_  ( D `  k
) )
774, 6, 8, 73, 76climge0 13489 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  0  <_  L )
7841, 77, 42ne0gt0d 9711 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  0  <  L )
7941, 78elrpd 11256 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  L  e.  RR+ )
8079adantr 463 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  RR )  ->  L  e.  RR+ )
8150, 70, 80ltmuldivd 11302 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( ( abs `  x
)  x.  L )  <  1  <->  ( abs `  x )  <  (
1  /  L ) ) )
8281adantr 463 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  RR )  /\  (
( abs `  x
)  x.  L )  =/=  1 )  -> 
( ( ( abs `  x )  x.  L
)  <  1  <->  ( abs `  x )  <  (
1  /  L ) ) )
83 elun 3631 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  ( ( RR 
i^i  { 0 } )  u.  ( RR  \  { 0 } ) )  <->  ( x  e.  ( RR  i^i  {
0 } )  \/  x  e.  ( RR 
\  { 0 } ) ) )
84 inundif 3894 . . . . . . . . . . . . . . . . . . 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 251 . . . . . . . . . . . . . . . . 17  |-  ( ( x  e.  ( RR 
i^i  { 0 } )  \/  x  e.  ( RR  \  { 0 } ) )  <->  x  e.  RR )
87 elin 3673 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  ( RR  i^i  { 0 } )  <->  ( x  e.  RR  /\  x  e. 
{ 0 } ) )
8887simprbi 462 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  ( RR  i^i  { 0 } )  ->  x  e.  { 0 } )
89 elsni 4041 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  { 0 }  ->  x  =  0 )
9088, 89syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  ( RR  i^i  { 0 } )  ->  x  =  0 )
91 fveq2 5848 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  =  0  ->  ( abs `  x )  =  ( abs `  0
) )
92 abs0 13200 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( abs `  0 )  =  0
9391, 92syl6eq 2511 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  =  0  ->  ( abs `  x )  =  0 )
9493oveq1d 6285 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  0  ->  (
( abs `  x
)  x.  L )  =  ( 0  x.  L ) )
9561mul02d 9767 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( 0  x.  L
)  =  0 )
9694, 95sylan9eqr 2517 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  = 
0 )  ->  (
( abs `  x
)  x.  L )  =  0 )
97 0lt1 10071 . . . . . . . . . . . . . . . . . . . . . 22  |-  0  <  1
9896, 97syl6eqbr 4476 . . . . . . . . . . . . . . . . . . . . 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 22977 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  0  e.  { r  e.  RR  |  seq 0 (  +  , 
( G `  r
) )  e.  dom  ~~>  } )
101 eleq1 2526 . . . . . . . . . . . . . . . . . . . . . . 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 222 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( x  =  0  ->  x  e.  {
r  e.  RR  |  seq 0 (  +  , 
( G `  r
) )  e.  dom  ~~>  } ) )
103102imp 427 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  = 
0 )  ->  x  e.  { r  e.  RR  |  seq 0 (  +  ,  ( G `  r ) )  e. 
dom 
~~>  } )
10498, 1032thd 240 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  = 
0 )  ->  (
( ( abs `  x
)  x.  L )  <  1  <->  x  e.  { r  e.  RR  |  seq 0 (  +  , 
( G `  r
) )  e.  dom  ~~>  } ) )
10590, 104sylan2 472 . . . . . . . . . . . . . . . . . . 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 712 . . . . . . . . . . . . . . . . . 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 9538 . . . . . . . . . . . . . . . . . . . . . . 23  |-  RR  C_  CC
108 ssdif 3625 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( RR  C_  CC  ->  ( RR  \  { 0 } ) 
C_  ( CC  \  { 0 } ) )
109107, 108ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( RR 
\  { 0 } )  C_  ( CC  \  { 0 } )
110109sseli 3485 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  ( RR  \  { 0 } )  ->  x  e.  ( CC  \  { 0 } ) )
111 nn0uz 11116 . . . . . . . . . . . . . . . . . . . . . 22  |-  NN0  =  ( ZZ>= `  0 )
1125ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  ( ( abs `  x )  x.  L
)  =/=  1 )  ->  M  e.  NN0 )
113 fvex 5858 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( G `
 x )  e. 
_V
114113a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  ( ( abs `  x )  x.  L
)  =/=  1 )  ->  ( G `  x )  e.  _V )
115 eldifi 3612 . . . . . . . . . . . . . . . . . . . . . . . 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 6118 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5941 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  x  e.  CC )  ->  ( G `
 x )  =  ( n  e.  NN0  |->  ( ( A `  n )  x.  (
x ^ n ) ) ) )
120119adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  x  e.  CC )  /\  k  e.  NN0 )  ->  ( G `  x )  =  ( n  e. 
NN0  |->  ( ( A `
 n )  x.  ( x ^ n
) ) ) )
121 fveq2 5848 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( n  =  k  ->  ( A `  n )  =  ( A `  k ) )
122 oveq2 6278 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( n  =  k  ->  (
x ^ n )  =  ( x ^
k ) )
123121, 122oveq12d 6288 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( n  =  k  ->  (
( A `  n
)  x.  ( x ^ n ) )  =  ( ( A `
 k )  x.  ( x ^ k
) ) )
124123adantl 464 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  x  e.  CC )  /\  k  e.  NN0 )  /\  n  =  k )  ->  ( ( A `  n )  x.  ( x ^ n
) )  =  ( ( A `  k
)  x.  ( x ^ k ) ) )
125 simpr 459 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  x  e.  CC )  /\  k  e.  NN0 )  ->  k  e.  NN0 )
126 ovex 6298 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5936 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  x  e.  CC )  /\  k  e.  NN0 )  ->  (
( G `  x
) `  k )  =  ( ( A `
 k )  x.  ( x ^ k
) ) )
12935adantlr 712 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  x  e.  CC )  /\  k  e.  NN0 )  ->  ( A `  k )  e.  CC )
130 simplr 753 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  x  e.  CC )  /\  k  e.  NN0 )  ->  x  e.  CC )
131130, 125expcld 12292 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  x  e.  CC )  /\  k  e.  NN0 )  ->  (
x ^ k )  e.  CC )
132129, 131mulcld 9605 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  x  e.  CC )  /\  k  e.  NN0 )  ->  (
( A `  k
)  x.  ( x ^ k ) )  e.  CC )
133128, 132eqeltrd 2542 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  x  e.  CC )  /\  k  e.  NN0 )  ->  (
( G `  x
) `  k )  e.  CC )
134115, 133sylanl2 649 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  NN0 )  ->  ( ( G `
 x ) `  k )  e.  CC )
135134adantlr 712 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  x  e.  ( CC  \  { 0 } ) )  /\  ( ( abs `  x )  x.  L )  =/=  1 )  /\  k  e.  NN0 )  ->  (
( G `  x
) `  k )  e.  CC )
13634adantlr 712 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  x  e.  CC )  /\  k  e.  Z )  ->  k  e.  NN0 )
137136, 128syldan 468 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  x  e.  CC )  /\  k  e.  Z )  ->  (
( G `  x
) `  k )  =  ( ( A `
 k )  x.  ( x ^ k
) ) )
138115, 137sylanl2 649 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( ( G `  x ) `  k )  =  ( ( A `  k
)  x.  ( x ^ k ) ) )
13936adantlr 712 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( A `  k )  e.  CC )
140115adantl 464 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  x  e.  ( CC  \  { 0 } ) )  ->  x  e.  CC )
141140adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  x  e.  CC )
14234adantlr 712 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  k  e.  NN0 )
143141, 142expcld 12292 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( x ^ k )  e.  CC )
14437adantlr 712 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( A `  k )  =/=  0
)
145 eldifsni 4142 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( x  e.  ( CC  \  { 0 } )  ->  x  =/=  0
)
146145ad2antlr 724 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  x  =/=  0 )
147142nn0zd 10963 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  k  e.  ZZ )
148141, 146, 147expne0d 12298 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( x ^ k )  =/=  0 )
149139, 143, 144, 148mulne0d 10197 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( ( A `  k )  x.  ( x ^ k
) )  =/=  0
)
150138, 149eqnetrd 2747 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( ( G `  x ) `  k )  =/=  0
)
151150adantlr 712 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  x  e.  ( CC  \  { 0 } ) )  /\  ( ( abs `  x )  x.  L )  =/=  1 )  /\  k  e.  Z )  ->  (
( G `  x
) `  k )  =/=  0 )
152 oveq1 6277 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( n  =  k  ->  (
n  +  1 )  =  ( k  +  1 ) )
153152fveq2d 5852 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( n  =  k  ->  (
( G `  x
) `  ( n  +  1 ) )  =  ( ( G `
 x ) `  ( k  +  1 ) ) )
154 fveq2 5848 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( n  =  k  ->  (
( G `  x
) `  n )  =  ( ( G `
 x ) `  k ) )
155153, 154oveq12d 6288 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( n  =  k  ->  (
( ( G `  x ) `  (
n  +  1 ) )  /  ( ( G `  x ) `
 n ) )  =  ( ( ( G `  x ) `
 ( k  +  1 ) )  / 
( ( G `  x ) `  k
) ) )
156155fveq2d 5852 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  =  k  ->  ( abs `  ( ( ( G `  x ) `
 ( n  + 
1 ) )  / 
( ( G `  x ) `  n
) ) )  =  ( abs `  (
( ( G `  x ) `  (
k  +  1 ) )  /  ( ( G `  x ) `
 k ) ) ) )
157156cbvmptv 4530 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( n  e.  Z  |->  ( abs `  ( ( ( G `
 x ) `  ( n  +  1
) )  /  (
( G `  x
) `  n )
) ) )  =  ( k  e.  Z  |->  ( abs `  (
( ( G `  x ) `  (
k  +  1 ) )  /  ( ( G `  x ) `
 k ) ) ) )
1584reseq2i 5259 . . . . . . . . . . . . . . . . . . . . . . . . 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 463 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  x  e.  ( CC  \  { 0 } ) )  ->  Z  C_  NN0 )
160159resmptd 5313 . . . . . . . . . . . . . . . . . . . . . . . . 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 2509 . . . . . . . . . . . . . . . . . . . . . . . 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 463 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  x  e.  ( CC  \  { 0 } ) )  ->  M  e.  ZZ )
1638adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  x  e.  ( CC  \  { 0 } ) )  ->  D 
~~>  L )
164140abscld 13349 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  x  e.  ( CC  \  { 0 } ) )  -> 
( abs `  x
)  e.  RR )
165164recnd 9611 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  x  e.  ( CC  \  { 0 } ) )  -> 
( abs `  x
)  e.  CC )
16610mptex 6118 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9611 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  k  e.  Z )  ->  ( D `  k )  e.  CC )
169168adantlr 712 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( D `  k )  e.  CC )
170 eqidd 2455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5858 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5936 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  x  e.  CC )  /\  k  e.  Z )  ->  ( G `  x )  =  ( n  e. 
NN0  |->  ( ( A `
 n )  x.  ( x ^ n
) ) ) )
176 simpr 459 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ph  /\  x  e.  CC )  /\  k  e.  Z
)  /\  n  =  ( k  +  1 ) )  ->  n  =  ( k  +  1 ) )
177176fveq2d 5852 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ph  /\  x  e.  CC )  /\  k  e.  Z
)  /\  n  =  ( k  +  1 ) )  ->  ( A `  n )  =  ( A `  ( k  +  1 ) ) )
178176oveq2d 6286 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ph  /\  x  e.  CC )  /\  k  e.  Z
)  /\  n  =  ( k  +  1 ) )  ->  (
x ^ n )  =  ( x ^
( k  +  1 ) ) )
179177, 178oveq12d 6288 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 10807 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  1  e.  NN0
181180a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ph  /\  x  e.  CC )  /\  k  e.  Z )  ->  1  e.  NN0 )
182136, 181nn0addcld 10852 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  x  e.  CC )  /\  k  e.  Z )  ->  (
k  +  1 )  e.  NN0 )
183 ovex 6298 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5936 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  x  e.  CC )  /\  k  e.  Z )  ->  (
( G `  x
) `  ( k  +  1 ) )  =  ( ( A `
 ( k  +  1 ) )  x.  ( x ^ (
k  +  1 ) ) ) )
186123adantl 464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5936 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  x  e.  CC )  /\  k  e.  Z )  ->  (
( G `  x
) `  k )  =  ( ( A `
 k )  x.  ( x ^ k
) ) )
189185, 188oveq12d 6288 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 649 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 712 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( A `  ( k  +  1 ) )  e.  CC )
192115, 182sylanl2 649 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( k  +  1 )  e. 
NN0 )
193141, 192expcld 12292 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( x ^ ( k  +  1 ) )  e.  CC )
194191, 139, 193, 143, 144, 148divmuldivd 10357 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 10850 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  k  e.  CC )
196 1cnd 9601 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  1  e.  CC )
197195, 196pncan2d 9924 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( (
k  +  1 )  -  k )  =  1 )
198197oveq2d 6286 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( x ^ ( ( k  +  1 )  -  k ) )  =  ( x ^ 1 ) )
199192nn0zd 10963 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( k  +  1 )  e.  ZZ )
200141, 146, 147, 199expsubd 12303 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( x ^ ( ( k  +  1 )  -  k ) )  =  ( ( x ^
( k  +  1 ) )  /  (
x ^ k ) ) )
201141exp1d 12287 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( x ^ 1 )  =  x )
202198, 200, 2013eqtr3d 2503 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( (
x ^ ( k  +  1 ) )  /  ( x ^
k ) )  =  x )
203202oveq2d 6286 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2501 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( (
( G `  x
) `  ( k  +  1 ) )  /  ( ( G `
 x ) `  k ) )  =  ( ( ( A `
 ( k  +  1 ) )  / 
( A `  k
) )  x.  x
) )
205204fveq2d 5852 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 712 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( ( A `  ( k  +  1 ) )  /  ( A `  k ) )  e.  CC )
207206, 141absmuld 13367 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2499 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2497 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  k  e.  Z )  ->  ( D `  k )  =  ( abs `  (
( A `  (
k  +  1 ) )  /  ( A `
 k ) ) ) )
210209adantlr 712 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( D `  k )  =  ( abs `  ( ( A `  ( k  +  1 ) )  /  ( A `  k ) ) ) )
211210eqcomd 2462 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( abs `  ( ( A `  ( k  +  1 ) )  /  ( A `  k )
) )  =  ( D `  k ) )
212211oveq1d 6285 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( ( abs `  ( ( A `
 ( k  +  1 ) )  / 
( A `  k
) ) )  x.  ( abs `  x
) )  =  ( ( D `  k
)  x.  ( abs `  x ) ) )
213165adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( abs `  x )  e.  CC )
214169, 213mulcomd 9606 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( ( D `  k )  x.  ( abs `  x
) )  =  ( ( abs `  x
)  x.  ( D `
 k ) ) )
215208, 212, 2143eqtrd 2499 . . . . . . . . . . . . . . . . . . . . . . . . . 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 13541 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  x  e.  ( CC  \  { 0 } ) )  -> 
( n  e.  NN0  |->  ( abs `  ( ( ( G `  x
) `  ( n  +  1 ) )  /  ( ( G `
 x ) `  n ) ) ) )  ~~>  ( ( abs `  x )  x.  L
) )
217 climres 13480 . . . . . . . . . . . . . . . . . . . . . . . . . 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 660 . . . . . . . . . . . . . . . . . . . . . . . . 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 232 . . . . . . . . . . . . . . . . . . . . . . . 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 4461 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  x  e.  ( CC  \  { 0 } ) )  -> 
( n  e.  Z  |->  ( abs `  (
( ( G `  x ) `  (
n  +  1 ) )  /  ( ( G `  x ) `
 n ) ) ) )  ~~>  ( ( abs `  x )  x.  L ) )
221220adantr 463 . . . . . . . . . . . . . . . . . . . . . 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 459 . . . . . . . . . . . . . . . . . . . . . 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 31435 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  ( ( abs `  x )  x.  L
)  =/=  1 )  ->  ( ( ( abs `  x )  x.  L )  <  1  <->  seq 0 (  +  ,  ( G `  x ) )  e. 
dom 
~~>  ) )
224110, 223sylanl2 649 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  x  e.  ( RR  \  {
0 } ) )  /\  ( ( abs `  x )  x.  L
)  =/=  1 )  ->  ( ( ( abs `  x )  x.  L )  <  1  <->  seq 0 (  +  ,  ( G `  x ) )  e. 
dom 
~~>  ) )
225 eldifi 3612 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  ( RR  \  { 0 } )  ->  x  e.  RR )
226 fveq2 5848 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( r  =  x  ->  ( G `  r )  =  ( G `  x ) )
227226seqeq3d 12097 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( r  =  x  ->  seq 0 (  +  , 
( G `  r
) )  =  seq 0 (  +  , 
( G `  x
) ) )
228227eleq1d 2523 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( r  =  x  ->  (  seq 0 (  +  , 
( G `  r
) )  e.  dom  ~~>  <->  seq 0 (  +  , 
( G `  x
) )  e.  dom  ~~>  ) )
229228elrab3 3255 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  RR  ->  (
x  e.  { r  e.  RR  |  seq 0 (  +  , 
( G `  r
) )  e.  dom  ~~>  }  <->  seq 0 (  +  , 
( G `  x
) )  e.  dom  ~~>  ) )
230225, 229syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  ( RR  \  { 0 } )  ->  ( x  e. 
{ r  e.  RR  |  seq 0 (  +  ,  ( G `  r ) )  e. 
dom 
~~>  }  <->  seq 0 (  +  ,  ( G `  x ) )  e. 
dom 
~~>  ) )
231230ad2antlr 724 . . . . . . . . . . . . . . . . . . . 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 256 . . . . . . . . . . . . . . . . . . 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 802 . . . . . . . . . . . . . . . . . 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 783 . . . . . . . . . . . . . . . . 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 474 . . . . . . . . . . . . . . . 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 802 . . . . . . . . . . . . . . 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 255 . . . . . . . . . . . . . 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 468 . . . . . . . . . . . . 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 292 . . . . . . . . . . . 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 253 . . . . . . . . . . 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 207 . . . . . . . . . 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 438 . . . . . . . . 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 432 . . . . . . 7  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( 1  /  L )  <  ( abs `  x
)  ->  -.  x  e.  { r  e.  RR  |  seq 0 (  +  ,  ( G `  r ) )  e. 
dom 
~~>  } ) )
245244con2d 115 . . . . . 6  |-  ( (
ph  /\  x  e.  RR )  ->  ( x  e.  { r  e.  RR  |  seq 0
(  +  ,  ( G `  r ) )  e.  dom  ~~>  }  ->  -.  ( 1  /  L
)  <  ( abs `  x ) ) )
24647adantr 463 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR )  /\  (
1  /  L )  <  x )  -> 
( 1  /  L
)  e.  RR )
247 simplr 753 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR )  /\  (
1  /  L )  <  x )  ->  x  e.  RR )
24850adantr 463 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR )  /\  (
1  /  L )  <  x )  -> 
( abs `  x
)  e.  RR )
249 simpr 459 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR )  /\  (
1  /  L )  <  x )  -> 
( 1  /  L
)  <  x )
250247leabsd 13328 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR )  /\  (
1  /  L )  <  x )  ->  x  <_  ( abs `  x
) )
251246, 247, 248, 249, 250ltletrd 9731 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR )  /\  (
1  /  L )  <  x )  -> 
( 1  /  L
)  <  ( abs `  x ) )
252251ex 432 . . . . . 6  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( 1  /  L )  <  x  ->  (
1  /  L )  <  ( abs `  x
) ) )
253245, 252nsyld 140 . . . . 5  |-  ( (
ph  /\  x  e.  RR )  ->  ( x  e.  { r  e.  RR  |  seq 0
(  +  ,  ( G `  r ) )  e.  dom  ~~>  }  ->  -.  ( 1  /  L
)  <  x )
)
25446, 253sylan2 472 . . . 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 9982 . . . . . . . . 9  |-  ( ph  -> 
-u ( 1  /  L )  e.  RR )
257256rexrd 9632 . . . . . . . 8  |-  ( ph  -> 
-u ( 1  /  L )  e.  RR* )
258 iooss1 11567 . . . . . . . 8  |-  ( (
-u ( 1  /  L )  e.  RR*  /\  -u ( 1  /  L
)  <_  x )  ->  ( x (,) (
1  /  L ) )  C_  ( -u (
1  /  L ) (,) ( 1  /  L ) ) )
259257, 258sylan 469 . . . . . . 7  |-  ( (
ph  /\  -u ( 1  /  L )  <_  x )  ->  (
x (,) ( 1  /  L ) ) 
C_  ( -u (
1  /  L ) (,) ( 1  /  L ) ) )
260259adantlr 712 . . . . . 6  |-  ( ( ( ph  /\  (
x  e.  RR*  /\  x  <  ( 1  /  L
) ) )  /\  -u ( 1  /  L
)  <_  x )  ->  ( x (,) (
1  /  L ) )  C_  ( -u (
1  /  L ) (,) ( 1  /  L ) ) )
261 eliooord 11587 . . . . . . . . . . 11  |-  ( k  e.  ( x (,) ( 1  /  L
) )  ->  (
x  <  k  /\  k  <  ( 1  /  L ) ) )
262261simpld 457 . . . . . . . . . 10  |-  ( k  e.  ( x (,) ( 1  /  L
) )  ->  x  <  k )
263262rgen 2814 . . . . . . . . 9  |-  A. k  e.  ( x (,) (
1  /  L ) ) x  <  k
264 ioon0 11558 . . . . . . . . . . . . 13  |-  ( ( x  e.  RR*  /\  (
1  /  L )  e.  RR* )  ->  (
( x (,) (
1  /  L ) )  =/=  (/)  <->  x  <  ( 1  /  L ) ) )
26544, 264sylan2 472 . . . . . . . . . . . 12  |-  ( ( x  e.  RR*  /\  ph )  ->  ( ( x (,) ( 1  /  L ) )  =/=  (/) 
<->  x  <  ( 1  /  L ) ) )
266265ancoms 451 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  RR* )  ->  ( (
x (,) ( 1  /  L ) )  =/=  (/)  <->  x  <  ( 1  /  L ) ) )
267266biimpar 483 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR* )  /\  x  <  ( 1  /  L
) )  ->  (
x (,) ( 1  /  L ) )  =/=  (/) )
268 r19.2zb 3907 . . . . . . . . . 10  |-  ( ( x (,) ( 1  /  L ) )  =/=  (/)  <->  ( A. k  e.  ( x (,) (
1  /  L ) ) x  <  k  ->  E. k  e.  ( x (,) ( 1  /  L ) ) x  <  k ) )
269267, 268sylib 196 . . . . . . . . 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 17 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR* )  /\  x  <  ( 1  /  L
) )  ->  E. k  e.  ( x (,) (
1  /  L ) ) x  <  k
)
271270anasss 645 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  RR*  /\  x  < 
( 1  /  L
) ) )  ->  E. k  e.  (
x (,) ( 1  /  L ) ) x  <  k )
272271adantr 463 . . . . . 6  |-  ( ( ( ph  /\  (
x  e.  RR*  /\  x  <  ( 1  /  L
) ) )  /\  -u ( 1  /  L
)  <_  x )  ->  E. k  e.  ( x (,) ( 1  /  L ) ) x  <  k )
273 ssrexv 3551 . . . . . 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 60 . . . . 5  |-  ( ( ( ph  /\  (
x  e.  RR*  /\  x  <  ( 1  /  L
) ) )  /\  -u ( 1  /  L
)  <_  x )  ->  E. k  e.  (
-u ( 1  /  L ) (,) (
1  /  L ) ) x  <  k
)
275 simplr 753 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR* )  /\  -.  -u ( 1  /  L
)  <_  x )  ->  x  e.  RR* )
276 xrltnle 9642 . . . . . . . . . . . . . . 15  |-  ( ( x  e.  RR*  /\  -u (
1  /  L )  e.  RR* )  ->  (
x  <  -u ( 1  /  L )  <->  -.  -u (
1  /  L )  <_  x ) )
277 xrltle 11358 . . . . . . . . . . . . . . 15  |-  ( ( x  e.  RR*  /\  -u (
1  /  L )  e.  RR* )  ->  (
x  <  -u ( 1  /  L )  ->  x  <_  -u ( 1  /  L ) ) )
278276, 277sylbird 235 . . . . . . . . . . . . . 14  |-  ( ( x  e.  RR*  /\  -u (
1  /  L )  e.  RR* )  ->  ( -.  -u ( 1  /  L )  <_  x  ->  x  <_  -u ( 1  /  L ) ) )
279257, 278sylan2 472 . . . . . . . . . . . . 13  |-  ( ( x  e.  RR*  /\  ph )  ->  ( -.  -u (
1  /  L )  <_  x  ->  x  <_ 
-u ( 1  /  L ) ) )
280279ancoms 451 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  RR* )  ->  ( -.  -u ( 1  /  L
)  <_  x  ->  x  <_  -u ( 1  /  L ) ) )
281280imp 427 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR* )  /\  -.  -u ( 1  /  L
)  <_  x )  ->  x  <_  -u ( 1  /  L ) )
282 iooss1 11567 . . . . . . . . . . 11  |-  ( ( x  e.  RR*  /\  x  <_ 
-u ( 1  /  L ) )  -> 
( -u ( 1  /  L ) (,) (
1  /  L ) )  C_  ( x (,) ( 1  /  L
) ) )
283275, 281, 282syl2anc 659 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR* )  /\  -.  -u ( 1  /  L
)  <_  x )  ->  ( -u ( 1  /  L ) (,) ( 1  /  L
) )  C_  (
x (,) ( 1  /  L ) ) )
284283sselda 3489 . . . . . . . . 9  |-  ( ( ( ( ph  /\  x  e.  RR* )  /\  -.  -u ( 1  /  L )  <_  x
)  /\  k  e.  ( -u ( 1  /  L ) (,) (
1  /  L ) ) )  ->  k  e.  ( x (,) (
1  /  L ) ) )
285284, 262syl 16 . . . . . . . 8  |-  ( ( ( ( ph  /\  x  e.  RR* )  /\  -.  -u ( 1  /  L )  <_  x
)  /\  k  e.  ( -u ( 1  /  L ) (,) (
1  /  L ) ) )  ->  x  <  k )
286285ralrimiva 2868 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR* )  /\  -.  -u ( 1  /  L
)  <_  x )  ->  A. k  e.  (
-u ( 1  /  L ) (,) (
1  /  L ) ) x  <  k
)
28741, 78recgt0d 10475 . . . . . . . . . . . . 13  |-  ( ph  ->  0  <  ( 1  /  L ) )
28843, 43, 287, 287addgt0d 10123 . . . . . . . . . . . 12  |-  ( ph  ->  0  <  ( ( 1  /  L )  +  ( 1  /  L ) ) )
28943recnd 9611 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 1  /  L
)  e.  CC )
290289, 289subnegd 9929 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( 1  /  L )  -  -u (
1  /  L ) )  =  ( ( 1  /  L )  +  ( 1  /  L ) ) )
291288, 290breqtrrd 4465 . . . . . . . . . . 11  |-  ( ph  ->  0  <  ( ( 1  /  L )  -  -u ( 1  /  L ) ) )
292256, 43posdifd 10135 . . . . . . . . . . 11  |-  ( ph  ->  ( -u ( 1  /  L )  < 
( 1  /  L
)  <->  0  <  (
( 1  /  L
)  -  -u (
1  /  L ) ) ) )
293291, 292mpbird 232 . . . . . . . . . 10  |-  ( ph  -> 
-u ( 1  /  L )  <  (
1  /  L ) )
294 ioon0 11558 . . . . . . . . . . 11  |-  ( (
-u ( 1  /  L )  e.  RR*  /\  ( 1  /  L
)  e.  RR* )  ->  ( ( -u (
1  /  L ) (,) ( 1  /  L ) )  =/=  (/) 
<-> 
-u ( 1  /  L )  <  (
1  /  L ) ) )
295257, 44, 294syl2anc 659 . . . . . . . . . 10  |-  ( ph  ->  ( ( -u (
1  /  L ) (,) ( 1  /  L ) )  =/=  (/) 
<-> 
-u ( 1  /  L )  <  (
1  /  L ) ) )
296293, 295mpbird 232 . . . . . . . . 9  |-  ( ph  ->  ( -u ( 1  /  L ) (,) ( 1  /  L
) )  =/=  (/) )
297 r19.2zb 3907 . . . . . . . . 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 196 . . . . . . . 8  |-  ( ph  ->  ( A. k  e.  ( -u ( 1  /  L ) (,) ( 1  /  L
) ) x  < 
k  ->  E. k  e.  ( -u ( 1  /  L ) (,) ( 1  /  L
) ) x  < 
k ) )
299298ad2antrr 723 . . . . . . 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 718 . . . . 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 789 . . . 4  |-  ( (
ph  /\  ( x  e.  RR*  /\  x  < 
( 1  /  L
) ) )  ->  E. k  e.  ( -u ( 1  /  L
) (,) ( 1  /  L ) ) x  <  k )
303 elioo2 11573 . . . . . . . . . . 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 659 . . . . . . . . . 10  |-  ( ph  ->  ( x  e.  (
-u ( 1  /  L ) (,) (
1  /  L ) )  <->  ( x  e.  RR  /\  -u (
1  /  L )  <  x  /\  x  <  ( 1  /  L
) ) ) )
305304biimpa 482 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( -u ( 1  /  L ) (,) (
1  /  L ) ) )  ->  (
x  e.  RR  /\  -u ( 1  /  L
)  <  x  /\  x  <  ( 1  /  L ) ) )
306 simpr 459 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  RR )  ->  x  e.  RR )
307306, 47absltd 13343 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( abs `  x )  <  ( 1  /  L )  <->  ( -u (
1  /  L )  <  x  /\  x  <  ( 1  /  L
) ) ) )
30850adantr 463 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  RR )  /\  ( abs `  x )  < 
( 1  /  L
) )  ->  ( abs `  x )  e.  RR )
309 simpr 459 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  RR )  /\  ( abs `  x )  < 
( 1  /  L
) )  ->  ( abs `  x )  < 
( 1  /  L
) )
310308, 309ltned 9710 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  RR )  /\  ( abs `  x )  < 
( 1  /  L
) )  ->  ( abs `  x )  =/=  ( 1  /  L
) )
311238biimpd 207 . . . . . . . . . . . . . . . . 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 438 . . . . . . . . . . . . . . . 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 432 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( abs `  x )  <  ( 1  /  L )  ->  x  e.  { r  e.  RR  |  seq 0 (  +  ,  ( G `  r ) )  e. 
dom 
~~>  } ) )
315307, 314sylbird 235 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  RR )  ->  ( (
-u ( 1  /  L )  <  x  /\  x  <  ( 1  /  L ) )  ->  x  e.  {
r  e.  RR  |  seq 0 (  +  , 
( G `  r
) )  e.  dom  ~~>  } ) )
316315impr 617 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( x  e.  RR  /\  ( -u ( 1  /  L
)  <  x  /\  x  <  ( 1  /  L ) ) ) )  ->  x  e.  { r  e.  RR  |  seq 0 (  +  , 
( G `  r
) )  e.  dom  ~~>  } )
317316expcom 433 . . . . . . . . . . 11  |-  ( ( x  e.  RR  /\  ( -u ( 1  /  L )  <  x  /\  x  <  ( 1  /  L ) ) )  ->  ( ph  ->  x  e.  { r  e.  RR  |  seq 0 (  +  , 
( G `  r
) )  e.  dom  ~~>  } ) )
3183173impb 1190 . . . . . . . . . 10  |-  ( ( x  e.  RR  /\  -u ( 1  /  L
)  <  x  /\  x  <  ( 1  /  L ) )  -> 
( ph  ->  x  e. 
{ r  e.  RR  |  seq 0 (  +  ,  ( G `  r ) )  e. 
dom 
~~>  } ) )
319318impcom 428 . . . . . . . . 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 468 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( -u ( 1  /  L ) (,) (
1  /  L ) ) )  ->  x  e.  { r  e.  RR  |  seq 0 (  +  ,  ( G `  r ) )  e. 
dom 
~~>  } )
321320ex 432 . . . . . . 7  |-  ( ph  ->  ( x  e.  (
-u ( 1  /  L ) (,) (
1  /  L ) )  ->  x  e.  { r  e.  RR  |  seq 0 (  +  , 
( G `  r
) )  e.  dom  ~~>  } ) )
322321ssrdv 3495 . . . . . 6  |-  ( ph  ->  ( -u ( 1  /  L ) (,) ( 1  /  L
) )  C_  { r  e.  RR  |  seq 0 (  +  , 
( G `  r
) )  e.  dom  ~~>  } )
323 ssrexv 3551 . . . . . 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 16 . . . . 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 463 . . . 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 7908 . 2  |-  ( ph  ->  sup ( { r  e.  RR  |  seq 0 (  +  , 
( G `  r
) )  e.  dom  ~~>  } ,  RR* ,  <  )  =  ( 1  /  L ) )
3281, 327syl5eq 2507 1  |-  ( ph  ->  R  =  ( 1  /  L ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    \/ wo 366    /\ wa 367    /\ w3a 971    = wceq 1398    e. wcel 1823    =/= wne 2649   A.wral 2804   E.wrex 2805   {crab 2808   _Vcvv 3106    \ cdif 3458    u. cun 3459    i^i cin 3460    C_ wss 3461   (/)c0 3783   {csn 4016   class class class wbr 4439    |-> cmpt 4497    Or wor 4788   dom cdm 4988    |` cres 4990   -->wf 5566   ` cfv 5570  (class class class)co 6270   supcsup 7892   CCcc 9479   RRcr 9480   0cc0 9481   1c1 9482    + caddc 9484    x. cmul 9486   RR*cxr 9616    < clt 9617    <_ cle 9618    - cmin 9796   -ucneg 9797    / cdiv 10202   NN0cn0 10791   ZZcz 10860   ZZ>=cuz 11082   RR+crp 11221   (,)cioo 11532    seqcseq 12089   ^cexp 12148   abscabs 13149    ~~> cli 13389
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-8 1825  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-rep 4550  ax-sep 4560  ax-nul 4568  ax-pow 4615  ax-pr 4676  ax-un 6565  ax-inf2 8049  ax-cnex 9537  ax-resscn 9538  ax-1cn 9539  ax-icn 9540  ax-addcl 9541  ax-addrcl 9542  ax-mulcl 9543  ax-mulrcl 9544  ax-mulcom 9545  ax-addass 9546  ax-mulass 9547  ax-distr 9548  ax-i2m1 9549  ax-1ne0 9550  ax-1rid 9551  ax-rnegex 9552  ax-rrecex 9553  ax-cnre 9554  ax-pre-lttri 9555  ax-pre-lttrn 9556  ax-pre-ltadd 9557  ax-pre-mulgt0 9558  ax-pre-sup 9559  ax-addf 9560  ax-mulf 9561
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1401  df-fal 1404  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-nel 2652  df-ral 2809  df-rex 2810  df-reu 2811  df-rmo 2812  df-rab 2813  df-v 3108  df-sbc 3325  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-pss 3477  df-nul 3784  df-if 3930  df-pw 4001  df-sn 4017  df-pr 4019  df-tp 4021  df-op 4023  df-uni 4236  df-int 4272  df-iun 4317  df-br 4440  df-opab 4498  df-mpt 4499  df-tr 4533  df-eprel 4780  df-id 4784  df-po 4789  df-so 4790  df-fr 4827  df-se 4828  df-we 4829  df-ord 4870  df-on 4871  df-lim 4872  df-suc 4873  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-rn 4999  df-res 5000  df-ima 5001  df-iota 5534  df-fun 5572  df-fn 5573  df-f 5574  df-f1 5575  df-fo 5576  df-f1o 5577  df-fv 5578  df-isom 5579  df-riota 6232  df-ov 6273  df-oprab 6274  df-mpt2 6275  df-om 6674  df-1st 6773  df-2nd 6774  df-recs 7034  df-rdg 7068  df-1o 7122  df-oadd 7126  df-er 7303  df-pm 7415  df-en 7510  df-dom 7511  df-sdom 7512  df-fin 7513  df-sup 7893  df-oi 7927  df-card 8311  df-pnf 9619  df-mnf 9620  df-xr 9621  df-ltxr 9622  df-le 9623  df-sub 9798  df-neg 9799  df-div 10203  df-nn 10532  df-2 10590  df-3 10591  df-n0 10792  df-z 10861  df-uz 11083  df-q 11184  df-rp 11222  df-ioo 11536  df-ico 11538  df-fz 11676  df-fzo 11800  df-fl 11910  df-seq 12090  df-exp 12149  df-hash 12388  df-shft 12982  df-cj 13014  df-re 13015  df-im 13016  df-sqrt 13150  df-abs 13151  df-limsup 13376  df-clim 13393  df-rlim 13394  df-sum 13591
This theorem is referenced by:  binomcxplemradcnv  31498
  Copyright terms: Public domain W3C validator