Metamath Proof Explorer

Theorem binomcxplemradcnv

Description: Lemma for binomcxp . By binomcxplemfrat and radcnvrat the radius of convergence of power series sum_ k e. NN0 ( ( Fk ) x. ( b ^ k ) ) is one. (Contributed by Steve Rodriguez, 22-Apr-2020)

Ref Expression
Hypotheses binomcxp.a 
|- ( ph -> A e. RR+ )
binomcxp.b 
|- ( ph -> B e. RR )
binomcxp.lt 
|- ( ph -> ( abs ` B ) < ( abs ` A ) )
binomcxp.c 
|- ( ph -> C e. CC )
binomcxplem.f 
|- F = ( j e. NN0 |-> ( C _Cc j ) )
binomcxplem.s 
|- S = ( b e. CC |-> ( k e. NN0 |-> ( ( F ` k ) x. ( b ^ k ) ) ) )
binomcxplem.r 
|- R = sup ( { r e. RR | seq 0 ( + , ( S ` r ) ) e. dom ~~> } , RR* , < )
Assertion binomcxplemradcnv 
|- ( ( ph /\ -. C e. NN0 ) -> R = 1 )

Proof

Step Hyp Ref Expression
1 binomcxp.a 
 |-  ( ph -> A e. RR+ )
2 binomcxp.b 
 |-  ( ph -> B e. RR )
3 binomcxp.lt 
 |-  ( ph -> ( abs ` B ) < ( abs ` A ) )
4 binomcxp.c 
 |-  ( ph -> C e. CC )
5 binomcxplem.f 
 |-  F = ( j e. NN0 |-> ( C _Cc j ) )
6 binomcxplem.s 
 |-  S = ( b e. CC |-> ( k e. NN0 |-> ( ( F ` k ) x. ( b ^ k ) ) ) )
7 binomcxplem.r 
 |-  R = sup ( { r e. RR | seq 0 ( + , ( S ` r ) ) e. dom ~~> } , RR* , < )
8 simpl 
 |-  ( ( b = x /\ k e. NN0 ) -> b = x )
9 8 oveq1d 
 |-  ( ( b = x /\ k e. NN0 ) -> ( b ^ k ) = ( x ^ k ) )
10 9 oveq2d 
 |-  ( ( b = x /\ k e. NN0 ) -> ( ( F ` k ) x. ( b ^ k ) ) = ( ( F ` k ) x. ( x ^ k ) ) )
11 10 mpteq2dva 
 |-  ( b = x -> ( k e. NN0 |-> ( ( F ` k ) x. ( b ^ k ) ) ) = ( k e. NN0 |-> ( ( F ` k ) x. ( x ^ k ) ) ) )
12 fveq2 
 |-  ( k = y -> ( F ` k ) = ( F ` y ) )
13 oveq2 
 |-  ( k = y -> ( x ^ k ) = ( x ^ y ) )
14 12 13 oveq12d 
 |-  ( k = y -> ( ( F ` k ) x. ( x ^ k ) ) = ( ( F ` y ) x. ( x ^ y ) ) )
15 14 cbvmptv 
 |-  ( k e. NN0 |-> ( ( F ` k ) x. ( x ^ k ) ) ) = ( y e. NN0 |-> ( ( F ` y ) x. ( x ^ y ) ) )
16 11 15 eqtrdi 
 |-  ( b = x -> ( k e. NN0 |-> ( ( F ` k ) x. ( b ^ k ) ) ) = ( y e. NN0 |-> ( ( F ` y ) x. ( x ^ y ) ) ) )
17 16 cbvmptv 
 |-  ( b e. CC |-> ( k e. NN0 |-> ( ( F ` k ) x. ( b ^ k ) ) ) ) = ( x e. CC |-> ( y e. NN0 |-> ( ( F ` y ) x. ( x ^ y ) ) ) )
