Metamath Proof Explorer

Theorem radcnvlem1

Description: Lemma for radcnvlt1 , radcnvle . If X is a point closer to zero than Y and the power series converges at Y , then it converges absolutely at X , even if the terms in the sequence are multiplied by n . (Contributed by Mario Carneiro, 31-Mar-2015)

Ref Expression
Hypotheses pser.g 
|- G = ( x e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( x ^ n ) ) ) )
radcnv.a 
|- ( ph -> A : NN0 --> CC )
psergf.x 
|- ( ph -> X e. CC )
radcnvlem2.y 
|- ( ph -> Y e. CC )
radcnvlem2.a 
|- ( ph -> ( abs ` X ) < ( abs ` Y ) )
radcnvlem2.c 
|- ( ph -> seq 0 ( + , ( G ` Y ) ) e. dom ~~> )
radcnvlem1.h 
|- H = ( m e. NN0 |-> ( m x. ( abs ` ( ( G ` X ) ` m ) ) ) )
Assertion radcnvlem1 
|- ( ph -> seq 0 ( + , H ) e. dom ~~> )

Proof

Step Hyp Ref Expression
1 pser.g 
 |-  G = ( x e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( x ^ n ) ) ) )
2 radcnv.a 
 |-  ( ph -> A : NN0 --> CC )
3 psergf.x 
 |-  ( ph -> X e. CC )
4 radcnvlem2.y 
 |-  ( ph -> Y e. CC )
5 radcnvlem2.a 
 |-  ( ph -> ( abs ` X ) < ( abs ` Y ) )
6 radcnvlem2.c 
 |-  ( ph -> seq 0 ( + , ( G ` Y ) ) e. dom ~~> )
7 radcnvlem1.h 
 |-  H = ( m e. NN0 |-> ( m x. ( abs ` ( ( G ` X ) ` m ) ) ) )
8 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
9 0zd 
 |-  ( ph -> 0 e. ZZ )
10 1rp 
 |-  1 e. RR+
11 10 a1i 
 |-  ( ph -> 1 e. RR+ )
12 1 pserval2 
 |-  ( ( Y e. CC /\ k e. NN0 ) -> ( ( G ` Y ) ` k ) = ( ( A ` k ) x. ( Y ^ k ) ) )
13 4 12 sylan 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( G ` Y ) ` k ) = ( ( A ` k ) x. ( Y ^ k ) ) )
14 fvexd 
 |-  ( ph -> ( G ` Y ) e. _V )
15 1 2 4 psergf 
 |-  ( ph -> ( G ` Y ) : NN0 --> CC )
16 15 ffvelrnda 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( G ` Y ) ` k ) e. CC )
17 8 9 14 6 16 serf0 
 |-  ( ph -> ( G ` Y ) ~~> 0 )
18 8 9 11 13 17 climi0 
 |-  ( ph -> E. j e. NN0 A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 )
19 simprl 
 |-  ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) -> j e. NN0 )
20 nn0re 
 |-  ( i e. NN0 -> i e. RR )
21 20 adantl 
 |-  ( ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) /\ i e. NN0 ) -> i e. RR )
22 3 adantr 
 |-  ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) -> X e. CC )
23 22 abscld 
 |-  ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) -> ( abs ` X ) e. RR )
24 4 adantr 
 |-  ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) -> Y e. CC )
25 24 abscld 
 |-  ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) -> ( abs ` Y ) e. RR )
26 0red 
 |-  ( ph -> 0 e. RR )
27 3 abscld 
 |-  ( ph -> ( abs ` X ) e. RR )
28 4 abscld 
 |-  ( ph -> ( abs ` Y ) e. RR )
29 3 absge0d 
 |-  ( ph -> 0 <_ ( abs ` X ) )
30 26 27 28 29 5 lelttrd 
 |-  ( ph -> 0 < ( abs ` Y ) )
31 30 gt0ne0d 
 |-  ( ph -> ( abs ` Y ) =/= 0 )
