Metamath Proof Explorer

Theorem dvradcnv

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 . (In fact they are equal, but we don't have as much use for the negative side of this claim.) (Contributed by Mario Carneiro, 31-Mar-2015)

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

Proof

Step Hyp Ref Expression
1 dvradcnv.g 
 |-  G = ( x e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( x ^ n ) ) ) )
2 dvradcnv.r 
 |-  R = sup ( { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } , RR* , < )
3 dvradcnv.h 
 |-  H = ( n e. NN0 |-> ( ( ( n + 1 ) x. ( A ` ( n + 1 ) ) ) x. ( X ^ n ) ) )
4 dvradcnv.a 
 |-  ( ph -> A : NN0 --> CC )
5 dvradcnv.x 
 |-  ( ph -> X e. CC )
6 dvradcnv.l 
 |-  ( ph -> ( abs ` X ) < R )
7 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
8 1nn0 
 |-  1 e. NN0
9 8 a1i 
 |-  ( ph -> 1 e. NN0 )
10 ax-1cn 
 |-  1 e. CC
11 nn0cn 
 |-  ( k e. NN0 -> k e. CC )
12 11 adantl 
 |-  ( ( ph /\ k e. NN0 ) -> k e. CC )
13 nn0ex 
 |-  NN0 e. _V
14 13 mptex 
 |-  ( i e. NN0 |-> ( i x. ( abs ` ( ( G ` X ) ` i ) ) ) ) e. _V
15 14 shftval4 
 |-  ( ( 1 e. CC /\ k e. CC ) -> ( ( ( i e. NN0 |-> ( i x. ( abs ` ( ( G ` X ) ` i ) ) ) ) shift -u 1 ) ` k ) = ( ( i e. NN0 |-> ( i x. ( abs ` ( ( G ` X ) ` i ) ) ) ) ` ( 1 + k ) ) )
16 10 12 15 sylancr 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( ( i e. NN0 |-> ( i x. ( abs ` ( ( G ` X ) ` i ) ) ) ) shift -u 1 ) ` k ) = ( ( i e. NN0 |-> ( i x. ( abs ` ( ( G ` X ) ` i ) ) ) ) ` ( 1 + k ) ) )
17 addcom 
 |-  ( ( 1 e. CC /\ k e. CC ) -> ( 1 + k ) = ( k + 1 ) )
18 10 12 17 sylancr 
 |-  ( ( ph /\ k e. NN0 ) -> ( 1 + k ) = ( k + 1 ) )
19 18 fveq2d 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( i e. NN0 |-> ( i x. ( abs ` ( ( G ` X ) ` i ) ) ) ) ` ( 1 + k ) ) = ( ( i e. NN0 |-> ( i x. ( abs ` ( ( G ` X ) ` i ) ) ) ) ` ( k + 1 ) ) )
20 peano2nn0 
 |-  ( k e. NN0 -> ( k + 1 ) e. NN0 )
21 20 adantl 
 |-  ( ( ph /\ k e. NN0 ) -> ( k + 1 ) e. NN0 )
22 id 
 |-  ( i = ( k + 1 ) -> i = ( k + 1 ) )
23 2fveq3 
 |-  ( i = ( k + 1 ) -> ( abs ` ( ( G ` X ) ` i ) ) = ( abs ` ( ( G ` X ) ` ( k + 1 ) ) ) )
24 22 23 oveq12d 
 |-  ( i = ( k + 1 ) -> ( i x. ( abs ` ( ( G ` X ) ` i ) ) ) = ( ( k + 1 ) x. ( abs ` ( ( G ` X ) ` ( k + 1 ) ) ) ) )
25 eqid 
 |-  ( i e. NN0 |-> ( i x. ( abs ` ( ( G ` X ) ` i ) ) ) ) = ( i e. NN0 |-> ( i x. ( abs ` ( ( G ` X ) ` i ) ) ) )
26 ovex 
 |-  ( ( k + 1 ) x. ( abs ` ( ( G ` X ) ` ( k + 1 ) ) ) ) e. _V
27 24 25 26 fvmpt 
 |-  ( ( k + 1 ) e. NN0 -> ( ( i e. NN0 |-> ( i x. ( abs ` ( ( G ` X ) ` i ) ) ) ) ` ( k + 1 ) ) = ( ( k + 1 ) x. ( abs ` ( ( G ` X ) ` ( k + 1 ) ) ) ) )
28 21 27 syl 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( i e. NN0 |-> ( i x. ( abs ` ( ( G ` X ) ` i ) ) ) ) ` ( k + 1 ) ) = ( ( k + 1 ) x. ( abs ` ( ( G ` X ) ` ( k + 1 ) ) ) ) )
29 1 pserval2 
 |-  ( ( X e. CC /\ ( k + 1 ) e. NN0 ) -> ( ( G ` X ) ` ( k + 1 ) ) = ( ( A ` ( k + 1 ) ) x. ( X ^ ( k + 1 ) ) ) )
30 5 20 29 syl2an 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( G ` X ) ` ( k + 1 ) ) = ( ( A ` ( k + 1 ) ) x. ( X ^ ( k + 1 ) ) ) )
31 30 fveq2d 
 |-  ( ( ph /\ k e. NN0 ) -> ( abs ` ( ( G ` X ) ` ( k + 1 ) ) ) = ( abs ` ( ( A ` ( k + 1 ) ) x. ( X ^ ( k + 1 ) ) ) ) )
32 31 oveq2d 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( k + 1 ) x. ( abs ` ( ( G ` X ) ` ( k + 1 ) ) ) ) = ( ( k + 1 ) x. ( abs ` ( ( A ` ( k + 1 ) ) x. ( X ^ ( k + 1 ) ) ) ) ) )
33 28 32 eqtrd 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( i e. NN0 |-> ( i x. ( abs ` ( ( G ` X ) ` i ) ) ) ) ` ( k + 1 ) ) = ( ( k + 1 ) x. ( abs ` ( ( A ` ( k + 1 ) ) x. ( X ^ ( k + 1 ) ) ) ) ) )
34 16 19 33 3eqtrd 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( ( i e. NN0 |-> ( i x. ( abs ` ( ( G ` X ) ` i ) ) ) ) shift -u 1 ) ` k ) = ( ( k + 1 ) x. ( abs ` ( ( A ` ( k + 1 ) ) x. ( X ^ ( k + 1 ) ) ) ) ) )
35 21 nn0red 
 |-  ( ( ph /\ k e. NN0 ) -> ( k + 1 ) e. RR )
