Metamath Proof Explorer

Theorem psercnlem1

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 ) )
psercn.m 
|- M = if ( R e. RR , ( ( ( abs ` a ) + R ) / 2 ) , ( ( abs ` a ) + 1 ) )
Assertion psercnlem1 
|- ( ( ph /\ a e. S ) -> ( M e. RR+ /\ ( abs ` a ) < M /\ M < R ) )

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 psercn.m 
 |-  M = if ( R e. RR , ( ( ( abs ` a ) + R ) / 2 ) , ( ( abs ` a ) + 1 ) )
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 readdcl 
 |-  ( ( ( abs ` a ) e. RR /\ R e. RR ) -> ( ( abs ` a ) + R ) e. RR )
16 14 15 sylan 
 |-  ( ( ( ph /\ a e. S ) /\ R e. RR ) -> ( ( abs ` a ) + R ) e. RR )
17 16 rehalfcld 
 |-  ( ( ( ph /\ a e. S ) /\ R e. RR ) -> ( ( ( abs ` a ) + R ) / 2 ) e. RR )
18 peano2re 
 |-  ( ( abs ` a ) e. RR -> ( ( abs ` a ) + 1 ) e. RR )
19 14 18 syl 
 |-  ( ( ph /\ a e. S ) -> ( ( abs ` a ) + 1 ) e. RR )
20 19 adantr 
 |-  ( ( ( ph /\ a e. S ) /\ -. R e. RR ) -> ( ( abs ` a ) + 1 ) e. RR )
21 17 20 ifclda 
 |-  ( ( ph /\ a e. S ) -> if ( R e. RR , ( ( ( abs ` a ) + R ) / 2 ) , ( ( abs ` a ) + 1 ) ) e. RR )
22 6 21 eqeltrid 
 |-  ( ( ph /\ a e. S ) -> M e. RR )
23 0re 
 |-  0 e. RR
24 23 a1i 
 |-  ( ( ph /\ a e. S ) -> 0 e. RR )
25 13 absge0d 
 |-  ( ( ph /\ a e. S ) -> 0 <_ ( abs ` a ) )
26 breq2 
 |-  ( ( ( ( abs ` a ) + R ) / 2 ) = if ( R e. RR , ( ( ( abs ` a ) + R ) / 2 ) , ( ( abs ` a ) + 1 ) ) -> ( ( abs ` a ) < ( ( ( abs ` a ) + R ) / 2 ) <-> ( abs ` a ) < if ( R e. RR , ( ( ( abs ` a ) + R ) / 2 ) , ( ( abs ` a ) + 1 ) ) ) )
27 breq2 
 |-  ( ( ( abs ` a ) + 1 ) = if ( R e. RR , ( ( ( abs ` a ) + R ) / 2 ) , ( ( abs ` a ) + 1 ) ) -> ( ( abs ` a ) < ( ( abs ` a ) + 1 ) <-> ( abs ` a ) < if ( R e. RR , ( ( ( abs ` a ) + R ) / 2 ) , ( ( abs ` a ) + 1 ) ) ) )
28 simpr 
 |-  ( ( ph /\ a e. S ) -> a e. S )
29 28 5 eleqtrdi 
 |-  ( ( ph /\ a e. S ) -> a e. ( `' abs " ( 0 [,) R ) ) )
30 ffn 
 |-  ( abs : CC --> RR -> abs Fn CC )
31 elpreima 
 |-  ( abs Fn CC -> ( a e. ( `' abs " ( 0 [,) R ) ) <-> ( a e. CC /\ ( abs ` a ) e. ( 0 [,) R ) ) ) )
32 8 30 31 mp2b 
 |-  ( a e. ( `' abs " ( 0 [,) R ) ) <-> ( a e. CC /\ ( abs ` a ) e. ( 0 [,) R ) ) )
33 29 32 sylib 
 |-  ( ( ph /\ a e. S ) -> ( a e. CC /\ ( abs ` a ) e. ( 0 [,) R ) ) )
34 33 simprd 
 |-  ( ( ph /\ a e. S ) -> ( abs ` a ) e. ( 0 [,) R ) )
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 elico2 
 |-  ( ( 0 e. RR /\ R e. RR* ) -> ( ( abs ` a ) e. ( 0 [,) R ) <-> ( ( abs ` a ) e. RR /\ 0 <_ ( abs ` a ) /\ ( abs ` a ) < R ) ) )
40 23 38 39 sylancr 
 |-  ( ( ph /\ a e. S ) -> ( ( abs ` a ) e. ( 0 [,) R ) <-> ( ( abs ` a ) e. RR /\ 0 <_ ( abs ` a ) /\ ( abs ` a ) < R ) ) )
41 34 40 mpbid 
 |-  ( ( ph /\ a e. S ) -> ( ( abs ` a ) e. RR /\ 0 <_ ( abs ` a ) /\ ( abs ` a ) < R ) )
42 41 simp3d 
 |-  ( ( ph /\ a e. S ) -> ( abs ` a ) < R )
43 42 adantr 
 |-  ( ( ( ph /\ a e. S ) /\ R e. RR ) -> ( abs ` a ) < R )
44 avglt1 
 |-  ( ( ( abs ` a ) e. RR /\ R e. RR ) -> ( ( abs ` a ) < R <-> ( abs ` a ) < ( ( ( abs ` a ) + R ) / 2 ) ) )
45 14 44 sylan 
 |-  ( ( ( ph /\ a e. S ) /\ R e. RR ) -> ( ( abs ` a ) < R <-> ( abs ` a ) < ( ( ( abs ` a ) + R ) / 2 ) ) )
46 43 45 mpbid 
 |-  ( ( ( ph /\ a e. S ) /\ R e. RR ) -> ( abs ` a ) < ( ( ( abs ` a ) + R ) / 2 ) )
47 14 ltp1d 
 |-  ( ( ph /\ a e. S ) -> ( abs ` a ) < ( ( abs ` a ) + 1 ) )
48 47 adantr 
 |-  ( ( ( ph /\ a e. S ) /\ -. R e. RR ) -> ( abs ` a ) < ( ( abs ` a ) + 1 ) )
49 26 27 46 48 ifbothda 
 |-  ( ( ph /\ a e. S ) -> ( abs ` a ) < if ( R e. RR , ( ( ( abs ` a ) + R ) / 2 ) , ( ( abs ` a ) + 1 ) ) )
50 49 6 breqtrrdi 
 |-  ( ( ph /\ a e. S ) -> ( abs ` a ) < M )
51 24 14 22 25 50 lelttrd 
 |-  ( ( ph /\ a e. S ) -> 0 < M )
52 22 51 elrpd 
 |-  ( ( ph /\ a e. S ) -> M e. RR+ )
53 breq1 
 |-  ( ( ( ( abs ` a ) + R ) / 2 ) = if ( R e. RR , ( ( ( abs ` a ) + R ) / 2 ) , ( ( abs ` a ) + 1 ) ) -> ( ( ( ( abs ` a ) + R ) / 2 ) < R <-> if ( R e. RR , ( ( ( abs ` a ) + R ) / 2 ) , ( ( abs ` a ) + 1 ) ) < R ) )