32 31 adantr 
 |-  ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) -> ( abs ` Y ) =/= 0 )
33 23 25 32 redivcld 
 |-  ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) -> ( ( abs ` X ) / ( abs ` Y ) ) e. RR )
34 reexpcl 
 |-  ( ( ( ( abs ` X ) / ( abs ` Y ) ) e. RR /\ i e. NN0 ) -> ( ( ( abs ` X ) / ( abs ` Y ) ) ^ i ) e. RR )
35 33 34 sylan 
 |-  ( ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) /\ i e. NN0 ) -> ( ( ( abs ` X ) / ( abs ` Y ) ) ^ i ) e. RR )
36 21 35 remulcld 
 |-  ( ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) /\ i e. NN0 ) -> ( i x. ( ( ( abs ` X ) / ( abs ` Y ) ) ^ i ) ) e. RR )
37 eqid 
 |-  ( i e. NN0 |-> ( i x. ( ( ( abs ` X ) / ( abs ` Y ) ) ^ i ) ) ) = ( i e. NN0 |-> ( i x. ( ( ( abs ` X ) / ( abs ` Y ) ) ^ i ) ) )
38 36 37 fmptd 
 |-  ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) -> ( i e. NN0 |-> ( i x. ( ( ( abs ` X ) / ( abs ` Y ) ) ^ i ) ) ) : NN0 --> RR )
39 38 ffvelrnda 
 |-  ( ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) /\ m e. NN0 ) -> ( ( i e. NN0 |-> ( i x. ( ( ( abs ` X ) / ( abs ` Y ) ) ^ i ) ) ) ` m ) e. RR )
40 nn0re 
 |-  ( m e. NN0 -> m e. RR )
41 40 adantl 
 |-  ( ( ph /\ m e. NN0 ) -> m e. RR )
42 1 2 3 psergf 
 |-  ( ph -> ( G ` X ) : NN0 --> CC )
43 42 ffvelrnda 
 |-  ( ( ph /\ m e. NN0 ) -> ( ( G ` X ) ` m ) e. CC )
44 43 abscld 
 |-  ( ( ph /\ m e. NN0 ) -> ( abs ` ( ( G ` X ) ` m ) ) e. RR )
45 41 44 remulcld 
 |-  ( ( ph /\ m e. NN0 ) -> ( m x. ( abs ` ( ( G ` X ) ` m ) ) ) e. RR )
46 45 7 fmptd 
 |-  ( ph -> H : NN0 --> RR )
47 46 adantr 
 |-  ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) -> H : NN0 --> RR )
48 47 ffvelrnda 
 |-  ( ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) /\ m e. NN0 ) -> ( H ` m ) e. RR )
49 48 recnd 
 |-  ( ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) /\ m e. NN0 ) -> ( H ` m ) e. CC )
50 27 28 31 redivcld 
 |-  ( ph -> ( ( abs ` X ) / ( abs ` Y ) ) e. RR )
51 50 recnd 
 |-  ( ph -> ( ( abs ` X ) / ( abs ` Y ) ) e. CC )
52 divge0 
 |-  ( ( ( ( abs ` X ) e. RR /\ 0 <_ ( abs ` X ) ) /\ ( ( abs ` Y ) e. RR /\ 0 < ( abs ` Y ) ) ) -> 0 <_ ( ( abs ` X ) / ( abs ` Y ) ) )
53 27 29 28 30 52 syl22anc 
 |-  ( ph -> 0 <_ ( ( abs ` X ) / ( abs ` Y ) ) )
54 50 53 absidd 
 |-  ( ph -> ( abs ` ( ( abs ` X ) / ( abs ` Y ) ) ) = ( ( abs ` X ) / ( abs ` Y ) ) )
55 28 recnd 
 |-  ( ph -> ( abs ` Y ) e. CC )
56 55 mulid1d 
 |-  ( ph -> ( ( abs ` Y ) x. 1 ) = ( abs ` Y ) )
57 5 56 breqtrrd 
 |-  ( ph -> ( abs ` X ) < ( ( abs ` Y ) x. 1 ) )
58 1red 
 |-  ( ph -> 1 e. RR )
59 ltdivmul 
 |-  ( ( ( abs ` X ) e. RR /\ 1 e. RR /\ ( ( abs ` Y ) e. RR /\ 0 < ( abs ` Y ) ) ) -> ( ( ( abs ` X ) / ( abs ` Y ) ) < 1 <-> ( abs ` X ) < ( ( abs ` Y ) x. 1 ) ) )
60 27 58 28 30 59 syl112anc 
 |-  ( ph -> ( ( ( abs ` X ) / ( abs ` Y ) ) < 1 <-> ( abs ` X ) < ( ( abs ` Y ) x. 1 ) ) )