36 ffvelcdm 
 |-  ( ( A : NN0 --> CC /\ ( k + 1 ) e. NN0 ) -> ( A ` ( k + 1 ) ) e. CC )
37 4 20 36 syl2an 
 |-  ( ( ph /\ k e. NN0 ) -> ( A ` ( k + 1 ) ) e. CC )
38 expcl 
 |-  ( ( X e. CC /\ ( k + 1 ) e. NN0 ) -> ( X ^ ( k + 1 ) ) e. CC )
39 5 20 38 syl2an 
 |-  ( ( ph /\ k e. NN0 ) -> ( X ^ ( k + 1 ) ) e. CC )
40 37 39 mulcld 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( A ` ( k + 1 ) ) x. ( X ^ ( k + 1 ) ) ) e. CC )
41 40 abscld 
 |-  ( ( ph /\ k e. NN0 ) -> ( abs ` ( ( A ` ( k + 1 ) ) x. ( X ^ ( k + 1 ) ) ) ) e. RR )
42 35 41 remulcld 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( k + 1 ) x. ( abs ` ( ( A ` ( k + 1 ) ) x. ( X ^ ( k + 1 ) ) ) ) ) e. RR )
43 34 42 eqeltrd 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( ( i e. NN0 |-> ( i x. ( abs ` ( ( G ` X ) ` i ) ) ) ) shift -u 1 ) ` k ) e. RR )
44 oveq1 
 |-  ( n = k -> ( n + 1 ) = ( k + 1 ) )
45 44 fveq2d 
 |-  ( n = k -> ( A ` ( n + 1 ) ) = ( A ` ( k + 1 ) ) )
46 44 45 oveq12d 
 |-  ( n = k -> ( ( n + 1 ) x. ( A ` ( n + 1 ) ) ) = ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) )
47 oveq2 
 |-  ( n = k -> ( X ^ n ) = ( X ^ k ) )
48 46 47 oveq12d 
 |-  ( n = k -> ( ( ( n + 1 ) x. ( A ` ( n + 1 ) ) ) x. ( X ^ n ) ) = ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( X ^ k ) ) )
49 ovex 
 |-  ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( X ^ k ) ) e. _V
50 48 3 49 fvmpt 
 |-  ( k e. NN0 -> ( H ` k ) = ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( X ^ k ) ) )
51 50 adantl 
 |-  ( ( ph /\ k e. NN0 ) -> ( H ` k ) = ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( X ^ k ) ) )
52 21 nn0cnd 
 |-  ( ( ph /\ k e. NN0 ) -> ( k + 1 ) e. CC )
53 52 37 mulcld 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) e. CC )
54 expcl 
 |-  ( ( X e. CC /\ k e. NN0 ) -> ( X ^ k ) e. CC )
55 5 54 sylan 
 |-  ( ( ph /\ k e. NN0 ) -> ( X ^ k ) e. CC )
56 53 55 mulcld 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( X ^ k ) ) e. CC )
57 51 56 eqeltrd 
 |-  ( ( ph /\ k e. NN0 ) -> ( H ` k ) e. CC )
58 id 
 |-  ( i = k -> i = k )
59 2fveq3 
 |-  ( i = k -> ( abs ` ( ( G ` X ) ` i ) ) = ( abs ` ( ( G ` X ) ` k ) ) )
60 58 59 oveq12d 
 |-  ( i = k -> ( i x. ( abs ` ( ( G ` X ) ` i ) ) ) = ( k x. ( abs ` ( ( G ` X ) ` k ) ) ) )
61 60 cbvmptv 
 |-  ( i e. NN0 |-> ( i x. ( abs ` ( ( G ` X ) ` i ) ) ) ) = ( k e. NN0 |-> ( k x. ( abs ` ( ( G ` X ) ` k ) ) ) )
62 1 4 2 5 6 61 radcnvlt1 
 |-  ( ph -> ( seq 0 ( + , ( i e. NN0 |-> ( i x. ( abs ` ( ( G ` X ) ` i ) ) ) ) ) e. dom ~~> /\ seq 0 ( + , ( abs o. ( G ` X ) ) ) e. dom ~~> ) )
63 62 simpld 
 |-  ( ph -> seq 0 ( + , ( i e. NN0 |-> ( i x. ( abs ` ( ( G ` X ) ` i ) ) ) ) ) e. dom ~~> )
64 climdm 
 |-  ( seq 0 ( + , ( i e. NN0 |-> ( i x. ( abs ` ( ( G ` X ) ` i ) ) ) ) ) e. dom ~~> <-> seq 0 ( + , ( i e. NN0 |-> ( i x. ( abs ` ( ( G ` X ) ` i ) ) ) ) ) ~~> ( ~~> ` seq 0 ( + , ( i e. NN0 |-> ( i x. ( abs ` ( ( G ` X ) ` i ) ) ) ) ) ) )
65 63 64 sylib 
 |-  ( ph -> seq 0 ( + , ( i e. NN0 |-> ( i x. ( abs ` ( ( G ` X ) ` i ) ) ) ) ) ~~> ( ~~> ` seq 0 ( + , ( i e. NN0 |-> ( i x. ( abs ` ( ( G ` X ) ` i ) ) ) ) ) ) )
66 0z 
 |-  0 e. ZZ
67 neg1z 
 |-  -u 1 e. ZZ
68 14 isershft 
 |-  ( ( 0 e. ZZ /\ -u 1 e. ZZ ) -> ( seq 0 ( + , ( i e. NN0 |-> ( i x. ( abs ` ( ( G ` X ) ` i ) ) ) ) ) ~~> ( ~~> ` seq 0 ( + , ( i e. NN0 |-> ( i x. ( abs ` ( ( G ` X ) ` i ) ) ) ) ) ) <-> seq ( 0 + -u 1 ) ( + , ( ( i e. NN0 |-> ( i x. ( abs ` ( ( G ` X ) ` i ) ) ) ) shift -u 1 ) ) ~~> ( ~~> ` seq 0 ( + , ( i e. NN0 |-> ( i x. ( abs ` ( ( G ` X ) ` i ) ) ) ) ) ) ) )
