Metamath Proof Explorer

Theorem dvradcnv2

Description: The radius of convergence of the (formal) derivative H of the power series G is (at least) as large as the radius of convergence of G . This version of dvradcnv uses a shifted version of H to match the sum form of ( CC _D F ) in pserdv2 (and shows how to use uzmptshftfval to shift a maps-to function on a set of upper integers). (Contributed by Steve Rodriguez, 22-Apr-2020)

Ref Expression
Hypotheses dvradcnv2.g 
|- G = ( x e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( x ^ n ) ) ) )
dvradcnv2.r 
|- R = sup ( { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } , RR* , < )
dvradcnv2.h 
|- H = ( n e. NN |-> ( ( n x. ( A ` n ) ) x. ( X ^ ( n - 1 ) ) ) )
dvradcnv2.a 
|- ( ph -> A : NN0 --> CC )
dvradcnv2.x 
|- ( ph -> X e. CC )
dvradcnv2.l 
|- ( ph -> ( abs ` X ) < R )
Assertion dvradcnv2 
|- ( ph -> seq 1 ( + , H ) e. dom ~~> )

Proof

Step Hyp Ref Expression
1 dvradcnv2.g 
 |-  G = ( x e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( x ^ n ) ) ) )
2 dvradcnv2.r 
 |-  R = sup ( { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } , RR* , < )
3 dvradcnv2.h 
 |-  H = ( n e. NN |-> ( ( n x. ( A ` n ) ) x. ( X ^ ( n - 1 ) ) ) )
4 dvradcnv2.a 
 |-  ( ph -> A : NN0 --> CC )
5 dvradcnv2.x 
 |-  ( ph -> X e. CC )
6 dvradcnv2.l 
 |-  ( ph -> ( abs ` X ) < R )
7 0cn 
 |-  0 e. CC
8 ax-1cn 
 |-  1 e. CC
9 7 8 subnegi 
 |-  ( 0 - -u 1 ) = ( 0 + 1 )
10 0p1e1 
 |-  ( 0 + 1 ) = 1
11 9 10 eqtri 
 |-  ( 0 - -u 1 ) = 1
12 seqeq1 
 |-  ( ( 0 - -u 1 ) = 1 -> seq ( 0 - -u 1 ) ( + , H ) = seq 1 ( + , H ) )
13 11 12 ax-mp 
 |-  seq ( 0 - -u 1 ) ( + , H ) = seq 1 ( + , H )
14 ovex 
 |-  ( ( n x. ( A ` n ) ) x. ( X ^ ( n - 1 ) ) ) e. _V
15 id 
 |-  ( n = ( m - -u 1 ) -> n = ( m - -u 1 ) )
16 fveq2 
 |-  ( n = ( m - -u 1 ) -> ( A ` n ) = ( A ` ( m - -u 1 ) ) )
17 15 16 oveq12d 
 |-  ( n = ( m - -u 1 ) -> ( n x. ( A ` n ) ) = ( ( m - -u 1 ) x. ( A ` ( m - -u 1 ) ) ) )
18 oveq1 
 |-  ( n = ( m - -u 1 ) -> ( n - 1 ) = ( ( m - -u 1 ) - 1 ) )
19 18 oveq2d 
 |-  ( n = ( m - -u 1 ) -> ( X ^ ( n - 1 ) ) = ( X ^ ( ( m - -u 1 ) - 1 ) ) )
20 17 19 oveq12d 
 |-  ( n = ( m - -u 1 ) -> ( ( n x. ( A ` n ) ) x. ( X ^ ( n - 1 ) ) ) = ( ( ( m - -u 1 ) x. ( A ` ( m - -u 1 ) ) ) x. ( X ^ ( ( m - -u 1 ) - 1 ) ) ) )
21 nnuz 
 |-  NN = ( ZZ>= ` 1 )
22 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
23 1pneg1e0 
 |-  ( 1 + -u 1 ) = 0
24 23 fveq2i 
 |-  ( ZZ>= ` ( 1 + -u 1 ) ) = ( ZZ>= ` 0 )
25 22 24 eqtr4i 
 |-  NN0 = ( ZZ>= ` ( 1 + -u 1 ) )
26 1zzd 
 |-  ( ph -> 1 e. ZZ )
27 26 znegcld 
 |-  ( ph -> -u 1 e. ZZ )
28 3 14 20 21 25 26 27 uzmptshftfval 
 |-  ( ph -> ( H shift -u 1 ) = ( m e. NN0 |-> ( ( ( m - -u 1 ) x. ( A ` ( m - -u 1 ) ) ) x. ( X ^ ( ( m - -u 1 ) - 1 ) ) ) ) )
