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

Theorem radcnvrat 36634
Description: Let  L be the limit, if one exists, of the ratio  ( abs `  (
( A `  (
k  +  1 ) )  /  ( A `
 k ) ) ) (as in the ratio test cvgdvgrat 36633) 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 11448 . . . 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 11046 . . . . . 6  |-  ( ph  ->  M  e.  ZZ )
74reseq2i 5121 . . . . . . 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 10883 . . . . . . . . . . 11  |-  NN0  e.  _V
1110mptex 6152 . . . . . . . . . 10  |-  ( k  e.  NN0  |->  ( abs `  ( ( A `  ( k  +  1 ) )  /  ( A `  k )
) ) )  e. 
_V
129, 11eqeltri 2503 . . . . . . . . 9  |-  D  e. 
_V
13 climres 13639 . . . . . . . . 9  |-  ( ( M  e.  ZZ  /\  D  e.  _V )  ->  ( ( D  |`  ( ZZ>= `  M )
)  ~~>  L  <->  D  ~~>  L ) )
146, 12, 13sylancl 666 . . . . . . . 8  |-  ( ph  ->  ( ( D  |`  ( ZZ>= `  M )
)  ~~>  L  <->  D  ~~>  L ) )
158, 14mpbird 235 . . . . . . 7  |-  ( ph  ->  ( D  |`  ( ZZ>=
`  M ) )  ~~>  L )
167, 15syl5eqbr 4457 . . . . . 6  |-  ( ph  ->  ( D  |`  Z )  ~~>  L )
179reseq1i 5120 . . . . . . . . 9  |-  ( D  |`  Z )  =  ( ( k  e.  NN0  |->  ( abs `  ( ( A `  ( k  +  1 ) )  /  ( A `  k ) ) ) )  |`  Z )
18 eluznn0 11236 . . . . . . . . . . . . . 14  |-  ( ( M  e.  NN0  /\  k  e.  ( ZZ>= `  M ) )  -> 
k  e.  NN0 )
195, 18sylan 473 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  ( ZZ>= `  M )
)  ->  k  e.  NN0 )
2019ex 435 . . . . . . . . . . . 12  |-  ( ph  ->  ( k  e.  (
ZZ>= `  M )  -> 
k  e.  NN0 )
)
2120ssrdv 3470 . . . . . . . . . . 11  |-  ( ph  ->  ( ZZ>= `  M )  C_ 
NN0 )
224, 21syl5eqss 3508 . . . . . . . . . 10  |-  ( ph  ->  Z  C_  NN0 )
2322resmptd 5175 . . . . . . . . 9  |-  ( ph  ->  ( ( k  e. 
NN0  |->  ( abs `  (
( A `  (
k  +  1 ) )  /  ( A `
 k ) ) ) )  |`  Z )  =  ( k  e.  Z  |->  ( abs `  (
( A `  (
k  +  1 ) )  /  ( A `
 k ) ) ) ) )
2417, 23syl5eq 2475 . . . . . . . 8  |-  ( ph  ->  ( D  |`  Z )  =  ( k  e.  Z  |->  ( abs `  (
( A `  (
k  +  1 ) )  /  ( A `
 k ) ) ) ) )
25 fvex 5892 . . . . . . . . 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 5976 . . . . . . 7  |-  ( (
ph  /\  k  e.  Z )  ->  (
( D  |`  Z ) `
 k )  =  ( abs `  (
( A `  (
k  +  1 ) )  /  ( A `
 k ) ) ) )
284peano2uzs 11221 . . . . . . . . . 10  |-  ( k  e.  Z  ->  (
k  +  1 )  e.  Z )
2922sselda 3464 . . . . . . . . . . 11  |-  ( (
ph  /\  ( k  +  1 )  e.  Z )  ->  (
k  +  1 )  e.  NN0 )
30 radcnvrat.a . . . . . . . . . . . 12  |-  ( ph  ->  A : NN0 --> CC )
3130ffvelrnda 6038 . . . . . . . . . . 11  |-  ( (
ph  /\  ( k  +  1 )  e. 
NN0 )  ->  ( A `  ( k  +  1 ) )  e.  CC )
3229, 31syldan 472 . . . . . . . . . 10  |-  ( (
ph  /\  ( k  +  1 )  e.  Z )  ->  ( A `  ( k  +  1 ) )  e.  CC )
3328, 32sylan2 476 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  Z )  ->  ( A `  ( k  +  1 ) )  e.  CC )
3422sselda 3464 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  Z )  ->  k  e.  NN0 )
3530ffvelrnda 6038 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( A `  k )  e.  CC )
3634, 35syldan 472 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  Z )  ->  ( A `  k )  e.  CC )
37 radcnvrat.n0 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  Z )  ->  ( A `  k )  =/=  0 )
3833, 36, 37divcld 10391 . . . . . . . 8  |-  ( (
ph  /\  k  e.  Z )  ->  (
( A `  (
k  +  1 ) )  /  ( A `
 k ) )  e.  CC )
3938abscld 13498 . . . . . . 7  |-  ( (
ph  /\  k  e.  Z )  ->  ( abs `  ( ( A `
 ( k  +  1 ) )  / 
( A `  k
) ) )  e.  RR )
4027, 39eqeltrd 2507 . . . . . 6  |-  ( (
ph  /\  k  e.  Z )  ->  (
( D  |`  Z ) `
 k )  e.  RR )
414, 6, 16, 40climrecl 13647 . . . . 5  |-  ( ph  ->  L  e.  RR )
42 radcnvrat.ln0 . . . . 5  |-  ( ph  ->  L  =/=  0 )
4341, 42rereccld 10442 . . . 4  |-  ( ph  ->  ( 1  /  L
)  e.  RR )
4443rexrd 9698 . . 3  |-  ( ph  ->  ( 1  /  L
)  e.  RR* )
45 simpr 462 . . . 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 3225 . . . . 5  |-  ( x  e.  { r  e.  RR  |  seq 0
(  +  ,  ( G `  r ) )  e.  dom  ~~>  }  ->  x  e.  RR )
4743adantr 466 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  RR )  ->  ( 1  /  L )  e.  RR )
48 recn 9637 . . . . . . . . . . . . 13  |-  ( x  e.  RR  ->  x  e.  CC )
4948abscld 13498 . . . . . . . . . . . 12  |-  ( x  e.  RR  ->  ( abs `  x )  e.  RR )
5049adantl 467 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  RR )  ->  ( abs `  x )  e.  RR )
5147, 50ltlend 9788 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( 1  /  L )  <  ( abs `  x
)  <->  ( ( 1  /  L )  <_ 
( abs `  x
)  /\  ( abs `  x )  =/=  (
1  /  L ) ) ) )
5251simplbda 628 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR )  /\  (
1  /  L )  <  ( abs `  x
) )  ->  ( abs `  x )  =/=  ( 1  /  L
) )
5351adantr 466 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR )  /\  ( abs `  x )  =/=  ( 1  /  L
) )  ->  (
( 1  /  L
)  <  ( abs `  x )  <->  ( (
1  /  L )  <_  ( abs `  x
)  /\  ( abs `  x )  =/=  (
1  /  L ) ) ) )
54 simpr 462 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  RR )  /\  ( abs `  x )  =/=  ( 1  /  L
) )  ->  ( abs `  x )  =/=  ( 1  /  L
) )
5554biantrud 509 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR )  /\  ( abs `  x )  =/=  ( 1  /  L
) )  ->  (
( 1  /  L
)  <_  ( abs `  x )  <->  ( (
1  /  L )  <_  ( abs `  x
)  /\  ( abs `  x )  =/=  (
1  /  L ) ) ) )
5647, 50lenltd 9789 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( 1  /  L )  <_  ( abs `  x
)  <->  -.  ( abs `  x )  <  (
1  /  L ) ) )
5756adantr 466 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR )  /\  ( abs `  x )  =/=  ( 1  /  L
) )  ->  (
( 1  /  L
)  <_  ( abs `  x )  <->  -.  ( abs `  x )  < 
( 1  /  L
) ) )
5853, 55, 573bitr2d 284 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR )  /\  ( abs `  x )  =/=  ( 1  /  L
) )  ->  (
( 1  /  L
)  <  ( abs `  x )  <->  -.  ( abs `  x )  < 
( 1  /  L
) ) )
59 1cnd 9667 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  RR )  ->  1  e.  CC )
6050recnd 9677 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  RR )  ->  ( abs `  x )  e.  CC )
6141recnd 9677 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  L  e.  CC )
6261adantr 466 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  RR )  ->  L  e.  CC )
6342adantr 466 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  RR )  ->  L  =/=  0 )
6459, 60, 62, 63divmul3d 10425 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( 1  /  L )  =  ( abs `  x
)  <->  1  =  ( ( abs `  x
)  x.  L ) ) )
65 eqcom 2431 . . . . . . . . . . . . . . . . 17  |-  ( ( 1  /  L )  =  ( abs `  x
)  <->  ( abs `  x
)  =  ( 1  /  L ) )
66 eqcom 2431 . . . . . . . . . . . . . . . . 17  |-  ( 1  =  ( ( abs `  x )  x.  L
)  <->  ( ( abs `  x )  x.  L
)  =  1 )
6764, 65, 663bitr3g 290 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( abs `  x )  =  ( 1  /  L )  <->  ( ( abs `  x )  x.  L )  =  1 ) )
6867necon3bid 2678 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( abs `  x )  =/=  ( 1  /  L )  <->  ( ( abs `  x )  x.  L )  =/=  1
) )
6968biimpa 486 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  RR )  /\  ( abs `  x )  =/=  ( 1  /  L
) )  ->  (
( abs `  x
)  x.  L )  =/=  1 )
70 1red 9666 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  RR )  ->  1  e.  RR )
71 fvres 5896 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( k  e.  Z  ->  (
( D  |`  Z ) `
 k )  =  ( D `  k
) )
7271adantl 467 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  k  e.  Z )  ->  (
( D  |`  Z ) `
 k )  =  ( D `  k
) )
7372, 40eqeltrrd 2508 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  k  e.  Z )  ->  ( D `  k )  e.  RR )
7438absge0d 13506 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  k  e.  Z )  ->  0  <_  ( abs `  (
( A `  (
k  +  1 ) )  /  ( A `
 k ) ) ) )
