Description: Zero is always a convergent point for any power series. (Contributed by Mario Carneiro, 26-Feb-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | pser.g | |
|
radcnv.a | |
||
Assertion | radcnv0 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pser.g | |
|
2 | radcnv.a | |
|
3 | fveq2 | |
|
4 | 3 | seqeq3d | |
5 | 4 | eleq1d | |
6 | 0red | |
|
7 | nn0uz | |
|
8 | 0zd | |
|
9 | snfi | |
|
10 | 9 | a1i | |
11 | 0nn0 | |
|
12 | 11 | a1i | |
13 | 12 | snssd | |
14 | ifid | |
|
15 | 0cnd | |
|
16 | 1 | pserval2 | |
17 | 15 16 | sylan | |
18 | 17 | adantr | |
19 | simpr | |
|
20 | elnn0 | |
|
21 | 19 20 | sylib | |
22 | 21 | ord | |
23 | velsn | |
|
24 | 22 23 | syl6ibr | |
25 | 24 | con1d | |
26 | 25 | imp | |
27 | 26 | 0expd | |
28 | 27 | oveq2d | |
29 | 2 | ffvelrnda | |
30 | 29 | adantr | |
31 | 30 | mul01d | |
32 | 18 28 31 | 3eqtrd | |
33 | 32 | ifeq2da | |
34 | 14 33 | eqtr3id | |
35 | 13 | sselda | |
36 | 1 2 15 | psergf | |
37 | 36 | ffvelrnda | |
38 | 35 37 | syldan | |
39 | 7 8 10 13 34 38 | fsumcvg3 | |
40 | 5 6 39 | elrabd | |