29 nn0cn 
 |-  ( m e. NN0 -> m e. CC )
30 29 adantl 
 |-  ( ( ph /\ m e. NN0 ) -> m e. CC )
31 1cnd 
 |-  ( ( ph /\ m e. NN0 ) -> 1 e. CC )
32 30 31 subnegd 
 |-  ( ( ph /\ m e. NN0 ) -> ( m - -u 1 ) = ( m + 1 ) )
33 32 fveq2d 
 |-  ( ( ph /\ m e. NN0 ) -> ( A ` ( m - -u 1 ) ) = ( A ` ( m + 1 ) ) )
34 32 33 oveq12d 
 |-  ( ( ph /\ m e. NN0 ) -> ( ( m - -u 1 ) x. ( A ` ( m - -u 1 ) ) ) = ( ( m + 1 ) x. ( A ` ( m + 1 ) ) ) )
35 32 oveq1d 
 |-  ( ( ph /\ m e. NN0 ) -> ( ( m - -u 1 ) - 1 ) = ( ( m + 1 ) - 1 ) )
36 30 31 pncand 
 |-  ( ( ph /\ m e. NN0 ) -> ( ( m + 1 ) - 1 ) = m )
37 35 36 eqtrd 
 |-  ( ( ph /\ m e. NN0 ) -> ( ( m - -u 1 ) - 1 ) = m )
38 37 oveq2d 
 |-  ( ( ph /\ m e. NN0 ) -> ( X ^ ( ( m - -u 1 ) - 1 ) ) = ( X ^ m ) )
39 34 38 oveq12d 
 |-  ( ( ph /\ m e. NN0 ) -> ( ( ( m - -u 1 ) x. ( A ` ( m - -u 1 ) ) ) x. ( X ^ ( ( m - -u 1 ) - 1 ) ) ) = ( ( ( m + 1 ) x. ( A ` ( m + 1 ) ) ) x. ( X ^ m ) ) )
40 39 mpteq2dva 
 |-  ( ph -> ( m e. NN0 |-> ( ( ( m - -u 1 ) x. ( A ` ( m - -u 1 ) ) ) x. ( X ^ ( ( m - -u 1 ) - 1 ) ) ) ) = ( m e. NN0 |-> ( ( ( m + 1 ) x. ( A ` ( m + 1 ) ) ) x. ( X ^ m ) ) ) )
41 28 40 eqtrd 
 |-  ( ph -> ( H shift -u 1 ) = ( m e. NN0 |-> ( ( ( m + 1 ) x. ( A ` ( m + 1 ) ) ) x. ( X ^ m ) ) ) )
42 41 seqeq3d 
 |-  ( ph -> seq 0 ( + , ( H shift -u 1 ) ) = seq 0 ( + , ( m e. NN0 |-> ( ( ( m + 1 ) x. ( A ` ( m + 1 ) ) ) x. ( X ^ m ) ) ) ) )
43 fveq2 
 |-  ( n = m -> ( A ` n ) = ( A ` m ) )
44 oveq2 
 |-  ( n = m -> ( x ^ n ) = ( x ^ m ) )
45 43 44 oveq12d 
 |-  ( n = m -> ( ( A ` n ) x. ( x ^ n ) ) = ( ( A ` m ) x. ( x ^ m ) ) )
46 45 cbvmptv 
 |-  ( n e. NN0 |-> ( ( A ` n ) x. ( x ^ n ) ) ) = ( m e. NN0 |-> ( ( A ` m ) x. ( x ^ m ) ) )
47 46 mpteq2i 
 |-  ( x e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( x ^ n ) ) ) ) = ( x e. CC |-> ( m e. NN0 |-> ( ( A ` m ) x. ( x ^ m ) ) ) )
48 1 47 eqtri 
 |-  G = ( x e. CC |-> ( m e. NN0 |-> ( ( A ` m ) x. ( x ^ m ) ) ) )
49 eqid 
 |-  ( m e. NN0 |-> ( ( ( m + 1 ) x. ( A ` ( m + 1 ) ) ) x. ( X ^ m ) ) ) = ( m e. NN0 |-> ( ( ( m + 1 ) x. ( A ` ( m + 1 ) ) ) x. ( X ^ m ) ) )