61 57 60 mpbird 
 |-  ( ph -> ( ( abs ` X ) / ( abs ` Y ) ) < 1 )
62 54 61 eqbrtrd 
 |-  ( ph -> ( abs ` ( ( abs ` X ) / ( abs ` Y ) ) ) < 1 )
63 37 geomulcvg 
 |-  ( ( ( ( abs ` X ) / ( abs ` Y ) ) e. CC /\ ( abs ` ( ( abs ` X ) / ( abs ` Y ) ) ) < 1 ) -> seq 0 ( + , ( i e. NN0 |-> ( i x. ( ( ( abs ` X ) / ( abs ` Y ) ) ^ i ) ) ) ) e. dom ~~> )
64 51 62 63 syl2anc 
 |-  ( ph -> seq 0 ( + , ( i e. NN0 |-> ( i x. ( ( ( abs ` X ) / ( abs ` Y ) ) ^ i ) ) ) ) e. dom ~~> )
65 64 adantr 
 |-  ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) -> seq 0 ( + , ( i e. NN0 |-> ( i x. ( ( ( abs ` X ) / ( abs ` Y ) ) ^ i ) ) ) ) e. dom ~~> )
66 1red 
 |-  ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) -> 1 e. RR )
67 42 ad2antrr 
 |-  ( ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) /\ m e. ( ZZ>= ` j ) ) -> ( G ` X ) : NN0 --> CC )
68 eluznn0 
 |-  ( ( j e. NN0 /\ m e. ( ZZ>= ` j ) ) -> m e. NN0 )
69 19 68 sylan 
 |-  ( ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) /\ m e. ( ZZ>= ` j ) ) -> m e. NN0 )
70 67 69 ffvelrnd 
 |-  ( ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) /\ m e. ( ZZ>= ` j ) ) -> ( ( G ` X ) ` m ) e. CC )
71 70 abscld 
 |-  ( ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) /\ m e. ( ZZ>= ` j ) ) -> ( abs ` ( ( G ` X ) ` m ) ) e. RR )
72 33 adantr 
 |-  ( ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) /\ m e. ( ZZ>= ` j ) ) -> ( ( abs ` X ) / ( abs ` Y ) ) e. RR )
73 72 69 reexpcld 
 |-  ( ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) /\ m e. ( ZZ>= ` j ) ) -> ( ( ( abs ` X ) / ( abs ` Y ) ) ^ m ) e. RR )
74 69 nn0red 
 |-  ( ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) /\ m e. ( ZZ>= ` j ) ) -> m e. RR )
75 69 nn0ge0d 
 |-  ( ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) /\ m e. ( ZZ>= ` j ) ) -> 0 <_ m )
76 2 ad2antrr 
 |-  ( ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) /\ m e. ( ZZ>= ` j ) ) -> A : NN0 --> CC )
77 76 69 ffvelrnd 
 |-  ( ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) /\ m e. ( ZZ>= ` j ) ) -> ( A ` m ) e. CC )
78 4 ad2antrr 
 |-  ( ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) /\ m e. ( ZZ>= ` j ) ) -> Y e. CC )
79 78 69 expcld 
 |-  ( ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) /\ m e. ( ZZ>= ` j ) ) -> ( Y ^ m ) e. CC )
80 77 79 mulcld 
 |-  ( ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) /\ m e. ( ZZ>= ` j ) ) -> ( ( A ` m ) x. ( Y ^ m ) ) e. CC )
81 80 abscld 
 |-  ( ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) /\ m e. ( ZZ>= ` j ) ) -> ( abs ` ( ( A ` m ) x. ( Y ^ m ) ) ) e. RR )
82 1red 
 |-  ( ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) /\ m e. ( ZZ>= ` j ) ) -> 1 e. RR )