69 66 67 68 mp2an 
 |-  ( seq 0 ( + , ( i e. NN0 |-> ( i x. ( abs ` ( ( G ` X ) ` i ) ) ) ) ) ~~> ( ~~> ` seq 0 ( + , ( i e. NN0 |-> ( i x. ( abs ` ( ( G ` X ) ` i ) ) ) ) ) ) <-> seq ( 0 + -u 1 ) ( + , ( ( i e. NN0 |-> ( i x. ( abs ` ( ( G ` X ) ` i ) ) ) ) shift -u 1 ) ) ~~> ( ~~> ` seq 0 ( + , ( i e. NN0 |-> ( i x. ( abs ` ( ( G ` X ) ` i ) ) ) ) ) ) )
70 65 69 sylib 
 |-  ( ph -> seq ( 0 + -u 1 ) ( + , ( ( i e. NN0 |-> ( i x. ( abs ` ( ( G ` X ) ` i ) ) ) ) shift -u 1 ) ) ~~> ( ~~> ` seq 0 ( + , ( i e. NN0 |-> ( i x. ( abs ` ( ( G ` X ) ` i ) ) ) ) ) ) )
71 seqex 
 |-  seq ( 0 + -u 1 ) ( + , ( ( i e. NN0 |-> ( i x. ( abs ` ( ( G ` X ) ` i ) ) ) ) shift -u 1 ) ) e. _V
72 fvex 
 |-  ( ~~> ` seq 0 ( + , ( i e. NN0 |-> ( i x. ( abs ` ( ( G ` X ) ` i ) ) ) ) ) ) e. _V
73 71 72 breldm 
 |-  ( seq ( 0 + -u 1 ) ( + , ( ( i e. NN0 |-> ( i x. ( abs ` ( ( G ` X ) ` i ) ) ) ) shift -u 1 ) ) ~~> ( ~~> ` seq 0 ( + , ( i e. NN0 |-> ( i x. ( abs ` ( ( G ` X ) ` i ) ) ) ) ) ) -> seq ( 0 + -u 1 ) ( + , ( ( i e. NN0 |-> ( i x. ( abs ` ( ( G ` X ) ` i ) ) ) ) shift -u 1 ) ) e. dom ~~> )
74 70 73 syl 
 |-  ( ph -> seq ( 0 + -u 1 ) ( + , ( ( i e. NN0 |-> ( i x. ( abs ` ( ( G ` X ) ` i ) ) ) ) shift -u 1 ) ) e. dom ~~> )
75 eqid 
 |-  ( ZZ>= ` ( 0 + -u 1 ) ) = ( ZZ>= ` ( 0 + -u 1 ) )
76 neg1cn 
 |-  -u 1 e. CC
77 76 addlidi 
 |-  ( 0 + -u 1 ) = -u 1
78 0le1 
 |-  0 <_ 1
79 1re 
 |-  1 e. RR
80 le0neg2 
 |-  ( 1 e. RR -> ( 0 <_ 1 <-> -u 1 <_ 0 ) )
81 79 80 ax-mp 
 |-  ( 0 <_ 1 <-> -u 1 <_ 0 )
82 78 81 mpbi 
 |-  -u 1 <_ 0
83 77 82 eqbrtri 
 |-  ( 0 + -u 1 ) <_ 0
84 77 67 eqeltri 
 |-  ( 0 + -u 1 ) e. ZZ
85 84 eluz1i 
 |-  ( 0 e. ( ZZ>= ` ( 0 + -u 1 ) ) <-> ( 0 e. ZZ /\ ( 0 + -u 1 ) <_ 0 ) )
86 66 83 85 mpbir2an 
 |-  0 e. ( ZZ>= ` ( 0 + -u 1 ) )
87 86 a1i 
 |-  ( ph -> 0 e. ( ZZ>= ` ( 0 + -u 1 ) ) )
88 eluzelcn 
 |-  ( k e. ( ZZ>= ` ( 0 + -u 1 ) ) -> k e. CC )
89 88 adantl 
 |-  ( ( ph /\ k e. ( ZZ>= ` ( 0 + -u 1 ) ) ) -> k e. CC )
90 10 89 15 sylancr 
 |-  ( ( ph /\ k e. ( ZZ>= ` ( 0 + -u 1 ) ) ) -> ( ( ( i e. NN0 |-> ( i x. ( abs ` ( ( G ` X ) ` i ) ) ) ) shift -u 1 ) ` k ) = ( ( i e. NN0 |-> ( i x. ( abs ` ( ( G ` X ) ` i ) ) ) ) ` ( 1 + k ) ) )
91 nn0re 
 |-  ( i e. NN0 -> i e. RR )
92 91 adantl 
 |-  ( ( ph /\ i e. NN0 ) -> i e. RR )
93 1 4 5 psergf 
 |-  ( ph -> ( G ` X ) : NN0 --> CC )
94 93 ffvelcdmda 
 |-  ( ( ph /\ i e. NN0 ) -> ( ( G ` X ) ` i ) e. CC )
95 94 abscld 
 |-  ( ( ph /\ i e. NN0 ) -> ( abs ` ( ( G ` X ) ` i ) ) e. RR )
96 92 95 remulcld 
 |-  ( ( ph /\ i e. NN0 ) -> ( i x. ( abs ` ( ( G ` X ) ` i ) ) ) e. RR )
97 96 recnd 
 |-  ( ( ph /\ i e. NN0 ) -> ( i x. ( abs ` ( ( G ` X ) ` i ) ) ) e. CC )
98 97 fmpttd 
 |-  ( ph -> ( i e. NN0 |-> ( i x. ( abs ` ( ( G ` X ) ` i ) ) ) ) : NN0 --> CC )