50 48 2 49 4 5 6 dvradcnv 
 |-  ( ph -> seq 0 ( + , ( m e. NN0 |-> ( ( ( m + 1 ) x. ( A ` ( m + 1 ) ) ) x. ( X ^ m ) ) ) ) e. dom ~~> )
51 42 50 eqeltrd 
 |-  ( ph -> seq 0 ( + , ( H shift -u 1 ) ) e. dom ~~> )
52 climdm 
 |-  ( seq 0 ( + , ( H shift -u 1 ) ) e. dom ~~> <-> seq 0 ( + , ( H shift -u 1 ) ) ~~> ( ~~> ` seq 0 ( + , ( H shift -u 1 ) ) ) )
53 51 52 sylib 
 |-  ( ph -> seq 0 ( + , ( H shift -u 1 ) ) ~~> ( ~~> ` seq 0 ( + , ( H shift -u 1 ) ) ) )
54 0z 
 |-  0 e. ZZ
55 neg1z 
 |-  -u 1 e. ZZ
56 nnex 
 |-  NN e. _V
57 56 mptex 
 |-  ( n e. NN |-> ( ( n x. ( A ` n ) ) x. ( X ^ ( n - 1 ) ) ) ) e. _V
58 3 57 eqeltri 
 |-  H e. _V
59 58 seqshft 
 |-  ( ( 0 e. ZZ /\ -u 1 e. ZZ ) -> seq 0 ( + , ( H shift -u 1 ) ) = ( seq ( 0 - -u 1 ) ( + , H ) shift -u 1 ) )
60 54 55 59 mp2an 
 |-  seq 0 ( + , ( H shift -u 1 ) ) = ( seq ( 0 - -u 1 ) ( + , H ) shift -u 1 )
61 60 breq1i 
 |-  ( seq 0 ( + , ( H shift -u 1 ) ) ~~> ( ~~> ` seq 0 ( + , ( H shift -u 1 ) ) ) <-> ( seq ( 0 - -u 1 ) ( + , H ) shift -u 1 ) ~~> ( ~~> ` seq 0 ( + , ( H shift -u 1 ) ) ) )
62 seqex 
 |-  seq ( 0 - -u 1 ) ( + , H ) e. _V
63 climshft 
 |-  ( ( -u 1 e. ZZ /\ seq ( 0 - -u 1 ) ( + , H ) e. _V ) -> ( ( seq ( 0 - -u 1 ) ( + , H ) shift -u 1 ) ~~> ( ~~> ` seq 0 ( + , ( H shift -u 1 ) ) ) <-> seq ( 0 - -u 1 ) ( + , H ) ~~> ( ~~> ` seq 0 ( + , ( H shift -u 1 ) ) ) ) )
64 55 62 63 mp2an 
 |-  ( ( seq ( 0 - -u 1 ) ( + , H ) shift -u 1 ) ~~> ( ~~> ` seq 0 ( + , ( H shift -u 1 ) ) ) <-> seq ( 0 - -u 1 ) ( + , H ) ~~> ( ~~> ` seq 0 ( + , ( H shift -u 1 ) ) ) )
65 61 64 bitri 
 |-  ( seq 0 ( + , ( H shift -u 1 ) ) ~~> ( ~~> ` seq 0 ( + , ( H shift -u 1 ) ) ) <-> seq ( 0 - -u 1 ) ( + , H ) ~~> ( ~~> ` seq 0 ( + , ( H shift -u 1 ) ) ) )
66 fvex 
 |-  ( ~~> ` seq 0 ( + , ( H shift -u 1 ) ) ) e. _V
67 62 66 breldm 
 |-  ( seq ( 0 - -u 1 ) ( + , H ) ~~> ( ~~> ` seq 0 ( + , ( H shift -u 1 ) ) ) -> seq ( 0 - -u 1 ) ( + , H ) e. dom ~~> )
68 65 67 sylbi 
 |-  ( seq 0 ( + , ( H shift -u 1 ) ) ~~> ( ~~> ` seq 0 ( + , ( H shift -u 1 ) ) ) -> seq ( 0 - -u 1 ) ( + , H ) e. dom ~~> )
69 53 68 syl 
 |-  ( ph -> seq ( 0 - -u 1 ) ( + , H ) e. dom ~~> )
70 13 69 eqeltrrid 
 |-  ( ph -> seq 1 ( + , H ) e. dom ~~> )