Metamath Proof Explorer

Theorem binomcxplemcvg

Description: Lemma for binomcxp . The sum in binomcxplemnn0 and its derivative (see the next theorem, binomcxplemdvsum ) converge, as long as their base J is within the disk of convergence. Part of remark "This convergence allows us to apply term-by-term differentiation..." in the Wikibooks proof. (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* , < )
binomcxplem.e 
|- E = ( b e. CC |-> ( k e. NN |-> ( ( k x. ( F ` k ) ) x. ( b ^ ( k - 1 ) ) ) ) )
binomcxplem.d 
|- D = ( `' abs " ( 0 [,) R ) )
Assertion binomcxplemcvg 
|- ( ( ph /\ J e. D ) -> ( seq 0 ( + , ( S ` J ) ) e. dom ~~> /\ seq 1 ( + , ( E ` J ) ) e. dom ~~> ) )

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 binomcxplem.e 
 |-  E = ( b e. CC |-> ( k e. NN |-> ( ( k x. ( F ` k ) ) x. ( b ^ ( k - 1 ) ) ) ) )
9 binomcxplem.d 
 |-  D = ( `' abs " ( 0 [,) R ) )
10 4 adantr 
 |-  ( ( ph /\ j e. NN0 ) -> C e. CC )
11 simpr 
 |-  ( ( ph /\ j e. NN0 ) -> j e. NN0 )
12 10 11 bcccl 
 |-  ( ( ph /\ j e. NN0 ) -> ( C _Cc j ) e. CC )
13 12 5 fmptd 
 |-  ( ph -> F : NN0 --> CC )
14 13 adantr 
 |-  ( ( ph /\ J e. D ) -> F : NN0 --> CC )
15 9 eleq2i 
 |-  ( J e. D <-> J e. ( `' abs " ( 0 [,) R ) ) )
16 absf 
 |-  abs : CC --> RR
17 ffn 
 |-  ( abs : CC --> RR -> abs Fn CC )
18 elpreima 
 |-  ( abs Fn CC -> ( J e. ( `' abs " ( 0 [,) R ) ) <-> ( J e. CC /\ ( abs ` J ) e. ( 0 [,) R ) ) ) )
19 16 17 18 mp2b 
 |-  ( J e. ( `' abs " ( 0 [,) R ) ) <-> ( J e. CC /\ ( abs ` J ) e. ( 0 [,) R ) ) )
20 15 19 bitri 
 |-  ( J e. D <-> ( J e. CC /\ ( abs ` J ) e. ( 0 [,) R ) ) )
21 20 simplbi 
 |-  ( J e. D -> J e. CC )
22 21 adantl 
 |-  ( ( ph /\ J e. D ) -> J e. CC )
23 20 simprbi 
 |-  ( J e. D -> ( abs ` J ) e. ( 0 [,) R ) )
24 0re 
 |-  0 e. RR
25 ssrab2 
 |-  { r e. RR | seq 0 ( + , ( S ` r ) ) e. dom ~~> } C_ RR
26 ressxr 
 |-  RR C_ RR*
27 25 26 sstri 
 |-  { r e. RR | seq 0 ( + , ( S ` r ) ) e. dom ~~> } C_ RR*
28 supxrcl 
 |-  ( { r e. RR | seq 0 ( + , ( S ` r ) ) e. dom ~~> } C_ RR* -> sup ( { r e. RR | seq 0 ( + , ( S ` r ) ) e. dom ~~> } , RR* , < ) e. RR* )
29 27 28 ax-mp 
 |-  sup ( { r e. RR | seq 0 ( + , ( S ` r ) ) e. dom ~~> } , RR* , < ) e. RR*
30 7 29 eqeltri 
 |-  R e. RR*
31 elico2 
 |-  ( ( 0 e. RR /\ R e. RR* ) -> ( ( abs ` J ) e. ( 0 [,) R ) <-> ( ( abs ` J ) e. RR /\ 0 <_ ( abs ` J ) /\ ( abs ` J ) < R ) ) )
32 24 30 31 mp2an 
 |-  ( ( abs ` J ) e. ( 0 [,) R ) <-> ( ( abs ` J ) e. RR /\ 0 <_ ( abs ` J ) /\ ( abs ` J ) < R ) )
33 32 simp3bi 
 |-  ( ( abs ` J ) e. ( 0 [,) R ) -> ( abs ` J ) < R )
34 23 33 syl 
 |-  ( J e. D -> ( abs ` J ) < R )
35 34 adantl 
 |-  ( ( ph /\ J e. D ) -> ( abs ` J ) < R )
36 6 14 7 22 35 radcnvlt2 
 |-  ( ( ph /\ J e. D ) -> seq 0 ( + , ( S ` J ) ) e. dom ~~> )
37 8 a1i 
 |-  ( ( ph /\ J e. CC ) -> E = ( b e. CC |-> ( k e. NN |-> ( ( k x. ( F ` k ) ) x. ( b ^ ( k - 1 ) ) ) ) ) )
38 simplr 
 |-  ( ( ( ( ph /\ J e. CC ) /\ b = J ) /\ k e. NN ) -> b = J )
39 38 oveq1d 
 |-  ( ( ( ( ph /\ J e. CC ) /\ b = J ) /\ k e. NN ) -> ( b ^ ( k - 1 ) ) = ( J ^ ( k - 1 ) ) )
40 39 oveq2d 
 |-  ( ( ( ( ph /\ J e. CC ) /\ b = J ) /\ k e. NN ) -> ( ( k x. ( F ` k ) ) x. ( b ^ ( k - 1 ) ) ) = ( ( k x. ( F ` k ) ) x. ( J ^ ( k - 1 ) ) ) )
41 40 mpteq2dva 
 |-  ( ( ( ph /\ J e. CC ) /\ b = J ) -> ( k e. NN |-> ( ( k x. ( F ` k ) ) x. ( b ^ ( k - 1 ) ) ) ) = ( k e. NN |-> ( ( k x. ( F ` k ) ) x. ( J ^ ( k - 1 ) ) ) ) )
42 simpr 
 |-  ( ( ph /\ J e. CC ) -> J e. CC )
43 nnex 
 |-  NN e. _V
44 43 mptex 
 |-  ( k e. NN |-> ( ( k x. ( F ` k ) ) x. ( J ^ ( k - 1 ) ) ) ) e. _V
45 44 a1i 
 |-  ( ( ph /\ J e. CC ) -> ( k e. NN |-> ( ( k x. ( F ` k ) ) x. ( J ^ ( k - 1 ) ) ) ) e. _V )
46 37 41 42 45 fvmptd 
 |-  ( ( ph /\ J e. CC ) -> ( E ` J ) = ( k e. NN |-> ( ( k x. ( F ` k ) ) x. ( J ^ ( k - 1 ) ) ) ) )
47 21 46 sylan2 
 |-  ( ( ph /\ J e. D ) -> ( E ` J ) = ( k e. NN |-> ( ( k x. ( F ` k ) ) x. ( J ^ ( k - 1 ) ) ) ) )
48 47 seqeq3d 
 |-  ( ( ph /\ J e. D ) -> seq 1 ( + , ( E ` J ) ) = seq 1 ( + , ( k e. NN |-> ( ( k x. ( F ` k ) ) x. ( J ^ ( k - 1 ) ) ) ) ) )
49 eqid 
 |-  ( k e. NN |-> ( ( k x. ( F ` k ) ) x. ( J ^ ( k - 1 ) ) ) ) = ( k e. NN |-> ( ( k x. ( F ` k ) ) x. ( J ^ ( k - 1 ) ) ) )
50 6 7 49 14 22 35 dvradcnv2 
 |-  ( ( ph /\ J e. D ) -> seq 1 ( + , ( k e. NN |-> ( ( k x. ( F ` k ) ) x. ( J ^ ( k - 1 ) ) ) ) ) e. dom ~~> )
51 48 50 eqeltrd 
 |-  ( ( ph /\ J e. D ) -> seq 1 ( + , ( E ` J ) ) e. dom ~~> )
52 36 51 jca 
 |-  ( ( ph /\ J e. D ) -> ( seq 0 ( + , ( S ` J ) ) e. dom ~~> /\ seq 1 ( + , ( E ` J ) ) e. dom ~~> ) )