99 10 88 17 sylancr 
 |-  ( k e. ( ZZ>= ` ( 0 + -u 1 ) ) -> ( 1 + k ) = ( k + 1 ) )
100 eluzp1p1 
 |-  ( k e. ( ZZ>= ` ( 0 + -u 1 ) ) -> ( k + 1 ) e. ( ZZ>= ` ( ( 0 + -u 1 ) + 1 ) ) )
101 77 oveq1i 
 |-  ( ( 0 + -u 1 ) + 1 ) = ( -u 1 + 1 )
102 1pneg1e0 
 |-  ( 1 + -u 1 ) = 0
103 10 76 102 addcomli 
 |-  ( -u 1 + 1 ) = 0
104 101 103 eqtri 
 |-  ( ( 0 + -u 1 ) + 1 ) = 0
105 104 fveq2i 
 |-  ( ZZ>= ` ( ( 0 + -u 1 ) + 1 ) ) = ( ZZ>= ` 0 )
106 7 105 eqtr4i 
 |-  NN0 = ( ZZ>= ` ( ( 0 + -u 1 ) + 1 ) )
107 100 106 eleqtrrdi 
 |-  ( k e. ( ZZ>= ` ( 0 + -u 1 ) ) -> ( k + 1 ) e. NN0 )
108 99 107 eqeltrd 
 |-  ( k e. ( ZZ>= ` ( 0 + -u 1 ) ) -> ( 1 + k ) e. NN0 )
109 ffvelcdm 
 |-  ( ( ( i e. NN0 |-> ( i x. ( abs ` ( ( G ` X ) ` i ) ) ) ) : NN0 --> CC /\ ( 1 + k ) e. NN0 ) -> ( ( i e. NN0 |-> ( i x. ( abs ` ( ( G ` X ) ` i ) ) ) ) ` ( 1 + k ) ) e. CC )
110 98 108 109 syl2an 
 |-  ( ( ph /\ k e. ( ZZ>= ` ( 0 + -u 1 ) ) ) -> ( ( i e. NN0 |-> ( i x. ( abs ` ( ( G ` X ) ` i ) ) ) ) ` ( 1 + k ) ) e. CC )
111 90 110 eqeltrd 
 |-  ( ( ph /\ k e. ( ZZ>= ` ( 0 + -u 1 ) ) ) -> ( ( ( i e. NN0 |-> ( i x. ( abs ` ( ( G ` X ) ` i ) ) ) ) shift -u 1 ) ` k ) e. CC )
112 75 87 111 iserex 
 |-  ( ph -> ( seq ( 0 + -u 1 ) ( + , ( ( i e. NN0 |-> ( i x. ( abs ` ( ( G ` X ) ` i ) ) ) ) shift -u 1 ) ) e. dom ~~> <-> seq 0 ( + , ( ( i e. NN0 |-> ( i x. ( abs ` ( ( G ` X ) ` i ) ) ) ) shift -u 1 ) ) e. dom ~~> ) )
113 74 112 mpbid 
 |-  ( ph -> seq 0 ( + , ( ( i e. NN0 |-> ( i x. ( abs ` ( ( G ` X ) ` i ) ) ) ) shift -u 1 ) ) e. dom ~~> )
114 1red 
 |-  ( ( ph /\ X = 0 ) -> 1 e. RR )
115 neqne 
 |-  ( -. X = 0 -> X =/= 0 )
116 absrpcl 
 |-  ( ( X e. CC /\ X =/= 0 ) -> ( abs ` X ) e. RR+ )
117 5 115 116 syl2an 
 |-  ( ( ph /\ -. X = 0 ) -> ( abs ` X ) e. RR+ )
118 117 rprecred 
 |-  ( ( ph /\ -. X = 0 ) -> ( 1 / ( abs ` X ) ) e. RR )
119 114 118 ifclda 
 |-  ( ph -> if ( X = 0 , 1 , ( 1 / ( abs ` X ) ) ) e. RR )