7574, 27breqtrrd 4450 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  k  e.  Z )  ->  0  <_  ( ( D  |`  Z ) `  k
) )
7675, 72breqtrd 4448 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  k  e.  Z )  ->  0  <_  ( D `  k
) )
774, 6, 8, 73, 76climge0 13648 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  0  <_  L )
7841, 77, 42ne0gt0d 9780 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  0  <  L )
7941, 78elrpd 11346 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  L  e.  RR+ )
8079adantr 466 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  RR )  ->  L  e.  RR+ )
8150, 70, 80ltmuldivd 11393 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( ( abs `  x
)  x.  L )  <  1  <->  ( abs `  x )  <  (
1  /  L ) ) )
8281adantr 466 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  RR )  /\  (
( abs `  x
)  x.  L )  =/=  1 )  -> 
( ( ( abs `  x )  x.  L
)  <  1  <->  ( abs `  x )  <  (
1  /  L ) ) )
83 elun 3606 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  ( ( RR 
i^i  { 0 } )  u.  ( RR  \  { 0 } ) )  <->  ( x  e.  ( RR  i^i  {
0 } )  \/  x  e.  ( RR 
\  { 0 } ) ) )
84 inundif 3875 . . . . . . . . . . . . . . . . . . 19  |-  ( ( RR  i^i  { 0 } )  u.  ( RR  \  { 0 } ) )  =  RR
8584eleq2i 2499 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  ( ( RR 
i^i  { 0 } )  u.  ( RR  \  { 0 } ) )  <->  x  e.  RR )
8683, 85bitr3i 254 . . . . . . . . . . . . . . . . 17  |-  ( ( x  e.  ( RR 
i^i  { 0 } )  \/  x  e.  ( RR  \  { 0 } ) )  <->  x  e.  RR )
87 elin 3649 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  ( RR  i^i  { 0 } )  <->  ( x  e.  RR  /\  x  e. 
{ 0 } ) )
8887simprbi 465 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  ( RR  i^i  { 0 } )  ->  x  e.  { 0 } )
89 elsni 4023 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  { 0 }  ->  x  =  0 )
9088, 89syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  ( RR  i^i  { 0 } )  ->  x  =  0 )
91 fveq2 5882 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  =  0  ->  ( abs `  x )  =  ( abs `  0
) )
92 abs0 13349 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( abs `  0 )  =  0
9391, 92syl6eq 2479 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  =  0  ->  ( abs `  x )  =  0 )
9493oveq1d 6321 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  0  ->  (
( abs `  x
)  x.  L )  =  ( 0  x.  L ) )
9561mul02d 9839 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( 0  x.  L
)  =  0 )
9694, 95sylan9eqr 2485 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  = 
0 )  ->  (
( abs `  x
)  x.  L )  =  0 )
97 0lt1 10144 . . . . . . . . . . . . . . . . . . . . . 22  |-  0  <  1
9896, 97syl6eqbr 4461 . . . . . . . . . . . . . . . . . . . . 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 23370 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  0  e.  { r  e.  RR  |  seq 0 (  +  , 
( G `  r
) )  e.  dom  ~~>  } )
101 eleq1 2495 . . . . . . . . . . . . . . . . . . . . . . 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 225 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( x  =  0  ->  x  e.  {
r  e.  RR  |  seq 0 (  +  , 
( G `  r
) )  e.  dom  ~~>  } ) )
103102imp 430 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  = 
0 )  ->  x  e.  { r  e.  RR  |  seq 0 (  +  ,  ( G `  r ) )  e. 
dom 
~~>  } )
10498, 1032thd 243 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  = 
0 )  ->  (
( ( abs `  x
)  x.  L )  <  1  <->  x  e.  { r  e.  RR  |  seq 0 (  +  , 
( G `  r
) )  e.  dom  ~~>  } ) )
10590, 104sylan2 476 . . . . . . . . . . . . . . . . . . 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 719 . . . . . . . . . . . . . . . . . 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 9604 . . . . . . . . . . . . . . . . . . . . . . 23  |-  RR  C_  CC
108 ssdif 3600 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( RR  C_  CC  ->  ( RR  \  { 0 } ) 
C_  ( CC  \  { 0 } ) )
109107, 108ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( RR 
\  { 0 } )  C_  ( CC  \  { 0 } )
110109sseli 3460 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  ( RR  \  { 0 } )  ->  x  e.  ( CC  \  { 0 } ) )
111 nn0uz 11201 . . . . . . . . . . . . . . . . . . . . . 22  |-  NN0  =  ( ZZ>= `  0 )
1125ad2antrr 730 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  ( ( abs `  x )  x.  L
)  =/=  1 )  ->  M  e.  NN0 )
113 fvex 5892 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( G `
 x )  e. 
_V
114113a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  ( ( abs `  x )  x.  L
)  =/=  1 )  ->  ( G `  x )  e.  _V )
115 eldifi 3587 . . . . . . . . . . . . . . . . . . . . . . . 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 6152 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5976 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  x  e.  CC )  ->  ( G `
 x )  =  ( n  e.  NN0  |->  ( ( A `  n )  x.  (
x ^ n ) ) ) )
120119adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  x  e.  CC )  /\  k  e.  NN0 )  ->  ( G `  x )  =  ( n  e. 
NN0  |->  ( ( A `
 n )  x.  ( x ^ n
) ) ) )
121 fveq2 5882 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( n  =  k  ->  ( A `  n )  =  ( A `  k ) )
122 oveq2 6314 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( n  =  k  ->  (
x ^ n )  =  ( x ^
k ) )
123121, 122oveq12d 6324 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( n  =  k  ->  (
( A `  n
)  x.  ( x ^ n ) )  =  ( ( A `
 k )  x.  ( x ^ k
) ) )
124123adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  x  e.  CC )  /\  k  e.  NN0 )  /\  n  =  k )  ->  ( ( A `  n )  x.  ( x ^ n
) )  =  ( ( A `  k
)  x.  ( x ^ k ) ) )
125 simpr 462 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  x  e.  CC )  /\  k  e.  NN0 )  ->  k  e.  NN0 )
126 ovex 6334 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5971 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  x  e.  CC )  /\  k  e.  NN0 )  ->  (
( G `  x
) `  k )  =  ( ( A `
 k )  x.  ( x ^ k
) ) )
12935adantlr 719 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  x  e.  CC )  /\  k  e.  NN0 )  ->  ( A `  k )  e.  CC )
130 simplr 760 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  x  e.  CC )  /\  k  e.  NN0 )  ->  x  e.  CC )
131130, 125expcld 12423 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  x  e.  CC )  /\  k  e.  NN0 )  ->  (
x ^ k )  e.  CC )
132129, 131mulcld 9671 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  x  e.  CC )  /\  k  e.  NN0 )  ->  (
( A `  k
)  x.  ( x ^ k ) )  e.  CC )
133128, 132eqeltrd 2507 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  x  e.  CC )  /\  k  e.  NN0 )  ->  (
( G `  x
) `  k )  e.  CC )
134115, 133sylanl2 655 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  NN0 )  ->  ( ( G `
 x ) `  k )  e.  CC )
135134adantlr 719 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  x  e.  ( CC  \  { 0 } ) )  /\  ( ( abs `  x )  x.  L )  =/=  1 )  /\  k  e.  NN0 )  ->  (
( G `  x
) `  k )  e.  CC )
13634adantlr 719 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  x  e.  CC )  /\  k  e.  Z )  ->  k  e.  NN0 )
137136, 128syldan 472 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  x  e.  CC )  /\  k  e.  Z )  ->  (
( G `  x
) `  k )  =  ( ( A `
 k )  x.  ( x ^ k
) ) )
138115, 137sylanl2 655 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( ( G `  x ) `  k )  =  ( ( A `  k
)  x.  ( x ^ k ) ) )
13936adantlr 719 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( A `  k )  e.  CC )
140115adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  x  e.  ( CC  \  { 0 } ) )  ->  x  e.  CC )
141140adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  x  e.  CC )
14234adantlr 719 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  k  e.  NN0 )
143141, 142expcld 12423 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( x ^ k )  e.  CC )
14437adantlr 719 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( A `  k )  =/=  0
)
145 eldifsni 4126 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( x  e.  ( CC  \  { 0 } )  ->  x  =/=  0
)
146145ad2antlr 731 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  x  =/=  0 )
147142nn0zd 11046 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  k  e.  ZZ )
148141, 146, 147expne0d 12429 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( x ^ k )  =/=  0 )
149139, 143, 144, 148mulne0d 10272 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( ( A `  k )  x.  ( x ^ k
) )  =/=  0
)
150138, 149eqnetrd 2713 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( ( G `  x ) `  k )  =/=  0
)
151150adantlr 719 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  x  e.  ( CC  \  { 0 } ) )  /\  ( ( abs `  x )  x.  L )  =/=  1 )  /\  k  e.  Z )  ->  (
( G `  x
) `  k )  =/=  0 )
152 oveq1 6313 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( n  =  k  ->  (
n  +  1 )  =  ( k  +  1 ) )
153152fveq2d 5886 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( n  =  k  ->  (
( G `  x
) `  ( n  +  1 ) )  =  ( ( G `
 x ) `  ( k  +  1 ) ) )
154 fveq2 5882 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( n  =  k  ->  (
( G `  x
) `  n )  =  ( ( G `
 x ) `  k ) )
155153, 154oveq12d 6324 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( n  =  k  ->  (
( ( G `  x ) `  (
n  +  1 ) )  /  ( ( G `  x ) `
 n ) )  =  ( ( ( G `  x ) `
 ( k  +  1 ) )  / 
( ( G `  x ) `  k
) ) )
156155fveq2d 5886 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  =  k  ->  ( abs `  ( ( ( G `  x ) `
 ( n  + 
1 ) )  / 
( ( G `  x ) `  n
) ) )  =  ( abs `  (
( ( G `  x ) `  (
k  +  1 ) )  /  ( ( G `  x ) `
 k ) ) ) )
157156cbvmptv 4516 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( n  e.  Z  |->  ( abs `  ( ( ( G `
 x ) `  ( n  +  1
) )  /  (
( G `  x
) `  n )
) ) )  =  ( k  e.  Z  |->  ( abs `  (
( ( G `  x ) `  (
k  +  1 ) )  /  ( ( G `  x ) `
 k ) ) ) )
1584reseq2i 5121 . . . . . . . . . . . . . . . . . . . . . . . . 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 466 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  x  e.  ( CC  \  { 0 } ) )  ->  Z  C_  NN0 )
160159resmptd 5175 . . . . . . . . . . . . . . . . . . . . . . . . 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 2477 . . . . . . . . . . . . . . . . . . . . . . . 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 466 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  x  e.  ( CC  \  { 0 } ) )  ->  M  e.  ZZ )
1638adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  x  e.  ( CC  \  { 0 } ) )  ->  D 
~~>  L )
164140abscld 13498 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  x  e.  ( CC  \  { 0 } ) )  -> 
( abs `  x
)  e.  RR )
165164recnd 9677 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  x  e.  ( CC  \  { 0 } ) )  -> 
( abs `  x
)  e.  CC )
16610mptex 6152 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9677 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  k  e.  Z )  ->  ( D `  k )  e.  CC )
169168adantlr 719 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( D `  k )  e.  CC )
170 eqidd 2423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5892 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5971 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  x  e.  CC )  /\  k  e.  Z )  ->  ( G `  x )  =  ( n  e. 
NN0  |->  ( ( A `
 n )  x.  ( x ^ n
) ) ) )
176 simpr 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ph  /\  x  e.  CC )  /\  k  e.  Z
)  /\  n  =  ( k  +  1 ) )  ->  n  =  ( k  +  1 ) )
177176fveq2d 5886 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ph  /\  x  e.  CC )  /\  k  e.  Z
)  /\  n  =  ( k  +  1 ) )  ->  ( A `  n )  =  ( A `  ( k  +  1 ) ) )
178176oveq2d 6322 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ph  /\  x  e.  CC )  /\  k  e.  Z
)  /\  n  =  ( k  +  1 ) )  ->  (
x ^ n )  =  ( x ^
( k  +  1 ) ) )
179177, 178oveq12d 6324 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 10893 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  1  e.  NN0
181180a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ph  /\  x  e.  CC )  /\  k  e.  Z )  ->  1  e.  NN0 )
182136, 181nn0addcld 10937 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  x  e.  CC )  /\  k  e.  Z )  ->  (
k  +  1 )  e.  NN0 )
183 ovex 6334 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5971 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  x  e.  CC )  /\  k  e.  Z )  ->  (
( G `  x
) `  ( k  +  1 ) )  =  ( ( A `
 ( k  +  1 ) )  x.  ( x ^ (
k  +  1 ) ) ) )
186123adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5971 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  x  e.  CC )  /\  k  e.  Z )  ->  (
( G `  x
) `  k )  =  ( ( A `
 k )  x.  ( x ^ k
) ) )
189185, 188oveq12d 6324 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 655 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 719 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( A `  ( k  +  1 ) )  e.  CC )
192115, 182sylanl2 655 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( k  +  1 )  e. 
NN0 )
193141, 192expcld 12423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( x ^ ( k  +  1 ) )  e.  CC )
194191, 139, 193, 143, 144, 148divmuldivd 10432 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 10935 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  k  e.  CC )
196 1cnd 9667 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  1  e.  CC )
197195, 196pncan2d 9996 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( (
k  +  1 )  -  k )  =  1 )
198197oveq2d 6322 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( x ^ ( ( k  +  1 )  -  k ) )  =  ( x ^ 1 ) )
199192nn0zd 11046 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( k  +  1 )  e.  ZZ )
200141, 146, 147, 199expsubd 12434 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( x ^ ( ( k  +  1 )  -  k ) )  =  ( ( x ^
( k  +  1 ) )  /  (
x ^ k ) ) )
201141exp1d 12418 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( x ^ 1 )  =  x )
202198, 200, 2013eqtr3d 2471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( (
x ^ ( k  +  1 ) )  /  ( x ^
k ) )  =  x )
203202oveq2d 6322 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( (
( G `  x
) `  ( k  +  1 ) )  /  ( ( G `
 x ) `  k ) )  =  ( ( ( A `
 ( k  +  1 ) )  / 
