Metamath Proof Explorer


Theorem radcnv0

Description: Zero is always a convergent point for any power series. (Contributed by Mario Carneiro, 26-Feb-2015)

Ref Expression
Hypotheses pser.g G=xn0Anxn
radcnv.a φA:0
Assertion radcnv0 φ0r|seq0+Grdom

Proof

Step Hyp Ref Expression
1 pser.g G=xn0Anxn
2 radcnv.a φA:0
3 fveq2 r=0Gr=G0
4 3 seqeq3d r=0seq0+Gr=seq0+G0
5 4 eleq1d r=0seq0+Grdomseq0+G0dom
6 0red φ0
7 nn0uz 0=0
8 0zd φ0
9 snfi 0Fin
10 9 a1i φ0Fin
11 0nn0 00
12 11 a1i φ00
13 12 snssd φ00
14 ifid ifk0G0kG0k=G0k
15 0cnd φ0
16 1 pserval2 0k0G0k=Ak0k
17 15 16 sylan φk0G0k=Ak0k
18 17 adantr φk0¬k0G0k=Ak0k
19 simpr φk0k0
20 elnn0 k0kk=0
21 19 20 sylib φk0kk=0
22 21 ord φk0¬kk=0
23 velsn k0k=0
24 22 23 syl6ibr φk0¬kk0
25 24 con1d φk0¬k0k
26 25 imp φk0¬k0k
27 26 0expd φk0¬k00k=0
28 27 oveq2d φk0¬k0Ak0k=Ak0
29 2 ffvelrnda φk0Ak
30 29 adantr φk0¬k0Ak
31 30 mul01d φk0¬k0Ak0=0
32 18 28 31 3eqtrd φk0¬k0G0k=0
33 32 ifeq2da φk0ifk0G0kG0k=ifk0G0k0
34 14 33 eqtr3id φk0G0k=ifk0G0k0
35 13 sselda φk0k0
36 1 2 15 psergf φG0:0
37 36 ffvelrnda φk0G0k
38 35 37 syldan φk0G0k
39 7 8 10 13 34 38 fsumcvg3 φseq0+G0dom
40 5 6 39 elrabd φ0r|seq0+Grdom