Metamath Proof Explorer


Theorem psercn

Description: An infinite series converges to a continuous function on the open disk of radius R , where R is the radius of convergence of the series. (Contributed by Mario Carneiro, 4-Mar-2015)

Ref Expression
Hypotheses pserf.g G = x n 0 A n x n
pserf.f F = y S j 0 G y j
pserf.a φ A : 0
pserf.r R = sup r | seq 0 + G r dom * <
psercn.s S = abs -1 0 R
psercn.m M = if R a + R 2 a + 1
Assertion psercn φ F : S cn

Proof

Step Hyp Ref Expression
1 pserf.g G = x n 0 A n x n
2 pserf.f F = y S j 0 G y j
3 pserf.a φ A : 0
4 pserf.r R = sup r | seq 0 + G r dom * <
5 psercn.s S = abs -1 0 R
6 psercn.m M = if R a + R 2 a + 1
7 sumex j 0 G y j V
8 7 rgenw y S j 0 G y j V
9 2 fnmpt y S j 0 G y j V F Fn S
10 8 9 mp1i φ F Fn S
11 cnvimass abs -1 0 R dom abs
12 absf abs :
13 12 fdmi dom abs =
14 11 13 sseqtri abs -1 0 R
15 5 14 eqsstri S
16 15 a1i φ S
17 16 sselda φ a S a
18 0cn 0
19 eqid abs = abs
20 19 cnmetdval 0 a 0 abs a = 0 a
21 18 17 20 sylancr φ a S 0 abs a = 0 a
22 abssub 0 a 0 a = a 0
23 18 17 22 sylancr φ a S 0 a = a 0
24 17 subid1d φ a S a 0 = a
25 24 fveq2d φ a S a 0 = a
26 21 23 25 3eqtrd φ a S 0 abs a = a
27 breq2 a + R 2 = if R a + R 2 a + 1 a < a + R 2 a < if R a + R 2 a + 1
28 breq2 a + 1 = if R a + R 2 a + 1 a < a + 1 a < if R a + R 2 a + 1
29 simpr φ a S a S
30 29 5 eleqtrdi φ a S a abs -1 0 R
31 ffn abs : abs Fn
32 elpreima abs Fn a abs -1 0 R a a 0 R
33 12 31 32 mp2b a abs -1 0 R a a 0 R
34 30 33 sylib φ a S a a 0 R
35 34 simprd φ a S a 0 R
36 0re 0
37 iccssxr 0 +∞ *
38 1 3 4 radcnvcl φ R 0 +∞
39 38 adantr φ a S R 0 +∞
40 37 39 sselid φ a S R *
41 elico2 0 R * a 0 R a 0 a a < R
42 36 40 41 sylancr φ a S a 0 R a 0 a a < R
43 35 42 mpbid φ a S a 0 a a < R
44 43 simp3d φ a S a < R
45 44 adantr φ a S R a < R
46 17 abscld φ a S a
47 avglt1 a R a < R a < a + R 2
48 46 47 sylan φ a S R a < R a < a + R 2
49 45 48 mpbid φ a S R a < a + R 2
50 46 ltp1d φ a S a < a + 1
51 50 adantr φ a S ¬ R a < a + 1
52 27 28 49 51 ifbothda φ a S a < if R a + R 2 a + 1
53 52 6 breqtrrdi φ a S a < M
54 26 53 eqbrtrd φ a S 0 abs a < M
55 cnxmet abs ∞Met
56 1 2 3 4 5 6 psercnlem1 φ a S M + a < M M < R
57 56 simp1d φ a S M +
58 57 rpxrd φ a S M *
59 elbl abs ∞Met 0 M * a 0 ball abs M a 0 abs a < M
60 55 18 58 59 mp3an12i φ a S a 0 ball abs M a 0 abs a < M
61 17 54 60 mpbir2and φ a S a 0 ball abs M
62 61 fvresd φ a S F 0 ball abs M a = F a
63 2 reseq1i F 0 ball abs M = y S j 0 G y j 0 ball abs M
64 1 2 3 4 5 56 psercnlem2 φ a S a 0 ball abs M 0 ball abs M abs -1 0 M abs -1 0 M S
65 64 simp2d φ a S 0 ball abs M abs -1 0 M
66 64 simp3d φ a S abs -1 0 M S
67 65 66 sstrd φ a S 0 ball abs M S
68 67 resmptd φ a S y S j 0 G y j 0 ball abs M = y 0 ball abs M j 0 G y j
69 63 68 syl5eq φ a S F 0 ball abs M = y 0 ball abs M j 0 G y j
70 eqid y 0 ball abs M j 0 G y j = y 0 ball abs M j 0 G y j
71 3 adantr φ a S A : 0
72 fveq2 k = y G k = G y
73 72 seqeq3d k = y seq 0 + G k = seq 0 + G y
74 73 fveq1d k = y seq 0 + G k s = seq 0 + G y s
75 74 cbvmptv k 0 ball abs M seq 0 + G k s = y 0 ball abs M seq 0 + G y s
76 fveq2 s = i seq 0 + G y s = seq 0 + G y i
77 76 mpteq2dv s = i y 0 ball abs M seq 0 + G y s = y 0 ball abs M seq 0 + G y i
78 75 77 syl5eq s = i k 0 ball abs M seq 0 + G k s = y 0 ball abs M seq 0 + G y i
79 78 cbvmptv s 0 k 0 ball abs M seq 0 + G k s = i 0 y 0 ball abs M seq 0 + G y i
80 57 rpred φ a S M
81 56 simp3d φ a S M < R
82 1 70 71 4 79 80 81 65 psercn2 φ a S y 0 ball abs M j 0 G y j : 0 ball abs M cn
83 69 82 eqeltrd φ a S F 0 ball abs M : 0 ball abs M cn
84 cncff F 0 ball abs M : 0 ball abs M cn F 0 ball abs M : 0 ball abs M
85 83 84 syl φ a S F 0 ball abs M : 0 ball abs M
86 85 61 ffvelrnd φ a S F 0 ball abs M a
87 62 86 eqeltrrd φ a S F a
88 87 ralrimiva φ a S F a
89 ffnfv F : S F Fn S a S F a
90 10 88 89 sylanbrc φ F : S
91 67 15 sstrdi φ a S 0 ball abs M
92 ssid
93 eqid TopOpen fld = TopOpen fld
94 eqid TopOpen fld 𝑡 0 ball abs M = TopOpen fld 𝑡 0 ball abs M
95 93 cnfldtopon TopOpen fld TopOn
96 95 toponrestid TopOpen fld = TopOpen fld 𝑡
97 93 94 96 cncfcn 0 ball abs M 0 ball abs M cn = TopOpen fld 𝑡 0 ball abs M Cn TopOpen fld
98 91 92 97 sylancl φ a S 0 ball abs M cn = TopOpen fld 𝑡 0 ball abs M Cn TopOpen fld
99 83 98 eleqtrd φ a S F 0 ball abs M TopOpen fld 𝑡 0 ball abs M Cn TopOpen fld
100 93 cnfldtop TopOpen fld Top
101 unicntop = TopOpen fld
102 101 restuni TopOpen fld Top 0 ball abs M 0 ball abs M = TopOpen fld 𝑡 0 ball abs M
103 100 91 102 sylancr φ a S 0 ball abs M = TopOpen fld 𝑡 0 ball abs M
104 61 103 eleqtrd φ a S a TopOpen fld 𝑡 0 ball abs M
105 eqid TopOpen fld 𝑡 0 ball abs M = TopOpen fld 𝑡 0 ball abs M
106 105 cncnpi F 0 ball abs M TopOpen fld 𝑡 0 ball abs M Cn TopOpen fld a TopOpen fld 𝑡 0 ball abs M F 0 ball abs M TopOpen fld 𝑡 0 ball abs M CnP TopOpen fld a
107 99 104 106 syl2anc φ a S F 0 ball abs M TopOpen fld 𝑡 0 ball abs M CnP TopOpen fld a
108 cnex V
109 108 15 ssexi S V
110 109 a1i φ a S S V
111 restabs TopOpen fld Top 0 ball abs M S S V TopOpen fld 𝑡 S 𝑡 0 ball abs M = TopOpen fld 𝑡 0 ball abs M
112 100 67 110 111 mp3an2i φ a S TopOpen fld 𝑡 S 𝑡 0 ball abs M = TopOpen fld 𝑡 0 ball abs M
113 112 oveq1d φ a S TopOpen fld 𝑡 S 𝑡 0 ball abs M CnP TopOpen fld = TopOpen fld 𝑡 0 ball abs M CnP TopOpen fld
114 113 fveq1d φ a S TopOpen fld 𝑡 S 𝑡 0 ball abs M CnP TopOpen fld a = TopOpen fld 𝑡 0 ball abs M CnP TopOpen fld a
115 107 114 eleqtrrd φ a S F 0 ball abs M TopOpen fld 𝑡 S 𝑡 0 ball abs M CnP TopOpen fld a
116 resttop TopOpen fld Top S V TopOpen fld 𝑡 S Top
117 100 109 116 mp2an TopOpen fld 𝑡 S Top
118 117 a1i φ a S TopOpen fld 𝑡 S Top
119 df-ss 0 ball abs M S 0 ball abs M S = 0 ball abs M
120 67 119 sylib φ a S 0 ball abs M S = 0 ball abs M
121 93 cnfldtopn TopOpen fld = MetOpen abs
122 121 blopn abs ∞Met 0 M * 0 ball abs M TopOpen fld
123 55 18 58 122 mp3an12i φ a S 0 ball abs M TopOpen fld
124 elrestr TopOpen fld Top S V 0 ball abs M TopOpen fld 0 ball abs M S TopOpen fld 𝑡 S
125 100 109 123 124 mp3an12i φ a S 0 ball abs M S TopOpen fld 𝑡 S
126 120 125 eqeltrrd φ a S 0 ball abs M TopOpen fld 𝑡 S
127 isopn3i TopOpen fld 𝑡 S Top 0 ball abs M TopOpen fld 𝑡 S int TopOpen fld 𝑡 S 0 ball abs M = 0 ball abs M
128 117 126 127 sylancr φ a S int TopOpen fld 𝑡 S 0 ball abs M = 0 ball abs M
129 61 128 eleqtrrd φ a S a int TopOpen fld 𝑡 S 0 ball abs M
130 90 adantr φ a S F : S
131 101 restuni TopOpen fld Top S S = TopOpen fld 𝑡 S
132 100 15 131 mp2an S = TopOpen fld 𝑡 S
133 132 101 cnprest TopOpen fld 𝑡 S Top 0 ball abs M S a int TopOpen fld 𝑡 S 0 ball abs M F : S F TopOpen fld 𝑡 S CnP TopOpen fld a F 0 ball abs M TopOpen fld 𝑡 S 𝑡 0 ball abs M CnP TopOpen fld a
134 118 67 129 130 133 syl22anc φ a S F TopOpen fld 𝑡 S CnP TopOpen fld a F 0 ball abs M TopOpen fld 𝑡 S 𝑡 0 ball abs M CnP TopOpen fld a
135 115 134 mpbird φ a S F TopOpen fld 𝑡 S CnP TopOpen fld a
136 135 ralrimiva φ a S F TopOpen fld 𝑡 S CnP TopOpen fld a
137 resttopon TopOpen fld TopOn S TopOpen fld 𝑡 S TopOn S
138 95 15 137 mp2an TopOpen fld 𝑡 S TopOn S
139 cncnp TopOpen fld 𝑡 S TopOn S TopOpen fld TopOn F TopOpen fld 𝑡 S Cn TopOpen fld F : S a S F TopOpen fld 𝑡 S CnP TopOpen fld a
140 138 95 139 mp2an F TopOpen fld 𝑡 S Cn TopOpen fld F : S a S F TopOpen fld 𝑡 S CnP TopOpen fld a
141 90 136 140 sylanbrc φ F TopOpen fld 𝑡 S Cn TopOpen fld
142 eqid TopOpen fld 𝑡 S = TopOpen fld 𝑡 S
143 93 142 96 cncfcn S S cn = TopOpen fld 𝑡 S Cn TopOpen fld
144 15 92 143 mp2an S cn = TopOpen fld 𝑡 S Cn TopOpen fld
145 141 144 eleqtrrdi φ F : S cn