54 breq1 
 |-  ( ( ( abs ` a ) + 1 ) = if ( R e. RR , ( ( ( abs ` a ) + R ) / 2 ) , ( ( abs ` a ) + 1 ) ) -> ( ( ( abs ` a ) + 1 ) < R <-> if ( R e. RR , ( ( ( abs ` a ) + R ) / 2 ) , ( ( abs ` a ) + 1 ) ) < R ) )
55 avglt2 
 |-  ( ( ( abs ` a ) e. RR /\ R e. RR ) -> ( ( abs ` a ) < R <-> ( ( ( abs ` a ) + R ) / 2 ) < R ) )
56 14 55 sylan 
 |-  ( ( ( ph /\ a e. S ) /\ R e. RR ) -> ( ( abs ` a ) < R <-> ( ( ( abs ` a ) + R ) / 2 ) < R ) )
57 43 56 mpbid 
 |-  ( ( ( ph /\ a e. S ) /\ R e. RR ) -> ( ( ( abs ` a ) + R ) / 2 ) < R )
58 19 rexrd 
 |-  ( ( ph /\ a e. S ) -> ( ( abs ` a ) + 1 ) e. RR* )
59 38 58 xrlenltd 
 |-  ( ( ph /\ a e. S ) -> ( R <_ ( ( abs ` a ) + 1 ) <-> -. ( ( abs ` a ) + 1 ) < R ) )
60 0xr 
 |-  0 e. RR*
61 pnfxr 
 |-  +oo e. RR*
62 elicc1 
 |-  ( ( 0 e. RR* /\ +oo e. RR* ) -> ( R e. ( 0 [,] +oo ) <-> ( R e. RR* /\ 0 <_ R /\ R <_ +oo ) ) )
63 60 61 62 mp2an 
 |-  ( R e. ( 0 [,] +oo ) <-> ( R e. RR* /\ 0 <_ R /\ R <_ +oo ) )
64 36 63 sylib 
 |-  ( ph -> ( R e. RR* /\ 0 <_ R /\ R <_ +oo ) )
65 64 simp2d 
 |-  ( ph -> 0 <_ R )
66 65 adantr 
 |-  ( ( ph /\ a e. S ) -> 0 <_ R )
67 ge0gtmnf 
 |-  ( ( R e. RR* /\ 0 <_ R ) -> -oo < R )
68 38 66 67 syl2anc 
 |-  ( ( ph /\ a e. S ) -> -oo < R )
69 xrre 
 |-  ( ( ( R e. RR* /\ ( ( abs ` a ) + 1 ) e. RR ) /\ ( -oo < R /\ R <_ ( ( abs ` a ) + 1 ) ) ) -> R e. RR )
70 69 expr 
 |-  ( ( ( R e. RR* /\ ( ( abs ` a ) + 1 ) e. RR ) /\ -oo < R ) -> ( R <_ ( ( abs ` a ) + 1 ) -> R e. RR ) )
71 38 19 68 70 syl21anc 
 |-  ( ( ph /\ a e. S ) -> ( R <_ ( ( abs ` a ) + 1 ) -> R e. RR ) )
72 59 71 sylbird 
 |-  ( ( ph /\ a e. S ) -> ( -. ( ( abs ` a ) + 1 ) < R -> R e. RR ) )
73 72 con1d 
 |-  ( ( ph /\ a e. S ) -> ( -. R e. RR -> ( ( abs ` a ) + 1 ) < R ) )
74 73 imp 
 |-  ( ( ( ph /\ a e. S ) /\ -. R e. RR ) -> ( ( abs ` a ) + 1 ) < R )
75 53 54 57 74 ifbothda 
 |-  ( ( ph /\ a e. S ) -> if ( R e. RR , ( ( ( abs ` a ) + R ) / 2 ) , ( ( abs ` a ) + 1 ) ) < R )
76 6 75 eqbrtrid 
 |-  ( ( ph /\ a e. S ) -> M < R )
77 52 50 76 3jca 
 |-  ( ( ph /\ a e. S ) -> ( M e. RR+ /\ ( abs ` a ) < M /\ M < R ) )