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