120 oveq1 
 |-  ( 1 = if ( X = 0 , 1 , ( 1 / ( abs ` X ) ) ) -> ( 1 x. ( ( k + 1 ) x. ( abs ` ( ( A ` ( k + 1 ) ) x. ( X ^ ( k + 1 ) ) ) ) ) ) = ( if ( X = 0 , 1 , ( 1 / ( abs ` X ) ) ) x. ( ( k + 1 ) x. ( abs ` ( ( A ` ( k + 1 ) ) x. ( X ^ ( k + 1 ) ) ) ) ) ) )
121 120 breq2d 
 |-  ( 1 = if ( X = 0 , 1 , ( 1 / ( abs ` X ) ) ) -> ( ( abs ` ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( X ^ k ) ) ) <_ ( 1 x. ( ( k + 1 ) x. ( abs ` ( ( A ` ( k + 1 ) ) x. ( X ^ ( k + 1 ) ) ) ) ) ) <-> ( abs ` ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( X ^ k ) ) ) <_ ( if ( X = 0 , 1 , ( 1 / ( abs ` X ) ) ) x. ( ( k + 1 ) x. ( abs ` ( ( A ` ( k + 1 ) ) x. ( X ^ ( k + 1 ) ) ) ) ) ) ) )
122 oveq1 
 |-  ( ( 1 / ( abs ` X ) ) = if ( X = 0 , 1 , ( 1 / ( abs ` X ) ) ) -> ( ( 1 / ( abs ` X ) ) x. ( ( k + 1 ) x. ( abs ` ( ( A ` ( k + 1 ) ) x. ( X ^ ( k + 1 ) ) ) ) ) ) = ( if ( X = 0 , 1 , ( 1 / ( abs ` X ) ) ) x. ( ( k + 1 ) x. ( abs ` ( ( A ` ( k + 1 ) ) x. ( X ^ ( k + 1 ) ) ) ) ) ) )
123 122 breq2d 
 |-  ( ( 1 / ( abs ` X ) ) = if ( X = 0 , 1 , ( 1 / ( abs ` X ) ) ) -> ( ( abs ` ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( X ^ k ) ) ) <_ ( ( 1 / ( abs ` X ) ) x. ( ( k + 1 ) x. ( abs ` ( ( A ` ( k + 1 ) ) x. ( X ^ ( k + 1 ) ) ) ) ) ) <-> ( abs ` ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( X ^ k ) ) ) <_ ( if ( X = 0 , 1 , ( 1 / ( abs ` X ) ) ) x. ( ( k + 1 ) x. ( abs ` ( ( A ` ( k + 1 ) ) x. ( X ^ ( k + 1 ) ) ) ) ) ) ) )
124 elnnuz 
 |-  ( k e. NN <-> k e. ( ZZ>= ` 1 ) )
125 nnnn0 
 |-  ( k e. NN -> k e. NN0 )
126 124 125 sylbir 
 |-  ( k e. ( ZZ>= ` 1 ) -> k e. NN0 )
127 21 nn0ge0d 
 |-  ( ( ph /\ k e. NN0 ) -> 0 <_ ( k + 1 ) )
128 40 absge0d 
 |-  ( ( ph /\ k e. NN0 ) -> 0 <_ ( abs ` ( ( A ` ( k + 1 ) ) x. ( X ^ ( k + 1 ) ) ) ) )
129 35 41 127 128 mulge0d 
 |-  ( ( ph /\ k e. NN0 ) -> 0 <_ ( ( k + 1 ) x. ( abs ` ( ( A ` ( k + 1 ) ) x. ( X ^ ( k + 1 ) ) ) ) ) )
130 126 129 sylan2 
 |-  ( ( ph /\ k e. ( ZZ>= ` 1 ) ) -> 0 <_ ( ( k + 1 ) x. ( abs ` ( ( A ` ( k + 1 ) ) x. ( X ^ ( k + 1 ) ) ) ) ) )
131 130 adantr 
 |-  ( ( ( ph /\ k e. ( ZZ>= ` 1 ) ) /\ X = 0 ) -> 0 <_ ( ( k + 1 ) x. ( abs ` ( ( A ` ( k + 1 ) ) x. ( X ^ ( k + 1 ) ) ) ) ) )
132 oveq1 
 |-  ( X = 0 -> ( X ^ k ) = ( 0 ^ k ) )
133 124 bilanri 
 |-  ( ( ph /\ k e. ( ZZ>= ` 1 ) ) -> k e. NN )
134 133 0expd 
 |-  ( ( ph /\ k e. ( ZZ>= ` 1 ) ) -> ( 0 ^ k ) = 0 )
135 132 134 sylan9eqr 
 |-  ( ( ( ph /\ k e. ( ZZ>= ` 1 ) ) /\ X = 0 ) -> ( X ^ k ) = 0 )
136 135 oveq2d 
 |-  ( ( ( ph /\ k e. ( ZZ>= ` 1 ) ) /\ X = 0 ) -> ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( X ^ k ) ) = ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. 0 ) )
137 53 mul01d 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. 0 ) = 0 )
138 126 137 sylan2 
 |-  ( ( ph /\ k e. ( ZZ>= ` 1 ) ) -> ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. 0 ) = 0 )
139 138 adantr 
 |-  ( ( ( ph /\ k e. ( ZZ>= ` 1 ) ) /\ X = 0 ) -> ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. 0 ) = 0 )