83 3 ad2antrr 
 |-  ( ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) /\ m e. ( ZZ>= ` j ) ) -> X e. CC )
84 83 abscld 
 |-  ( ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) /\ m e. ( ZZ>= ` j ) ) -> ( abs ` X ) e. RR )
85 84 69 reexpcld 
 |-  ( ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) /\ m e. ( ZZ>= ` j ) ) -> ( ( abs ` X ) ^ m ) e. RR )
86 83 absge0d 
 |-  ( ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) /\ m e. ( ZZ>= ` j ) ) -> 0 <_ ( abs ` X ) )
87 84 69 86 expge0d 
 |-  ( ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) /\ m e. ( ZZ>= ` j ) ) -> 0 <_ ( ( abs ` X ) ^ m ) )
88 simprr 
 |-  ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) -> A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 )
89 fveq2 
 |-  ( k = m -> ( A ` k ) = ( A ` m ) )
90 oveq2 
 |-  ( k = m -> ( Y ^ k ) = ( Y ^ m ) )
91 89 90 oveq12d 
 |-  ( k = m -> ( ( A ` k ) x. ( Y ^ k ) ) = ( ( A ` m ) x. ( Y ^ m ) ) )
92 91 fveq2d 
 |-  ( k = m -> ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) = ( abs ` ( ( A ` m ) x. ( Y ^ m ) ) ) )
93 92 breq1d 
 |-  ( k = m -> ( ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 <-> ( abs ` ( ( A ` m ) x. ( Y ^ m ) ) ) < 1 ) )
94 93 rspccva 
 |-  ( ( A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 /\ m e. ( ZZ>= ` j ) ) -> ( abs ` ( ( A ` m ) x. ( Y ^ m ) ) ) < 1 )
95 88 94 sylan 
 |-  ( ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) /\ m e. ( ZZ>= ` j ) ) -> ( abs ` ( ( A ` m ) x. ( Y ^ m ) ) ) < 1 )
96 1re 
 |-  1 e. RR
97 ltle 
 |-  ( ( ( abs ` ( ( A ` m ) x. ( Y ^ m ) ) ) e. RR /\ 1 e. RR ) -> ( ( abs ` ( ( A ` m ) x. ( Y ^ m ) ) ) < 1 -> ( abs ` ( ( A ` m ) x. ( Y ^ m ) ) ) <_ 1 ) )
98 81 96 97 sylancl 
 |-  ( ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) /\ m e. ( ZZ>= ` j ) ) -> ( ( abs ` ( ( A ` m ) x. ( Y ^ m ) ) ) < 1 -> ( abs ` ( ( A ` m ) x. ( Y ^ m ) ) ) <_ 1 ) )
99 95 98 mpd 
 |-  ( ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) /\ m e. ( ZZ>= ` j ) ) -> ( abs ` ( ( A ` m ) x. ( Y ^ m ) ) ) <_ 1 )
100 81 82 85 87 99 lemul1ad 
 |-  ( ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) /\ m e. ( ZZ>= ` j ) ) -> ( ( abs ` ( ( A ` m ) x. ( Y ^ m ) ) ) x. ( ( abs ` X ) ^ m ) ) <_ ( 1 x. ( ( abs ` X ) ^ m ) ) )
101 83 69 expcld 
 |-  ( ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) /\ m e. ( ZZ>= ` j ) ) -> ( X ^ m ) e. CC )
102 77 101 mulcld 
 |-  ( ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) /\ m e. ( ZZ>= ` j ) ) -> ( ( A ` m ) x. ( X ^ m ) ) e. CC )
103 102 79 absmuld 
 |-  ( ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) /\ m e. ( ZZ>= ` j ) ) -> ( abs ` ( ( ( A ` m ) x. ( X ^ m ) ) x. ( Y ^ m ) ) ) = ( ( abs ` ( ( A ` m ) x. ( X ^ m ) ) ) x. ( abs ` ( Y ^ m ) ) ) )
104 80 101 absmuld 
 |-  ( ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) /\ m e. ( ZZ>= ` j ) ) -> ( abs ` ( ( ( A ` m ) x. ( Y ^ m ) ) x. ( X ^ m ) ) ) = ( ( abs ` ( ( A ` m ) x. ( Y ^ m ) ) ) x. ( abs ` ( X ^ m ) ) ) )
105 77 79 101 mul32d 
 |-  ( ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) /\ m e. ( ZZ>= ` j ) ) -> ( ( ( A ` m ) x. ( Y ^ m ) ) x. ( X ^ m ) ) = ( ( ( A ` m ) x. ( X ^ m ) ) x. ( Y ^ m ) ) )
