pserdvlem2

	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 ⇝\} ℝ^{*} <)$
	psercn.s	$⊢ S = {abs}^{-1} [[0, R)]$
	psercn.m	$⊢ M = if (R \in ℝ, \frac{\|a\| + R}{2}, \|a\| + 1)$
	pserdv.b	$⊢ B = 0 ball (abs \circ -) (\frac{\|a\| + M}{2})$
Assertion	pserdvlem2	$⊢ (φ \land a \in S) \to ℂ D ({F ↾}_{B}) = (y \in B ⟼ \sum_{k \in ℕ_{0}} (k + 1) A (k + 1) y^{k})$

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		psercn.s	$⊢ S = {abs}^{-1} [[0, R)]$
6		psercn.m	$⊢ M = if (R \in ℝ, \frac{\|a\| + R}{2}, \|a\| + 1)$
7		pserdv.b	$⊢ B = 0 ball (abs \circ -) (\frac{\|a\| + M}{2})$
8		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
9		cnelprrecn	$⊢ ℂ \in \{ℝ, ℂ\}$
10	9	a1i	$⊢ (φ \land a \in S) \to ℂ \in \{ℝ, ℂ\}$
11		0zd	$⊢ (φ \land a \in S) \to 0 \in ℤ$
12		fzfid	$⊢ (((φ \land a \in S) \land k \in ℕ_{0}) \land y \in B) \to (0 \dots k) \in Fin$
13	3	ad3antrrr	$⊢ (((φ \land a \in S) \land k \in ℕ_{0}) \land y \in B) \to A : ℕ_{0} ⟶ ℂ$
14		cnxmet	$⊢ abs \circ - \in ∞Met (ℂ)$
15		0cnd	$⊢ (φ \land a \in S) \to 0 \in ℂ$
16	1 2 3 4 5 6	pserdvlem1	$⊢ (φ \land a \in S) \to (\frac{\|a\| + M}{2} \in ℝ^{+} \land \|a\| < \frac{\|a\| + M}{2} \land \frac{\|a\| + M}{2} < R)$
17	16	simp1d	$⊢ (φ \land a \in S) \to \frac{\|a\| + M}{2} \in ℝ^{+}$
18	17	rpxrd	$⊢ (φ \land a \in S) \to \frac{\|a\| + M}{2} \in ℝ^{*}$
19		blssm	$⊢ (abs \circ - \in ∞Met (ℂ) \land 0 \in ℂ \land \frac{\|a\| + M}{2} \in ℝ^{*}) \to 0 ball (abs \circ -) (\frac{\|a\| + M}{2}) \subseteq ℂ$
20	14 15 18 19	mp3an2i	$⊢ (φ \land a \in S) \to 0 ball (abs \circ -) (\frac{\|a\| + M}{2}) \subseteq ℂ$
21	7 20	eqsstrid	$⊢ (φ \land a \in S) \to B \subseteq ℂ$
22	21	adantr	$⊢ ((φ \land a \in S) \land k \in ℕ_{0}) \to B \subseteq ℂ$
23	22	sselda	$⊢ (((φ \land a \in S) \land k \in ℕ_{0}) \land y \in B) \to y \in ℂ$
24	1 13 23	psergf	$⊢ (((φ \land a \in S) \land k \in ℕ_{0}) \land y \in B) \to G (y) : ℕ_{0} ⟶ ℂ$
25		elfznn0	$⊢ i \in (0 \dots k) \to i \in ℕ_{0}$
26		ffvelrn	$⊢ (G (y) : ℕ_{0} ⟶ ℂ \land i \in ℕ_{0}) \to G (y) (i) \in ℂ$
27	24 25 26	syl2an	$⊢ ((((φ \land a \in S) \land k \in ℕ_{0}) \land y \in B) \land i \in (0 \dots k)) \to G (y) (i) \in ℂ$
28	12 27	fsumcl	$⊢ (((φ \land a \in S) \land k \in ℕ_{0}) \land y \in B) \to \sum_{i = 0}^{k} G (y) (i) \in ℂ$
29	28	fmpttd	$⊢ ((φ \land a \in S) \land k \in ℕ_{0}) \to (y \in B ⟼ \sum_{i = 0}^{k} G (y) (i)) : B ⟶ ℂ$
30		cnex	$⊢ ℂ \in V$
31	7	ovexi	$⊢ B \in V$
32	30 31	elmap	$⊢ (y \in B ⟼ \sum_{i = 0}^{k} G (y) (i)) \in (ℂ^{B}) \leftrightarrow (y \in B ⟼ \sum_{i = 0}^{k} G (y) (i)) : B ⟶ ℂ$
33	29 32	sylibr	$⊢ ((φ \land a \in S) \land k \in ℕ_{0}) \to (y \in B ⟼ \sum_{i = 0}^{k} G (y) (i)) \in (ℂ^{B})$
34	33	fmpttd	$⊢ (φ \land a \in S) \to (k \in ℕ_{0} ⟼ (y \in B ⟼ \sum_{i = 0}^{k} G (y) (i))) : ℕ_{0} ⟶ ℂ^{B}$
35	1 2 3 4 5 6	psercn	$⊢ φ \to F : S \underset{cn}{⟶} ℂ$
36		cncff	$⊢ F : S \underset{cn}{⟶} ℂ \to F : S ⟶ ℂ$
37	35 36	syl	$⊢ φ \to F : S ⟶ ℂ$
38	37	adantr	$⊢ (φ \land a \in S) \to F : S ⟶ ℂ$
39	1 2 3 4 5 16	psercnlem2	$⊢ (φ \land a \in S) \to (a \in (0 ball (abs \circ -) (\frac{\|a\| + M}{2})) \land 0 ball (abs \circ -) (\frac{\|a\| + M}{2}) \subseteq {abs}^{-1} [[0, \frac{\|a\| + M}{2}]] \land {abs}^{-1} [[0, \frac{\|a\| + M}{2}]] \subseteq S)$
40	39	simp2d	$⊢ (φ \land a \in S) \to 0 ball (abs \circ -) (\frac{\|a\| + M}{2}) \subseteq {abs}^{-1} [[0, \frac{\|a\| + M}{2}]]$
41	7 40	eqsstrid	$⊢ (φ \land a \in S) \to B \subseteq {abs}^{-1} [[0, \frac{\|a\| + M}{2}]]$
42	39	simp3d	$⊢ (φ \land a \in S) \to {abs}^{-1} [[0, \frac{\|a\| + M}{2}]] \subseteq S$
43	41 42	sstrd	$⊢ (φ \land a \in S) \to B \subseteq S$
44	38 43	fssresd	$⊢ (φ \land a \in S) \to ({F ↾}_{B}) : B ⟶ ℂ$
45		0zd	$⊢ ((φ \land a \in S) \land z \in B) \to 0 \in ℤ$
46		eqidd	$⊢ (((φ \land a \in S) \land z \in B) \land j \in ℕ_{0}) \to G (z) (j) = G (z) (j)$
47	3	ad2antrr	$⊢ ((φ \land a \in S) \land z \in B) \to A : ℕ_{0} ⟶ ℂ$
48	21	sselda	$⊢ ((φ \land a \in S) \land z \in B) \to z \in ℂ$
49	1 47 48	psergf	$⊢ ((φ \land a \in S) \land z \in B) \to G (z) : ℕ_{0} ⟶ ℂ$
50	49	ffvelrnda	$⊢ (((φ \land a \in S) \land z \in B) \land j \in ℕ_{0}) \to G (z) (j) \in ℂ$
51	48	abscld	$⊢ ((φ \land a \in S) \land z \in B) \to \|z\| \in ℝ$
52	51	rexrd	$⊢ ((φ \land a \in S) \land z \in B) \to \|z\| \in ℝ^{*}$
53	18	adantr	$⊢ ((φ \land a \in S) \land z \in B) \to \frac{\|a\| + M}{2} \in ℝ^{*}$
54		iccssxr	$⊢ [0, +∞] \subseteq ℝ^{*}$
55	1 3 4	radcnvcl	$⊢ φ \to R \in [0, +∞]$
56	54 55	sselid	$⊢ φ \to R \in ℝ^{*}$
57	56	ad2antrr	$⊢ ((φ \land a \in S) \land z \in B) \to R \in ℝ^{*}$
58		0cn	$⊢ 0 \in ℂ$
59		eqid	$⊢ abs \circ - = abs \circ -$
60	59	cnmetdval	$⊢ (z \in ℂ \land 0 \in ℂ) \to z (abs \circ -) 0 = \|z - 0\|$
61	48 58 60	sylancl	$⊢ ((φ \land a \in S) \land z \in B) \to z (abs \circ -) 0 = \|z - 0\|$
62	48	subid1d	$⊢ ((φ \land a \in S) \land z \in B) \to z - 0 = z$
63	62	fveq2d	$⊢ ((φ \land a \in S) \land z \in B) \to \|z - 0\| = \|z\|$
64	61 63	eqtrd	$⊢ ((φ \land a \in S) \land z \in B) \to z (abs \circ -) 0 = \|z\|$
65		simpr	$⊢ ((φ \land a \in S) \land z \in B) \to z \in B$
66	65 7	eleqtrdi	$⊢ ((φ \land a \in S) \land z \in B) \to z \in (0 ball (abs \circ -) (\frac{\|a\| + M}{2}))$
67	14	a1i	$⊢ ((φ \land a \in S) \land z \in B) \to abs \circ - \in ∞Met (ℂ)$
68		0cnd	$⊢ ((φ \land a \in S) \land z \in B) \to 0 \in ℂ$
69		elbl3	$⊢ ((abs \circ - \in ∞Met (ℂ) \land \frac{\|a\| + M}{2} \in ℝ^{*}) \land (0 \in ℂ \land z \in ℂ)) \to (z \in (0 ball (abs \circ -) (\frac{\|a\| + M}{2})) \leftrightarrow z (abs \circ -) 0 < \frac{\|a\| + M}{2})$
70	67 53 68 48 69	syl22anc	$⊢ ((φ \land a \in S) \land z \in B) \to (z \in (0 ball (abs \circ -) (\frac{\|a\| + M}{2})) \leftrightarrow z (abs \circ -) 0 < \frac{\|a\| + M}{2})$
71	66 70	mpbid	$⊢ ((φ \land a \in S) \land z \in B) \to z (abs \circ -) 0 < \frac{\|a\| + M}{2}$
72	64 71	eqbrtrrd	$⊢ ((φ \land a \in S) \land z \in B) \to \|z\| < \frac{\|a\| + M}{2}$
73	16	simp3d	$⊢ (φ \land a \in S) \to \frac{\|a\| + M}{2} < R$
74	73	adantr	$⊢ ((φ \land a \in S) \land z \in B) \to \frac{\|a\| + M}{2} < R$
75	52 53 57 72 74	xrlttrd	$⊢ ((φ \land a \in S) \land z \in B) \to \|z\| < R$
76	1 47 4 48 75	radcnvlt2	$⊢ ((φ \land a \in S) \land z \in B) \to seq 0 (+ G (z)) \in dom ⇝$
77	8 45 46 50 76	isumclim2	$⊢ ((φ \land a \in S) \land z \in B) \to seq 0 (+ G (z)) ⇝ \sum_{j \in ℕ_{0}} G (z) (j)$
78	43	sselda	$⊢ ((φ \land a \in S) \land z \in B) \to z \in S$
79		fveq2	$⊢ y = z \to G (y) = G (z)$
80	79	fveq1d	$⊢ y = z \to G (y) (j) = G (z) (j)$
81	80	sumeq2sdv	$⊢ y = z \to \sum_{j \in ℕ_{0}} G (y) (j) = \sum_{j \in ℕ_{0}} G (z) (j)$
82		sumex	$⊢ \sum_{j \in ℕ_{0}} G (z) (j) \in V$
83	81 2 82	fvmpt	$⊢ z \in S \to F (z) = \sum_{j \in ℕ_{0}} G (z) (j)$
84	78 83	syl	$⊢ ((φ \land a \in S) \land z \in B) \to F (z) = \sum_{j \in ℕ_{0}} G (z) (j)$
85	77 84	breqtrrd	$⊢ ((φ \land a \in S) \land z \in B) \to seq 0 (+ G (z)) ⇝ F (z)$
86		oveq2	$⊢ k = m \to (0 \dots k) = (0 \dots m)$
87	86	sumeq1d	$⊢ k = m \to \sum_{i = 0}^{k} G (y) (i) = \sum_{i = 0}^{m} G (y) (i)$
88	87	mpteq2dv	$⊢ k = m \to (y \in B ⟼ \sum_{i = 0}^{k} G (y) (i)) = (y \in B ⟼ \sum_{i = 0}^{m} G (y) (i))$
89		eqid	$⊢ (k \in ℕ_{0} ⟼ (y \in B ⟼ \sum_{i = 0}^{k} G (y) (i))) = (k \in ℕ_{0} ⟼ (y \in B ⟼ \sum_{i = 0}^{k} G (y) (i)))$
90	31	mptex	$⊢ (y \in B ⟼ \sum_{i = 0}^{m} G (y) (i)) \in V$
91	88 89 90	fvmpt	$⊢ m \in ℕ_{0} \to (k \in ℕ_{0} ⟼ (y \in B ⟼ \sum_{i = 0}^{k} G (y) (i))) (m) = (y \in B ⟼ \sum_{i = 0}^{m} G (y) (i))$
92	91	adantl	$⊢ (((φ \land a \in S) \land z \in B) \land m \in ℕ_{0}) \to (k \in ℕ_{0} ⟼ (y \in B ⟼ \sum_{i = 0}^{k} G (y) (i))) (m) = (y \in B ⟼ \sum_{i = 0}^{m} G (y) (i))$
93	92	fveq1d	$⊢ (((φ \land a \in S) \land z \in B) \land m \in ℕ_{0}) \to (k \in ℕ_{0} ⟼ (y \in B ⟼ \sum_{i = 0}^{k} G (y) (i))) (m) (z) = (y \in B ⟼ \sum_{i = 0}^{m} G (y) (i)) (z)$
94	79	fveq1d	$⊢ y = z \to G (y) (i) = G (z) (i)$
95	94	sumeq2sdv	$⊢ y = z \to \sum_{i = 0}^{m} G (y) (i) = \sum_{i = 0}^{m} G (z) (i)$
96		eqid	$⊢ (y \in B ⟼ \sum_{i = 0}^{m} G (y) (i)) = (y \in B ⟼ \sum_{i = 0}^{m} G (y) (i))$
97		sumex	$⊢ \sum_{i = 0}^{m} G (z) (i) \in V$
98	95 96 97	fvmpt	$⊢ z \in B \to (y \in B ⟼ \sum_{i = 0}^{m} G (y) (i)) (z) = \sum_{i = 0}^{m} G (z) (i)$
99	98	ad2antlr	$⊢ (((φ \land a \in S) \land z \in B) \land m \in ℕ_{0}) \to (y \in B ⟼ \sum_{i = 0}^{m} G (y) (i)) (z) = \sum_{i = 0}^{m} G (z) (i)$
100		eqidd	$⊢ ((((φ \land a \in S) \land z \in B) \land m \in ℕ_{0}) \land i \in (0 \dots m)) \to G (z) (i) = G (z) (i)$
101		simpr	$⊢ (((φ \land a \in S) \land z \in B) \land m \in ℕ_{0}) \to m \in ℕ_{0}$
102	101 8	eleqtrdi	$⊢ (((φ \land a \in S) \land z \in B) \land m \in ℕ_{0}) \to m \in ℤ_{\geq 0}$
103	49	adantr	$⊢ (((φ \land a \in S) \land z \in B) \land m \in ℕ_{0}) \to G (z) : ℕ_{0} ⟶ ℂ$
104		elfznn0	$⊢ i \in (0 \dots m) \to i \in ℕ_{0}$
105		ffvelrn	$⊢ (G (z) : ℕ_{0} ⟶ ℂ \land i \in ℕ_{0}) \to G (z) (i) \in ℂ$
106	103 104 105	syl2an	$⊢ ((((φ \land a \in S) \land z \in B) \land m \in ℕ_{0}) \land i \in (0 \dots m)) \to G (z) (i) \in ℂ$
107	100 102 106	fsumser	$⊢ (((φ \land a \in S) \land z \in B) \land m \in ℕ_{0}) \to \sum_{i = 0}^{m} G (z) (i) = seq 0 (+ G (z)) (m)$
108	93 99 107	3eqtrd	$⊢ (((φ \land a \in S) \land z \in B) \land m \in ℕ_{0}) \to (k \in ℕ_{0} ⟼ (y \in B ⟼ \sum_{i = 0}^{k} G (y) (i))) (m) (z) = seq 0 (+ G (z)) (m)$
109	108	mpteq2dva	$⊢ ((φ \land a \in S) \land z \in B) \to (m \in ℕ_{0} ⟼ (k \in ℕ_{0} ⟼ (y \in B ⟼ \sum_{i = 0}^{k} G (y) (i))) (m) (z)) = (m \in ℕ_{0} ⟼ seq 0 (+ G (z)) (m))$
110		0z	$⊢ 0 \in ℤ$
111		seqfn	$⊢ 0 \in ℤ \to seq 0 (+ G (z)) Fn ℤ_{\geq 0}$
112	110 111	ax-mp	$⊢ seq 0 (+ G (z)) Fn ℤ_{\geq 0}$
113	8	fneq2i	$⊢ seq 0 (+ G (z)) Fn ℕ_{0} \leftrightarrow seq 0 (+ G (z)) Fn ℤ_{\geq 0}$
114	112 113	mpbir	$⊢ seq 0 (+ G (z)) Fn ℕ_{0}$
115		dffn5	$⊢ seq 0 (+ G (z)) Fn ℕ_{0} \leftrightarrow seq 0 (+ G (z)) = (m \in ℕ_{0} ⟼ seq 0 (+ G (z)) (m))$
116	114 115	mpbi	$⊢ seq 0 (+ G (z)) = (m \in ℕ_{0} ⟼ seq 0 (+ G (z)) (m))$
117	109 116	eqtr4di	$⊢ ((φ \land a \in S) \land z \in B) \to (m \in ℕ_{0} ⟼ (k \in ℕ_{0} ⟼ (y \in B ⟼ \sum_{i = 0}^{k} G (y) (i))) (m) (z)) = seq 0 (+ G (z))$
118		fvres	$⊢ z \in B \to ({F ↾}_{B}) (z) = F (z)$
119	118	adantl	$⊢ ((φ \land a \in S) \land z \in B) \to ({F ↾}_{B}) (z) = F (z)$
120	85 117 119	3brtr4d	$⊢ ((φ \land a \in S) \land z \in B) \to (m \in ℕ_{0} ⟼ (k \in ℕ_{0} ⟼ (y \in B ⟼ \sum_{i = 0}^{k} G (y) (i))) (m) (z)) ⇝ ({F ↾}_{B}) (z)$
121	91	adantl	$⊢ ((φ \land a \in S) \land m \in ℕ_{0}) \to (k \in ℕ_{0} ⟼ (y \in B ⟼ \sum_{i = 0}^{k} G (y) (i))) (m) = (y \in B ⟼ \sum_{i = 0}^{m} G (y) (i))$
122	121	oveq2d	$⊢ ((φ \land a \in S) \land m \in ℕ_{0}) \to ℂ D (k \in ℕ_{0} ⟼ (y \in B ⟼ \sum_{i = 0}^{k} G (y) (i))) (m) = \frac{d (y \in B⟼ \sum_{i = 0}^{m} G (y) (i))}{d_{ℂ} y}$
123		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
124	123	cnfldtopon	$⊢ TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
125	124	toponrestid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ$
126	9	a1i	$⊢ ((φ \land a \in S) \land m \in ℕ_{0}) \to ℂ \in \{ℝ, ℂ\}$
127	123	cnfldtopn	$⊢ TopOpen (ℂ_{fld}) = MetOpen (abs \circ -)$
128	127	blopn	$⊢ (abs \circ - \in ∞Met (ℂ) \land 0 \in ℂ \land \frac{\|a\| + M}{2} \in ℝ^{*}) \to 0 ball (abs \circ -) (\frac{\|a\| + M}{2}) \in TopOpen (ℂ_{fld})$
129	14 15 18 128	mp3an2i	$⊢ (φ \land a \in S) \to 0 ball (abs \circ -) (\frac{\|a\| + M}{2}) \in TopOpen (ℂ_{fld})$
130	7 129	eqeltrid	$⊢ (φ \land a \in S) \to B \in TopOpen (ℂ_{fld})$
131	130	adantr	$⊢ ((φ \land a \in S) \land m \in ℕ_{0}) \to B \in TopOpen (ℂ_{fld})$
132		fzfid	$⊢ ((φ \land a \in S) \land m \in ℕ_{0}) \to (0 \dots m) \in Fin$
133	3	ad2antrr	$⊢ ((φ \land a \in S) \land m \in ℕ_{0}) \to A : ℕ_{0} ⟶ ℂ$
134	133	3ad2ant1	$⊢ (((φ \land a \in S) \land m \in ℕ_{0}) \land i \in (0 \dots m) \land y \in B) \to A : ℕ_{0} ⟶ ℂ$
135	21	adantr	$⊢ ((φ \land a \in S) \land m \in ℕ_{0}) \to B \subseteq ℂ$
136	135	sselda	$⊢ (((φ \land a \in S) \land m \in ℕ_{0}) \land y \in B) \to y \in ℂ$
137	136	3adant2	$⊢ (((φ \land a \in S) \land m \in ℕ_{0}) \land i \in (0 \dots m) \land y \in B) \to y \in ℂ$
138	1 134 137	psergf	$⊢ (((φ \land a \in S) \land m \in ℕ_{0}) \land i \in (0 \dots m) \land y \in B) \to G (y) : ℕ_{0} ⟶ ℂ$
139	104	3ad2ant2	$⊢ (((φ \land a \in S) \land m \in ℕ_{0}) \land i \in (0 \dots m) \land y \in B) \to i \in ℕ_{0}$
140	138 139	ffvelrnd	$⊢ (((φ \land a \in S) \land m \in ℕ_{0}) \land i \in (0 \dots m) \land y \in B) \to G (y) (i) \in ℂ$
141	9	a1i	$⊢ (((φ \land a \in S) \land m \in ℕ_{0}) \land i \in (0 \dots m)) \to ℂ \in \{ℝ, ℂ\}$
142		ffvelrn	$⊢ (A : ℕ_{0} ⟶ ℂ \land i \in ℕ_{0}) \to A (i) \in ℂ$
143	133 104 142	syl2an	$⊢ (((φ \land a \in S) \land m \in ℕ_{0}) \land i \in (0 \dots m)) \to A (i) \in ℂ$
144	143	adantr	$⊢ ((((φ \land a \in S) \land m \in ℕ_{0}) \land i \in (0 \dots m)) \land y \in B) \to A (i) \in ℂ$
145	136	adantlr	$⊢ ((((φ \land a \in S) \land m \in ℕ_{0}) \land i \in (0 \dots m)) \land y \in B) \to y \in ℂ$
146		id	$⊢ y \in ℂ \to y \in ℂ$
147	104	adantl	$⊢ (((φ \land a \in S) \land m \in ℕ_{0}) \land i \in (0 \dots m)) \to i \in ℕ_{0}$
148		expcl	$⊢ (y \in ℂ \land i \in ℕ_{0}) \to y^{i} \in ℂ$
149	146 147 148	syl2anr	$⊢ ((((φ \land a \in S) \land m \in ℕ_{0}) \land i \in (0 \dots m)) \land y \in ℂ) \to y^{i} \in ℂ$
150	145 149	syldan	$⊢ ((((φ \land a \in S) \land m \in ℕ_{0}) \land i \in (0 \dots m)) \land y \in B) \to y^{i} \in ℂ$
151	144 150	mulcld	$⊢ ((((φ \land a \in S) \land m \in ℕ_{0}) \land i \in (0 \dots m)) \land y \in B) \to A (i) y^{i} \in ℂ$
152		ovexd	$⊢ ((((φ \land a \in S) \land m \in ℕ_{0}) \land i \in (0 \dots m)) \land y \in B) \to A (i) if (i = 0, 0, i y^{i - 1}) \in V$
153		c0ex	$⊢ 0 \in V$
154		ovex	$⊢ i y^{i - 1} \in V$
155	153 154	ifex	$⊢ if (i = 0, 0, i y^{i - 1}) \in V$
156	155	a1i	$⊢ ((((φ \land a \in S) \land m \in ℕ_{0}) \land i \in (0 \dots m)) \land y \in B) \to if (i = 0, 0, i y^{i - 1}) \in V$
157	155	a1i	$⊢ ((((φ \land a \in S) \land m \in ℕ_{0}) \land i \in (0 \dots m)) \land y \in ℂ) \to if (i = 0, 0, i y^{i - 1}) \in V$
158		dvexp2	$⊢ i \in ℕ_{0} \to \frac{d (y \in ℂ⟼ y^{i})}{d_{ℂ} y} = (y \in ℂ ⟼ if (i = 0, 0, i y^{i - 1}))$
159	147 158	syl	$⊢ (((φ \land a \in S) \land m \in ℕ_{0}) \land i \in (0 \dots m)) \to \frac{d (y \in ℂ⟼ y^{i})}{d_{ℂ} y} = (y \in ℂ ⟼ if (i = 0, 0, i y^{i - 1}))$
160	21	ad2antrr	$⊢ (((φ \land a \in S) \land m \in ℕ_{0}) \land i \in (0 \dots m)) \to B \subseteq ℂ$
161	130	ad2antrr	$⊢ (((φ \land a \in S) \land m \in ℕ_{0}) \land i \in (0 \dots m)) \to B \in TopOpen (ℂ_{fld})$
162	141 149 157 159 160 125 123 161	dvmptres	$⊢ (((φ \land a \in S) \land m \in ℕ_{0}) \land i \in (0 \dots m)) \to \frac{d (y \in B⟼ y^{i})}{d_{ℂ} y} = (y \in B ⟼ if (i = 0, 0, i y^{i - 1}))$
163	141 150 156 162 143	dvmptcmul	$⊢ (((φ \land a \in S) \land m \in ℕ_{0}) \land i \in (0 \dots m)) \to \frac{d (y \in B⟼ A (i) y^{i})}{d_{ℂ} y} = (y \in B ⟼ A (i) if (i = 0, 0, i y^{i - 1}))$
164	141 151 152 163	dvmptcl	$⊢ ((((φ \land a \in S) \land m \in ℕ_{0}) \land i \in (0 \dots m)) \land y \in B) \to A (i) if (i = 0, 0, i y^{i - 1}) \in ℂ$
165	164	3impa	$⊢ (((φ \land a \in S) \land m \in ℕ_{0}) \land i \in (0 \dots m) \land y \in B) \to A (i) if (i = 0, 0, i y^{i - 1}) \in ℂ$
166	104	ad2antlr	$⊢ ((((φ \land a \in S) \land m \in ℕ_{0}) \land i \in (0 \dots m)) \land y \in B) \to i \in ℕ_{0}$
167	1	pserval2	$⊢ (y \in ℂ \land i \in ℕ_{0}) \to G (y) (i) = A (i) y^{i}$
168	145 166 167	syl2anc	$⊢ ((((φ \land a \in S) \land m \in ℕ_{0}) \land i \in (0 \dots m)) \land y \in B) \to G (y) (i) = A (i) y^{i}$
169	168	mpteq2dva	$⊢ (((φ \land a \in S) \land m \in ℕ_{0}) \land i \in (0 \dots m)) \to (y \in B ⟼ G (y) (i)) = (y \in B ⟼ A (i) y^{i})$
170	169	oveq2d	$⊢ (((φ \land a \in S) \land m \in ℕ_{0}) \land i \in (0 \dots m)) \to \frac{d (y \in B⟼ G (y) (i))}{d_{ℂ} y} = \frac{d (y \in B⟼ A (i) y^{i})}{d_{ℂ} y}$
171	170 163	eqtrd	$⊢ (((φ \land a \in S) \land m \in ℕ_{0}) \land i \in (0 \dots m)) \to \frac{d (y \in B⟼ G (y) (i))}{d_{ℂ} y} = (y \in B ⟼ A (i) if (i = 0, 0, i y^{i - 1}))$
172	125 123 126 131 132 140 165 171	dvmptfsum	$⊢ ((φ \land a \in S) \land m \in ℕ_{0}) \to \frac{d (y \in B⟼ \sum_{i = 0}^{m} G (y) (i))}{d_{ℂ} y} = (y \in B ⟼ \sum_{i = 0}^{m} A (i) if (i = 0, 0, i y^{i - 1}))$
173	122 172	eqtrd	$⊢ ((φ \land a \in S) \land m \in ℕ_{0}) \to ℂ D (k \in ℕ_{0} ⟼ (y \in B ⟼ \sum_{i = 0}^{k} G (y) (i))) (m) = (y \in B ⟼ \sum_{i = 0}^{m} A (i) if (i = 0, 0, i y^{i - 1}))$
174	173	mpteq2dva	$⊢ (φ \land a \in S) \to (m \in ℕ_{0} ⟼ ℂ D (k \in ℕ_{0} ⟼ (y \in B ⟼ \sum_{i = 0}^{k} G (y) (i))) (m)) = (m \in ℕ_{0} ⟼ (y \in B ⟼ \sum_{i = 0}^{m} A (i) if (i = 0, 0, i y^{i - 1})))$
175		nnssnn0	$⊢ ℕ \subseteq ℕ_{0}$
176		resmpt	$⊢ ℕ \subseteq ℕ_{0} \to {(m \in ℕ_{0} ⟼ (y \in B ⟼ \sum_{i = 0}^{m} A (i) if (i = 0, 0, i y^{i - 1}))) ↾}_{ℕ} = (m \in ℕ ⟼ (y \in B ⟼ \sum_{i = 0}^{m} A (i) if (i = 0, 0, i y^{i - 1})))$
177	175 176	ax-mp	$⊢ {(m \in ℕ_{0} ⟼ (y \in B ⟼ \sum_{i = 0}^{m} A (i) if (i = 0, 0, i y^{i - 1}))) ↾}_{ℕ} = (m \in ℕ ⟼ (y \in B ⟼ \sum_{i = 0}^{m} A (i) if (i = 0, 0, i y^{i - 1})))$
178		oveq1	$⊢ a = x \to a^{i} = x^{i}$
179	178	oveq2d	$⊢ a = x \to (i + 1) A (i + 1) a^{i} = (i + 1) A (i + 1) x^{i}$
180	179	mpteq2dv	$⊢ a = x \to (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i}) = (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) x^{i})$
181		oveq1	$⊢ i = n \to i + 1 = n + 1$
182		fvoveq1	$⊢ i = n \to A (i + 1) = A (n + 1)$
183	181 182	oveq12d	$⊢ i = n \to (i + 1) A (i + 1) = (n + 1) A (n + 1)$
184		oveq2	$⊢ i = n \to x^{i} = x^{n}$
185	183 184	oveq12d	$⊢ i = n \to (i + 1) A (i + 1) x^{i} = (n + 1) A (n + 1) x^{n}$
186	185	cbvmptv	$⊢ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) x^{i}) = (n \in ℕ_{0} ⟼ (n + 1) A (n + 1) x^{n})$
187		oveq1	$⊢ m = n \to m + 1 = n + 1$
188		fvoveq1	$⊢ m = n \to A (m + 1) = A (n + 1)$
189	187 188	oveq12d	$⊢ m = n \to (m + 1) A (m + 1) = (n + 1) A (n + 1)$
190		eqid	$⊢ (m \in ℕ_{0} ⟼ (m + 1) A (m + 1)) = (m \in ℕ_{0} ⟼ (m + 1) A (m + 1))$
191		ovex	$⊢ (n + 1) A (n + 1) \in V$
192	189 190 191	fvmpt	$⊢ n \in ℕ_{0} \to (m \in ℕ_{0} ⟼ (m + 1) A (m + 1)) (n) = (n + 1) A (n + 1)$
193	192	oveq1d	$⊢ n \in ℕ_{0} \to (m \in ℕ_{0} ⟼ (m + 1) A (m + 1)) (n) x^{n} = (n + 1) A (n + 1) x^{n}$
194	193	mpteq2ia	$⊢ (n \in ℕ_{0} ⟼ (m \in ℕ_{0} ⟼ (m + 1) A (m + 1)) (n) x^{n}) = (n \in ℕ_{0} ⟼ (n + 1) A (n + 1) x^{n})$
195	186 194	eqtr4i	$⊢ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) x^{i}) = (n \in ℕ_{0} ⟼ (m \in ℕ_{0} ⟼ (m + 1) A (m + 1)) (n) x^{n})$
196	180 195	eqtrdi	$⊢ a = x \to (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i}) = (n \in ℕ_{0} ⟼ (m \in ℕ_{0} ⟼ (m + 1) A (m + 1)) (n) x^{n})$
197	196	cbvmptv	$⊢ (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) = (x \in ℂ ⟼ (n \in ℕ_{0} ⟼ (m \in ℕ_{0} ⟼ (m + 1) A (m + 1)) (n) x^{n}))$
198		fveq2	$⊢ y = z \to (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (y) = (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (z)$
199	198	fveq1d	$⊢ y = z \to (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (y) (k) = (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (z) (k)$
200	199	sumeq2sdv	$⊢ y = z \to \sum_{k \in ℕ_{0}} (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (y) (k) = \sum_{k \in ℕ_{0}} (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (z) (k)$
201	200	cbvmptv	$⊢ (y \in B ⟼ \sum_{k \in ℕ_{0}} (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (y) (k)) = (z \in B ⟼ \sum_{k \in ℕ_{0}} (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (z) (k))$
202		peano2nn0	$⊢ m \in ℕ_{0} \to m + 1 \in ℕ_{0}$
203	202	adantl	$⊢ ((φ \land a \in S) \land m \in ℕ_{0}) \to m + 1 \in ℕ_{0}$
204	203	nn0cnd	$⊢ ((φ \land a \in S) \land m \in ℕ_{0}) \to m + 1 \in ℂ$
205	133 203	ffvelrnd	$⊢ ((φ \land a \in S) \land m \in ℕ_{0}) \to A (m + 1) \in ℂ$
206	204 205	mulcld	$⊢ ((φ \land a \in S) \land m \in ℕ_{0}) \to (m + 1) A (m + 1) \in ℂ$
207	206	fmpttd	$⊢ (φ \land a \in S) \to (m \in ℕ_{0} ⟼ (m + 1) A (m + 1)) : ℕ_{0} ⟶ ℂ$
208		fveq2	$⊢ r = j \to (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (r) = (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (j)$
209	208	seqeq3d	$⊢ r = j \to seq 0 (+ (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (r)) = seq 0 (+ (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (j))$
210	209	eleq1d	$⊢ r = j \to (seq 0 (+ (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (r)) \in dom ⇝ \leftrightarrow seq 0 (+ (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (j)) \in dom ⇝)$
211	210	cbvrabv	$⊢ \{r \in ℝ \| seq 0 (+ (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (r)) \in dom ⇝\} = \{j \in ℝ \| seq 0 (+ (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (j)) \in dom ⇝\}$
212	211	supeq1i	$⊢ sup (\{r \in ℝ \| seq 0 (+ (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (r)) \in dom ⇝\} ℝ^{} <) = sup (\{j \in ℝ \| seq 0 (+ (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (j)) \in dom ⇝\} ℝ^{} <)$
213	198	seqeq3d	$⊢ y = z \to seq 0 (+ (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (y)) = seq 0 (+ (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (z))$
214	213	fveq1d	$⊢ y = z \to seq 0 (+ (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (y)) (j) = seq 0 (+ (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (z)) (j)$
215	214	cbvmptv	$⊢ (y \in B ⟼ seq 0 (+ (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (y)) (j)) = (z \in B ⟼ seq 0 (+ (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (z)) (j))$
216		fveq2	$⊢ j = m \to seq 0 (+ (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (z)) (j) = seq 0 (+ (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (z)) (m)$
217	216	mpteq2dv	$⊢ j = m \to (z \in B ⟼ seq 0 (+ (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (z)) (j)) = (z \in B ⟼ seq 0 (+ (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (z)) (m))$
218	215 217	eqtrid	$⊢ j = m \to (y \in B ⟼ seq 0 (+ (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (y)) (j)) = (z \in B ⟼ seq 0 (+ (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (z)) (m))$
219	218	cbvmptv	$⊢ (j \in ℕ_{0} ⟼ (y \in B ⟼ seq 0 (+ (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (y)) (j))) = (m \in ℕ_{0} ⟼ (z \in B ⟼ seq 0 (+ (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (z)) (m)))$
220	17	rpred	$⊢ (φ \land a \in S) \to \frac{\|a\| + M}{2} \in ℝ$
221	1 2 3 4 5 6	psercnlem1	$⊢ (φ \land a \in S) \to (M \in ℝ^{+} \land \|a\| < M \land M < R)$
222	221	simp1d	$⊢ (φ \land a \in S) \to M \in ℝ^{+}$
223	222	rpxrd	$⊢ (φ \land a \in S) \to M \in ℝ^{*}$
224	197 207 212	radcnvcl	$⊢ (φ \land a \in S) \to sup (\{r \in ℝ \| seq 0 (+ (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (r)) \in dom ⇝\} ℝ^{*} <) \in [0, +∞]$
225	54 224	sselid	$⊢ (φ \land a \in S) \to sup (\{r \in ℝ \| seq 0 (+ (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (r)) \in dom ⇝\} ℝ^{} <) \in ℝ^{}$
226	221	simp2d	$⊢ (φ \land a \in S) \to \|a\| < M$
227		cnvimass	$⊢ {abs}^{-1} [[0, R)] \subseteq dom abs$
228		absf	$⊢ abs : ℂ ⟶ ℝ$
229	228	fdmi	$⊢ dom abs = ℂ$
230	227 229	sseqtri	$⊢ {abs}^{-1} [[0, R)] \subseteq ℂ$
231	5 230	eqsstri	$⊢ S \subseteq ℂ$
232	231	a1i	$⊢ φ \to S \subseteq ℂ$
233	232	sselda	$⊢ (φ \land a \in S) \to a \in ℂ$
234	233	abscld	$⊢ (φ \land a \in S) \to \|a\| \in ℝ$
235	222	rpred	$⊢ (φ \land a \in S) \to M \in ℝ$
236		avglt2	$⊢ (\|a\| \in ℝ \land M \in ℝ) \to (\|a\| < M \leftrightarrow \frac{\|a\| + M}{2} < M)$
237	234 235 236	syl2anc	$⊢ (φ \land a \in S) \to (\|a\| < M \leftrightarrow \frac{\|a\| + M}{2} < M)$
238	226 237	mpbid	$⊢ (φ \land a \in S) \to \frac{\|a\| + M}{2} < M$
239	222	rpge0d	$⊢ (φ \land a \in S) \to 0 \leq M$
240	235 239	absidd	$⊢ (φ \land a \in S) \to \|M\| = M$
241	222	rpcnd	$⊢ (φ \land a \in S) \to M \in ℂ$
242		oveq1	$⊢ w = M \to w^{i} = M^{i}$
243	242	oveq2d	$⊢ w = M \to (i + 1) A (i + 1) w^{i} = (i + 1) A (i + 1) M^{i}$
244	243	mpteq2dv	$⊢ w = M \to (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) w^{i}) = (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) M^{i})$
245		oveq1	$⊢ a = w \to a^{i} = w^{i}$
246	245	oveq2d	$⊢ a = w \to (i + 1) A (i + 1) a^{i} = (i + 1) A (i + 1) w^{i}$
247	246	mpteq2dv	$⊢ a = w \to (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i}) = (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) w^{i})$
248	247	cbvmptv	$⊢ (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) = (w \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) w^{i}))$
249		nn0ex	$⊢ ℕ_{0} \in V$
250	249	mptex	$⊢ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) M^{i}) \in V$
251	244 248 250	fvmpt	$⊢ M \in ℂ \to (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (M) = (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) M^{i})$
252	241 251	syl	$⊢ (φ \land a \in S) \to (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (M) = (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) M^{i})$
253	252	seqeq3d	$⊢ (φ \land a \in S) \to seq 0 (+ (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (M)) = seq 0 (+ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) M^{i}))$
254		fveq2	$⊢ n = i \to A (n) = A (i)$
255		oveq2	$⊢ n = i \to x^{n} = x^{i}$
256	254 255	oveq12d	$⊢ n = i \to A (n) x^{n} = A (i) x^{i}$
257	256	cbvmptv	$⊢ (n \in ℕ_{0} ⟼ A (n) x^{n}) = (i \in ℕ_{0} ⟼ A (i) x^{i})$
258		oveq1	$⊢ x = y \to x^{i} = y^{i}$
259	258	oveq2d	$⊢ x = y \to A (i) x^{i} = A (i) y^{i}$
260	259	mpteq2dv	$⊢ x = y \to (i \in ℕ_{0} ⟼ A (i) x^{i}) = (i \in ℕ_{0} ⟼ A (i) y^{i})$
261	257 260	eqtrid	$⊢ x = y \to (n \in ℕ_{0} ⟼ A (n) x^{n}) = (i \in ℕ_{0} ⟼ A (i) y^{i})$
262	261	cbvmptv	$⊢ (x \in ℂ ⟼ (n \in ℕ_{0} ⟼ A (n) x^{n})) = (y \in ℂ ⟼ (i \in ℕ_{0} ⟼ A (i) y^{i}))$
263	1 262	eqtri	$⊢ G = (y \in ℂ ⟼ (i \in ℕ_{0} ⟼ A (i) y^{i}))$
264		fveq2	$⊢ r = s \to G (r) = G (s)$
265	264	seqeq3d	$⊢ r = s \to seq 0 (+ G (r)) = seq 0 (+ G (s))$
266	265	eleq1d	$⊢ r = s \to (seq 0 (+ G (r)) \in dom ⇝ \leftrightarrow seq 0 (+ G (s)) \in dom ⇝)$
267	266	cbvrabv	$⊢ \{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\} = \{s \in ℝ \| seq 0 (+ G (s)) \in dom ⇝\}$
268	267	supeq1i	$⊢ sup (\{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\} ℝ^{} <) = sup (\{s \in ℝ \| seq 0 (+ G (s)) \in dom ⇝\} ℝ^{} <)$
269	4 268	eqtri	$⊢ R = sup (\{s \in ℝ \| seq 0 (+ G (s)) \in dom ⇝\} ℝ^{*} <)$
270		eqid	$⊢ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) M^{i}) = (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) M^{i})$
271	3	adantr	$⊢ (φ \land a \in S) \to A : ℕ_{0} ⟶ ℂ$
272	221	simp3d	$⊢ (φ \land a \in S) \to M < R$
273	240 272	eqbrtrd	$⊢ (φ \land a \in S) \to \|M\| < R$
274	263 269 270 271 241 273	dvradcnv	$⊢ (φ \land a \in S) \to seq 0 (+ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) M^{i})) \in dom ⇝$
275	253 274	eqeltrd	$⊢ (φ \land a \in S) \to seq 0 (+ (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (M)) \in dom ⇝$
276	197 207 212 241 275	radcnvle	$⊢ (φ \land a \in S) \to \|M\| \leq sup (\{r \in ℝ \| seq 0 (+ (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (r)) \in dom ⇝\} ℝ^{*} <)$
277	240 276	eqbrtrrd	$⊢ (φ \land a \in S) \to M \leq sup (\{r \in ℝ \| seq 0 (+ (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (r)) \in dom ⇝\} ℝ^{*} <)$
278	18 223 225 238 277	xrltletrd	$⊢ (φ \land a \in S) \to \frac{\|a\| + M}{2} < sup (\{r \in ℝ \| seq 0 (+ (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (r)) \in dom ⇝\} ℝ^{*} <)$
279	197 201 207 212 219 220 278 41	pserulm	$⊢ (φ \land a \in S) \to (j \in ℕ_{0} ⟼ (y \in B ⟼ seq 0 (+ (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (y)) (j))) \underset{u}{⇝} (B) (y \in B ⟼ \sum_{k \in ℕ_{0}} (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (y) (k))$
280	21	sselda	$⊢ ((φ \land a \in S) \land y \in B) \to y \in ℂ$
281		oveq1	$⊢ a = y \to a^{i} = y^{i}$
282	281	oveq2d	$⊢ a = y \to (i + 1) A (i + 1) a^{i} = (i + 1) A (i + 1) y^{i}$
283	282	mpteq2dv	$⊢ a = y \to (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i}) = (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) y^{i})$
284		eqid	$⊢ (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) = (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i}))$
285	249	mptex	$⊢ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) y^{i}) \in V$
286	283 284 285	fvmpt	$⊢ y \in ℂ \to (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (y) = (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) y^{i})$
287	280 286	syl	$⊢ ((φ \land a \in S) \land y \in B) \to (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (y) = (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) y^{i})$
288	287	adantr	$⊢ (((φ \land a \in S) \land y \in B) \land k \in ℕ_{0}) \to (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (y) = (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) y^{i})$
289	288	fveq1d	$⊢ (((φ \land a \in S) \land y \in B) \land k \in ℕ_{0}) \to (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (y) (k) = (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) y^{i}) (k)$
290		oveq1	$⊢ i = k \to i + 1 = k + 1$
291		fvoveq1	$⊢ i = k \to A (i + 1) = A (k + 1)$
292	290 291	oveq12d	$⊢ i = k \to (i + 1) A (i + 1) = (k + 1) A (k + 1)$
293		oveq2	$⊢ i = k \to y^{i} = y^{k}$
294	292 293	oveq12d	$⊢ i = k \to (i + 1) A (i + 1) y^{i} = (k + 1) A (k + 1) y^{k}$
295		eqid	$⊢ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) y^{i}) = (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) y^{i})$
296		ovex	$⊢ (k + 1) A (k + 1) y^{k} \in V$
297	294 295 296	fvmpt	$⊢ k \in ℕ_{0} \to (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) y^{i}) (k) = (k + 1) A (k + 1) y^{k}$
298	297	adantl	$⊢ (((φ \land a \in S) \land y \in B) \land k \in ℕ_{0}) \to (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) y^{i}) (k) = (k + 1) A (k + 1) y^{k}$
299	289 298	eqtrd	$⊢ (((φ \land a \in S) \land y \in B) \land k \in ℕ_{0}) \to (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (y) (k) = (k + 1) A (k + 1) y^{k}$
300	299	sumeq2dv	$⊢ ((φ \land a \in S) \land y \in B) \to \sum_{k \in ℕ_{0}} (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (y) (k) = \sum_{k \in ℕ_{0}} (k + 1) A (k + 1) y^{k}$
301	300	mpteq2dva	$⊢ (φ \land a \in S) \to (y \in B ⟼ \sum_{k \in ℕ_{0}} (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (y) (k)) = (y \in B ⟼ \sum_{k \in ℕ_{0}} (k + 1) A (k + 1) y^{k})$
302	279 301	breqtrd	$⊢ (φ \land a \in S) \to (j \in ℕ_{0} ⟼ (y \in B ⟼ seq 0 (+ (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (y)) (j))) \underset{u}{⇝} (B) (y \in B ⟼ \sum_{k \in ℕ_{0}} (k + 1) A (k + 1) y^{k})$
303		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
304		1e0p1	$⊢ 1 = 0 + 1$
305	304	fveq2i	$⊢ ℤ_{\geq 1} = ℤ_{\geq (0 + 1)}$
306	303 305	eqtri	$⊢ ℕ = ℤ_{\geq (0 + 1)}$
307		1zzd	$⊢ (φ \land a \in S) \to 1 \in ℤ$
308		0zd	$⊢ ((φ \land a \in S) \land y \in B) \to 0 \in ℤ$
309		peano2nn0	$⊢ i \in ℕ_{0} \to i + 1 \in ℕ_{0}$
310	309	nn0cnd	$⊢ i \in ℕ_{0} \to i + 1 \in ℂ$
311	310	adantl	$⊢ (((φ \land a \in S) \land y \in B) \land i \in ℕ_{0}) \to i + 1 \in ℂ$
312	3	ad2antrr	$⊢ ((φ \land a \in S) \land y \in B) \to A : ℕ_{0} ⟶ ℂ$
313		ffvelrn	$⊢ (A : ℕ_{0} ⟶ ℂ \land i + 1 \in ℕ_{0}) \to A (i + 1) \in ℂ$
314	312 309 313	syl2an	$⊢ (((φ \land a \in S) \land y \in B) \land i \in ℕ_{0}) \to A (i + 1) \in ℂ$
315	311 314	mulcld	$⊢ (((φ \land a \in S) \land y \in B) \land i \in ℕ_{0}) \to (i + 1) A (i + 1) \in ℂ$
316	280 148	sylan	$⊢ (((φ \land a \in S) \land y \in B) \land i \in ℕ_{0}) \to y^{i} \in ℂ$
317	315 316	mulcld	$⊢ (((φ \land a \in S) \land y \in B) \land i \in ℕ_{0}) \to (i + 1) A (i + 1) y^{i} \in ℂ$
318	287 317	fmpt3d	$⊢ ((φ \land a \in S) \land y \in B) \to (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (y) : ℕ_{0} ⟶ ℂ$
319	318	ffvelrnda	$⊢ (((φ \land a \in S) \land y \in B) \land m \in ℕ_{0}) \to (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (y) (m) \in ℂ$
320	8 308 319	serf	$⊢ ((φ \land a \in S) \land y \in B) \to seq 0 (+ (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (y)) : ℕ_{0} ⟶ ℂ$
321	320	ffvelrnda	$⊢ (((φ \land a \in S) \land y \in B) \land j \in ℕ_{0}) \to seq 0 (+ (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (y)) (j) \in ℂ$
322	321	an32s	$⊢ (((φ \land a \in S) \land j \in ℕ_{0}) \land y \in B) \to seq 0 (+ (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (y)) (j) \in ℂ$
323	322	fmpttd	$⊢ ((φ \land a \in S) \land j \in ℕ_{0}) \to (y \in B ⟼ seq 0 (+ (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (y)) (j)) : B ⟶ ℂ$
324	30 31	elmap	$⊢ (y \in B ⟼ seq 0 (+ (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (y)) (j)) \in (ℂ^{B}) \leftrightarrow (y \in B ⟼ seq 0 (+ (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (y)) (j)) : B ⟶ ℂ$
325	323 324	sylibr	$⊢ ((φ \land a \in S) \land j \in ℕ_{0}) \to (y \in B ⟼ seq 0 (+ (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (y)) (j)) \in (ℂ^{B})$
326	325	fmpttd	$⊢ (φ \land a \in S) \to (j \in ℕ_{0} ⟼ (y \in B ⟼ seq 0 (+ (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (y)) (j))) : ℕ_{0} ⟶ ℂ^{B}$
327		elfznn	$⊢ i \in (1 \dots m) \to i \in ℕ$
328	327	nnne0d	$⊢ i \in (1 \dots m) \to i \neq 0$
329	328	neneqd	$⊢ i \in (1 \dots m) \to \neg i = 0$
330	329	iffalsed	$⊢ i \in (1 \dots m) \to if (i = 0, 0, i y^{i - 1}) = i y^{i - 1}$
331	330	oveq2d	$⊢ i \in (1 \dots m) \to A (i) if (i = 0, 0, i y^{i - 1}) = A (i) i y^{i - 1}$
332	331	sumeq2i	$⊢ \sum_{i = 1}^{m} A (i) if (i = 0, 0, i y^{i - 1}) = \sum_{i = 1}^{m} A (i) i y^{i - 1}$
333		1zzd	$⊢ (((φ \land a \in S) \land m \in ℕ) \land y \in B) \to 1 \in ℤ$
334		nnz	$⊢ m \in ℕ \to m \in ℤ$
335	334	ad2antlr	$⊢ (((φ \land a \in S) \land m \in ℕ) \land y \in B) \to m \in ℤ$
336	271	ad2antrr	$⊢ (((φ \land a \in S) \land m \in ℕ) \land y \in B) \to A : ℕ_{0} ⟶ ℂ$
337	327	nnnn0d	$⊢ i \in (1 \dots m) \to i \in ℕ_{0}$
338	336 337 142	syl2an	$⊢ ((((φ \land a \in S) \land m \in ℕ) \land y \in B) \land i \in (1 \dots m)) \to A (i) \in ℂ$
339	327	adantl	$⊢ ((((φ \land a \in S) \land m \in ℕ) \land y \in B) \land i \in (1 \dots m)) \to i \in ℕ$
340	339	nncnd	$⊢ ((((φ \land a \in S) \land m \in ℕ) \land y \in B) \land i \in (1 \dots m)) \to i \in ℂ$
341	280	adantlr	$⊢ (((φ \land a \in S) \land m \in ℕ) \land y \in B) \to y \in ℂ$
342		nnm1nn0	$⊢ i \in ℕ \to i - 1 \in ℕ_{0}$
343	327 342	syl	$⊢ i \in (1 \dots m) \to i - 1 \in ℕ_{0}$
344		expcl	$⊢ (y \in ℂ \land i - 1 \in ℕ_{0}) \to y^{i - 1} \in ℂ$
345	341 343 344	syl2an	$⊢ ((((φ \land a \in S) \land m \in ℕ) \land y \in B) \land i \in (1 \dots m)) \to y^{i - 1} \in ℂ$
346	340 345	mulcld	$⊢ ((((φ \land a \in S) \land m \in ℕ) \land y \in B) \land i \in (1 \dots m)) \to i y^{i - 1} \in ℂ$
347	338 346	mulcld	$⊢ ((((φ \land a \in S) \land m \in ℕ) \land y \in B) \land i \in (1 \dots m)) \to A (i) i y^{i - 1} \in ℂ$
348		fveq2	$⊢ i = k + 1 \to A (i) = A (k + 1)$
349		id	$⊢ i = k + 1 \to i = k + 1$
350		oveq1	$⊢ i = k + 1 \to i - 1 = k + 1 - 1$
351	350	oveq2d	$⊢ i = k + 1 \to y^{i - 1} = y^{k + 1 - 1}$
352	349 351	oveq12d	$⊢ i = k + 1 \to i y^{i - 1} = (k + 1) y^{k + 1 - 1}$
353	348 352	oveq12d	$⊢ i = k + 1 \to A (i) i y^{i - 1} = A (k + 1) (k + 1) y^{k + 1 - 1}$
354	333 333 335 347 353	fsumshftm	$⊢ (((φ \land a \in S) \land m \in ℕ) \land y \in B) \to \sum_{i = 1}^{m} A (i) i y^{i - 1} = \sum_{k = 1 - 1}^{m - 1} A (k + 1) (k + 1) y^{k + 1 - 1}$
355	332 354	eqtrid	$⊢ (((φ \land a \in S) \land m \in ℕ) \land y \in B) \to \sum_{i = 1}^{m} A (i) if (i = 0, 0, i y^{i - 1}) = \sum_{k = 1 - 1}^{m - 1} A (k + 1) (k + 1) y^{k + 1 - 1}$
356		fz1ssfz0	$⊢ (1 \dots m) \subseteq (0 \dots m)$
357	356	a1i	$⊢ (((φ \land a \in S) \land m \in ℕ) \land y \in B) \to (1 \dots m) \subseteq (0 \dots m)$
358	331	adantl	$⊢ ((((φ \land a \in S) \land m \in ℕ) \land y \in B) \land i \in (1 \dots m)) \to A (i) if (i = 0, 0, i y^{i - 1}) = A (i) i y^{i - 1}$
359	358 347	eqeltrd	$⊢ ((((φ \land a \in S) \land m \in ℕ) \land y \in B) \land i \in (1 \dots m)) \to A (i) if (i = 0, 0, i y^{i - 1}) \in ℂ$
360		eldif	$⊢ i \in ((0 \dots m) ∖ (0 + 1 \dots m)) \leftrightarrow (i \in (0 \dots m) \land \neg i \in (0 + 1 \dots m))$
361		elfzuz2	$⊢ i \in (0 \dots m) \to m \in ℤ_{\geq 0}$
362		elfzp12	$⊢ m \in ℤ_{\geq 0} \to (i \in (0 \dots m) \leftrightarrow (i = 0 \lor i \in (0 + 1 \dots m)))$
363	361 362	syl	$⊢ i \in (0 \dots m) \to (i \in (0 \dots m) \leftrightarrow (i = 0 \lor i \in (0 + 1 \dots m)))$
364	363	ibi	$⊢ i \in (0 \dots m) \to (i = 0 \lor i \in (0 + 1 \dots m))$
365	364	ord	$⊢ i \in (0 \dots m) \to (\neg i = 0 \to i \in (0 + 1 \dots m))$
366	365	con1d	$⊢ i \in (0 \dots m) \to (\neg i \in (0 + 1 \dots m) \to i = 0)$
367	366	imp	$⊢ (i \in (0 \dots m) \land \neg i \in (0 + 1 \dots m)) \to i = 0$
368	360 367	sylbi	$⊢ i \in ((0 \dots m) ∖ (0 + 1 \dots m)) \to i = 0$
369	304	oveq1i	$⊢ (1 \dots m) = (0 + 1 \dots m)$
370	369	difeq2i	$⊢ (0 \dots m) ∖ (1 \dots m) = (0 \dots m) ∖ (0 + 1 \dots m)$
371	368 370	eleq2s	$⊢ i \in ((0 \dots m) ∖ (1 \dots m)) \to i = 0$
372	371	adantl	$⊢ ((((φ \land a \in S) \land m \in ℕ) \land y \in B) \land i \in ((0 \dots m) ∖ (1 \dots m))) \to i = 0$
373	372	iftrued	$⊢ ((((φ \land a \in S) \land m \in ℕ) \land y \in B) \land i \in ((0 \dots m) ∖ (1 \dots m))) \to if (i = 0, 0, i y^{i - 1}) = 0$
374	373	oveq2d	$⊢ ((((φ \land a \in S) \land m \in ℕ) \land y \in B) \land i \in ((0 \dots m) ∖ (1 \dots m))) \to A (i) if (i = 0, 0, i y^{i - 1}) = A (i) \cdot 0$
375		eldifi	$⊢ i \in ((0 \dots m) ∖ (1 \dots m)) \to i \in (0 \dots m)$
376	375 104	syl	$⊢ i \in ((0 \dots m) ∖ (1 \dots m)) \to i \in ℕ_{0}$
377	336 376 142	syl2an	$⊢ ((((φ \land a \in S) \land m \in ℕ) \land y \in B) \land i \in ((0 \dots m) ∖ (1 \dots m))) \to A (i) \in ℂ$
378	377	mul01d	$⊢ ((((φ \land a \in S) \land m \in ℕ) \land y \in B) \land i \in ((0 \dots m) ∖ (1 \dots m))) \to A (i) \cdot 0 = 0$
379	374 378	eqtrd	$⊢ ((((φ \land a \in S) \land m \in ℕ) \land y \in B) \land i \in ((0 \dots m) ∖ (1 \dots m))) \to A (i) if (i = 0, 0, i y^{i - 1}) = 0$
380		fzfid	$⊢ (((φ \land a \in S) \land m \in ℕ) \land y \in B) \to (0 \dots m) \in Fin$
381	357 359 379 380	fsumss	$⊢ (((φ \land a \in S) \land m \in ℕ) \land y \in B) \to \sum_{i = 1}^{m} A (i) if (i = 0, 0, i y^{i - 1}) = \sum_{i = 0}^{m} A (i) if (i = 0, 0, i y^{i - 1})$
382		1m1e0	$⊢ 1 - 1 = 0$
383	382	oveq1i	$⊢ (1 - 1 \dots m - 1) = (0 \dots m - 1)$
384	383	sumeq1i	$⊢ \sum_{k = 1 - 1}^{m - 1} A (k + 1) (k + 1) y^{k + 1 - 1} = \sum_{k = 0}^{m - 1} A (k + 1) (k + 1) y^{k + 1 - 1}$
385		elfznn0	$⊢ k \in (0 \dots m - 1) \to k \in ℕ_{0}$
386	385	adantl	$⊢ ((((φ \land a \in S) \land m \in ℕ) \land y \in B) \land k \in (0 \dots m - 1)) \to k \in ℕ_{0}$
387	386 297	syl	$⊢ ((((φ \land a \in S) \land m \in ℕ) \land y \in B) \land k \in (0 \dots m - 1)) \to (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) y^{i}) (k) = (k + 1) A (k + 1) y^{k}$
388	341	adantr	$⊢ ((((φ \land a \in S) \land m \in ℕ) \land y \in B) \land k \in (0 \dots m - 1)) \to y \in ℂ$
389	388 286	syl	$⊢ ((((φ \land a \in S) \land m \in ℕ) \land y \in B) \land k \in (0 \dots m - 1)) \to (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (y) = (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) y^{i})$
390	389	fveq1d	$⊢ ((((φ \land a \in S) \land m \in ℕ) \land y \in B) \land k \in (0 \dots m - 1)) \to (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (y) (k) = (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) y^{i}) (k)$
391	336	adantr	$⊢ ((((φ \land a \in S) \land m \in ℕ) \land y \in B) \land k \in (0 \dots m - 1)) \to A : ℕ_{0} ⟶ ℂ$
392		peano2nn0	$⊢ k \in ℕ_{0} \to k + 1 \in ℕ_{0}$
393	386 392	syl	$⊢ ((((φ \land a \in S) \land m \in ℕ) \land y \in B) \land k \in (0 \dots m - 1)) \to k + 1 \in ℕ_{0}$
394	391 393	ffvelrnd	$⊢ ((((φ \land a \in S) \land m \in ℕ) \land y \in B) \land k \in (0 \dots m - 1)) \to A (k + 1) \in ℂ$
395	393	nn0cnd	$⊢ ((((φ \land a \in S) \land m \in ℕ) \land y \in B) \land k \in (0 \dots m - 1)) \to k + 1 \in ℂ$
396		expcl	$⊢ (y \in ℂ \land k \in ℕ_{0}) \to y^{k} \in ℂ$
397	341 385 396	syl2an	$⊢ ((((φ \land a \in S) \land m \in ℕ) \land y \in B) \land k \in (0 \dots m - 1)) \to y^{k} \in ℂ$
398	394 395 397	mul12d	$⊢ ((((φ \land a \in S) \land m \in ℕ) \land y \in B) \land k \in (0 \dots m - 1)) \to A (k + 1) (k + 1) y^{k} = (k + 1) A (k + 1) y^{k}$
399	386	nn0cnd	$⊢ ((((φ \land a \in S) \land m \in ℕ) \land y \in B) \land k \in (0 \dots m - 1)) \to k \in ℂ$
400		ax-1cn	$⊢ 1 \in ℂ$
401		pncan	$⊢ (k \in ℂ \land 1 \in ℂ) \to k + 1 - 1 = k$
402	399 400 401	sylancl	$⊢ ((((φ \land a \in S) \land m \in ℕ) \land y \in B) \land k \in (0 \dots m - 1)) \to k + 1 - 1 = k$
403	402	oveq2d	$⊢ ((((φ \land a \in S) \land m \in ℕ) \land y \in B) \land k \in (0 \dots m - 1)) \to y^{k + 1 - 1} = y^{k}$
404	403	oveq2d	$⊢ ((((φ \land a \in S) \land m \in ℕ) \land y \in B) \land k \in (0 \dots m - 1)) \to (k + 1) y^{k + 1 - 1} = (k + 1) y^{k}$
405	404	oveq2d	$⊢ ((((φ \land a \in S) \land m \in ℕ) \land y \in B) \land k \in (0 \dots m - 1)) \to A (k + 1) (k + 1) y^{k + 1 - 1} = A (k + 1) (k + 1) y^{k}$
406	395 394 397	mulassd	$⊢ ((((φ \land a \in S) \land m \in ℕ) \land y \in B) \land k \in (0 \dots m - 1)) \to (k + 1) A (k + 1) y^{k} = (k + 1) A (k + 1) y^{k}$
407	398 405 406	3eqtr4d	$⊢ ((((φ \land a \in S) \land m \in ℕ) \land y \in B) \land k \in (0 \dots m - 1)) \to A (k + 1) (k + 1) y^{k + 1 - 1} = (k + 1) A (k + 1) y^{k}$
408	387 390 407	3eqtr4d	$⊢ ((((φ \land a \in S) \land m \in ℕ) \land y \in B) \land k \in (0 \dots m - 1)) \to (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (y) (k) = A (k + 1) (k + 1) y^{k + 1 - 1}$
409		nnm1nn0	$⊢ m \in ℕ \to m - 1 \in ℕ_{0}$
410	409	adantl	$⊢ ((φ \land a \in S) \land m \in ℕ) \to m - 1 \in ℕ_{0}$
411	410	adantr	$⊢ (((φ \land a \in S) \land m \in ℕ) \land y \in B) \to m - 1 \in ℕ_{0}$
412	411 8	eleqtrdi	$⊢ (((φ \land a \in S) \land m \in ℕ) \land y \in B) \to m - 1 \in ℤ_{\geq 0}$
413	403 397	eqeltrd	$⊢ ((((φ \land a \in S) \land m \in ℕ) \land y \in B) \land k \in (0 \dots m - 1)) \to y^{k + 1 - 1} \in ℂ$
414	395 413	mulcld	$⊢ ((((φ \land a \in S) \land m \in ℕ) \land y \in B) \land k \in (0 \dots m - 1)) \to (k + 1) y^{k + 1 - 1} \in ℂ$
415	394 414	mulcld	$⊢ ((((φ \land a \in S) \land m \in ℕ) \land y \in B) \land k \in (0 \dots m - 1)) \to A (k + 1) (k + 1) y^{k + 1 - 1} \in ℂ$
416	408 412 415	fsumser	$⊢ (((φ \land a \in S) \land m \in ℕ) \land y \in B) \to \sum_{k = 0}^{m - 1} A (k + 1) (k + 1) y^{k + 1 - 1} = seq 0 (+ (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (y)) (m - 1)$
417	384 416	eqtrid	$⊢ (((φ \land a \in S) \land m \in ℕ) \land y \in B) \to \sum_{k = 1 - 1}^{m - 1} A (k + 1) (k + 1) y^{k + 1 - 1} = seq 0 (+ (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (y)) (m - 1)$
418	355 381 417	3eqtr3d	$⊢ (((φ \land a \in S) \land m \in ℕ) \land y \in B) \to \sum_{i = 0}^{m} A (i) if (i = 0, 0, i y^{i - 1}) = seq 0 (+ (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (y)) (m - 1)$
419	418	mpteq2dva	$⊢ ((φ \land a \in S) \land m \in ℕ) \to (y \in B ⟼ \sum_{i = 0}^{m} A (i) if (i = 0, 0, i y^{i - 1})) = (y \in B ⟼ seq 0 (+ (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (y)) (m - 1))$
420		fveq2	$⊢ j = m - 1 \to seq 0 (+ (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (y)) (j) = seq 0 (+ (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (y)) (m - 1)$
421	420	mpteq2dv	$⊢ j = m - 1 \to (y \in B ⟼ seq 0 (+ (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (y)) (j)) = (y \in B ⟼ seq 0 (+ (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (y)) (m - 1))$
422		eqid	$⊢ (j \in ℕ_{0} ⟼ (y \in B ⟼ seq 0 (+ (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (y)) (j))) = (j \in ℕ_{0} ⟼ (y \in B ⟼ seq 0 (+ (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (y)) (j)))$
423	31	mptex	$⊢ (y \in B ⟼ seq 0 (+ (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (y)) (m - 1)) \in V$
424	421 422 423	fvmpt	$⊢ m - 1 \in ℕ_{0} \to (j \in ℕ_{0} ⟼ (y \in B ⟼ seq 0 (+ (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (y)) (j))) (m - 1) = (y \in B ⟼ seq 0 (+ (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (y)) (m - 1))$
425	410 424	syl	$⊢ ((φ \land a \in S) \land m \in ℕ) \to (j \in ℕ_{0} ⟼ (y \in B ⟼ seq 0 (+ (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (y)) (j))) (m - 1) = (y \in B ⟼ seq 0 (+ (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (y)) (m - 1))$
426	419 425	eqtr4d	$⊢ ((φ \land a \in S) \land m \in ℕ) \to (y \in B ⟼ \sum_{i = 0}^{m} A (i) if (i = 0, 0, i y^{i - 1})) = (j \in ℕ_{0} ⟼ (y \in B ⟼ seq 0 (+ (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (y)) (j))) (m - 1)$
427	426	mpteq2dva	$⊢ (φ \land a \in S) \to (m \in ℕ ⟼ (y \in B ⟼ \sum_{i = 0}^{m} A (i) if (i = 0, 0, i y^{i - 1}))) = (m \in ℕ ⟼ (j \in ℕ_{0} ⟼ (y \in B ⟼ seq 0 (+ (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (y)) (j))) (m - 1))$
428	8 306 11 307 326 427	ulmshft	$⊢ (φ \land a \in S) \to ((j \in ℕ_{0} ⟼ (y \in B ⟼ seq 0 (+ (a \in ℂ ⟼ (i \in ℕ_{0} ⟼ (i + 1) A (i + 1) a^{i})) (y)) (j))) \underset{u}{⇝} (B) (y \in B ⟼ \sum_{k \in ℕ_{0}} (k + 1) A (k + 1) y^{k}) \leftrightarrow (m \in ℕ ⟼ (y \in B ⟼ \sum_{i = 0}^{m} A (i) if (i = 0, 0, i y^{i - 1}))) \underset{u}{⇝} (B) (y \in B ⟼ \sum_{k \in ℕ_{0}} (k + 1) A (k + 1) y^{k}))$
429	302 428	mpbid	$⊢ (φ \land a \in S) \to (m \in ℕ ⟼ (y \in B ⟼ \sum_{i = 0}^{m} A (i) if (i = 0, 0, i y^{i - 1}))) \underset{u}{⇝} (B) (y \in B ⟼ \sum_{k \in ℕ_{0}} (k + 1) A (k + 1) y^{k})$
430	177 429	eqbrtrid	$⊢ (φ \land a \in S) \to ({(m \in ℕ_{0} ⟼ (y \in B ⟼ \sum_{i = 0}^{m} A (i) if (i = 0, 0, i y^{i - 1}))) ↾}_{ℕ}) \underset{u}{⇝} (B) (y \in B ⟼ \sum_{k \in ℕ_{0}} (k + 1) A (k + 1) y^{k})$
431		1nn0	$⊢ 1 \in ℕ_{0}$
432	431	a1i	$⊢ (φ \land a \in S) \to 1 \in ℕ_{0}$
433		fzfid	$⊢ (((φ \land a \in S) \land m \in ℕ_{0}) \land y \in B) \to (0 \dots m) \in Fin$
434	164	an32s	$⊢ ((((φ \land a \in S) \land m \in ℕ_{0}) \land y \in B) \land i \in (0 \dots m)) \to A (i) if (i = 0, 0, i y^{i - 1}) \in ℂ$
435	433 434	fsumcl	$⊢ (((φ \land a \in S) \land m \in ℕ_{0}) \land y \in B) \to \sum_{i = 0}^{m} A (i) if (i = 0, 0, i y^{i - 1}) \in ℂ$
436	435	fmpttd	$⊢ ((φ \land a \in S) \land m \in ℕ_{0}) \to (y \in B ⟼ \sum_{i = 0}^{m} A (i) if (i = 0, 0, i y^{i - 1})) : B ⟶ ℂ$
437	30 31	elmap	$⊢ (y \in B ⟼ \sum_{i = 0}^{m} A (i) if (i = 0, 0, i y^{i - 1})) \in (ℂ^{B}) \leftrightarrow (y \in B ⟼ \sum_{i = 0}^{m} A (i) if (i = 0, 0, i y^{i - 1})) : B ⟶ ℂ$
438	436 437	sylibr	$⊢ ((φ \land a \in S) \land m \in ℕ_{0}) \to (y \in B ⟼ \sum_{i = 0}^{m} A (i) if (i = 0, 0, i y^{i - 1})) \in (ℂ^{B})$
439	438	fmpttd	$⊢ (φ \land a \in S) \to (m \in ℕ_{0} ⟼ (y \in B ⟼ \sum_{i = 0}^{m} A (i) if (i = 0, 0, i y^{i - 1}))) : ℕ_{0} ⟶ ℂ^{B}$
440	8 303 432 439	ulmres	$⊢ (φ \land a \in S) \to ((m \in ℕ_{0} ⟼ (y \in B ⟼ \sum_{i = 0}^{m} A (i) if (i = 0, 0, i y^{i - 1}))) \underset{u}{⇝} (B) (y \in B ⟼ \sum_{k \in ℕ_{0}} (k + 1) A (k + 1) y^{k}) \leftrightarrow ({(m \in ℕ_{0} ⟼ (y \in B ⟼ \sum_{i = 0}^{m} A (i) if (i = 0, 0, i y^{i - 1}))) ↾}_{ℕ}) \underset{u}{⇝} (B) (y \in B ⟼ \sum_{k \in ℕ_{0}} (k + 1) A (k + 1) y^{k}))$
441	430 440	mpbird	$⊢ (φ \land a \in S) \to (m \in ℕ_{0} ⟼ (y \in B ⟼ \sum_{i = 0}^{m} A (i) if (i = 0, 0, i y^{i - 1}))) \underset{u}{⇝} (B) (y \in B ⟼ \sum_{k \in ℕ_{0}} (k + 1) A (k + 1) y^{k})$
442	174 441	eqbrtrd	$⊢ (φ \land a \in S) \to (m \in ℕ_{0} ⟼ ℂ D (k \in ℕ_{0} ⟼ (y \in B ⟼ \sum_{i = 0}^{k} G (y) (i))) (m)) \underset{u}{⇝} (B) (y \in B ⟼ \sum_{k \in ℕ_{0}} (k + 1) A (k + 1) y^{k})$
443	8 10 11 34 44 120 442	ulmdv	$⊢ (φ \land a \in S) \to ℂ D ({F ↾}_{B}) = (y \in B ⟼ \sum_{k \in ℕ_{0}} (k + 1) A (k + 1) y^{k})$

Metamath Proof Explorer

Theorem pserdvlem2

Proof