140 136 139 eqtrd 
 |-  ( ( ( ph /\ k e. ( ZZ>= ` 1 ) ) /\ X = 0 ) -> ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( X ^ k ) ) = 0 )
141 140 abs00bd 
 |-  ( ( ( ph /\ k e. ( ZZ>= ` 1 ) ) /\ X = 0 ) -> ( abs ` ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( X ^ k ) ) ) = 0 )
142 42 recnd 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( k + 1 ) x. ( abs ` ( ( A ` ( k + 1 ) ) x. ( X ^ ( k + 1 ) ) ) ) ) e. CC )
143 142 mullidd 
 |-  ( ( ph /\ k e. NN0 ) -> ( 1 x. ( ( k + 1 ) x. ( abs ` ( ( A ` ( k + 1 ) ) x. ( X ^ ( k + 1 ) ) ) ) ) ) = ( ( k + 1 ) x. ( abs ` ( ( A ` ( k + 1 ) ) x. ( X ^ ( k + 1 ) ) ) ) ) )
144 126 143 sylan2 
 |-  ( ( ph /\ k e. ( ZZ>= ` 1 ) ) -> ( 1 x. ( ( k + 1 ) x. ( abs ` ( ( A ` ( k + 1 ) ) x. ( X ^ ( k + 1 ) ) ) ) ) ) = ( ( k + 1 ) x. ( abs ` ( ( A ` ( k + 1 ) ) x. ( X ^ ( k + 1 ) ) ) ) ) )
145 144 adantr 
 |-  ( ( ( ph /\ k e. ( ZZ>= ` 1 ) ) /\ X = 0 ) -> ( 1 x. ( ( k + 1 ) x. ( abs ` ( ( A ` ( k + 1 ) ) x. ( X ^ ( k + 1 ) ) ) ) ) ) = ( ( k + 1 ) x. ( abs ` ( ( A ` ( k + 1 ) ) x. ( X ^ ( k + 1 ) ) ) ) ) )
146 131 141 145 3brtr4d 
 |-  ( ( ( ph /\ k e. ( ZZ>= ` 1 ) ) /\ X = 0 ) -> ( abs ` ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( X ^ k ) ) ) <_ ( 1 x. ( ( k + 1 ) x. ( abs ` ( ( A ` ( k + 1 ) ) x. ( X ^ ( k + 1 ) ) ) ) ) ) )
147 df-ne 
 |-  ( X =/= 0 <-> -. X = 0 )
148 56 abscld 
 |-  ( ( ph /\ k e. NN0 ) -> ( abs ` ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( X ^ k ) ) ) e. RR )
149 52 37 55 mulassd 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( X ^ k ) ) = ( ( k + 1 ) x. ( ( A ` ( k + 1 ) ) x. ( X ^ k ) ) ) )
150 149 fveq2d 
 |-  ( ( ph /\ k e. NN0 ) -> ( abs ` ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( X ^ k ) ) ) = ( abs ` ( ( k + 1 ) x. ( ( A ` ( k + 1 ) ) x. ( X ^ k ) ) ) ) )
151 37 55 mulcld 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( A ` ( k + 1 ) ) x. ( X ^ k ) ) e. CC )
152 52 151 absmuld 
 |-  ( ( ph /\ k e. NN0 ) -> ( abs ` ( ( k + 1 ) x. ( ( A ` ( k + 1 ) ) x. ( X ^ k ) ) ) ) = ( ( abs ` ( k + 1 ) ) x. ( abs ` ( ( A ` ( k + 1 ) ) x. ( X ^ k ) ) ) ) )
153 35 127 absidd 
 |-  ( ( ph /\ k e. NN0 ) -> ( abs ` ( k + 1 ) ) = ( k + 1 ) )
154 153 oveq1d 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( abs ` ( k + 1 ) ) x. ( abs ` ( ( A ` ( k + 1 ) ) x. ( X ^ k ) ) ) ) = ( ( k + 1 ) x. ( abs ` ( ( A ` ( k + 1 ) ) x. ( X ^ k ) ) ) ) )
155 150 152 154 3eqtrd 
 |-  ( ( ph /\ k e. NN0 ) -> ( abs ` ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( X ^ k ) ) ) = ( ( k + 1 ) x. ( abs ` ( ( A ` ( k + 1 ) ) x. ( X ^ k ) ) ) ) )
156 148 155 eqled 
 |-  ( ( ph /\ k e. NN0 ) -> ( abs ` ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( X ^ k ) ) ) <_ ( ( k + 1 ) x. ( abs ` ( ( A ` ( k + 1 ) ) x. ( X ^ k ) ) ) ) )
157 156 adantr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ X =/= 0 ) -> ( abs ` ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( X ^ k ) ) ) <_ ( ( k + 1 ) x. ( abs ` ( ( A ` ( k + 1 ) ) x. ( X ^ k ) ) ) ) )
158 5 adantr 
 |-  ( ( ph /\ k e. NN0 ) -> X e. CC )
159 116 rpreccld 
 |-  ( ( X e. CC /\ X =/= 0 ) -> ( 1 / ( abs ` X ) ) e. RR+ )
160 158 159 sylan 
 |-  ( ( ( ph /\ k e. NN0 ) /\ X =/= 0 ) -> ( 1 / ( abs ` X ) ) e. RR+ )
161 160 rpcnd 
 |-  ( ( ( ph /\ k e. NN0 ) /\ X =/= 0 ) -> ( 1 / ( abs ` X ) ) e. CC )
