Metamath Proof Explorer

Theorem pserdvlem1

Description: Lemma for pserdv . (Contributed by Mario Carneiro, 7-May-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 pserdvlem1 
|- ( ( ph /\ a e. S ) -> ( ( ( ( abs ` a ) + M ) / 2 ) e. RR+ /\ ( abs ` a ) < ( ( ( abs ` a ) + M ) / 2 ) /\ ( ( ( abs ` a ) + M ) / 2 ) < 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 1 2 3 4 5 6 psercnlem1 
 |-  ( ( ph /\ a e. S ) -> ( M e. RR+ /\ ( abs ` a ) < M /\ M < R ) )
16 15 simp1d 
 |-  ( ( ph /\ a e. S ) -> M e. RR+ )
17 16 rpred 
 |-  ( ( ph /\ a e. S ) -> M e. RR )
18 14 17 readdcld 
 |-  ( ( ph /\ a e. S ) -> ( ( abs ` a ) + M ) e. RR )
19 0red 
 |-  ( ( ph /\ a e. S ) -> 0 e. RR )
20 13 absge0d 
 |-  ( ( ph /\ a e. S ) -> 0 <_ ( abs ` a ) )
21 14 16 ltaddrpd 
 |-  ( ( ph /\ a e. S ) -> ( abs ` a ) < ( ( abs ` a ) + M ) )
22 19 14 18 20 21 lelttrd 
 |-  ( ( ph /\ a e. S ) -> 0 < ( ( abs ` a ) + M ) )
23 18 22 elrpd 
 |-  ( ( ph /\ a e. S ) -> ( ( abs ` a ) + M ) e. RR+ )
24 23 rphalfcld 
 |-  ( ( ph /\ a e. S ) -> ( ( ( abs ` a ) + M ) / 2 ) e. RR+ )
25 15 simp2d 
 |-  ( ( ph /\ a e. S ) -> ( abs ` a ) < M )
26 avglt1 
 |-  ( ( ( abs ` a ) e. RR /\ M e. RR ) -> ( ( abs ` a ) < M <-> ( abs ` a ) < ( ( ( abs ` a ) + M ) / 2 ) ) )
27 14 17 26 syl2anc 
 |-  ( ( ph /\ a e. S ) -> ( ( abs ` a ) < M <-> ( abs ` a ) < ( ( ( abs ` a ) + M ) / 2 ) ) )
28 25 27 mpbid 
 |-  ( ( ph /\ a e. S ) -> ( abs ` a ) < ( ( ( abs ` a ) + M ) / 2 ) )
29 18 rehalfcld 
 |-  ( ( ph /\ a e. S ) -> ( ( ( abs ` a ) + M ) / 2 ) e. RR )
30 29 rexrd 
 |-  ( ( ph /\ a e. S ) -> ( ( ( abs ` a ) + M ) / 2 ) e. RR* )
31 17 rexrd 
 |-  ( ( ph /\ a e. S ) -> M e. RR* )
32 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
33 1 3 4 radcnvcl 
 |-  ( ph -> R e. ( 0 [,] +oo ) )
34 32 33 sselid 
 |-  ( ph -> R e. RR* )
35 34 adantr 
 |-  ( ( ph /\ a e. S ) -> R e. RR* )
36 avglt2 
 |-  ( ( ( abs ` a ) e. RR /\ M e. RR ) -> ( ( abs ` a ) < M <-> ( ( ( abs ` a ) + M ) / 2 ) < M ) )
37 14 17 36 syl2anc 
 |-  ( ( ph /\ a e. S ) -> ( ( abs ` a ) < M <-> ( ( ( abs ` a ) + M ) / 2 ) < M ) )
38 25 37 mpbid 
 |-  ( ( ph /\ a e. S ) -> ( ( ( abs ` a ) + M ) / 2 ) < M )
39 15 simp3d 
 |-  ( ( ph /\ a e. S ) -> M < R )
40 30 31 35 38 39 xrlttrd 
 |-  ( ( ph /\ a e. S ) -> ( ( ( abs ` a ) + M ) / 2 ) < R )
41 24 28 40 3jca 
 |-  ( ( ph /\ a e. S ) -> ( ( ( ( abs ` a ) + M ) / 2 ) e. RR+ /\ ( abs ` a ) < ( ( ( abs ` a ) + M ) / 2 ) /\ ( ( ( abs ` a ) + M ) / 2 ) < R ) )