106 105 fveq2d 
 |-  ( ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) /\ m e. ( ZZ>= ` j ) ) -> ( abs ` ( ( ( A ` m ) x. ( Y ^ m ) ) x. ( X ^ m ) ) ) = ( abs ` ( ( ( A ` m ) x. ( X ^ m ) ) x. ( Y ^ m ) ) ) )
107 83 69 absexpd 
 |-  ( ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) /\ m e. ( ZZ>= ` j ) ) -> ( abs ` ( X ^ m ) ) = ( ( abs ` X ) ^ m ) )
108 107 oveq2d 
 |-  ( ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) /\ m e. ( ZZ>= ` j ) ) -> ( ( abs ` ( ( A ` m ) x. ( Y ^ m ) ) ) x. ( abs ` ( X ^ m ) ) ) = ( ( abs ` ( ( A ` m ) x. ( Y ^ m ) ) ) x. ( ( abs ` X ) ^ m ) ) )
109 104 106 108 3eqtr3d 
 |-  ( ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) /\ m e. ( ZZ>= ` j ) ) -> ( abs ` ( ( ( A ` m ) x. ( X ^ m ) ) x. ( Y ^ m ) ) ) = ( ( abs ` ( ( A ` m ) x. ( Y ^ m ) ) ) x. ( ( abs ` X ) ^ m ) ) )
110 78 69 absexpd 
 |-  ( ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) /\ m e. ( ZZ>= ` j ) ) -> ( abs ` ( Y ^ m ) ) = ( ( abs ` Y ) ^ m ) )
111 110 oveq2d 
 |-  ( ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) /\ m e. ( ZZ>= ` j ) ) -> ( ( abs ` ( ( A ` m ) x. ( X ^ m ) ) ) x. ( abs ` ( Y ^ m ) ) ) = ( ( abs ` ( ( A ` m ) x. ( X ^ m ) ) ) x. ( ( abs ` Y ) ^ m ) ) )
112 103 109 111 3eqtr3d 
 |-  ( ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) /\ m e. ( ZZ>= ` j ) ) -> ( ( abs ` ( ( A ` m ) x. ( Y ^ m ) ) ) x. ( ( abs ` X ) ^ m ) ) = ( ( abs ` ( ( A ` m ) x. ( X ^ m ) ) ) x. ( ( abs ` Y ) ^ m ) ) )
113 85 recnd 
 |-  ( ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) /\ m e. ( ZZ>= ` j ) ) -> ( ( abs ` X ) ^ m ) e. CC )
114 113 mulid2d 
 |-  ( ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) /\ m e. ( ZZ>= ` j ) ) -> ( 1 x. ( ( abs ` X ) ^ m ) ) = ( ( abs ` X ) ^ m ) )
115 100 112 114 3brtr3d 
 |-  ( ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) /\ m e. ( ZZ>= ` j ) ) -> ( ( abs ` ( ( A ` m ) x. ( X ^ m ) ) ) x. ( ( abs ` Y ) ^ m ) ) <_ ( ( abs ` X ) ^ m ) )
116 102 abscld 
 |-  ( ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) /\ m e. ( ZZ>= ` j ) ) -> ( abs ` ( ( A ` m ) x. ( X ^ m ) ) ) e. RR )
117 25 adantr 
 |-  ( ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) /\ m e. ( ZZ>= ` j ) ) -> ( abs ` Y ) e. RR )
118 117 69 reexpcld 
 |-  ( ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) /\ m e. ( ZZ>= ` j ) ) -> ( ( abs ` Y ) ^ m ) e. RR )
119 eluzelz 
 |-  ( m e. ( ZZ>= ` j ) -> m e. ZZ )
120 119 adantl 
 |-  ( ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) /\ m e. ( ZZ>= ` j ) ) -> m e. ZZ )
121 30 ad2antrr 
 |-  ( ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) /\ m e. ( ZZ>= ` j ) ) -> 0 < ( abs ` Y ) )
122 expgt0 
 |-  ( ( ( abs ` Y ) e. RR /\ m e. ZZ /\ 0 < ( abs ` Y ) ) -> 0 < ( ( abs ` Y ) ^ m ) )
123 117 120 121 122 syl3anc 
 |-  ( ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) /\ m e. ( ZZ>= ` j ) ) -> 0 < ( ( abs ` Y ) ^ m ) )