162 52 adantr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ X =/= 0 ) -> ( k + 1 ) e. CC )
163 41 adantr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ X =/= 0 ) -> ( abs ` ( ( A ` ( k + 1 ) ) x. ( X ^ ( k + 1 ) ) ) ) e. RR )
164 163 recnd 
 |-  ( ( ( ph /\ k e. NN0 ) /\ X =/= 0 ) -> ( abs ` ( ( A ` ( k + 1 ) ) x. ( X ^ ( k + 1 ) ) ) ) e. CC )
165 161 162 164 mul12d 
 |-  ( ( ( ph /\ k e. NN0 ) /\ X =/= 0 ) -> ( ( 1 / ( abs ` X ) ) x. ( ( k + 1 ) x. ( abs ` ( ( A ` ( k + 1 ) ) x. ( X ^ ( k + 1 ) ) ) ) ) ) = ( ( k + 1 ) x. ( ( 1 / ( abs ` X ) ) x. ( abs ` ( ( A ` ( k + 1 ) ) x. ( X ^ ( k + 1 ) ) ) ) ) ) )
166 40 adantr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ X =/= 0 ) -> ( ( A ` ( k + 1 ) ) x. ( X ^ ( k + 1 ) ) ) e. CC )
167 5 ad2antrr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ X =/= 0 ) -> X e. CC )
168 simpr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ X =/= 0 ) -> X =/= 0 )
169 166 167 168 absdivd 
 |-  ( ( ( ph /\ k e. NN0 ) /\ X =/= 0 ) -> ( abs ` ( ( ( A ` ( k + 1 ) ) x. ( X ^ ( k + 1 ) ) ) / X ) ) = ( ( abs ` ( ( A ` ( k + 1 ) ) x. ( X ^ ( k + 1 ) ) ) ) / ( abs ` X ) ) )
170 37 adantr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ X =/= 0 ) -> ( A ` ( k + 1 ) ) e. CC )
171 39 adantr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ X =/= 0 ) -> ( X ^ ( k + 1 ) ) e. CC )
172 170 171 167 168 divassd 
 |-  ( ( ( ph /\ k e. NN0 ) /\ X =/= 0 ) -> ( ( ( A ` ( k + 1 ) ) x. ( X ^ ( k + 1 ) ) ) / X ) = ( ( A ` ( k + 1 ) ) x. ( ( X ^ ( k + 1 ) ) / X ) ) )
173 12 adantr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ X =/= 0 ) -> k e. CC )
174 pncan 
 |-  ( ( k e. CC /\ 1 e. CC ) -> ( ( k + 1 ) - 1 ) = k )
175 173 10 174 sylancl 
 |-  ( ( ( ph /\ k e. NN0 ) /\ X =/= 0 ) -> ( ( k + 1 ) - 1 ) = k )
176 175 oveq2d 
 |-  ( ( ( ph /\ k e. NN0 ) /\ X =/= 0 ) -> ( X ^ ( ( k + 1 ) - 1 ) ) = ( X ^ k ) )
177 21 nn0zd 
 |-  ( ( ph /\ k e. NN0 ) -> ( k + 1 ) e. ZZ )
178 177 adantr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ X =/= 0 ) -> ( k + 1 ) e. ZZ )
179 167 168 178 expm1d 
 |-  ( ( ( ph /\ k e. NN0 ) /\ X =/= 0 ) -> ( X ^ ( ( k + 1 ) - 1 ) ) = ( ( X ^ ( k + 1 ) ) / X ) )
180 176 179 eqtr3d 
 |-  ( ( ( ph /\ k e. NN0 ) /\ X =/= 0 ) -> ( X ^ k ) = ( ( X ^ ( k + 1 ) ) / X ) )
181 180 oveq2d 
 |-  ( ( ( ph /\ k e. NN0 ) /\ X =/= 0 ) -> ( ( A ` ( k + 1 ) ) x. ( X ^ k ) ) = ( ( A ` ( k + 1 ) ) x. ( ( X ^ ( k + 1 ) ) / X ) ) )
182 172 181 eqtr4d 
 |-  ( ( ( ph /\ k e. NN0 ) /\ X =/= 0 ) -> ( ( ( A ` ( k + 1 ) ) x. ( X ^ ( k + 1 ) ) ) / X ) = ( ( A ` ( k + 1 ) ) x. ( X ^ k ) ) )
183 182 fveq2d 
 |-  ( ( ( ph /\ k e. NN0 ) /\ X =/= 0 ) -> ( abs ` ( ( ( A ` ( k + 1 ) ) x. ( X ^ ( k + 1 ) ) ) / X ) ) = ( abs ` ( ( A ` ( k + 1 ) ) x. ( X ^ k ) ) ) )
184 5 abscld 
 |-  ( ph -> ( abs ` X ) e. RR )
185 184 ad2antrr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ X =/= 0 ) -> ( abs ` X ) e. RR )
186 185 recnd 
 |-  ( ( ( ph /\ k e. NN0 ) /\ X =/= 0 ) -> ( abs ` X ) e. CC )
187 158 116 sylan 
 |-  ( ( ( ph /\ k e. NN0 ) /\ X =/= 0 ) -> ( abs ` X ) e. RR+ )
188 187 rpne0d 
 |-  ( ( ( ph /\ k e. NN0 ) /\ X =/= 0 ) -> ( abs ` X ) =/= 0 )
189 164 186 188 divrec2d 
 |-  ( ( ( ph /\ k e. NN0 ) /\ X =/= 0 ) -> ( ( abs ` ( ( A ` ( k + 1 ) ) x. ( X ^ ( k + 1 ) ) ) ) / ( abs ` X ) ) = ( ( 1 / ( abs ` X ) ) x. ( abs ` ( ( A ` ( k + 1 ) ) x. ( X ^ ( k + 1 ) ) ) ) ) )
