pserulm

Description: If S is a region contained in a circle of radius M < R , then the sequence of partial sums of the infinite series converges uniformly on S . (Contributed by Mario Carneiro, 26-Feb-2015)

	Ref	Expression
Hypotheses	pserf.g	$⊢ G = (x \in ℂ ⟼ (n \in ℕ_{0} ⟼ A (n) x^{n}))$
	pserf.f	$⊢ F = (y \in S ⟼ \sum_{j \in ℕ_{0}} G (y) (j))$
	pserf.a	$⊢ φ \to A : ℕ_{0} ⟶ ℂ$
	pserf.r	$⊢ R = sup (\{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\} ℝ^{*} <)$
	pserulm.h	$⊢ H = (i \in ℕ_{0} ⟼ (y \in S ⟼ seq 0 (+ G (y)) (i)))$
	pserulm.m	$⊢ φ \to M \in ℝ$
	pserulm.l	$⊢ φ \to M < R$
	pserulm.y	$⊢ φ \to S \subseteq {abs}^{-1} [[0, M]]$
Assertion	pserulm	$⊢ φ \to H \underset{u}{⇝} (S) F$

Proof

Step	Hyp	Ref	Expression
1		pserf.g	$⊢ G = (x \in ℂ ⟼ (n \in ℕ_{0} ⟼ A (n) x^{n}))$
2		pserf.f	$⊢ F = (y \in S ⟼ \sum_{j \in ℕ_{0}} G (y) (j))$
3		pserf.a	$⊢ φ \to A : ℕ_{0} ⟶ ℂ$
4		pserf.r	$⊢ R = sup (\{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\} ℝ^{*} <)$
5		pserulm.h	$⊢ H = (i \in ℕ_{0} ⟼ (y \in S ⟼ seq 0 (+ G (y)) (i)))$
6		pserulm.m	$⊢ φ \to M \in ℝ$
7		pserulm.l	$⊢ φ \to M < R$
8		pserulm.y	$⊢ φ \to S \subseteq {abs}^{-1} [[0, M]]$
9	8	adantr	$⊢ (φ \land M < 0) \to S \subseteq {abs}^{-1} [[0, M]]$
10		0xr	$⊢ 0 \in ℝ^{*}$
11	6	rexrd	$⊢ φ \to M \in ℝ^{*}$
12		icc0	$⊢ (0 \in ℝ^{} \land M \in ℝ^{}) \to ([0, M] = \emptyset \leftrightarrow M < 0)$
13	10 11 12	sylancr	$⊢ φ \to ([0, M] = \emptyset \leftrightarrow M < 0)$
14	13	biimpar	$⊢ (φ \land M < 0) \to [0, M] = \emptyset$
15	14	imaeq2d	$⊢ (φ \land M < 0) \to {abs}^{-1} [[0, M]] = {abs}^{-1} [\emptyset]$
16		ima0	$⊢ {abs}^{-1} [\emptyset] = \emptyset$
17	15 16	eqtrdi	$⊢ (φ \land M < 0) \to {abs}^{-1} [[0, M]] = \emptyset$
18	9 17	sseqtrd	$⊢ (φ \land M < 0) \to S \subseteq \emptyset$
19		ss0	$⊢ S \subseteq \emptyset \to S = \emptyset$
20	18 19	syl	$⊢ (φ \land M < 0) \to S = \emptyset$
21		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
22		0zd	$⊢ φ \to 0 \in ℤ$
23		0zd	$⊢ (φ \land y \in S) \to 0 \in ℤ$
24	3	adantr	$⊢ (φ \land y \in S) \to A : ℕ_{0} ⟶ ℂ$
25		cnvimass	$⊢ {abs}^{-1} [[0, M]] \subseteq dom abs$
26		absf	$⊢ abs : ℂ ⟶ ℝ$
27	26	fdmi	$⊢ dom abs = ℂ$
28	25 27	sseqtri	$⊢ {abs}^{-1} [[0, M]] \subseteq ℂ$
29	8 28	sstrdi	$⊢ φ \to S \subseteq ℂ$
30	29	sselda	$⊢ (φ \land y \in S) \to y \in ℂ$
31	1 24 30	psergf	$⊢ (φ \land y \in S) \to G (y) : ℕ_{0} ⟶ ℂ$
32	31	ffvelrnda	$⊢ ((φ \land y \in S) \land j \in ℕ_{0}) \to G (y) (j) \in ℂ$
33	21 23 32	serf	$⊢ (φ \land y \in S) \to seq 0 (+ G (y)) : ℕ_{0} ⟶ ℂ$
34	33	ffvelrnda	$⊢ ((φ \land y \in S) \land i \in ℕ_{0}) \to seq 0 (+ G (y)) (i) \in ℂ$
35	34	an32s	$⊢ ((φ \land i \in ℕ_{0}) \land y \in S) \to seq 0 (+ G (y)) (i) \in ℂ$
36	35	fmpttd	$⊢ (φ \land i \in ℕ_{0}) \to (y \in S ⟼ seq 0 (+ G (y)) (i)) : S ⟶ ℂ$
37		cnex	$⊢ ℂ \in V$
38		ssexg	$⊢ (S \subseteq ℂ \land ℂ \in V) \to S \in V$
39	29 37 38	sylancl	$⊢ φ \to S \in V$
40	39	adantr	$⊢ (φ \land i \in ℕ_{0}) \to S \in V$
41		elmapg	$⊢ (ℂ \in V \land S \in V) \to ((y \in S ⟼ seq 0 (+ G (y)) (i)) \in (ℂ^{S}) \leftrightarrow (y \in S ⟼ seq 0 (+ G (y)) (i)) : S ⟶ ℂ)$
42	37 40 41	sylancr	$⊢ (φ \land i \in ℕ_{0}) \to ((y \in S ⟼ seq 0 (+ G (y)) (i)) \in (ℂ^{S}) \leftrightarrow (y \in S ⟼ seq 0 (+ G (y)) (i)) : S ⟶ ℂ)$
43	36 42	mpbird	$⊢ (φ \land i \in ℕ_{0}) \to (y \in S ⟼ seq 0 (+ G (y)) (i)) \in (ℂ^{S})$
44	43 5	fmptd	$⊢ φ \to H : ℕ_{0} ⟶ ℂ^{S}$
45		eqidd	$⊢ ((φ \land y \in S) \land j \in ℕ_{0}) \to G (y) (j) = G (y) (j)$
46	8	sselda	$⊢ (φ \land y \in S) \to y \in {abs}^{-1} [[0, M]]$
47		ffn	$⊢ abs : ℂ ⟶ ℝ \to abs Fn ℂ$
48		elpreima	$⊢ abs Fn ℂ \to (y \in {abs}^{-1} [[0, M]] \leftrightarrow (y \in ℂ \land \|y\| \in [0, M]))$
49	26 47 48	mp2b	$⊢ y \in {abs}^{-1} [[0, M]] \leftrightarrow (y \in ℂ \land \|y\| \in [0, M])$
50	46 49	sylib	$⊢ (φ \land y \in S) \to (y \in ℂ \land \|y\| \in [0, M])$
51	50	simprd	$⊢ (φ \land y \in S) \to \|y\| \in [0, M]$
52		0re	$⊢ 0 \in ℝ$
53	6	adantr	$⊢ (φ \land y \in S) \to M \in ℝ$
54		elicc2	$⊢ (0 \in ℝ \land M \in ℝ) \to (\|y\| \in [0, M] \leftrightarrow (\|y\| \in ℝ \land 0 \leq \|y\| \land \|y\| \leq M))$
55	52 53 54	sylancr	$⊢ (φ \land y \in S) \to (\|y\| \in [0, M] \leftrightarrow (\|y\| \in ℝ \land 0 \leq \|y\| \land \|y\| \leq M))$
56	51 55	mpbid	$⊢ (φ \land y \in S) \to (\|y\| \in ℝ \land 0 \leq \|y\| \land \|y\| \leq M)$
57	56	simp1d	$⊢ (φ \land y \in S) \to \|y\| \in ℝ$
58	57	rexrd	$⊢ (φ \land y \in S) \to \|y\| \in ℝ^{*}$
59	11	adantr	$⊢ (φ \land y \in S) \to M \in ℝ^{*}$
60		iccssxr	$⊢ [0, +∞] \subseteq ℝ^{*}$
61	1 3 4	radcnvcl	$⊢ φ \to R \in [0, +∞]$
62	60 61	sselid	$⊢ φ \to R \in ℝ^{*}$
63	62	adantr	$⊢ (φ \land y \in S) \to R \in ℝ^{*}$
64	56	simp3d	$⊢ (φ \land y \in S) \to \|y\| \leq M$
65	7	adantr	$⊢ (φ \land y \in S) \to M < R$
66	58 59 63 64 65	xrlelttrd	$⊢ (φ \land y \in S) \to \|y\| < R$
67	1 24 4 30 66	radcnvlt2	$⊢ (φ \land y \in S) \to seq 0 (+ G (y)) \in dom ⇝$
68	21 23 45 32 67	isumcl	$⊢ (φ \land y \in S) \to \sum_{j \in ℕ_{0}} G (y) (j) \in ℂ$
69	68 2	fmptd	$⊢ φ \to F : S ⟶ ℂ$
70	21 22 44 69	ulm0	$⊢ (φ \land S = \emptyset) \to H \underset{u}{⇝} (S) F$
71	20 70	syldan	$⊢ (φ \land M < 0) \to H \underset{u}{⇝} (S) F$
72		simpr	$⊢ (φ \land i \in ℕ_{0}) \to i \in ℕ_{0}$
73	72 21	eleqtrdi	$⊢ (φ \land i \in ℕ_{0}) \to i \in ℤ_{\geq 0}$
74		eqid	$⊢ (m \in ℕ_{0} ⟼ (w \in S ⟼ G (w) (m))) = (m \in ℕ_{0} ⟼ (w \in S ⟼ G (w) (m)))$
75		fveq2	$⊢ w = y \to G (w) = G (y)$
76	75	fveq1d	$⊢ w = y \to G (w) (m) = G (y) (m)$
77	76	cbvmptv	$⊢ (w \in S ⟼ G (w) (m)) = (y \in S ⟼ G (y) (m))$
78		fveq2	$⊢ m = k \to G (y) (m) = G (y) (k)$
79	78	mpteq2dv	$⊢ m = k \to (y \in S ⟼ G (y) (m)) = (y \in S ⟼ G (y) (k))$
80	77 79	syl5eq	$⊢ m = k \to (w \in S ⟼ G (w) (m)) = (y \in S ⟼ G (y) (k))$
81		elfznn0	$⊢ k \in (0 \dots i) \to k \in ℕ_{0}$
82	81	adantl	$⊢ ((φ \land i \in ℕ_{0}) \land k \in (0 \dots i)) \to k \in ℕ_{0}$
83	39	ad2antrr	$⊢ ((φ \land i \in ℕ_{0}) \land k \in (0 \dots i)) \to S \in V$
84	83	mptexd	$⊢ ((φ \land i \in ℕ_{0}) \land k \in (0 \dots i)) \to (y \in S ⟼ G (y) (k)) \in V$
85	74 80 82 84	fvmptd3	$⊢ ((φ \land i \in ℕ_{0}) \land k \in (0 \dots i)) \to (m \in ℕ_{0} ⟼ (w \in S ⟼ G (w) (m))) (k) = (y \in S ⟼ G (y) (k))$
86	40 73 85	seqof	$⊢ (φ \land i \in ℕ_{0}) \to seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (w \in S ⟼ G (w) (m)))) (i) = (y \in S ⟼ seq 0 (+ G (y)) (i))$
87	86	eqcomd	$⊢ (φ \land i \in ℕ_{0}) \to (y \in S ⟼ seq 0 (+ G (y)) (i)) = seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (w \in S ⟼ G (w) (m)))) (i)$
88	87	mpteq2dva	$⊢ φ \to (i \in ℕ_{0} ⟼ (y \in S ⟼ seq 0 (+ G (y)) (i))) = (i \in ℕ_{0} ⟼ seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (w \in S ⟼ G (w) (m)))) (i))$
89		0z	$⊢ 0 \in ℤ$
90		seqfn	$⊢ 0 \in ℤ \to seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (w \in S ⟼ G (w) (m)))) Fn ℤ_{\geq 0}$
91	89 90	ax-mp	$⊢ seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (w \in S ⟼ G (w) (m)))) Fn ℤ_{\geq 0}$
92	21	fneq2i	$⊢ seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (w \in S ⟼ G (w) (m)))) Fn ℕ_{0} \leftrightarrow seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (w \in S ⟼ G (w) (m)))) Fn ℤ_{\geq 0}$
93	91 92	mpbir	$⊢ seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (w \in S ⟼ G (w) (m)))) Fn ℕ_{0}$
94		dffn5	$⊢ seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (w \in S ⟼ G (w) (m)))) Fn ℕ_{0} \leftrightarrow seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (w \in S ⟼ G (w) (m)))) = (i \in ℕ_{0} ⟼ seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (w \in S ⟼ G (w) (m)))) (i))$
95	93 94	mpbi	$⊢ seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (w \in S ⟼ G (w) (m)))) = (i \in ℕ_{0} ⟼ seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (w \in S ⟼ G (w) (m)))) (i))$
96	88 5 95	3eqtr4g	$⊢ φ \to H = seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (w \in S ⟼ G (w) (m))))$
97	96	adantr	$⊢ (φ \land 0 \leq M) \to H = seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (w \in S ⟼ G (w) (m))))$
98		0zd	$⊢ (φ \land 0 \leq M) \to 0 \in ℤ$
99	39	adantr	$⊢ (φ \land 0 \leq M) \to S \in V$
100	3	adantr	$⊢ (φ \land w \in S) \to A : ℕ_{0} ⟶ ℂ$
101	29	sselda	$⊢ (φ \land w \in S) \to w \in ℂ$
102	1 100 101	psergf	$⊢ (φ \land w \in S) \to G (w) : ℕ_{0} ⟶ ℂ$
103	102	ffvelrnda	$⊢ ((φ \land w \in S) \land m \in ℕ_{0}) \to G (w) (m) \in ℂ$
104	103	an32s	$⊢ ((φ \land m \in ℕ_{0}) \land w \in S) \to G (w) (m) \in ℂ$
105	104	fmpttd	$⊢ (φ \land m \in ℕ_{0}) \to (w \in S ⟼ G (w) (m)) : S ⟶ ℂ$
106	39	adantr	$⊢ (φ \land m \in ℕ_{0}) \to S \in V$
107		elmapg	$⊢ (ℂ \in V \land S \in V) \to ((w \in S ⟼ G (w) (m)) \in (ℂ^{S}) \leftrightarrow (w \in S ⟼ G (w) (m)) : S ⟶ ℂ)$
108	37 106 107	sylancr	$⊢ (φ \land m \in ℕ_{0}) \to ((w \in S ⟼ G (w) (m)) \in (ℂ^{S}) \leftrightarrow (w \in S ⟼ G (w) (m)) : S ⟶ ℂ)$
109	105 108	mpbird	$⊢ (φ \land m \in ℕ_{0}) \to (w \in S ⟼ G (w) (m)) \in (ℂ^{S})$
110	109	fmpttd	$⊢ φ \to (m \in ℕ_{0} ⟼ (w \in S ⟼ G (w) (m))) : ℕ_{0} ⟶ ℂ^{S}$
111	110	adantr	$⊢ (φ \land 0 \leq M) \to (m \in ℕ_{0} ⟼ (w \in S ⟼ G (w) (m))) : ℕ_{0} ⟶ ℂ^{S}$
112		fex	$⊢ (abs : ℂ ⟶ ℝ \land ℂ \in V) \to abs \in V$
113	26 37 112	mp2an	$⊢ abs \in V$
114		fvex	$⊢ G (M) \in V$
115	113 114	coex	$⊢ abs \circ G (M) \in V$
116	115	a1i	$⊢ (φ \land 0 \leq M) \to abs \circ G (M) \in V$
117	3	adantr	$⊢ (φ \land 0 \leq M) \to A : ℕ_{0} ⟶ ℂ$
118	6	adantr	$⊢ (φ \land 0 \leq M) \to M \in ℝ$
119	118	recnd	$⊢ (φ \land 0 \leq M) \to M \in ℂ$
120	1 117 119	psergf	$⊢ (φ \land 0 \leq M) \to G (M) : ℕ_{0} ⟶ ℂ$
121		fco	$⊢ (abs : ℂ ⟶ ℝ \land G (M) : ℕ_{0} ⟶ ℂ) \to (abs \circ G (M)) : ℕ_{0} ⟶ ℝ$
122	26 120 121	sylancr	$⊢ (φ \land 0 \leq M) \to (abs \circ G (M)) : ℕ_{0} ⟶ ℝ$
123	122	ffvelrnda	$⊢ ((φ \land 0 \leq M) \land k \in ℕ_{0}) \to (abs \circ G (M)) (k) \in ℝ$
124	29	ad2antrr	$⊢ ((φ \land 0 \leq M) \land (k \in ℕ_{0} \land z \in S)) \to S \subseteq ℂ$
125		simprr	$⊢ ((φ \land 0 \leq M) \land (k \in ℕ_{0} \land z \in S)) \to z \in S$
126	124 125	sseldd	$⊢ ((φ \land 0 \leq M) \land (k \in ℕ_{0} \land z \in S)) \to z \in ℂ$
127		simprl	$⊢ ((φ \land 0 \leq M) \land (k \in ℕ_{0} \land z \in S)) \to k \in ℕ_{0}$
128	126 127	expcld	$⊢ ((φ \land 0 \leq M) \land (k \in ℕ_{0} \land z \in S)) \to z^{k} \in ℂ$
129	128	abscld	$⊢ ((φ \land 0 \leq M) \land (k \in ℕ_{0} \land z \in S)) \to \|z^{k}\| \in ℝ$
130	119	adantr	$⊢ ((φ \land 0 \leq M) \land (k \in ℕ_{0} \land z \in S)) \to M \in ℂ$
131	130 127	expcld	$⊢ ((φ \land 0 \leq M) \land (k \in ℕ_{0} \land z \in S)) \to M^{k} \in ℂ$
132	131	abscld	$⊢ ((φ \land 0 \leq M) \land (k \in ℕ_{0} \land z \in S)) \to \|M^{k}\| \in ℝ$
133	3	ad2antrr	$⊢ ((φ \land 0 \leq M) \land (k \in ℕ_{0} \land z \in S)) \to A : ℕ_{0} ⟶ ℂ$
134	133 127	ffvelrnd	$⊢ ((φ \land 0 \leq M) \land (k \in ℕ_{0} \land z \in S)) \to A (k) \in ℂ$
135	134	abscld	$⊢ ((φ \land 0 \leq M) \land (k \in ℕ_{0} \land z \in S)) \to \|A (k)\| \in ℝ$
136	134	absge0d	$⊢ ((φ \land 0 \leq M) \land (k \in ℕ_{0} \land z \in S)) \to 0 \leq \|A (k)\|$
137	126	abscld	$⊢ ((φ \land 0 \leq M) \land (k \in ℕ_{0} \land z \in S)) \to \|z\| \in ℝ$
138	6	ad2antrr	$⊢ ((φ \land 0 \leq M) \land (k \in ℕ_{0} \land z \in S)) \to M \in ℝ$
139	126	absge0d	$⊢ ((φ \land 0 \leq M) \land (k \in ℕ_{0} \land z \in S)) \to 0 \leq \|z\|$
140		fveq2	$⊢ y = z \to \|y\| = \|z\|$
141	140	breq1d	$⊢ y = z \to (\|y\| \leq M \leftrightarrow \|z\| \leq M)$
142	64	ralrimiva	$⊢ φ \to \forall y \in S \|y\| \leq M$
143	142	ad2antrr	$⊢ ((φ \land 0 \leq M) \land (k \in ℕ_{0} \land z \in S)) \to \forall y \in S \|y\| \leq M$
144	141 143 125	rspcdva	$⊢ ((φ \land 0 \leq M) \land (k \in ℕ_{0} \land z \in S)) \to \|z\| \leq M$
145		leexp1a	$⊢ ((\|z\| \in ℝ \land M \in ℝ \land k \in ℕ_{0}) \land (0 \leq \|z\| \land \|z\| \leq M)) \to {\|z\|}^{k} \leq M^{k}$
146	137 138 127 139 144 145	syl32anc	$⊢ ((φ \land 0 \leq M) \land (k \in ℕ_{0} \land z \in S)) \to {\|z\|}^{k} \leq M^{k}$
147	126 127	absexpd	$⊢ ((φ \land 0 \leq M) \land (k \in ℕ_{0} \land z \in S)) \to \|z^{k}\| = {\|z\|}^{k}$
148	130 127	absexpd	$⊢ ((φ \land 0 \leq M) \land (k \in ℕ_{0} \land z \in S)) \to \|M^{k}\| = {\|M\|}^{k}$
149		absid	$⊢ (M \in ℝ \land 0 \leq M) \to \|M\| = M$
150	6 149	sylan	$⊢ (φ \land 0 \leq M) \to \|M\| = M$
151	150	adantr	$⊢ ((φ \land 0 \leq M) \land (k \in ℕ_{0} \land z \in S)) \to \|M\| = M$
152	151	oveq1d	$⊢ ((φ \land 0 \leq M) \land (k \in ℕ_{0} \land z \in S)) \to {\|M\|}^{k} = M^{k}$
153	148 152	eqtrd	$⊢ ((φ \land 0 \leq M) \land (k \in ℕ_{0} \land z \in S)) \to \|M^{k}\| = M^{k}$
154	146 147 153	3brtr4d	$⊢ ((φ \land 0 \leq M) \land (k \in ℕ_{0} \land z \in S)) \to \|z^{k}\| \leq \|M^{k}\|$
155	129 132 135 136 154	lemul2ad	$⊢ ((φ \land 0 \leq M) \land (k \in ℕ_{0} \land z \in S)) \to \|A (k)\| \|z^{k}\| \leq \|A (k)\| \|M^{k}\|$
156	134 128	absmuld	$⊢ ((φ \land 0 \leq M) \land (k \in ℕ_{0} \land z \in S)) \to \|A (k) z^{k}\| = \|A (k)\| \|z^{k}\|$
157	134 131	absmuld	$⊢ ((φ \land 0 \leq M) \land (k \in ℕ_{0} \land z \in S)) \to \|A (k) M^{k}\| = \|A (k)\| \|M^{k}\|$
158	155 156 157	3brtr4d	$⊢ ((φ \land 0 \leq M) \land (k \in ℕ_{0} \land z \in S)) \to \|A (k) z^{k}\| \leq \|A (k) M^{k}\|$
159	39	ad2antrr	$⊢ ((φ \land 0 \leq M) \land (k \in ℕ_{0} \land z \in S)) \to S \in V$
160	159	mptexd	$⊢ ((φ \land 0 \leq M) \land (k \in ℕ_{0} \land z \in S)) \to (y \in S ⟼ G (y) (k)) \in V$
161	74 80 127 160	fvmptd3	$⊢ ((φ \land 0 \leq M) \land (k \in ℕ_{0} \land z \in S)) \to (m \in ℕ_{0} ⟼ (w \in S ⟼ G (w) (m))) (k) = (y \in S ⟼ G (y) (k))$
162	161	fveq1d	$⊢ ((φ \land 0 \leq M) \land (k \in ℕ_{0} \land z \in S)) \to (m \in ℕ_{0} ⟼ (w \in S ⟼ G (w) (m))) (k) (z) = (y \in S ⟼ G (y) (k)) (z)$
163		fveq2	$⊢ y = z \to G (y) = G (z)$
164	163	fveq1d	$⊢ y = z \to G (y) (k) = G (z) (k)$
165		eqid	$⊢ (y \in S ⟼ G (y) (k)) = (y \in S ⟼ G (y) (k))$
166		fvex	$⊢ G (z) (k) \in V$
167	164 165 166	fvmpt	$⊢ z \in S \to (y \in S ⟼ G (y) (k)) (z) = G (z) (k)$
168	167	ad2antll	$⊢ ((φ \land 0 \leq M) \land (k \in ℕ_{0} \land z \in S)) \to (y \in S ⟼ G (y) (k)) (z) = G (z) (k)$
169	1	pserval2	$⊢ (z \in ℂ \land k \in ℕ_{0}) \to G (z) (k) = A (k) z^{k}$
170	126 127 169	syl2anc	$⊢ ((φ \land 0 \leq M) \land (k \in ℕ_{0} \land z \in S)) \to G (z) (k) = A (k) z^{k}$
171	162 168 170	3eqtrd	$⊢ ((φ \land 0 \leq M) \land (k \in ℕ_{0} \land z \in S)) \to (m \in ℕ_{0} ⟼ (w \in S ⟼ G (w) (m))) (k) (z) = A (k) z^{k}$
172	171	fveq2d	$⊢ ((φ \land 0 \leq M) \land (k \in ℕ_{0} \land z \in S)) \to \|(m \in ℕ_{0} ⟼ (w \in S ⟼ G (w) (m))) (k) (z)\| = \|A (k) z^{k}\|$
173	120	adantr	$⊢ ((φ \land 0 \leq M) \land (k \in ℕ_{0} \land z \in S)) \to G (M) : ℕ_{0} ⟶ ℂ$
174		fvco3	$⊢ (G (M) : ℕ_{0} ⟶ ℂ \land k \in ℕ_{0}) \to (abs \circ G (M)) (k) = \|G (M) (k)\|$
175	173 127 174	syl2anc	$⊢ ((φ \land 0 \leq M) \land (k \in ℕ_{0} \land z \in S)) \to (abs \circ G (M)) (k) = \|G (M) (k)\|$
176	1	pserval2	$⊢ (M \in ℂ \land k \in ℕ_{0}) \to G (M) (k) = A (k) M^{k}$
177	130 127 176	syl2anc	$⊢ ((φ \land 0 \leq M) \land (k \in ℕ_{0} \land z \in S)) \to G (M) (k) = A (k) M^{k}$
178	177	fveq2d	$⊢ ((φ \land 0 \leq M) \land (k \in ℕ_{0} \land z \in S)) \to \|G (M) (k)\| = \|A (k) M^{k}\|$
179	175 178	eqtrd	$⊢ ((φ \land 0 \leq M) \land (k \in ℕ_{0} \land z \in S)) \to (abs \circ G (M)) (k) = \|A (k) M^{k}\|$
180	158 172 179	3brtr4d	$⊢ ((φ \land 0 \leq M) \land (k \in ℕ_{0} \land z \in S)) \to \|(m \in ℕ_{0} ⟼ (w \in S ⟼ G (w) (m))) (k) (z)\| \leq (abs \circ G (M)) (k)$
181	7	adantr	$⊢ (φ \land 0 \leq M) \to M < R$
182	150 181	eqbrtrd	$⊢ (φ \land 0 \leq M) \to \|M\| < R$
183		id	$⊢ i = m \to i = m$
184		2fveq3	$⊢ i = m \to \|G (M) (i)\| = \|G (M) (m)\|$
185	183 184	oveq12d	$⊢ i = m \to i \|G (M) (i)\| = m \|G (M) (m)\|$
186	185	cbvmptv	$⊢ (i \in ℕ_{0} ⟼ i \|G (M) (i)\|) = (m \in ℕ_{0} ⟼ m \|G (M) (m)\|)$
187	1 117 4 119 182 186	radcnvlt1	$⊢ (φ \land 0 \leq M) \to (seq 0 (+ (i \in ℕ_{0} ⟼ i \|G (M) (i)\|)) \in dom ⇝ \land seq 0 (+ (abs \circ G (M))) \in dom ⇝)$
188	187	simprd	$⊢ (φ \land 0 \leq M) \to seq 0 (+ (abs \circ G (M))) \in dom ⇝$
189	21 98 99 111 116 123 180 188	mtest	$⊢ (φ \land 0 \leq M) \to seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (w \in S ⟼ G (w) (m)))) \in dom \underset{u}{⇝} (S)$
190	97 189	eqeltrd	$⊢ (φ \land 0 \leq M) \to H \in dom \underset{u}{⇝} (S)$
191		simpr	$⊢ (φ \land H \underset{u}{⇝} (S) f) \to H \underset{u}{⇝} (S) f$
192		ulmcl	$⊢ H \underset{u}{⇝} (S) f \to f : S ⟶ ℂ$
193	192	adantl	$⊢ (φ \land H \underset{u}{⇝} (S) f) \to f : S ⟶ ℂ$
194	193	feqmptd	$⊢ (φ \land H \underset{u}{⇝} (S) f) \to f = (y \in S ⟼ f (y))$
195		0zd	$⊢ ((φ \land H \underset{u}{⇝} (S) f) \land y \in S) \to 0 \in ℤ$
196		eqidd	$⊢ (((φ \land H \underset{u}{⇝} (S) f) \land y \in S) \land j \in ℕ_{0}) \to G (y) (j) = G (y) (j)$
197	31	adantlr	$⊢ ((φ \land H \underset{u}{⇝} (S) f) \land y \in S) \to G (y) : ℕ_{0} ⟶ ℂ$
198	197	ffvelrnda	$⊢ (((φ \land H \underset{u}{⇝} (S) f) \land y \in S) \land j \in ℕ_{0}) \to G (y) (j) \in ℂ$
199	44	ad2antrr	$⊢ ((φ \land H \underset{u}{⇝} (S) f) \land y \in S) \to H : ℕ_{0} ⟶ ℂ^{S}$
200		simpr	$⊢ ((φ \land H \underset{u}{⇝} (S) f) \land y \in S) \to y \in S$
201		seqex	$⊢ seq 0 (+ G (y)) \in V$
202	201	a1i	$⊢ ((φ \land H \underset{u}{⇝} (S) f) \land y \in S) \to seq 0 (+ G (y)) \in V$
203		simpr	$⊢ (((φ \land H \underset{u}{⇝} (S) f) \land y \in S) \land i \in ℕ_{0}) \to i \in ℕ_{0}$
204	39	ad3antrrr	$⊢ (((φ \land H \underset{u}{⇝} (S) f) \land y \in S) \land i \in ℕ_{0}) \to S \in V$
205	204	mptexd	$⊢ (((φ \land H \underset{u}{⇝} (S) f) \land y \in S) \land i \in ℕ_{0}) \to (y \in S ⟼ seq 0 (+ G (y)) (i)) \in V$
206	5	fvmpt2	$⊢ (i \in ℕ_{0} \land (y \in S ⟼ seq 0 (+ G (y)) (i)) \in V) \to H (i) = (y \in S ⟼ seq 0 (+ G (y)) (i))$
207	203 205 206	syl2anc	$⊢ (((φ \land H \underset{u}{⇝} (S) f) \land y \in S) \land i \in ℕ_{0}) \to H (i) = (y \in S ⟼ seq 0 (+ G (y)) (i))$
208	207	fveq1d	$⊢ (((φ \land H \underset{u}{⇝} (S) f) \land y \in S) \land i \in ℕ_{0}) \to H (i) (y) = (y \in S ⟼ seq 0 (+ G (y)) (i)) (y)$
209		simplr	$⊢ (((φ \land H \underset{u}{⇝} (S) f) \land y \in S) \land i \in ℕ_{0}) \to y \in S$
210		fvex	$⊢ seq 0 (+ G (y)) (i) \in V$
211		eqid	$⊢ (y \in S ⟼ seq 0 (+ G (y)) (i)) = (y \in S ⟼ seq 0 (+ G (y)) (i))$
212	211	fvmpt2	$⊢ (y \in S \land seq 0 (+ G (y)) (i) \in V) \to (y \in S ⟼ seq 0 (+ G (y)) (i)) (y) = seq 0 (+ G (y)) (i)$
213	209 210 212	sylancl	$⊢ (((φ \land H \underset{u}{⇝} (S) f) \land y \in S) \land i \in ℕ_{0}) \to (y \in S ⟼ seq 0 (+ G (y)) (i)) (y) = seq 0 (+ G (y)) (i)$
214	208 213	eqtrd	$⊢ (((φ \land H \underset{u}{⇝} (S) f) \land y \in S) \land i \in ℕ_{0}) \to H (i) (y) = seq 0 (+ G (y)) (i)$
215		simplr	$⊢ ((φ \land H \underset{u}{⇝} (S) f) \land y \in S) \to H \underset{u}{⇝} (S) f$
216	21 195 199 200 202 214 215	ulmclm	$⊢ ((φ \land H \underset{u}{⇝} (S) f) \land y \in S) \to seq 0 (+ G (y)) ⇝ f (y)$
217	21 195 196 198 216	isumclim	$⊢ ((φ \land H \underset{u}{⇝} (S) f) \land y \in S) \to \sum_{j \in ℕ_{0}} G (y) (j) = f (y)$
218	217	mpteq2dva	$⊢ (φ \land H \underset{u}{⇝} (S) f) \to (y \in S ⟼ \sum_{j \in ℕ_{0}} G (y) (j)) = (y \in S ⟼ f (y))$
219	2 218	syl5eq	$⊢ (φ \land H \underset{u}{⇝} (S) f) \to F = (y \in S ⟼ f (y))$
220	194 219	eqtr4d	$⊢ (φ \land H \underset{u}{⇝} (S) f) \to f = F$
221	191 220	breqtrd	$⊢ (φ \land H \underset{u}{⇝} (S) f) \to H \underset{u}{⇝} (S) F$
222	221	ex	$⊢ φ \to (H \underset{u}{⇝} (S) f \to H \underset{u}{⇝} (S) F)$
223	222	exlimdv	$⊢ φ \to (\exists f H \underset{u}{⇝} (S) f \to H \underset{u}{⇝} (S) F)$
224		eldmg	$⊢ H \in dom \underset{u}{⇝} (S) \to (H \in dom \underset{u}{⇝} (S) \leftrightarrow \exists f H \underset{u}{⇝} (S) f)$
225	224	ibi	$⊢ H \in dom \underset{u}{⇝} (S) \to \exists f H \underset{u}{⇝} (S) f$
226	223 225	impel	$⊢ (φ \land H \in dom \underset{u}{⇝} (S)) \to H \underset{u}{⇝} (S) F$
227	190 226	syldan	$⊢ (φ \land 0 \leq M) \to H \underset{u}{⇝} (S) F$
228		0red	$⊢ φ \to 0 \in ℝ$
229	71 227 6 228	ltlecasei	$⊢ φ \to H \underset{u}{⇝} (S) F$

Metamath Proof Explorer

Theorem pserulm

Proof