Metamath Proof Explorer

Theorem pserulm

Description: If S is a region contained in a circle of radius M < R , then the sequence of partial sums of the infinite series converges uniformly on S . (Contributed by Mario Carneiro, 26-Feb-2015)

Ref Expression
Hypotheses pserf.g 
|- G = ( x e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( x ^ n ) ) ) )
pserf.f 
|- F = ( y e. S |-> sum_ j e. NN0 ( ( G ` y ) ` j ) )
pserf.a 
|- ( ph -> A : NN0 --> CC )
pserf.r 
|- R = sup ( { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } , RR* , < )
pserulm.h 
|- H = ( i e. NN0 |-> ( y e. S |-> ( seq 0 ( + , ( G ` y ) ) ` i ) ) )
pserulm.m 
|- ( ph -> M e. RR )
pserulm.l 
|- ( ph -> M < R )
pserulm.y 
|- ( ph -> S C_ ( `' abs " ( 0 [,] M ) ) )
Assertion pserulm 
|- ( ph -> H ( ~~>u ` S ) F )

Proof

Step Hyp Ref Expression
1 pserf.g 
 |-  G = ( x e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( x ^ n ) ) ) )
2 pserf.f 
 |-  F = ( y e. S |-> sum_ j e. NN0 ( ( G ` y ) ` j ) )
3 pserf.a 
 |-  ( ph -> A : NN0 --> CC )
4 pserf.r 
 |-  R = sup ( { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } , RR* , < )
5 pserulm.h 
 |-  H = ( i e. NN0 |-> ( y e. S |-> ( seq 0 ( + , ( G ` y ) ) ` i ) ) )
6 pserulm.m 
 |-  ( ph -> M e. RR )
7 pserulm.l 
 |-  ( ph -> M < R )
8 pserulm.y 
 |-  ( ph -> S C_ ( `' abs " ( 0 [,] M ) ) )
9 8 adantr 
 |-  ( ( ph /\ M < 0 ) -> S C_ ( `' abs " ( 0 [,] M ) ) )
10 0xr 
 |-  0 e. RR*
11 6 rexrd 
 |-  ( ph -> M e. RR* )
12 icc0 
 |-  ( ( 0 e. RR* /\ M e. RR* ) -> ( ( 0 [,] M ) = (/) <-> M < 0 ) )
13 10 11 12 sylancr 
 |-  ( ph -> ( ( 0 [,] M ) = (/) <-> M < 0 ) )
14 13 biimpar 
 |-  ( ( ph /\ M < 0 ) -> ( 0 [,] M ) = (/) )
15 14 imaeq2d 
 |-  ( ( ph /\ M < 0 ) -> ( `' abs " ( 0 [,] M ) ) = ( `' abs " (/) ) )
16 ima0 
 |-  ( `' abs " (/) ) = (/)
17 15 16 eqtrdi 
 |-  ( ( ph /\ M < 0 ) -> ( `' abs " ( 0 [,] M ) ) = (/) )
18 9 17 sseqtrd 
 |-  ( ( ph /\ M < 0 ) -> S C_ (/) )
19 ss0 
 |-  ( S C_ (/) -> S = (/) )
20 18 19 syl 
 |-  ( ( ph /\ M < 0 ) -> S = (/) )
21 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
22 0zd 
 |-  ( ph -> 0 e. ZZ )
23 0zd 
 |-  ( ( ph /\ y e. S ) -> 0 e. ZZ )
24 3 adantr 
 |-  ( ( ph /\ y e. S ) -> A : NN0 --> CC )
25 cnvimass 
 |-  ( `' abs " ( 0 [,] M ) ) C_ dom abs
26 absf 
 |-  abs : CC --> RR
27 26 fdmi 
 |-  dom abs = CC
28 25 27 sseqtri 
 |-  ( `' abs " ( 0 [,] M ) ) C_ CC
29 8 28 sstrdi 
 |-  ( ph -> S C_ CC )
30 29 sselda 
 |-  ( ( ph /\ y e. S ) -> y e. CC )
31 1 24 30 psergf 
 |-  ( ( ph /\ y e. S ) -> ( G ` y ) : NN0 --> CC )
32 31 ffvelrnda 
 |-  ( ( ( ph /\ y e. S ) /\ j e. NN0 ) -> ( ( G ` y ) ` j ) e. CC )
33 21 23 32 serf 
 |-  ( ( ph /\ y e. S ) -> seq 0 ( + , ( G ` y ) ) : NN0 --> CC )
34 33 ffvelrnda 
 |-  ( ( ( ph /\ y e. S ) /\ i e. NN0 ) -> ( seq 0 ( + , ( G ` y ) ) ` i ) e. CC )
35 34 an32s 
 |-  ( ( ( ph /\ i e. NN0 ) /\ y e. S ) -> ( seq 0 ( + , ( G ` y ) ) ` i ) e. CC )
36 35 fmpttd 
 |-  ( ( ph /\ i e. NN0 ) -> ( y e. S |-> ( seq 0 ( + , ( G ` y ) ) ` i ) ) : S --> CC )
37 cnex 
 |-  CC e. _V
38 ssexg 
 |-  ( ( S C_ CC /\ CC e. _V ) -> S e. _V )
39 29 37 38 sylancl 
 |-  ( ph -> S e. _V )
40 39 adantr 
 |-  ( ( ph /\ i e. NN0 ) -> S e. _V )
41 elmapg 
 |-  ( ( CC e. _V /\ S e. _V ) -> ( ( y e. S |-> ( seq 0 ( + , ( G ` y ) ) ` i ) ) e. ( CC ^m S ) <-> ( y e. S |-> ( seq 0 ( + , ( G ` y ) ) ` i ) ) : S --> CC ) )
42 37 40 41 sylancr 
 |-  ( ( ph /\ i e. NN0 ) -> ( ( y e. S |-> ( seq 0 ( + , ( G ` y ) ) ` i ) ) e. ( CC ^m S ) <-> ( y e. S |-> ( seq 0 ( + , ( G ` y ) ) ` i ) ) : S --> CC ) )
43 36 42 mpbird 
 |-  ( ( ph /\ i e. NN0 ) -> ( y e. S |-> ( seq 0 ( + , ( G ` y ) ) ` i ) ) e. ( CC ^m S ) )
44 43 5 fmptd 
 |-  ( ph -> H : NN0 --> ( CC ^m S ) )
45 eqidd 
 |-  ( ( ( ph /\ y e. S ) /\ j e. NN0 ) -> ( ( G ` y ) ` j ) = ( ( G ` y ) ` j ) )
46 8 sselda 
 |-  ( ( ph /\ y e. S ) -> y e. ( `' abs " ( 0 [,] M ) ) )
47 ffn 
 |-  ( abs : CC --> RR -> abs Fn CC )
48 elpreima 
 |-  ( abs Fn CC -> ( y e. ( `' abs " ( 0 [,] M ) ) <-> ( y e. CC /\ ( abs ` y ) e. ( 0 [,] M ) ) ) )
49 26 47 48 mp2b 
 |-  ( y e. ( `' abs " ( 0 [,] M ) ) <-> ( y e. CC /\ ( abs ` y ) e. ( 0 [,] M ) ) )
50 46 49 sylib 
 |-  ( ( ph /\ y e. S ) -> ( y e. CC /\ ( abs ` y ) e. ( 0 [,] M ) ) )
51 50 simprd 
 |-  ( ( ph /\ y e. S ) -> ( abs ` y ) e. ( 0 [,] M ) )
52 0re 
 |-  0 e. RR
53 6 adantr 
 |-  ( ( ph /\ y e. S ) -> M e. RR )
54 elicc2 
 |-  ( ( 0 e. RR /\ M e. RR ) -> ( ( abs ` y ) e. ( 0 [,] M ) <-> ( ( abs ` y ) e. RR /\ 0 <_ ( abs ` y ) /\ ( abs ` y ) <_ M ) ) )
55 52 53 54 sylancr 
 |-  ( ( ph /\ y e. S ) -> ( ( abs ` y ) e. ( 0 [,] M ) <-> ( ( abs ` y ) e. RR /\ 0 <_ ( abs ` y ) /\ ( abs ` y ) <_ M ) ) )
56 51 55 mpbid 
 |-  ( ( ph /\ y e. S ) -> ( ( abs ` y ) e. RR /\ 0 <_ ( abs ` y ) /\ ( abs ` y ) <_ M ) )
57 56 simp1d 
 |-  ( ( ph /\ y e. S ) -> ( abs ` y ) e. RR )
58 57 rexrd 
 |-  ( ( ph /\ y e. S ) -> ( abs ` y ) e. RR* )
59 11 adantr 
 |-  ( ( ph /\ y e. S ) -> M e. RR* )
60 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
61 1 3 4 radcnvcl 
 |-  ( ph -> R e. ( 0 [,] +oo ) )
62 60 61 sseldi 
 |-  ( ph -> R e. RR* )
63 62 adantr 
 |-  ( ( ph /\ y e. S ) -> R e. RR* )
64 56 simp3d 
 |-  ( ( ph /\ y e. S ) -> ( abs ` y ) <_ M )
65 7 adantr 
 |-  ( ( ph /\ y e. S ) -> M < R )
66 58 59 63 64 65 xrlelttrd 
 |-  ( ( ph /\ y e. S ) -> ( abs ` y ) < R )
67 1 24 4 30 66 radcnvlt2 
 |-  ( ( ph /\ y e. S ) -> seq 0 ( + , ( G ` y ) ) e. dom ~~> )
68 21 23 45 32 67 isumcl 
 |-  ( ( ph /\ y e. S ) -> sum_ j e. NN0 ( ( G ` y ) ` j ) e. CC )
69 68 2 fmptd 
 |-  ( ph -> F : S --> CC )
70 21 22 44 69 ulm0 
 |-  ( ( ph /\ S = (/) ) -> H ( ~~>u ` S ) F )
71 20 70 syldan 
 |-  ( ( ph /\ M < 0 ) -> H ( ~~>u ` S ) F )
72 simpr 
 |-  ( ( ph /\ i e. NN0 ) -> i e. NN0 )
73 72 21 eleqtrdi 
 |-  ( ( ph /\ i e. NN0 ) -> i e. ( ZZ>= ` 0 ) )
74 eqid 
 |-  ( m e. NN0 |-> ( w e. S |-> ( ( G ` w ) ` m ) ) ) = ( m e. NN0 |-> ( w e. S |-> ( ( G ` w ) ` m ) ) )
75 fveq2 
 |-  ( w = y -> ( G ` w ) = ( G ` y ) )
76 75 fveq1d 
 |-  ( w = y -> ( ( G ` w ) ` m ) = ( ( G ` y ) ` m ) )
77 76 cbvmptv 
 |-  ( w e. S |-> ( ( G ` w ) ` m ) ) = ( y e. S |-> ( ( G ` y ) ` m ) )
78 fveq2 
 |-  ( m = k -> ( ( G ` y ) ` m ) = ( ( G ` y ) ` k ) )
79 78 mpteq2dv 
 |-  ( m = k -> ( y e. S |-> ( ( G ` y ) ` m ) ) = ( y e. S |-> ( ( G ` y ) ` k ) ) )
80 77 79 syl5eq 
 |-  ( m = k -> ( w e. S |-> ( ( G ` w ) ` m ) ) = ( y e. S |-> ( ( G ` y ) ` k ) ) )
81 elfznn0 
 |-  ( k e. ( 0 ... i ) -> k e. NN0 )
82 81 adantl 
 |-  ( ( ( ph /\ i e. NN0 ) /\ k e. ( 0 ... i ) ) -> k e. NN0 )
83 39 ad2antrr 
 |-  ( ( ( ph /\ i e. NN0 ) /\ k e. ( 0 ... i ) ) -> S e. _V )
84 83 mptexd 
 |-  ( ( ( ph /\ i e. NN0 ) /\ k e. ( 0 ... i ) ) -> ( y e. S |-> ( ( G ` y ) ` k ) ) e. _V )
85 74 80 82 84 fvmptd3 
 |-  ( ( ( ph /\ i e. NN0 ) /\ k e. ( 0 ... i ) ) -> ( ( m e. NN0 |-> ( w e. S |-> ( ( G ` w ) ` m ) ) ) ` k ) = ( y e. S |-> ( ( G ` y ) ` k ) ) )
86 40 73 85 seqof 
 |-  ( ( ph /\ i e. NN0 ) -> ( seq 0 ( oF + , ( m e. NN0 |-> ( w e. S |-> ( ( G ` w ) ` m ) ) ) ) ` i ) = ( y e. S |-> ( seq 0 ( + , ( G ` y ) ) ` i ) ) )
87 86 eqcomd 
 |-  ( ( ph /\ i e. NN0 ) -> ( y e. S |-> ( seq 0 ( + , ( G ` y ) ) ` i ) ) = ( seq 0 ( oF + , ( m e. NN0 |-> ( w e. S |-> ( ( G ` w ) ` m ) ) ) ) ` i ) )
88 87 mpteq2dva 
 |-  ( ph -> ( i e. NN0 |-> ( y e. S |-> ( seq 0 ( + , ( G ` y ) ) ` i ) ) ) = ( i e. NN0 |-> ( seq 0 ( oF + , ( m e. NN0 |-> ( w e. S |-> ( ( G ` w ) ` m ) ) ) ) ` i ) ) )
89 0z 
 |-  0 e. ZZ
90 seqfn 
 |-  ( 0 e. ZZ -> seq 0 ( oF + , ( m e. NN0 |-> ( w e. S |-> ( ( G ` w ) ` m ) ) ) ) Fn ( ZZ>= ` 0 ) )
91 89 90 ax-mp 
 |-  seq 0 ( oF + , ( m e. NN0 |-> ( w e. S |-> ( ( G ` w ) ` m ) ) ) ) Fn ( ZZ>= ` 0 )
92 21 fneq2i 
 |-  ( seq 0 ( oF + , ( m e. NN0 |-> ( w e. S |-> ( ( G ` w ) ` m ) ) ) ) Fn NN0 <-> seq 0 ( oF + , ( m e. NN0 |-> ( w e. S |-> ( ( G ` w ) ` m ) ) ) ) Fn ( ZZ>= ` 0 ) )
93 91 92 mpbir 
 |-  seq 0 ( oF + , ( m e. NN0 |-> ( w e. S |-> ( ( G ` w ) ` m ) ) ) ) Fn NN0
94 dffn5 
 |-  ( seq 0 ( oF + , ( m e. NN0 |-> ( w e. S |-> ( ( G ` w ) ` m ) ) ) ) Fn NN0 <-> seq 0 ( oF + , ( m e. NN0 |-> ( w e. S |-> ( ( G ` w ) ` m ) ) ) ) = ( i e. NN0 |-> ( seq 0 ( oF + , ( m e. NN0 |-> ( w e. S |-> ( ( G ` w ) ` m ) ) ) ) ` i ) ) )
95 93 94 mpbi 
 |-  seq 0 ( oF + , ( m e. NN0 |-> ( w e. S |-> ( ( G ` w ) ` m ) ) ) ) = ( i e. NN0 |-> ( seq 0 ( oF + , ( m e. NN0 |-> ( w e. S |-> ( ( G ` w ) ` m ) ) ) ) ` i ) )
96 88 5 95 3eqtr4g 
 |-  ( ph -> H = seq 0 ( oF + , ( m e. NN0 |-> ( w e. S |-> ( ( G ` w ) ` m ) ) ) ) )
97 96 adantr 
 |-  ( ( ph /\ 0 <_ M ) -> H = seq 0 ( oF + , ( m e. NN0 |-> ( w e. S |-> ( ( G ` w ) ` m ) ) ) ) )
98 0zd 
 |-  ( ( ph /\ 0 <_ M ) -> 0 e. ZZ )
99 39 adantr 
 |-  ( ( ph /\ 0 <_ M ) -> S e. _V )
100 3 adantr 
 |-  ( ( ph /\ w e. S ) -> A : NN0 --> CC )
101 29 sselda 
 |-  ( ( ph /\ w e. S ) -> w e. CC )
102 1 100 101 psergf 
 |-  ( ( ph /\ w e. S ) -> ( G ` w ) : NN0 --> CC )
103 102 ffvelrnda 
 |-  ( ( ( ph /\ w e. S ) /\ m e. NN0 ) -> ( ( G ` w ) ` m ) e. CC )
104 103 an32s 
 |-  ( ( ( ph /\ m e. NN0 ) /\ w e. S ) -> ( ( G ` w ) ` m ) e. CC )
105 104 fmpttd 
 |-  ( ( ph /\ m e. NN0 ) -> ( w e. S |-> ( ( G ` w ) ` m ) ) : S --> CC )
106 39 adantr 
 |-  ( ( ph /\ m e. NN0 ) -> S e. _V )
107 elmapg 
 |-  ( ( CC e. _V /\ S e. _V ) -> ( ( w e. S |-> ( ( G ` w ) ` m ) ) e. ( CC ^m S ) <-> ( w e. S |-> ( ( G ` w ) ` m ) ) : S --> CC ) )
108 37 106 107 sylancr 
 |-  ( ( ph /\ m e. NN0 ) -> ( ( w e. S |-> ( ( G ` w ) ` m ) ) e. ( CC ^m S ) <-> ( w e. S |-> ( ( G ` w ) ` m ) ) : S --> CC ) )
109 105 108 mpbird 
 |-  ( ( ph /\ m e. NN0 ) -> ( w e. S |-> ( ( G ` w ) ` m ) ) e. ( CC ^m S ) )
110 109 fmpttd 
 |-  ( ph -> ( m e. NN0 |-> ( w e. S |-> ( ( G ` w ) ` m ) ) ) : NN0 --> ( CC ^m S ) )
111 110 adantr 
 |-  ( ( ph /\ 0 <_ M ) -> ( m e. NN0 |-> ( w e. S |-> ( ( G ` w ) ` m ) ) ) : NN0 --> ( CC ^m S ) )
112 fex 
 |-  ( ( abs : CC --> RR /\ CC e. _V ) -> abs e. _V )
113 26 37 112 mp2an 
 |-  abs e. _V
114 fvex 
 |-  ( G ` M ) e. _V
115 113 114 coex 
 |-  ( abs o. ( G ` M ) ) e. _V
116 115 a1i 
 |-  ( ( ph /\ 0 <_ M ) -> ( abs o. ( G ` M ) ) e. _V )
117 3 adantr 
 |-  ( ( ph /\ 0 <_ M ) -> A : NN0 --> CC )
118 6 adantr 
 |-  ( ( ph /\ 0 <_ M ) -> M e. RR )
119 118 recnd 
 |-  ( ( ph /\ 0 <_ M ) -> M e. CC )
120 1 117 119 psergf 
 |-  ( ( ph /\ 0 <_ M ) -> ( G ` M ) : NN0 --> CC )
121 fco 
 |-  ( ( abs : CC --> RR /\ ( G ` M ) : NN0 --> CC ) -> ( abs o. ( G ` M ) ) : NN0 --> RR )
122 26 120 121 sylancr 
 |-  ( ( ph /\ 0 <_ M ) -> ( abs o. ( G ` M ) ) : NN0 --> RR )
123 122 ffvelrnda 
 |-  ( ( ( ph /\ 0 <_ M ) /\ k e. NN0 ) -> ( ( abs o. ( G ` M ) ) ` k ) e. RR )
124 29 ad2antrr 
 |-  ( ( ( ph /\ 0 <_ M ) /\ ( k e. NN0 /\ z e. S ) ) -> S C_ CC )
125 simprr 
 |-  ( ( ( ph /\ 0 <_ M ) /\ ( k e. NN0 /\ z e. S ) ) -> z e. S )
126 124 125 sseldd 
 |-  ( ( ( ph /\ 0 <_ M ) /\ ( k e. NN0 /\ z e. S ) ) -> z e. CC )
127 simprl 
 |-  ( ( ( ph /\ 0 <_ M ) /\ ( k e. NN0 /\ z e. S ) ) -> k e. NN0 )
128 126 127 expcld 
 |-  ( ( ( ph /\ 0 <_ M ) /\ ( k e. NN0 /\ z e. S ) ) -> ( z ^ k ) e. CC )
129 128 abscld 
 |-  ( ( ( ph /\ 0 <_ M ) /\ ( k e. NN0 /\ z e. S ) ) -> ( abs ` ( z ^ k ) ) e. RR )
130 119 adantr 
 |-  ( ( ( ph /\ 0 <_ M ) /\ ( k e. NN0 /\ z e. S ) ) -> M e. CC )
131 130 127 expcld 
 |-  ( ( ( ph /\ 0 <_ M ) /\ ( k e. NN0 /\ z e. S ) ) -> ( M ^ k ) e. CC )
132 131 abscld 
 |-  ( ( ( ph /\ 0 <_ M ) /\ ( k e. NN0 /\ z e. S ) ) -> ( abs ` ( M ^ k ) ) e. RR )
133 3 ad2antrr 
 |-  ( ( ( ph /\ 0 <_ M ) /\ ( k e. NN0 /\ z e. S ) ) -> A : NN0 --> CC )
134 133 127 ffvelrnd 
 |-  ( ( ( ph /\ 0 <_ M ) /\ ( k e. NN0 /\ z e. S ) ) -> ( A ` k ) e. CC )
135 134 abscld 
 |-  ( ( ( ph /\ 0 <_ M ) /\ ( k e. NN0 /\ z e. S ) ) -> ( abs ` ( A ` k ) ) e. RR )
136 134 absge0d 
 |-  ( ( ( ph /\ 0 <_ M ) /\ ( k e. NN0 /\ z e. S ) ) -> 0 <_ ( abs ` ( A ` k ) ) )
137 126 abscld 
 |-  ( ( ( ph /\ 0 <_ M ) /\ ( k e. NN0 /\ z e. S ) ) -> ( abs ` z ) e. RR )
138 6 ad2antrr 
 |-  ( ( ( ph /\ 0 <_ M ) /\ ( k e. NN0 /\ z e. S ) ) -> M e. RR )
139 126 absge0d 
 |-  ( ( ( ph /\ 0 <_ M ) /\ ( k e. NN0 /\ z e. S ) ) -> 0 <_ ( abs ` z ) )
140 fveq2 
 |-  ( y = z -> ( abs ` y ) = ( abs ` z ) )
141 140 breq1d 
 |-  ( y = z -> ( ( abs ` y ) <_ M <-> ( abs ` z ) <_ M ) )
142 64 ralrimiva 
 |-  ( ph -> A. y e. S ( abs ` y ) <_ M )
143 142 ad2antrr 
 |-  ( ( ( ph /\ 0 <_ M ) /\ ( k e. NN0 /\ z e. S ) ) -> A. y e. S ( abs ` y ) <_ M )
144 141 143 125 rspcdva 
 |-  ( ( ( ph /\ 0 <_ M ) /\ ( k e. NN0 /\ z e. S ) ) -> ( abs ` z ) <_ M )
145 leexp1a 
 |-  ( ( ( ( abs ` z ) e. RR /\ M e. RR /\ k e. NN0 ) /\ ( 0 <_ ( abs ` z ) /\ ( abs ` z ) <_ M ) ) -> ( ( abs ` z ) ^ k ) <_ ( M ^ k ) )
146 137 138 127 139 144 145 syl32anc 
 |-  ( ( ( ph /\ 0 <_ M ) /\ ( k e. NN0 /\ z e. S ) ) -> ( ( abs ` z ) ^ k ) <_ ( M ^ k ) )
147 126 127 absexpd 
 |-  ( ( ( ph /\ 0 <_ M ) /\ ( k e. NN0 /\ z e. S ) ) -> ( abs ` ( z ^ k ) ) = ( ( abs ` z ) ^ k ) )
148 130 127 absexpd 
 |-  ( ( ( ph /\ 0 <_ M ) /\ ( k e. NN0 /\ z e. S ) ) -> ( abs ` ( M ^ k ) ) = ( ( abs ` M ) ^ k ) )
149 absid 
 |-  ( ( M e. RR /\ 0 <_ M ) -> ( abs ` M ) = M )
150 6 149 sylan 
 |-  ( ( ph /\ 0 <_ M ) -> ( abs ` M ) = M )
151 150 adantr 
 |-  ( ( ( ph /\ 0 <_ M ) /\ ( k e. NN0 /\ z e. S ) ) -> ( abs ` M ) = M )
152 151 oveq1d 
 |-  ( ( ( ph /\ 0 <_ M ) /\ ( k e. NN0 /\ z e. S ) ) -> ( ( abs ` M ) ^ k ) = ( M ^ k ) )
153 148 152 eqtrd 
 |-  ( ( ( ph /\ 0 <_ M ) /\ ( k e. NN0 /\ z e. S ) ) -> ( abs ` ( M ^ k ) ) = ( M ^ k ) )
154 146 147 153 3brtr4d 
 |-  ( ( ( ph /\ 0 <_ M ) /\ ( k e. NN0 /\ z e. S ) ) -> ( abs ` ( z ^ k ) ) <_ ( abs ` ( M ^ k ) ) )
155 129 132 135 136 154 lemul2ad 
 |-  ( ( ( ph /\ 0 <_ M ) /\ ( k e. NN0 /\ z e. S ) ) -> ( ( abs ` ( A ` k ) ) x. ( abs ` ( z ^ k ) ) ) <_ ( ( abs ` ( A ` k ) ) x. ( abs ` ( M ^ k ) ) ) )
156 134 128 absmuld 
 |-  ( ( ( ph /\ 0 <_ M ) /\ ( k e. NN0 /\ z e. S ) ) -> ( abs ` ( ( A ` k ) x. ( z ^ k ) ) ) = ( ( abs ` ( A ` k ) ) x. ( abs ` ( z ^ k ) ) ) )
157 134 131 absmuld 
 |-  ( ( ( ph /\ 0 <_ M ) /\ ( k e. NN0 /\ z e. S ) ) -> ( abs ` ( ( A ` k ) x. ( M ^ k ) ) ) = ( ( abs ` ( A ` k ) ) x. ( abs ` ( M ^ k ) ) ) )
158 155 156 157 3brtr4d 
 |-  ( ( ( ph /\ 0 <_ M ) /\ ( k e. NN0 /\ z e. S ) ) -> ( abs ` ( ( A ` k ) x. ( z ^ k ) ) ) <_ ( abs ` ( ( A ` k ) x. ( M ^ k ) ) ) )
159 39 ad2antrr 
 |-  ( ( ( ph /\ 0 <_ M ) /\ ( k e. NN0 /\ z e. S ) ) -> S e. _V )
160 159 mptexd 
 |-  ( ( ( ph /\ 0 <_ M ) /\ ( k e. NN0 /\ z e. S ) ) -> ( y e. S |-> ( ( G ` y ) ` k ) ) e. _V )
161 74 80 127 160 fvmptd3 
 |-  ( ( ( ph /\ 0 <_ M ) /\ ( k e. NN0 /\ z e. S ) ) -> ( ( m e. NN0 |-> ( w e. S |-> ( ( G ` w ) ` m ) ) ) ` k ) = ( y e. S |-> ( ( G ` y ) ` k ) ) )
162 161 fveq1d 
 |-  ( ( ( ph /\ 0 <_ M ) /\ ( k e. NN0 /\ z e. S ) ) -> ( ( ( m e. NN0 |-> ( w e. S |-> ( ( G ` w ) ` m ) ) ) ` k ) ` z ) = ( ( y e. S |-> ( ( G ` y ) ` k ) ) ` z ) )
163 fveq2 
 |-  ( y = z -> ( G ` y ) = ( G ` z ) )
164 163 fveq1d 
 |-  ( y = z -> ( ( G ` y ) ` k ) = ( ( G ` z ) ` k ) )
165 eqid 
 |-  ( y e. S |-> ( ( G ` y ) ` k ) ) = ( y e. S |-> ( ( G ` y ) ` k ) )
166 fvex 
 |-  ( ( G ` z ) ` k ) e. _V
167 164 165 166 fvmpt 
 |-  ( z e. S -> ( ( y e. S |-> ( ( G ` y ) ` k ) ) ` z ) = ( ( G ` z ) ` k ) )
168 167 ad2antll 
 |-  ( ( ( ph /\ 0 <_ M ) /\ ( k e. NN0 /\ z e. S ) ) -> ( ( y e. S |-> ( ( G ` y ) ` k ) ) ` z ) = ( ( G ` z ) ` k ) )
169 1 pserval2 
 |-  ( ( z e. CC /\ k e. NN0 ) -> ( ( G ` z ) ` k ) = ( ( A ` k ) x. ( z ^ k ) ) )
170 126 127 169 syl2anc 
 |-  ( ( ( ph /\ 0 <_ M ) /\ ( k e. NN0 /\ z e. S ) ) -> ( ( G ` z ) ` k ) = ( ( A ` k ) x. ( z ^ k ) ) )
171 162 168 170 3eqtrd 
 |-  ( ( ( ph /\ 0 <_ M ) /\ ( k e. NN0 /\ z e. S ) ) -> ( ( ( m e. NN0 |-> ( w e. S |-> ( ( G ` w ) ` m ) ) ) ` k ) ` z ) = ( ( A ` k ) x. ( z ^ k ) ) )
172 171 fveq2d 
 |-  ( ( ( ph /\ 0 <_ M ) /\ ( k e. NN0 /\ z e. S ) ) -> ( abs ` ( ( ( m e. NN0 |-> ( w e. S |-> ( ( G ` w ) ` m ) ) ) ` k ) ` z ) ) = ( abs ` ( ( A ` k ) x. ( z ^ k ) ) ) )
173 120 adantr 
 |-  ( ( ( ph /\ 0 <_ M ) /\ ( k e. NN0 /\ z e. S ) ) -> ( G ` M ) : NN0 --> CC )
174 fvco3 
 |-  ( ( ( G ` M ) : NN0 --> CC /\ k e. NN0 ) -> ( ( abs o. ( G ` M ) ) ` k ) = ( abs ` ( ( G ` M ) ` k ) ) )
175 173 127 174 syl2anc 
 |-  ( ( ( ph /\ 0 <_ M ) /\ ( k e. NN0 /\ z e. S ) ) -> ( ( abs o. ( G ` M ) ) ` k ) = ( abs ` ( ( G ` M ) ` k ) ) )
176 1 pserval2 
 |-  ( ( M e. CC /\ k e. NN0 ) -> ( ( G ` M ) ` k ) = ( ( A ` k ) x. ( M ^ k ) ) )
177 130 127 176 syl2anc 
 |-  ( ( ( ph /\ 0 <_ M ) /\ ( k e. NN0 /\ z e. S ) ) -> ( ( G ` M ) ` k ) = ( ( A ` k ) x. ( M ^ k ) ) )
178 177 fveq2d 
 |-  ( ( ( ph /\ 0 <_ M ) /\ ( k e. NN0 /\ z e. S ) ) -> ( abs ` ( ( G ` M ) ` k ) ) = ( abs ` ( ( A ` k ) x. ( M ^ k ) ) ) )
179 175 178 eqtrd 
 |-  ( ( ( ph /\ 0 <_ M ) /\ ( k e. NN0 /\ z e. S ) ) -> ( ( abs o. ( G ` M ) ) ` k ) = ( abs ` ( ( A ` k ) x. ( M ^ k ) ) ) )
180 158 172 179 3brtr4d 
 |-  ( ( ( ph /\ 0 <_ M ) /\ ( k e. NN0 /\ z e. S ) ) -> ( abs ` ( ( ( m e. NN0 |-> ( w e. S |-> ( ( G ` w ) ` m ) ) ) ` k ) ` z ) ) <_ ( ( abs o. ( G ` M ) ) ` k ) )
181 7 adantr 
 |-  ( ( ph /\ 0 <_ M ) -> M < R )
182 150 181 eqbrtrd 
 |-  ( ( ph /\ 0 <_ M ) -> ( abs ` M ) < R )
183 id 
 |-  ( i = m -> i = m )
184 2fveq3 
 |-  ( i = m -> ( abs ` ( ( G ` M ) ` i ) ) = ( abs ` ( ( G ` M ) ` m ) ) )
185 183 184 oveq12d 
 |-  ( i = m -> ( i x. ( abs ` ( ( G ` M ) ` i ) ) ) = ( m x. ( abs ` ( ( G ` M ) ` m ) ) ) )
186 185 cbvmptv 
 |-  ( i e. NN0 |-> ( i x. ( abs ` ( ( G ` M ) ` i ) ) ) ) = ( m e. NN0 |-> ( m x. ( abs ` ( ( G ` M ) ` m ) ) ) )
187 1 117 4 119 182 186 radcnvlt1 
 |-  ( ( ph /\ 0 <_ M ) -> ( seq 0 ( + , ( i e. NN0 |-> ( i x. ( abs ` ( ( G ` M ) ` i ) ) ) ) ) e. dom ~~> /\ seq 0 ( + , ( abs o. ( G ` M ) ) ) e. dom ~~> ) )
188 187 simprd 
 |-  ( ( ph /\ 0 <_ M ) -> seq 0 ( + , ( abs o. ( G ` M ) ) ) e. dom ~~> )
189 21 98 99 111 116 123 180 188 mtest 
 |-  ( ( ph /\ 0 <_ M ) -> seq 0 ( oF + , ( m e. NN0 |-> ( w e. S |-> ( ( G ` w ) ` m ) ) ) ) e. dom ( ~~>u ` S ) )
190 97 189 eqeltrd 
 |-  ( ( ph /\ 0 <_ M ) -> H e. dom ( ~~>u ` S ) )
191 simpr 
 |-  ( ( ph /\ H ( ~~>u ` S ) f ) -> H ( ~~>u ` S ) f )
192 ulmcl 
 |-  ( H ( ~~>u ` S ) f -> f : S --> CC )
193 192 adantl 
 |-  ( ( ph /\ H ( ~~>u ` S ) f ) -> f : S --> CC )
194 193 feqmptd 
 |-  ( ( ph /\ H ( ~~>u ` S ) f ) -> f = ( y e. S |-> ( f ` y ) ) )
195 0zd 
 |-  ( ( ( ph /\ H ( ~~>u ` S ) f ) /\ y e. S ) -> 0 e. ZZ )
196 eqidd 
 |-  ( ( ( ( ph /\ H ( ~~>u ` S ) f ) /\ y e. S ) /\ j e. NN0 ) -> ( ( G ` y ) ` j ) = ( ( G ` y ) ` j ) )
197 31 adantlr 
 |-  ( ( ( ph /\ H ( ~~>u ` S ) f ) /\ y e. S ) -> ( G ` y ) : NN0 --> CC )
198 197 ffvelrnda 
 |-  ( ( ( ( ph /\ H ( ~~>u ` S ) f ) /\ y e. S ) /\ j e. NN0 ) -> ( ( G ` y ) ` j ) e. CC )
199 44 ad2antrr 
 |-  ( ( ( ph /\ H ( ~~>u ` S ) f ) /\ y e. S ) -> H : NN0 --> ( CC ^m S ) )
200 simpr 
 |-  ( ( ( ph /\ H ( ~~>u ` S ) f ) /\ y e. S ) -> y e. S )
201 seqex 
 |-  seq 0 ( + , ( G ` y ) ) e. _V
202 201 a1i 
 |-  ( ( ( ph /\ H ( ~~>u ` S ) f ) /\ y e. S ) -> seq 0 ( + , ( G ` y ) ) e. _V )
203 simpr 
 |-  ( ( ( ( ph /\ H ( ~~>u ` S ) f ) /\ y e. S ) /\ i e. NN0 ) -> i e. NN0 )
204 39 ad3antrrr 
 |-  ( ( ( ( ph /\ H ( ~~>u ` S ) f ) /\ y e. S ) /\ i e. NN0 ) -> S e. _V )
205 204 mptexd 
 |-  ( ( ( ( ph /\ H ( ~~>u ` S ) f ) /\ y e. S ) /\ i e. NN0 ) -> ( y e. S |-> ( seq 0 ( + , ( G ` y ) ) ` i ) ) e. _V )
206 5 fvmpt2 
 |-  ( ( i e. NN0 /\ ( y e. S |-> ( seq 0 ( + , ( G ` y ) ) ` i ) ) e. _V ) -> ( H ` i ) = ( y e. S |-> ( seq 0 ( + , ( G ` y ) ) ` i ) ) )
207 203 205 206 syl2anc 
 |-  ( ( ( ( ph /\ H ( ~~>u ` S ) f ) /\ y e. S ) /\ i e. NN0 ) -> ( H ` i ) = ( y e. S |-> ( seq 0 ( + , ( G ` y ) ) ` i ) ) )
208 207 fveq1d 
 |-  ( ( ( ( ph /\ H ( ~~>u ` S ) f ) /\ y e. S ) /\ i e. NN0 ) -> ( ( H ` i ) ` y ) = ( ( y e. S |-> ( seq 0 ( + , ( G ` y ) ) ` i ) ) ` y ) )
209 simplr 
 |-  ( ( ( ( ph /\ H ( ~~>u ` S ) f ) /\ y e. S ) /\ i e. NN0 ) -> y e. S )
210 fvex 
 |-  ( seq 0 ( + , ( G ` y ) ) ` i ) e. _V
211 eqid 
 |-  ( y e. S |-> ( seq 0 ( + , ( G ` y ) ) ` i ) ) = ( y e. S |-> ( seq 0 ( + , ( G ` y ) ) ` i ) )
212 211 fvmpt2 
 |-  ( ( y e. S /\ ( seq 0 ( + , ( G ` y ) ) ` i ) e. _V ) -> ( ( y e. S |-> ( seq 0 ( + , ( G ` y ) ) ` i ) ) ` y ) = ( seq 0 ( + , ( G ` y ) ) ` i ) )
213 209 210 212 sylancl 
 |-  ( ( ( ( ph /\ H ( ~~>u ` S ) f ) /\ y e. S ) /\ i e. NN0 ) -> ( ( y e. S |-> ( seq 0 ( + , ( G ` y ) ) ` i ) ) ` y ) = ( seq 0 ( + , ( G ` y ) ) ` i ) )
214 208 213 eqtrd 
 |-  ( ( ( ( ph /\ H ( ~~>u ` S ) f ) /\ y e. S ) /\ i e. NN0 ) -> ( ( H ` i ) ` y ) = ( seq 0 ( + , ( G ` y ) ) ` i ) )
215 simplr 
 |-  ( ( ( ph /\ H ( ~~>u ` S ) f ) /\ y e. S ) -> H ( ~~>u ` S ) f )
216 21 195 199 200 202 214 215 ulmclm 
 |-  ( ( ( ph /\ H ( ~~>u ` S ) f ) /\ y e. S ) -> seq 0 ( + , ( G ` y ) ) ~~> ( f ` y ) )
217 21 195 196 198 216 isumclim 
 |-  ( ( ( ph /\ H ( ~~>u ` S ) f ) /\ y e. S ) -> sum_ j e. NN0 ( ( G ` y ) ` j ) = ( f ` y ) )
218 217 mpteq2dva 
 |-  ( ( ph /\ H ( ~~>u ` S ) f ) -> ( y e. S |-> sum_ j e. NN0 ( ( G ` y ) ` j ) ) = ( y e. S |-> ( f ` y ) ) )
219 2 218 syl5eq 
 |-  ( ( ph /\ H ( ~~>u ` S ) f ) -> F = ( y e. S |-> ( f ` y ) ) )
220 194 219 eqtr4d 
 |-  ( ( ph /\ H ( ~~>u ` S ) f ) -> f = F )
221 191 220 breqtrd 
 |-  ( ( ph /\ H ( ~~>u ` S ) f ) -> H ( ~~>u ` S ) F )
222 221 ex 
 |-  ( ph -> ( H ( ~~>u ` S ) f -> H ( ~~>u ` S ) F ) )
223 222 exlimdv 
 |-  ( ph -> ( E. f H ( ~~>u ` S ) f -> H ( ~~>u ` S ) F ) )
224 eldmg 
 |-  ( H e. dom ( ~~>u ` S ) -> ( H e. dom ( ~~>u ` S ) <-> E. f H ( ~~>u ` S ) f ) )
225 224 ibi 
 |-  ( H e. dom ( ~~>u ` S ) -> E. f H ( ~~>u ` S ) f )
226 223 225 impel 
 |-  ( ( ph /\ H e. dom ( ~~>u ` S ) ) -> H ( ~~>u ` S ) F )
227 190 226 syldan 
 |-  ( ( ph /\ 0 <_ M ) -> H ( ~~>u ` S ) F )
228 0red 
 |-  ( ph -> 0 e. RR )
229 71 227 6 228 ltlecasei 
 |-  ( ph -> H ( ~~>u ` S ) F )