18 6 17 eqtri 
 |-  S = ( x e. CC |-> ( y e. NN0 |-> ( ( F ` y ) x. ( x ^ y ) ) ) )
19 4 ad2antrr 
 |-  ( ( ( ph /\ -. C e. NN0 ) /\ j e. NN0 ) -> C e. CC )
20 simpr 
 |-  ( ( ( ph /\ -. C e. NN0 ) /\ j e. NN0 ) -> j e. NN0 )
21 19 20 bcccl 
 |-  ( ( ( ph /\ -. C e. NN0 ) /\ j e. NN0 ) -> ( C _Cc j ) e. CC )
22 21 5 fmptd 
 |-  ( ( ph /\ -. C e. NN0 ) -> F : NN0 --> CC )
23 fvoveq1 
 |-  ( k = i -> ( F ` ( k + 1 ) ) = ( F ` ( i + 1 ) ) )
24 fveq2 
 |-  ( k = i -> ( F ` k ) = ( F ` i ) )
25 23 24 oveq12d 
 |-  ( k = i -> ( ( F ` ( k + 1 ) ) / ( F ` k ) ) = ( ( F ` ( i + 1 ) ) / ( F ` i ) ) )
26 25 fveq2d 
 |-  ( k = i -> ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) = ( abs ` ( ( F ` ( i + 1 ) ) / ( F ` i ) ) ) )
27 26 cbvmptv 
 |-  ( k e. NN0 |-> ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) ) = ( i e. NN0 |-> ( abs ` ( ( F ` ( i + 1 ) ) / ( F ` i ) ) ) )
28 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
29 0nn0 
 |-  0 e. NN0
30 29 a1i 
 |-  ( ( ph /\ -. C e. NN0 ) -> 0 e. NN0 )
31 5 a1i 
 |-  ( ( ( ph /\ -. C e. NN0 ) /\ i e. NN0 ) -> F = ( j e. NN0 |-> ( C _Cc j ) ) )
32 simpr 
 |-  ( ( ( ( ph /\ -. C e. NN0 ) /\ i e. NN0 ) /\ j = i ) -> j = i )
33 32 oveq2d 
 |-  ( ( ( ( ph /\ -. C e. NN0 ) /\ i e. NN0 ) /\ j = i ) -> ( C _Cc j ) = ( C _Cc i ) )
34 simpr 
 |-  ( ( ( ph /\ -. C e. NN0 ) /\ i e. NN0 ) -> i e. NN0 )
35 ovexd 
 |-  ( ( ( ph /\ -. C e. NN0 ) /\ i e. NN0 ) -> ( C _Cc i ) e. _V )
36 31 33 34 35 fvmptd 
 |-  ( ( ( ph /\ -. C e. NN0 ) /\ i e. NN0 ) -> ( F ` i ) = ( C _Cc i ) )
37 elfznn0 
 |-  ( C e. ( 0 ... ( i - 1 ) ) -> C e. NN0 )
38 37 con3i 
 |-  ( -. C e. NN0 -> -. C e. ( 0 ... ( i - 1 ) ) )
39 38 ad2antlr 
 |-  ( ( ( ph /\ -. C e. NN0 ) /\ i e. NN0 ) -> -. C e. ( 0 ... ( i - 1 ) ) )
40 4 adantr 
 |-  ( ( ph /\ i e. NN0 ) -> C e. CC )
41 simpr 
 |-  ( ( ph /\ i e. NN0 ) -> i e. NN0 )
42 40 41 bcc0 
 |-  ( ( ph /\ i e. NN0 ) -> ( ( C _Cc i ) = 0 <-> C e. ( 0 ... ( i - 1 ) ) ) )
43 42 necon3abid 
 |-  ( ( ph /\ i e. NN0 ) -> ( ( C _Cc i ) =/= 0 <-> -. C e. ( 0 ... ( i - 1 ) ) ) )
44 43 adantlr 
 |-  ( ( ( ph /\ -. C e. NN0 ) /\ i e. NN0 ) -> ( ( C _Cc i ) =/= 0 <-> -. C e. ( 0 ... ( i - 1 ) ) ) )
45 39 44 mpbird 
 |-  ( ( ( ph /\ -. C e. NN0 ) /\ i e. NN0 ) -> ( C _Cc i ) =/= 0 )
46 36 45 eqnetrd 
 |-  ( ( ( ph /\ -. C e. NN0 ) /\ i e. NN0 ) -> ( F ` i ) =/= 0 )
47 1 2 3 4 5 binomcxplemfrat 
 |-  ( ( ph /\ -. C e. NN0 ) -> ( k e. NN0 |-> ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) ) ~~> 1 )
48 ax-1ne0 
 |-  1 =/= 0
49 48 a1i 
 |-  ( ( ph /\ -. C e. NN0 ) -> 1 =/= 0 )
50 18 22 7 27 28 30 46 47 49 radcnvrat 
 |-  ( ( ph /\ -. C e. NN0 ) -> R = ( 1 / 1 ) )
51 1div1e1 
 |-  ( 1 / 1 ) = 1
52 50 51 eqtrdi 
 |-  ( ( ph /\ -. C e. NN0 ) -> R = 1 )