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