190 169 183 189 3eqtr3rd 
 |-  ( ( ( ph /\ k e. NN0 ) /\ X =/= 0 ) -> ( ( 1 / ( abs ` X ) ) x. ( abs ` ( ( A ` ( k + 1 ) ) x. ( X ^ ( k + 1 ) ) ) ) ) = ( abs ` ( ( A ` ( k + 1 ) ) x. ( X ^ k ) ) ) )
191 190 oveq2d 
 |-  ( ( ( ph /\ k e. NN0 ) /\ X =/= 0 ) -> ( ( k + 1 ) x. ( ( 1 / ( abs ` X ) ) x. ( abs ` ( ( A ` ( k + 1 ) ) x. ( X ^ ( k + 1 ) ) ) ) ) ) = ( ( k + 1 ) x. ( abs ` ( ( A ` ( k + 1 ) ) x. ( X ^ k ) ) ) ) )
192 165 191 eqtrd 
 |-  ( ( ( ph /\ k e. NN0 ) /\ X =/= 0 ) -> ( ( 1 / ( abs ` X ) ) x. ( ( k + 1 ) x. ( abs ` ( ( A ` ( k + 1 ) ) x. ( X ^ ( k + 1 ) ) ) ) ) ) = ( ( k + 1 ) x. ( abs ` ( ( A ` ( k + 1 ) ) x. ( X ^ k ) ) ) ) )
193 157 192 breqtrrd 
 |-  ( ( ( ph /\ k e. NN0 ) /\ X =/= 0 ) -> ( abs ` ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( X ^ k ) ) ) <_ ( ( 1 / ( abs ` X ) ) x. ( ( k + 1 ) x. ( abs ` ( ( A ` ( k + 1 ) ) x. ( X ^ ( k + 1 ) ) ) ) ) ) )
194 126 193 sylanl2 
 |-  ( ( ( ph /\ k e. ( ZZ>= ` 1 ) ) /\ X =/= 0 ) -> ( abs ` ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( X ^ k ) ) ) <_ ( ( 1 / ( abs ` X ) ) x. ( ( k + 1 ) x. ( abs ` ( ( A ` ( k + 1 ) ) x. ( X ^ ( k + 1 ) ) ) ) ) ) )
195 147 194 sylan2br 
 |-  ( ( ( ph /\ k e. ( ZZ>= ` 1 ) ) /\ -. X = 0 ) -> ( abs ` ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( X ^ k ) ) ) <_ ( ( 1 / ( abs ` X ) ) x. ( ( k + 1 ) x. ( abs ` ( ( A ` ( k + 1 ) ) x. ( X ^ ( k + 1 ) ) ) ) ) ) )
196 121 123 146 195 ifbothda 
 |-  ( ( ph /\ k e. ( ZZ>= ` 1 ) ) -> ( abs ` ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( X ^ k ) ) ) <_ ( if ( X = 0 , 1 , ( 1 / ( abs ` X ) ) ) x. ( ( k + 1 ) x. ( abs ` ( ( A ` ( k + 1 ) ) x. ( X ^ ( k + 1 ) ) ) ) ) ) )
197 51 fveq2d 
 |-  ( ( ph /\ k e. NN0 ) -> ( abs ` ( H ` k ) ) = ( abs ` ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( X ^ k ) ) ) )
198 126 197 sylan2 
 |-  ( ( ph /\ k e. ( ZZ>= ` 1 ) ) -> ( abs ` ( H ` k ) ) = ( abs ` ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( X ^ k ) ) ) )
199 34 oveq2d 
 |-  ( ( ph /\ k e. NN0 ) -> ( if ( X = 0 , 1 , ( 1 / ( abs ` X ) ) ) x. ( ( ( i e. NN0 |-> ( i x. ( abs ` ( ( G ` X ) ` i ) ) ) ) shift -u 1 ) ` k ) ) = ( if ( X = 0 , 1 , ( 1 / ( abs ` X ) ) ) x. ( ( k + 1 ) x. ( abs ` ( ( A ` ( k + 1 ) ) x. ( X ^ ( k + 1 ) ) ) ) ) ) )
200 126 199 sylan2 
 |-  ( ( ph /\ k e. ( ZZ>= ` 1 ) ) -> ( if ( X = 0 , 1 , ( 1 / ( abs ` X ) ) ) x. ( ( ( i e. NN0 |-> ( i x. ( abs ` ( ( G ` X ) ` i ) ) ) ) shift -u 1 ) ` k ) ) = ( if ( X = 0 , 1 , ( 1 / ( abs ` X ) ) ) x. ( ( k + 1 ) x. ( abs ` ( ( A ` ( k + 1 ) ) x. ( X ^ ( k + 1 ) ) ) ) ) ) )
201 196 198 200 3brtr4d 
 |-  ( ( ph /\ k e. ( ZZ>= ` 1 ) ) -> ( abs ` ( H ` k ) ) <_ ( if ( X = 0 , 1 , ( 1 / ( abs ` X ) ) ) x. ( ( ( i e. NN0 |-> ( i x. ( abs ` ( ( G ` X ) ` i ) ) ) ) shift -u 1 ) ` k ) ) )
202 7 9 43 57 113 119 201 cvgcmpce 
 |-  ( ph -> seq 0 ( + , H ) e. dom ~~> )