124 lemuldiv 
 |-  ( ( ( abs ` ( ( A ` m ) x. ( X ^ m ) ) ) e. RR /\ ( ( abs ` X ) ^ m ) e. RR /\ ( ( ( abs ` Y ) ^ m ) e. RR /\ 0 < ( ( abs ` Y ) ^ m ) ) ) -> ( ( ( abs ` ( ( A ` m ) x. ( X ^ m ) ) ) x. ( ( abs ` Y ) ^ m ) ) <_ ( ( abs ` X ) ^ m ) <-> ( abs ` ( ( A ` m ) x. ( X ^ m ) ) ) <_ ( ( ( abs ` X ) ^ m ) / ( ( abs ` Y ) ^ m ) ) ) )
125 116 85 118 123 124 syl112anc 
 |-  ( ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) /\ m e. ( ZZ>= ` j ) ) -> ( ( ( abs ` ( ( A ` m ) x. ( X ^ m ) ) ) x. ( ( abs ` Y ) ^ m ) ) <_ ( ( abs ` X ) ^ m ) <-> ( abs ` ( ( A ` m ) x. ( X ^ m ) ) ) <_ ( ( ( abs ` X ) ^ m ) / ( ( abs ` Y ) ^ m ) ) ) )
126 115 125 mpbid 
 |-  ( ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) /\ m e. ( ZZ>= ` j ) ) -> ( abs ` ( ( A ` m ) x. ( X ^ m ) ) ) <_ ( ( ( abs ` X ) ^ m ) / ( ( abs ` Y ) ^ m ) ) )
127 1 pserval2 
 |-  ( ( X e. CC /\ m e. NN0 ) -> ( ( G ` X ) ` m ) = ( ( A ` m ) x. ( X ^ m ) ) )
128 83 69 127 syl2anc 
 |-  ( ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) /\ m e. ( ZZ>= ` j ) ) -> ( ( G ` X ) ` m ) = ( ( A ` m ) x. ( X ^ m ) ) )
129 128 fveq2d 
 |-  ( ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) /\ m e. ( ZZ>= ` j ) ) -> ( abs ` ( ( G ` X ) ` m ) ) = ( abs ` ( ( A ` m ) x. ( X ^ m ) ) ) )
130 23 recnd 
 |-  ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) -> ( abs ` X ) e. CC )
131 130 adantr 
 |-  ( ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) /\ m e. ( ZZ>= ` j ) ) -> ( abs ` X ) e. CC )
132 25 recnd 
 |-  ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) -> ( abs ` Y ) e. CC )
133 132 adantr 
 |-  ( ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) /\ m e. ( ZZ>= ` j ) ) -> ( abs ` Y ) e. CC )
134 31 ad2antrr 
 |-  ( ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) /\ m e. ( ZZ>= ` j ) ) -> ( abs ` Y ) =/= 0 )
135 131 133 134 69 expdivd 
 |-  ( ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) /\ m e. ( ZZ>= ` j ) ) -> ( ( ( abs ` X ) / ( abs ` Y ) ) ^ m ) = ( ( ( abs ` X ) ^ m ) / ( ( abs ` Y ) ^ m ) ) )
136 126 129 135 3brtr4d 
 |-  ( ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) /\ m e. ( ZZ>= ` j ) ) -> ( abs ` ( ( G ` X ) ` m ) ) <_ ( ( ( abs ` X ) / ( abs ` Y ) ) ^ m ) )
137 71 73 74 75 136 lemul2ad 
 |-  ( ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) /\ m e. ( ZZ>= ` j ) ) -> ( m x. ( abs ` ( ( G ` X ) ` m ) ) ) <_ ( m x. ( ( ( abs ` X ) / ( abs ` Y ) ) ^ m ) ) )
138 74 71 remulcld 
 |-  ( ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) /\ m e. ( ZZ>= ` j ) ) -> ( m x. ( abs ` ( ( G ` X ) ` m ) ) ) e. RR )
139 70 absge0d 
 |-  ( ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) /\ m e. ( ZZ>= ` j ) ) -> 0 <_ ( abs ` ( ( G ` X ) ` m ) ) )
140 74 71 75 139 mulge0d 
 |-  ( ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) /\ m e. ( ZZ>= ` j ) ) -> 0 <_ ( m x. ( abs ` ( ( G ` X ) ` m ) ) ) )
141 138 140 absidd 
 |-  ( ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) /\ m e. ( ZZ>= ` j ) ) -> ( abs ` ( m x. ( abs ` ( ( G ` X ) ` m ) ) ) ) = ( m x. ( abs ` ( ( G ` X ) ` m ) ) ) )
142 74 73 remulcld 
 |-  ( ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) /\ m e. ( ZZ>= ` j ) ) -> ( m x. ( ( ( abs ` X ) / ( abs ` Y ) ) ^ m ) ) e. RR )
