| 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 |
|
psercn.s |
|- S = ( `' abs " ( 0 [,) R ) ) |
| 6 |
|
psercnlem2.i |
|- ( ( ph /\ a e. S ) -> ( M e. RR+ /\ ( abs ` a ) < M /\ M < R ) ) |
| 7 |
|
cnvimass |
|- ( `' abs " ( 0 [,) R ) ) C_ dom abs |
| 8 |
|
absf |
|- abs : CC --> RR |
| 9 |
8
|
fdmi |
|- dom abs = CC |
| 10 |
7 9
|
sseqtri |
|- ( `' abs " ( 0 [,) R ) ) C_ CC |
| 11 |
5 10
|
eqsstri |
|- S C_ CC |
| 12 |
11
|
a1i |
|- ( ph -> S C_ CC ) |
| 13 |
12
|
sselda |
|- ( ( ph /\ a e. S ) -> a e. CC ) |
| 14 |
13
|
abscld |
|- ( ( ph /\ a e. S ) -> ( abs ` a ) e. RR ) |
| 15 |
13
|
absge0d |
|- ( ( ph /\ a e. S ) -> 0 <_ ( abs ` a ) ) |
| 16 |
6
|
simp2d |
|- ( ( ph /\ a e. S ) -> ( abs ` a ) < M ) |
| 17 |
|
0re |
|- 0 e. RR |
| 18 |
6
|
simp1d |
|- ( ( ph /\ a e. S ) -> M e. RR+ ) |
| 19 |
18
|
rpxrd |
|- ( ( ph /\ a e. S ) -> M e. RR* ) |
| 20 |
|
elico2 |
|- ( ( 0 e. RR /\ M e. RR* ) -> ( ( abs ` a ) e. ( 0 [,) M ) <-> ( ( abs ` a ) e. RR /\ 0 <_ ( abs ` a ) /\ ( abs ` a ) < M ) ) ) |
| 21 |
17 19 20
|
sylancr |
|- ( ( ph /\ a e. S ) -> ( ( abs ` a ) e. ( 0 [,) M ) <-> ( ( abs ` a ) e. RR /\ 0 <_ ( abs ` a ) /\ ( abs ` a ) < M ) ) ) |
| 22 |
14 15 16 21
|
mpbir3and |
|- ( ( ph /\ a e. S ) -> ( abs ` a ) e. ( 0 [,) M ) ) |
| 23 |
|
ffn |
|- ( abs : CC --> RR -> abs Fn CC ) |
| 24 |
|
elpreima |
|- ( abs Fn CC -> ( a e. ( `' abs " ( 0 [,) M ) ) <-> ( a e. CC /\ ( abs ` a ) e. ( 0 [,) M ) ) ) ) |
| 25 |
8 23 24
|
mp2b |
|- ( a e. ( `' abs " ( 0 [,) M ) ) <-> ( a e. CC /\ ( abs ` a ) e. ( 0 [,) M ) ) ) |
| 26 |
13 22 25
|
sylanbrc |
|- ( ( ph /\ a e. S ) -> a e. ( `' abs " ( 0 [,) M ) ) ) |
| 27 |
|
eqid |
|- ( abs o. - ) = ( abs o. - ) |
| 28 |
27
|
cnbl0 |
|- ( M e. RR* -> ( `' abs " ( 0 [,) M ) ) = ( 0 ( ball ` ( abs o. - ) ) M ) ) |
| 29 |
19 28
|
syl |
|- ( ( ph /\ a e. S ) -> ( `' abs " ( 0 [,) M ) ) = ( 0 ( ball ` ( abs o. - ) ) M ) ) |
| 30 |
26 29
|
eleqtrd |
|- ( ( ph /\ a e. S ) -> a e. ( 0 ( ball ` ( abs o. - ) ) M ) ) |
| 31 |
|
icossicc |
|- ( 0 [,) M ) C_ ( 0 [,] M ) |
| 32 |
|
imass2 |
|- ( ( 0 [,) M ) C_ ( 0 [,] M ) -> ( `' abs " ( 0 [,) M ) ) C_ ( `' abs " ( 0 [,] M ) ) ) |
| 33 |
31 32
|
mp1i |
|- ( ( ph /\ a e. S ) -> ( `' abs " ( 0 [,) M ) ) C_ ( `' abs " ( 0 [,] M ) ) ) |
| 34 |
29 33
|
eqsstrrd |
|- ( ( ph /\ a e. S ) -> ( 0 ( ball ` ( abs o. - ) ) M ) C_ ( `' abs " ( 0 [,] M ) ) ) |
| 35 |
|
iccssxr |
|- ( 0 [,] +oo ) C_ RR* |
| 36 |
1 3 4
|
radcnvcl |
|- ( ph -> R e. ( 0 [,] +oo ) ) |
| 37 |
36
|
adantr |
|- ( ( ph /\ a e. S ) -> R e. ( 0 [,] +oo ) ) |
| 38 |
35 37
|
sselid |
|- ( ( ph /\ a e. S ) -> R e. RR* ) |
| 39 |
6
|
simp3d |
|- ( ( ph /\ a e. S ) -> M < R ) |
| 40 |
|
df-ico |
|- [,) = ( u e. RR* , v e. RR* |-> { w e. RR* | ( u <_ w /\ w < v ) } ) |
| 41 |
|
df-icc |
|- [,] = ( u e. RR* , v e. RR* |-> { w e. RR* | ( u <_ w /\ w <_ v ) } ) |
| 42 |
|
xrlelttr |
|- ( ( z e. RR* /\ M e. RR* /\ R e. RR* ) -> ( ( z <_ M /\ M < R ) -> z < R ) ) |
| 43 |
40 41 42
|
ixxss2 |
|- ( ( R e. RR* /\ M < R ) -> ( 0 [,] M ) C_ ( 0 [,) R ) ) |
| 44 |
38 39 43
|
syl2anc |
|- ( ( ph /\ a e. S ) -> ( 0 [,] M ) C_ ( 0 [,) R ) ) |
| 45 |
|
imass2 |
|- ( ( 0 [,] M ) C_ ( 0 [,) R ) -> ( `' abs " ( 0 [,] M ) ) C_ ( `' abs " ( 0 [,) R ) ) ) |
| 46 |
44 45
|
syl |
|- ( ( ph /\ a e. S ) -> ( `' abs " ( 0 [,] M ) ) C_ ( `' abs " ( 0 [,) R ) ) ) |
| 47 |
46 5
|
sseqtrrdi |
|- ( ( ph /\ a e. S ) -> ( `' abs " ( 0 [,] M ) ) C_ S ) |
| 48 |
30 34 47
|
3jca |
|- ( ( ph /\ a e. S ) -> ( a e. ( 0 ( ball ` ( abs o. - ) ) M ) /\ ( 0 ( ball ` ( abs o. - ) ) M ) C_ ( `' abs " ( 0 [,] M ) ) /\ ( `' abs " ( 0 [,] M ) ) C_ S ) ) |