( A `  k
) )  x.  x
) )
205204fveq2d 5886 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 719 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( ( A `  ( k  +  1 ) )  /  ( A `  k ) )  e.  CC )
207206, 141absmuld 13516 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2467 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  k  e.  Z )  ->  ( D `  k )  =  ( abs `  (
( A `  (
k  +  1 ) )  /  ( A `
 k ) ) ) )
210209adantlr 719 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( D `  k )  =  ( abs `  ( ( A `  ( k  +  1 ) )  /  ( A `  k ) ) ) )
211210eqcomd 2430 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( abs `  ( ( A `  ( k  +  1 ) )  /  ( A `  k )
) )  =  ( D `  k ) )
212211oveq1d 6321 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( ( abs `  ( ( A `
 ( k  +  1 ) )  / 
( A `  k
) ) )  x.  ( abs `  x
) )  =  ( ( D `  k
)  x.  ( abs `  x ) ) )
213165adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( abs `  x )  e.  CC )
214169, 213mulcomd 9672 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  k  e.  Z
)  ->  ( ( D `  k )  x.  ( abs `  x
) )  =  ( ( abs `  x
)  x.  ( D `
 k ) ) )
215208, 212, 2143eqtrd 2467 . . . . . . . . . . . . . . . . . . . . . . . . . 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 13700 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  x  e.  ( CC  \  { 0 } ) )  -> 
( n  e.  NN0  |->  ( abs `  ( ( ( G `  x
) `  ( n  +  1 ) )  /  ( ( G `
 x ) `  n ) ) ) )  ~~>  ( ( abs `  x )  x.  L
) )
217 climres 13639 . . . . . . . . . . . . . . . . . . . . . . . . . 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 666 . . . . . . . . . . . . . . . . . . . . . . . . 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 235 . . . . . . . . . . . . . . . . . . . . . . . 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 4446 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  x  e.  ( CC  \  { 0 } ) )  -> 
( n  e.  Z  |->  ( abs `  (
( ( G `  x ) `  (
n  +  1 ) )  /  ( ( G `  x ) `
 n ) ) ) )  ~~>  ( ( abs `  x )  x.  L ) )