143 142 recnd 
 |-  ( ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) /\ m e. ( ZZ>= ` j ) ) -> ( m x. ( ( ( abs ` X ) / ( abs ` Y ) ) ^ m ) ) e. CC )
144 143 mulid2d 
 |-  ( ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) /\ m e. ( ZZ>= ` j ) ) -> ( 1 x. ( m x. ( ( ( abs ` X ) / ( abs ` Y ) ) ^ m ) ) ) = ( m x. ( ( ( abs ` X ) / ( abs ` Y ) ) ^ m ) ) )
145 137 141 144 3brtr4d 
 |-  ( ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) /\ m e. ( ZZ>= ` j ) ) -> ( abs ` ( m x. ( abs ` ( ( G ` X ) ` m ) ) ) ) <_ ( 1 x. ( m x. ( ( ( abs ` X ) / ( abs ` Y ) ) ^ m ) ) ) )
146 ovex 
 |-  ( m x. ( abs ` ( ( G ` X ) ` m ) ) ) e. _V
147 7 fvmpt2 
 |-  ( ( m e. NN0 /\ ( m x. ( abs ` ( ( G ` X ) ` m ) ) ) e. _V ) -> ( H ` m ) = ( m x. ( abs ` ( ( G ` X ) ` m ) ) ) )
148 69 146 147 sylancl 
 |-  ( ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) /\ m e. ( ZZ>= ` j ) ) -> ( H ` m ) = ( m x. ( abs ` ( ( G ` X ) ` m ) ) ) )
149 148 fveq2d 
 |-  ( ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) /\ m e. ( ZZ>= ` j ) ) -> ( abs ` ( H ` m ) ) = ( abs ` ( m x. ( abs ` ( ( G ` X ) ` m ) ) ) ) )
150 id 
 |-  ( i = m -> i = m )
151 oveq2 
 |-  ( i = m -> ( ( ( abs ` X ) / ( abs ` Y ) ) ^ i ) = ( ( ( abs ` X ) / ( abs ` Y ) ) ^ m ) )
152 150 151 oveq12d 
 |-  ( i = m -> ( i x. ( ( ( abs ` X ) / ( abs ` Y ) ) ^ i ) ) = ( m x. ( ( ( abs ` X ) / ( abs ` Y ) ) ^ m ) ) )
153 ovex 
 |-  ( m x. ( ( ( abs ` X ) / ( abs ` Y ) ) ^ m ) ) e. _V
154 152 37 153 fvmpt 
 |-  ( m e. NN0 -> ( ( i e. NN0 |-> ( i x. ( ( ( abs ` X ) / ( abs ` Y ) ) ^ i ) ) ) ` m ) = ( m x. ( ( ( abs ` X ) / ( abs ` Y ) ) ^ m ) ) )
155 69 154 syl 
 |-  ( ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) /\ m e. ( ZZ>= ` j ) ) -> ( ( i e. NN0 |-> ( i x. ( ( ( abs ` X ) / ( abs ` Y ) ) ^ i ) ) ) ` m ) = ( m x. ( ( ( abs ` X ) / ( abs ` Y ) ) ^ m ) ) )
156 155 oveq2d 
 |-  ( ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) /\ m e. ( ZZ>= ` j ) ) -> ( 1 x. ( ( i e. NN0 |-> ( i x. ( ( ( abs ` X ) / ( abs ` Y ) ) ^ i ) ) ) ` m ) ) = ( 1 x. ( m x. ( ( ( abs ` X ) / ( abs ` Y ) ) ^ m ) ) ) )
157 145 149 156 3brtr4d 
 |-  ( ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) /\ m e. ( ZZ>= ` j ) ) -> ( abs ` ( H ` m ) ) <_ ( 1 x. ( ( i e. NN0 |-> ( i x. ( ( ( abs ` X ) / ( abs ` Y ) ) ^ i ) ) ) ` m ) ) )
158 8 19 39 49 65 66 157 cvgcmpce 
 |-  ( ( ph /\ ( j e. NN0 /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( A ` k ) x. ( Y ^ k ) ) ) < 1 ) ) -> seq 0 ( + , H ) e. dom ~~> )
159 18 158 rexlimddv 
 |-  ( ph -> seq 0 ( + , H ) e. dom ~~> )