Metamath Proof Explorer

Theorem psercnlem2

Description: Lemma for psercn . (Contributed by Mario Carneiro, 18-Mar-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* , < )
psercn.s 
|- S = ( `' abs " ( 0 [,) R ) )
psercnlem2.i 
|- ( ( ph /\ a e. S ) -> ( M e. RR+ /\ ( abs ` a ) < M /\ M < R ) )
Assertion psercnlem2 
|- ( ( 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 ) )

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 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 sseldi 
 |-  ( ( 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 ) )