221220adantr 466 . . . . . . . . . . . . . . . . . . . . . 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 462 . . . . . . . . . . . . . . . . . . . . . 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 36633 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  x  e.  ( CC  \  {
0 } ) )  /\  ( ( abs `  x )  x.  L
)  =/=  1 )  ->  ( ( ( abs `  x )  x.  L )  <  1  <->  seq 0 (  +  ,  ( G `  x ) )  e. 
dom 
~~>  ) )
224110, 223sylanl2 655 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  x  e.  ( RR  \  {
0 } ) )  /\  ( ( abs `  x )  x.  L
)  =/=  1 )  ->  ( ( ( abs `  x )  x.  L )  <  1  <->  seq 0 (  +  ,  ( G `  x ) )  e. 
dom 
~~>  ) )
225 eldifi 3587 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  ( RR  \  { 0 } )  ->  x  e.  RR )
226 fveq2 5882 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( r  =  x  ->  ( G `  r )  =  ( G `  x ) )
227226seqeq3d 12228 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( r  =  x  ->  seq 0 (  +  , 
( G `  r
) )  =  seq 0 (  +  , 
( G `  x
) ) )
228227eleq1d 2491 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( r  =  x  ->  (  seq 0 (  +  , 
( G `  r
) )  e.  dom  ~~>  <->  seq 0 (  +  , 
( G `  x
) )  e.  dom  ~~>  ) )
229228elrab3 3229 . . . . . . . . . . . . . . . . . . . . . 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 731 . . . . . . . . . . . . . . . . . . . 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 259 . . . . . . . . . . . . . . . . . . 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 811 . . . . . . . . . . . . . . . . . 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 792 . . . . . . . . . . . . . . . . 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 478 . . . . . . . . . . . . . . . 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 811 . . . . . . . . . . . . . . 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 258 . . . . . . . . . . . . . 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 472 . . . . . . . . . . . . 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 295 . . . . . . . . . . . 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 256 . . . . . . . . . . 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 210 . . . . . . . . . 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 441 . . . . . . . . 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 435 . . . . . . 7  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( 1  /  L )  <  ( abs `  x
)  ->  -.  x  e.  { r  e.  RR  |  seq 0 (  +  ,  ( G `  r ) )  e. 
dom 
~~>  } ) )
245244con2d 118 . . . . . 6  |-  ( (
ph  /\  x  e.  RR )  ->  ( x  e.  { r  e.  RR  |  seq 0
(  +  ,  ( G `  r ) )  e.  dom  ~~>  }  ->  -.  ( 1  /  L
)  <  ( abs `  x ) ) )
24647adantr 466 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR )  /\  (
1  /  L )  <  x )  -> 
( 1  /  L
)  e.  RR )
247 simplr 760 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR )  /\  (
1  /  L )  <  x )  ->  x  e.  RR )
24850adantr 466 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR )  /\  (
1  /  L )  <  x )  -> 
( abs `  x
)  e.  RR )
249 simpr 462 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR )  /\  (
1  /  L )  <  x )  -> 
( 1  /  L
)  <  x )
250247leabsd 13477 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR )  /\  (
1  /  L )  <  x )  ->  x  <_  ( abs `  x
) )
251246, 247, 248, 249, 250ltletrd 9803 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR )  /\  (
1  /  L )  <  x )  -> 
( 1  /  L
)  <  ( abs `  x ) )
252251ex 435 . . . . . 6  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( 1  /  L )  <  x  ->  (
1  /  L )  <  ( abs `  x
) ) )
253245, 252nsyld 145 . . . . 5  |-  ( (
ph  /\  x  e.  RR )  ->  ( x  e.  { r  e.  RR  |  seq 0
(  +  ,  ( G `  r ) )  e.  dom  ~~>  }  ->  -.  ( 1  /  L
)  <  x )
)
25446, 253sylan2 476 . . . 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 10054 . . . . . . . . 9  |-  ( ph  -> 
-u ( 1  /  L )  e.  RR )
257256rexrd 9698 . . . . . . . 8  |-  ( ph  -> 
-u ( 1  /  L )  e.  RR* )
258 iooss1 11679 . . . . . . . 8  |-  ( (
-u ( 1  /  L )  e.  RR*  /\  -u ( 1  /  L
)  <_  x )  ->  ( x (,) (
1  /  L ) )  C_  ( -u (
1  /  L ) (,) ( 1  /  L ) ) )
259257, 258sylan 473 . . . . . . 7  |-  ( (
ph  /\  -u ( 1  /  L )  <_  x )  ->  (
x (,) ( 1  /  L ) ) 
C_  ( -u (
1  /  L ) (,) ( 1  /  L ) ) )
260259adantlr 719 . . . . . 6  |-  ( ( ( ph  /\  (
x  e.  RR*  /\  x  <  ( 1  /  L
) ) )  /\  -u ( 1  /  L
)  <_  x )  ->  ( x (,) (
1  /  L ) )  C_  ( -u (
1  /  L ) (,) ( 1  /  L ) ) )
261 eliooord 11702 . . . . . . . . . . 11  |-  ( k  e.  ( x (,) ( 1  /  L
) )  ->  (
x  <  k  /\  k  <  ( 1  /  L ) ) )
262261simpld 460 . . . . . . . . . 10  |-  ( k  e.  ( x (,) ( 1  /  L
) )  ->  x  <  k )
263262rgen 2781 . . . . . . . . 9  |-  A. k  e.  ( x (,) (
1  /  L ) ) x  <  k
264 ioon0 11670 . . . . . . . . . . . . 13  |-  ( ( x  e.  RR*  /\  (
1  /  L )  e.  RR* )  ->  (
( x (,) (
1  /  L ) )  =/=  (/)  <->  x  <  ( 1  /  L ) ) )
26544, 264sylan2 476 . . . . . . . . . . . 12  |-  ( ( x  e.  RR*  /\  ph )  ->  ( ( x (,) ( 1  /  L ) )  =/=  (/) 
<->  x  <  ( 1  /  L ) ) )
266265ancoms 454 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  RR* )  ->  ( (
x (,) ( 1  /  L ) )  =/=  (/)  <->  x  <  ( 1  /  L ) ) )
267266biimpar 487 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR* )  /\  x  <  ( 1  /  L
) )  ->  (
x (,) ( 1  /  L ) )  =/=  (/) )
268 r19.2zb 3889 . . . . . . . . . 10  |-  ( ( x (,) ( 1  /  L ) )  =/=  (/)  <->  ( A. k  e.  ( x (,) (
1  /  L ) ) x  <  k  ->  E. k  e.  ( x (,) ( 1  /  L ) ) x  <  k ) )
269267, 268sylib 199 . . . . . . . . 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 651 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  RR*  /\  x  < 
( 1  /  L
) ) )  ->  E. k  e.  (
x (,) ( 1  /  L ) ) x  <  k )
272271adantr 466 . . . . . 6  |-  ( ( ( ph  /\  (
x  e.  RR*  /\  x  <  ( 1  /  L
) ) )  /\  -u ( 1  /  L
)  <_  x )  ->  E. k  e.  ( x (,) ( 1  /  L ) ) x  <  k )
273 ssrexv 3526 . . . . . 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 760 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR* )  /\  -.  -u ( 1  /  L
)  <_  x )  ->  x  e.  RR* )
276 xrltnle 9709 . . . . . . . . . . . . . . 15  |-  ( ( x  e.  RR*  /\  -u (
1  /  L )  e.  RR* )  ->  (
x  <  -u ( 1  /  L )  <->  -.  -u (
1  /  L )  <_  x ) )
277 xrltle 11456 . . . . . . . . . . . . . . 15  |-  ( ( x  e.  RR*  /\  -u (
1  /  L )  e.  RR* )  ->  (
x  <  -u ( 1  /  L )  ->  x  <_  -u ( 1  /  L ) ) )
278276, 277sylbird 238 . . . . . . . . . . . . . 14  |-  ( ( x  e.  RR*  /\  -u (
1  /  L )  e.  RR* )  ->  ( -.  -u ( 1  /  L )  <_  x  ->  x  <_  -u ( 1  /  L ) ) )
279257, 278sylan2 476 . . . . . . . . . . . . 13  |-  ( ( x  e.  RR*  /\  ph )  ->  ( -.  -u (
1  /  L )  <_  x  ->  x  <_ 
-u ( 1  /  L ) ) )
280279ancoms 454 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  RR* )  ->  ( -.  -u ( 1  /  L
)  <_  x  ->  x  <_  -u ( 1  /  L ) ) )
281280imp 430 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR* )  /\  -.  -u ( 1  /  L
)  <_  x )  ->  x  <_  -u ( 1  /  L ) )
282 iooss1 11679 . . . . . . . . . . 11  |-  ( ( x  e.  RR*  /\  x  <_ 
-u ( 1  /  L ) )  -> 
( -u ( 1  /  L ) (,) (
1  /  L ) )  C_  ( x (,) ( 1  /  L
) ) )
283275, 281, 282syl2anc 665 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR* )  /\  -.  -u ( 1  /  L
)  <_  x )  ->  ( -u ( 1  /  L ) (,) ( 1  /  L
) )  C_  (
x (,) ( 1  /  L ) ) )
284283sselda 3464 . . . . . . . . 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 2836 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR* )  /\  -.  -u ( 1  /  L
)  <_  x )  ->  A. k  e.  (
-u ( 1  /  L ) (,) (
1  /  L ) ) x  <  k
)
28741, 78recgt0d 10549 . . . . . . . . . . . . 13  |-  ( ph  ->  0  <  ( 1  /  L ) )
28843, 43, 287, 287addgt0d 10196 . . . . . . . . . . . 12  |-  ( ph  ->  0  <  ( ( 1  /  L )  +  ( 1  /  L ) ) )
28943recnd 9677 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 1  /  L
)  e.  CC )
290289, 289subnegd 10001 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( 1  /  L )  -  -u (
1  /  L ) )  =  ( ( 1  /  L )  +  ( 1  /  L ) ) )
291288, 290breqtrrd 4450 . . . . . . . . . . 11  |-  ( ph  ->  0  <  ( ( 1  /  L )  -  -u ( 1  /  L ) ) )
292256, 43posdifd 10208 . . . . . . . . . . 11  |-  ( ph  ->  ( -u ( 1  /  L )  < 
( 1  /  L
)  <->  0  <  (
( 1  /  L
)  -  -u (
1  /  L ) ) ) )
293291, 292mpbird 235 . . . . . . . . . 10  |-  ( ph  -> 
-u ( 1  /  L )  <  (
1  /  L ) )
294 ioon0 11670 . . . . . . . . . . 11  |-  ( (
-u ( 1  /  L )  e.  RR*  /\  ( 1  /  L
)  e.  RR* )  ->  ( ( -u (
1  /  L ) (,) ( 1  /  L ) )  =/=  (/) 
<-> 
-u ( 1  /  L )  <  (
1  /  L ) ) )
295257, 44, 294syl2anc 665 . . . . . . . . . 10  |-  ( ph  ->  ( ( -u (
1  /  L ) (,) ( 1  /  L ) )  =/=  (/) 
<-> 
-u ( 1  /  L )  <  (
1  /  L ) ) )
296293, 295mpbird 235 . . . . . . . . 9  |-  ( ph  ->  ( -u ( 1  /  L ) (,) ( 1  /  L
) )  =/=  (/) )
297 r19.2zb 3889 . . . . . . . . 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 199 . . . . . . . 8  |-  ( ph  ->  ( A. k  e.  ( -u ( 1  /  L ) (,) ( 1  /  L
) ) x  < 
k  ->  E. k  e.  ( -u ( 1  /  L ) (,) ( 1  /  L
) ) x  < 
k ) )
299298ad2antrr 730 . . . . . . 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 725 . . . . 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 798 . . . 4  |-  ( (
ph  /\  ( x  e.  RR*  /\  x  < 
( 1  /  L
) ) )  ->  E. k  e.  ( -u ( 1  /  L
) (,) ( 1  /  L ) ) x  <  k )
303 elioo2 11685 . . . . . . . . . . 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 665 . . . . . . . . . 10  |-  ( ph  ->  ( x  e.  (
-u ( 1  /  L ) (,) (
1  /  L ) )  <->  ( x  e.  RR  /\  -u (
1  /  L )  <  x  /\  x  <  ( 1  /  L
) ) ) )
305304biimpa 486 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( -u ( 1  /  L ) (,) (
1  /  L ) ) )  ->  (
x  e.  RR  /\  -u ( 1  /  L
)  <  x  /\  x  <  ( 1  /  L ) ) )
306 simpr 462 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  RR )  ->  x  e.  RR )
307306, 47absltd 13492 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( abs `  x )  <  ( 1  /  L )  <->  ( -u (
1  /  L )  <  x  /\  x  <  ( 1  /  L
) ) ) )
30850adantr 466 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  RR )  /\  ( abs `  x )  < 
( 1  /  L
) )  ->  ( abs `  x )  e.  RR )
309 simpr 462 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  RR )  /\  ( abs `  x )  < 
( 1  /  L
) )  ->  ( abs `  x )  < 
( 1  /  L
) )
310308, 309ltned 9779 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  RR )  /\  ( abs `  x )  < 
( 1  /  L
) )  ->  ( abs `  x )  =/=  ( 1  /  L
) )
311238biimpd 210 . . . . . . . . . . . . . . . . 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 441 . . . . . . . . . . . . . . . 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 435 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( abs `  x )  <  ( 1  /  L )  ->  x  e.  { r  e.  RR  |  seq 0 (  +  ,  ( G `  r ) )  e. 
dom 
~~>  } ) )
315307, 314sylbird 238 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  RR )  ->  ( (
-u ( 1  /  L )  <  x  /\  x  <  ( 1  /  L ) )  ->  x  e.  {
r  e.  RR  |  seq 0 (  +  , 
( G `  r
) )  e.  dom  ~~>  } ) )
316315impr 623 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( x  e.  RR  /\  ( -u ( 1  /  L
)  <  x  /\  x  <  ( 1  /  L ) ) ) )  ->  x  e.  { r  e.  RR  |  seq 0 (  +  , 
( G `  r
) )  e.  dom  ~~>  } )
317316expcom 436 . . . . . . . . . . 11  |-  ( ( x  e.  RR  /\  ( -u ( 1  /  L )  <  x  /\  x  <  ( 1  /  L ) ) )  ->  ( ph  ->  x  e.  { r  e.  RR  |  seq 0 (  +  , 
( G `  r
) )  e.  dom  ~~>  } ) )
3183173impb 1201 . . . . . . . . . 10  |-  ( ( x  e.  RR  /\  -u ( 1  /  L
)  <  x  /\  x  <  ( 1  /  L ) )  -> 
( ph  ->  x  e. 
{ r  e.  RR  |  seq 0 (  +  ,  ( G `  r ) )  e. 
dom 
~~>  } ) )
319318impcom 431 . . . . . . . . 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 472 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( -u ( 1  /  L ) (,) (
1  /  L ) ) )  ->  x  e.  { r  e.  RR  |  seq 0 (  +  ,  ( G `  r ) )  e. 
dom 
~~>  } )
321320ex 435 . . . . . . 7  |-  ( ph  ->  ( x  e.  (
-u ( 1  /  L ) (,) (
1  /  L ) )  ->  x  e.  { r  e.  RR  |  seq 0 (  +  , 
( G `  r
) )  e.  dom  ~~>  } ) )
322321ssrdv 3470 . . . . . 6  |-  ( ph  ->  ( -u ( 1  /  L ) (,) ( 1  /  L
) )  C_  { r  e.  RR  |  seq 0 (  +  , 
( G `  r
) )  e.  dom  ~~>  } )
323 ssrexv 3526 . . . . . 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 466 . . . 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 7981 . 2  |-  ( ph  ->  sup ( { r  e.  RR  |  seq 0 (  +  , 
( G `  r
) )  e.  dom  ~~>  } ,  RR* ,  <  )  =  ( 1  /  L ) )
3281, 327syl5eq 2475 1  |-  ( ph  ->  R  =  ( 1  /  L ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 187    \/ wo 369    /\ wa 370    /\ w3a 982    = wceq 1437    e. wcel 1872    =/= wne 2614   A.wral 2771   E.wrex 2772   {crab 2775   _Vcvv 3080    \ cdif 3433    u. cun 3434    i^i cin 3435    C_ wss 3436   (/)c0 3761   {csn 3998   class class class wbr 4423    |-> cmpt 4482    Or wor 4773   dom cdm 4853    |` cres 4855   -->wf 5597   ` cfv 5601  (class class class)co 6306   supcsup 7964   CCcc 9545   RRcr 9546   0cc0 9547   1c1 9548    + caddc 9550    x. cmul 9552   RR*cxr 9682    < clt 9683    <_ cle 9684    - cmin 9868   -ucneg 9869    / cdiv 10277   NN0cn0 10877   ZZcz 10945   ZZ>=cuz 11167   RR+crp 11310   (,)cioo 11643    seqcseq 12220   ^cexp 12279   abscabs 13298    ~~> cli 13548
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-rep 4536  ax-sep 4546  ax-nul 4555  ax-pow 4602  ax-pr 4660  ax-un 6598  ax-inf2 8156  ax-cnex 9603  ax-resscn 9604  ax-1cn 9605  ax-icn 9606  ax-addcl 9607  ax-addrcl 9608  ax-mulcl 9609  ax-mulrcl 9610  ax-mulcom 9611  ax-addass 9612  ax-mulass 9613  ax-distr 9614  ax-i2m1 9615  ax-1ne0 9616  ax-1rid 9617  ax-rnegex 9618  ax-rrecex 9619  ax-cnre 9620  ax-pre-lttri 9621  ax-pre-lttrn 9622  ax-pre-ltadd 9623  ax-pre-mulgt0 9624  ax-pre-sup 9625  ax-addf 9626  ax-mulf 9627
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-fal 1443  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-nel 2617  df-ral 2776  df-rex 2777  df-reu 2778  df-rmo 2779  df-rab 2780  df-v 3082  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-tp 4003  df-op 4005  df-uni 4220  df-int 4256  df-iun 4301  df-br 4424  df-opab 4483  df-mpt 4484  df-tr 4519  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-se 4813  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-isom 5610  df-riota 6268  df-ov 6309  df-oprab 6310  df-mpt2 6311  df-om 6708  df-1st 6808  df-2nd 6809  df-wrecs 7040  df-recs 7102  df-rdg 7140  df-1o 7194  df-oadd 7198  df-er 7375  df-pm 7487  df-en 7582  df-dom 7583  df-sdom 7584  df-fin 7585  df-sup 7966  df-inf 7967  df-oi 8035  df-card 8382  df-pnf 9685  df-mnf 9686  df-xr 9687  df-ltxr 9688  df-le 9689  df-sub 9870  df-neg 9871  df-div 10278  df-nn 10618  df-2 10676  df-3 10677  df-n0 10878  df-z 10946  df-uz 11168  df-q 11273  df-rp 11311  df-ioo 11647  df-ico 11649  df-fz 11793  df-fzo 11924  df-fl 12035  df-seq 12221  df-exp 12280  df-hash 12523  df-shft 13131  df-cj 13163  df-re 13164  df-im 13165  df-sqrt 13299  df-abs 13300  df-limsup 13526  df-clim 13552  df-rlim 13553  df-sum 13753
This theorem is referenced by:  binomcxplemradcnv  36672
  Copyright terms: Public domain W3C validator