Theorem abelthlem9

Description: Lemma for abelth . By adjusting the constant term, we can assume that the entire series converges to 0 . (Contributed by Mario Carneiro, 1-Apr-2015)

	Ref	Expression
Hypotheses	abelth.1	$$⊢\phi \to A:{\mathbb{N}}_0⟶ℂ$$
	abelth.2	$$⊢\phi \to seq0\left(+,A\right)\in \mathrm{dom}⇝$$
	abelth.3	$$⊢\phi \to M\in ℝ$$
	abelth.4	$$⊢\phi \to 0\le M$$
	abelth.5	$$⊢S=\left\{z\in ℂ|\left|1-z\right|\le M\left(1-\left|z\right|\right)\right\}$$
	abelth.6	$$⊢F=\left(x\in S⟼\sum _{n\in {\mathbb{N}}_0}A\left(n\right)x^n\right)$$
Assertion	abelthlem9	$$⊢\left(\phi \wedge R\in {ℝ}^{+}\right)\to \exists w\in {ℝ}^{+}\forall y\in S\left(\left|1-y\right|<w\to \left|F\left(1\right)-F\left(y\right)\right|<R\right)$$

Proof

Step	Hyp	Ref	Expression
1		abelth.1	$$⊢\phi \to A:{\mathbb{N}}_0⟶ℂ$$
2		abelth.2	$$⊢\phi \to seq0\left(+,A\right)\in \mathrm{dom}⇝$$
3		abelth.3	$$⊢\phi \to M\in ℝ$$
4		abelth.4	$$⊢\phi \to 0\le M$$
5		abelth.5	$$⊢S=\left\{z\in ℂ|\left|1-z\right|\le M\left(1-\left|z\right|\right)\right\}$$
6		abelth.6	$$⊢F=\left(x\in S⟼\sum _{n\in {\mathbb{N}}_0}A\left(n\right)x^n\right)$$
7		0nn0	$$⊢0\in {\mathbb{N}}_0$$
8	7	a1i	$$⊢k\in {\mathbb{N}}_0\to 0\in {\mathbb{N}}_0$$
9		ffvelcdm	$$⊢\left(A:{\mathbb{N}}_0⟶ℂ\wedge 0\in {\mathbb{N}}_0\right)\to A\left(0\right)\in ℂ$$
10	1 8 9	syl2an	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to A\left(0\right)\in ℂ$$
11		nn0uz	$$⊢{\mathbb{N}}_0={\mathbb{Z}}_{\ge 0}$$
12		0zd	$$⊢\phi \to 0\in \mathbb{Z}$$
13		eqidd	$$⊢\left(\phi \wedge m\in {\mathbb{N}}_0\right)\to A\left(m\right)=A\left(m\right)$$
14	1	ffvelcdmda	$$⊢\left(\phi \wedge m\in {\mathbb{N}}_0\right)\to A\left(m\right)\in ℂ$$
15	11 12 13 14 2	isumcl	$$⊢\phi \to \sum _{m\in {\mathbb{N}}_0}A\left(m\right)\in ℂ$$
16	15	adantr	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to \sum _{m\in {\mathbb{N}}_0}A\left(m\right)\in ℂ$$
17	10 16	subcld	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right)\in ℂ$$
18	1	ffvelcdmda	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to A\left(k\right)\in ℂ$$
19	17 18	ifcld	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)\in ℂ$$
20	19	fmpttd	$$⊢\phi \to \left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)\right):{\mathbb{N}}_0⟶ℂ$$
21	7	a1i	$$⊢\phi \to 0\in {\mathbb{N}}_0$$
22	20	ffvelcdmda	$$⊢\left(\phi \wedge i\in {\mathbb{N}}_0\right)\to \left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)\right)\left(i\right)\in ℂ$$
23		1e0p1	$$⊢1=0+1$$
24		1z	$$⊢1\in \mathbb{Z}$$
25	23 24	eqeltrri	$$⊢0+1\in \mathbb{Z}$$
26	25	a1i	$$⊢\phi \to 0+1\in \mathbb{Z}$$
27		nnuz	$$⊢\mathbb{N}={\mathbb{Z}}_{\ge 1}$$
28	23	fveq2i	$$⊢{\mathbb{Z}}_{\ge 1}={\mathbb{Z}}_{\ge \left(0+1\right)}$$
29	27 28	eqtri	$$⊢\mathbb{N}={\mathbb{Z}}_{\ge \left(0+1\right)}$$
30	29	eleq2i	$$⊢i\in \mathbb{N}\leftrightarrow i\in {\mathbb{Z}}_{\ge \left(0+1\right)}$$
31		nnnn0	$$⊢i\in \mathbb{N}\to i\in {\mathbb{N}}_0$$
32	31	adantl	$$⊢\left(\phi \wedge i\in \mathbb{N}\right)\to i\in {\mathbb{N}}_0$$
33		eqeq1	$$⊢k=i\to \left(k=0\leftrightarrow i=0\right)$$
34		fveq2	$$⊢k=i\to A\left(k\right)=A\left(i\right)$$
35	33 34	ifbieq2d	$$⊢k=i\to if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)=if\left(i=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(i\right)\right)$$
36		eqid	$$⊢\left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)\right)=\left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)\right)$$
37		ovex	$$⊢A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right)\in \mathrm{V}$$
38		fvex	$$⊢A\left(i\right)\in \mathrm{V}$$
39	37 38	ifex	$$⊢if\left(i=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(i\right)\right)\in \mathrm{V}$$
40	35 36 39	fvmpt	$$⊢i\in {\mathbb{N}}_0\to \left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)\right)\left(i\right)=if\left(i=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(i\right)\right)$$
41	32 40	syl	$$⊢\left(\phi \wedge i\in \mathbb{N}\right)\to \left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)\right)\left(i\right)=if\left(i=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(i\right)\right)$$
42		nnne0	$$⊢i\in \mathbb{N}\to i\ne 0$$
43	42	adantl	$$⊢\left(\phi \wedge i\in \mathbb{N}\right)\to i\ne 0$$
44	43	neneqd	$$⊢\left(\phi \wedge i\in \mathbb{N}\right)\to \neg i=0$$
45	44	iffalsed	$$⊢\left(\phi \wedge i\in \mathbb{N}\right)\to if\left(i=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(i\right)\right)=A\left(i\right)$$
46	41 45	eqtrd	$$⊢\left(\phi \wedge i\in \mathbb{N}\right)\to \left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)\right)\left(i\right)=A\left(i\right)$$
47	30 46	sylan2br	$$⊢\left(\phi \wedge i\in {\mathbb{Z}}_{\ge \left(0+1\right)}\right)\to \left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)\right)\left(i\right)=A\left(i\right)$$
48	26 47	seqfeq	$$⊢\phi \to seq\left(0+1\right)\left(+,\left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)\right)\right)=seq\left(0+1\right)\left(+,A\right)$$
49	11 12 13 14 2	isumclim2	$$⊢\phi \to seq0\left(+,A\right)⇝\sum _{m\in {\mathbb{N}}_0}A\left(m\right)$$
50	11 21 18 49	clim2ser	$$⊢\phi \to seq\left(0+1\right)\left(+,A\right)⇝\left(\sum _{m\in {\mathbb{N}}_0}A\left(m\right)-seq0\left(+,A\right)\left(0\right)\right)$$
51		0z	$$⊢0\in \mathbb{Z}$$
52		seq1	$$⊢0\in \mathbb{Z}\to seq0\left(+,A\right)\left(0\right)=A\left(0\right)$$
53	51 52	ax-mp	$$⊢seq0\left(+,A\right)\left(0\right)=A\left(0\right)$$
54	53	oveq2i	$$⊢\sum _{m\in {\mathbb{N}}_0}A\left(m\right)-seq0\left(+,A\right)\left(0\right)=\sum _{m\in {\mathbb{N}}_0}A\left(m\right)-A\left(0\right)$$
55	50 54	breqtrdi	$$⊢\phi \to seq\left(0+1\right)\left(+,A\right)⇝\left(\sum _{m\in {\mathbb{N}}_0}A\left(m\right)-A\left(0\right)\right)$$
56	48 55	eqbrtrd	$$⊢\phi \to seq\left(0+1\right)\left(+,\left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)\right)\right)⇝\left(\sum _{m\in {\mathbb{N}}_0}A\left(m\right)-A\left(0\right)\right)$$
57	11 21 22 56	clim2ser2	$$⊢\phi \to seq0\left(+,\left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)\right)\right)⇝\left(\sum _{m\in {\mathbb{N}}_0}A\left(m\right)-A\left(0\right)+seq0\left(+,\left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)\right)\right)\left(0\right)\right)$$
58		seq1	$$⊢0\in \mathbb{Z}\to seq0\left(+,\left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)\right)\right)\left(0\right)=\left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)\right)\left(0\right)$$
59	51 58	ax-mp	$$⊢seq0\left(+,\left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)\right)\right)\left(0\right)=\left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)\right)\left(0\right)$$
60		iftrue	$$⊢k=0\to if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)=A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right)$$
61	60 36 37	fvmpt	$$⊢0\in {\mathbb{N}}_0\to \left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)\right)\left(0\right)=A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right)$$
62	7 61	ax-mp	$$⊢\left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)\right)\left(0\right)=A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right)$$
63	59 62	eqtri	$$⊢seq0\left(+,\left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)\right)\right)\left(0\right)=A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right)$$
64	63	oveq2i	$$⊢\sum _{m\in {\mathbb{N}}_0}A\left(m\right)-A\left(0\right)+seq0\left(+,\left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)\right)\right)\left(0\right)=\left(\sum _{m\in {\mathbb{N}}_0}A\left(m\right)-A\left(0\right)\right)+A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right)$$
65	1 7 9	sylancl	$$⊢\phi \to A\left(0\right)\in ℂ$$
66		npncan2	$$⊢\left(\sum _{m\in {\mathbb{N}}_0}A\left(m\right)\in ℂ\wedge A\left(0\right)\in ℂ\right)\to \left(\sum _{m\in {\mathbb{N}}_0}A\left(m\right)-A\left(0\right)\right)+A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right)=0$$
67	15 65 66	syl2anc	$$⊢\phi \to \left(\sum _{m\in {\mathbb{N}}_0}A\left(m\right)-A\left(0\right)\right)+A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right)=0$$
68	64 67	eqtrid	$$⊢\phi \to \sum _{m\in {\mathbb{N}}_0}A\left(m\right)-A\left(0\right)+seq0\left(+,\left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)\right)\right)\left(0\right)=0$$
69	57 68	breqtrd	$$⊢\phi \to seq0\left(+,\left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)\right)\right)⇝0$$
70		seqex	$$⊢seq0\left(+,\left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)\right)\right)\in \mathrm{V}$$
71		c0ex	$$⊢0\in \mathrm{V}$$
72	70 71	breldm	$$⊢seq0\left(+,\left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)\right)\right)⇝0\to seq0\left(+,\left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)\right)\right)\in \mathrm{dom}⇝$$
73	69 72	syl	$$⊢\phi \to seq0\left(+,\left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)\right)\right)\in \mathrm{dom}⇝$$
74		eqid	$$⊢\left(x\in S⟼\sum _{i\in {\mathbb{N}}_0}\left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)\right)\left(i\right)x^i\right)=\left(x\in S⟼\sum _{i\in {\mathbb{N}}_0}\left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)\right)\left(i\right)x^i\right)$$
75	20 73 3 4 5 74 69	abelthlem8	$$⊢\left(\phi \wedge R\in {ℝ}^{+}\right)\to \exists w\in {ℝ}^{+}\forall y\in S\left(\left|1-y\right|<w\to \left|\left(x\in S⟼\sum _{i\in {\mathbb{N}}_0}\left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)\right)\left(i\right)x^i\right)\left(1\right)-\left(x\in S⟼\sum _{i\in {\mathbb{N}}_0}\left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)\right)\left(i\right)x^i\right)\left(y\right)\right|<R\right)$$
76	1 2 3 4 5	abelthlem2	$$⊢\phi \to \left(1\in S\wedge S\setminus \left\{1\right\}\subseteq 0\mathrm{ball}\left(\mathrm{abs}\circ -\right)1\right)$$
77	76	simpld	$$⊢\phi \to 1\in S$$
78	77	adantr	$$⊢\left(\phi \wedge y\in S\right)\to 1\in S$$
79	40	adantl	$$⊢\left(x=1\wedge i\in {\mathbb{N}}_0\right)\to \left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)\right)\left(i\right)=if\left(i=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(i\right)\right)$$
80		oveq1	$$⊢x=1\to x^i=1^i$$
81		nn0z	$$⊢i\in {\mathbb{N}}_0\to i\in \mathbb{Z}$$
82		1exp	$$⊢i\in \mathbb{Z}\to 1^i=1$$
83	81 82	syl	$$⊢i\in {\mathbb{N}}_0\to 1^i=1$$
84	80 83	sylan9eq	$$⊢\left(x=1\wedge i\in {\mathbb{N}}_0\right)\to x^i=1$$
85	79 84	oveq12d	$$⊢\left(x=1\wedge i\in {\mathbb{N}}_0\right)\to \left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)\right)\left(i\right)x^i=if\left(i=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(i\right)\right)\cdot 1$$
86	85	sumeq2dv	$$⊢x=1\to \sum _{i\in {\mathbb{N}}_0}\left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)\right)\left(i\right)x^i=\sum _{i\in {\mathbb{N}}_0}if\left(i=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(i\right)\right)\cdot 1$$
87		sumex	$$⊢\sum _{i\in {\mathbb{N}}_0}if\left(i=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(i\right)\right)\cdot 1\in \mathrm{V}$$
88	86 74 87	fvmpt	$$⊢1\in S\to \left(x\in S⟼\sum _{i\in {\mathbb{N}}_0}\left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)\right)\left(i\right)x^i\right)\left(1\right)=\sum _{i\in {\mathbb{N}}_0}if\left(i=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(i\right)\right)\cdot 1$$
89	78 88	syl	$$⊢\left(\phi \wedge y\in S\right)\to \left(x\in S⟼\sum _{i\in {\mathbb{N}}_0}\left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)\right)\left(i\right)x^i\right)\left(1\right)=\sum _{i\in {\mathbb{N}}_0}if\left(i=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(i\right)\right)\cdot 1$$
90		0zd	$$⊢\left(\phi \wedge y\in S\right)\to 0\in \mathbb{Z}$$
91	40	adantl	$$⊢\left(\left(\phi \wedge y\in S\right)\wedge i\in {\mathbb{N}}_0\right)\to \left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)\right)\left(i\right)=if\left(i=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(i\right)\right)$$
92	65 15	subcld	$$⊢\phi \to A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right)\in ℂ$$
93	92	ad2antrr	$$⊢\left(\left(\phi \wedge y\in S\right)\wedge i\in {\mathbb{N}}_0\right)\to A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right)\in ℂ$$
94	1	ffvelcdmda	$$⊢\left(\phi \wedge i\in {\mathbb{N}}_0\right)\to A\left(i\right)\in ℂ$$
95	94	adantlr	$$⊢\left(\left(\phi \wedge y\in S\right)\wedge i\in {\mathbb{N}}_0\right)\to A\left(i\right)\in ℂ$$
96	93 95	ifcld	$$⊢\left(\left(\phi \wedge y\in S\right)\wedge i\in {\mathbb{N}}_0\right)\to if\left(i=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(i\right)\right)\in ℂ$$
97	96	mulridd	$$⊢\left(\left(\phi \wedge y\in S\right)\wedge i\in {\mathbb{N}}_0\right)\to if\left(i=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(i\right)\right)\cdot 1=if\left(i=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(i\right)\right)$$
98	91 97	eqtr4d	$$⊢\left(\left(\phi \wedge y\in S\right)\wedge i\in {\mathbb{N}}_0\right)\to \left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)\right)\left(i\right)=if\left(i=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(i\right)\right)\cdot 1$$
99	97 96	eqeltrd	$$⊢\left(\left(\phi \wedge y\in S\right)\wedge i\in {\mathbb{N}}_0\right)\to if\left(i=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(i\right)\right)\cdot 1\in ℂ$$
100		oveq1	$$⊢x=1\to x^n=1^n$$
101		nn0z	$$⊢n\in {\mathbb{N}}_0\to n\in \mathbb{Z}$$
102		1exp	$$⊢n\in \mathbb{Z}\to 1^n=1$$
103	101 102	syl	$$⊢n\in {\mathbb{N}}_0\to 1^n=1$$
104	100 103	sylan9eq	$$⊢\left(x=1\wedge n\in {\mathbb{N}}_0\right)\to x^n=1$$
105	104	oveq2d	$$⊢\left(x=1\wedge n\in {\mathbb{N}}_0\right)\to A\left(n\right)x^n=A\left(n\right)\cdot 1$$
106	105	sumeq2dv	$$⊢x=1\to \sum _{n\in {\mathbb{N}}_0}A\left(n\right)x^n=\sum _{n\in {\mathbb{N}}_0}A\left(n\right)\cdot 1$$
107		fveq2	$$⊢n=m\to A\left(n\right)=A\left(m\right)$$
108	107	oveq1d	$$⊢n=m\to A\left(n\right)\cdot 1=A\left(m\right)\cdot 1$$
109	108	cbvsumv	$$⊢\sum _{n\in {\mathbb{N}}_0}A\left(n\right)\cdot 1=\sum _{m\in {\mathbb{N}}_0}A\left(m\right)\cdot 1$$
110	106 109	eqtrdi	$$⊢x=1\to \sum _{n\in {\mathbb{N}}_0}A\left(n\right)x^n=\sum _{m\in {\mathbb{N}}_0}A\left(m\right)\cdot 1$$
111		sumex	$$⊢\sum _{m\in {\mathbb{N}}_0}A\left(m\right)\cdot 1\in \mathrm{V}$$
112	110 6 111	fvmpt	$$⊢1\in S\to F\left(1\right)=\sum _{m\in {\mathbb{N}}_0}A\left(m\right)\cdot 1$$
113	77 112	syl	$$⊢\phi \to F\left(1\right)=\sum _{m\in {\mathbb{N}}_0}A\left(m\right)\cdot 1$$
114	14	mulridd	$$⊢\left(\phi \wedge m\in {\mathbb{N}}_0\right)\to A\left(m\right)\cdot 1=A\left(m\right)$$
115	114	sumeq2dv	$$⊢\phi \to \sum _{m\in {\mathbb{N}}_0}A\left(m\right)\cdot 1=\sum _{m\in {\mathbb{N}}_0}A\left(m\right)$$
116	113 115	eqtrd	$$⊢\phi \to F\left(1\right)=\sum _{m\in {\mathbb{N}}_0}A\left(m\right)$$
117	116	oveq1d	$$⊢\phi \to F\left(1\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right)=\sum _{m\in {\mathbb{N}}_0}A\left(m\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right)$$
118	15	subidd	$$⊢\phi \to \sum _{m\in {\mathbb{N}}_0}A\left(m\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right)=0$$
119	117 118	eqtrd	$$⊢\phi \to F\left(1\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right)=0$$
120	69 119	breqtrrd	$$⊢\phi \to seq0\left(+,\left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)\right)\right)⇝\left(F\left(1\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right)\right)$$
121	120	adantr	$$⊢\left(\phi \wedge y\in S\right)\to seq0\left(+,\left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)\right)\right)⇝\left(F\left(1\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right)\right)$$
122	11 90 98 99 121	isumclim	$$⊢\left(\phi \wedge y\in S\right)\to \sum _{i\in {\mathbb{N}}_0}if\left(i=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(i\right)\right)\cdot 1=F\left(1\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right)$$
123	89 122	eqtrd	$$⊢\left(\phi \wedge y\in S\right)\to \left(x\in S⟼\sum _{i\in {\mathbb{N}}_0}\left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)\right)\left(i\right)x^i\right)\left(1\right)=F\left(1\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right)$$
124		oveq1	$$⊢x=y\to x^i=y^i$$
125	40 124	oveqan12rd	$$⊢\left(x=y\wedge i\in {\mathbb{N}}_0\right)\to \left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)\right)\left(i\right)x^i=if\left(i=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(i\right)\right)y^i$$
126	125	sumeq2dv	$$⊢x=y\to \sum _{i\in {\mathbb{N}}_0}\left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)\right)\left(i\right)x^i=\sum _{i\in {\mathbb{N}}_0}if\left(i=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(i\right)\right)y^i$$
127		sumex	$$⊢\sum _{i\in {\mathbb{N}}_0}if\left(i=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(i\right)\right)y^i\in \mathrm{V}$$
128	126 74 127	fvmpt	$$⊢y\in S\to \left(x\in S⟼\sum _{i\in {\mathbb{N}}_0}\left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)\right)\left(i\right)x^i\right)\left(y\right)=\sum _{i\in {\mathbb{N}}_0}if\left(i=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(i\right)\right)y^i$$
129	128	adantl	$$⊢\left(\phi \wedge y\in S\right)\to \left(x\in S⟼\sum _{i\in {\mathbb{N}}_0}\left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)\right)\left(i\right)x^i\right)\left(y\right)=\sum _{i\in {\mathbb{N}}_0}if\left(i=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(i\right)\right)y^i$$
130		oveq2	$$⊢k=i\to y^k=y^i$$
131	35 130	oveq12d	$$⊢k=i\to if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)y^k=if\left(i=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(i\right)\right)y^i$$
132		eqid	$$⊢\left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)y^k\right)=\left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)y^k\right)$$
133		ovex	$$⊢if\left(i=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(i\right)\right)y^i\in \mathrm{V}$$
134	131 132 133	fvmpt	$$⊢i\in {\mathbb{N}}_0\to \left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)y^k\right)\left(i\right)=if\left(i=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(i\right)\right)y^i$$
135	134	adantl	$$⊢\left(\left(\phi \wedge y\in S\right)\wedge i\in {\mathbb{N}}_0\right)\to \left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)y^k\right)\left(i\right)=if\left(i=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(i\right)\right)y^i$$
136	5	ssrab3	$$⊢S\subseteq ℂ$$
137	136	a1i	$$⊢\phi \to S\subseteq ℂ$$
138	137	sselda	$$⊢\left(\phi \wedge y\in S\right)\to y\in ℂ$$
139		expcl	$$⊢\left(y\in ℂ\wedge i\in {\mathbb{N}}_0\right)\to y^i\in ℂ$$
140	138 139	sylan	$$⊢\left(\left(\phi \wedge y\in S\right)\wedge i\in {\mathbb{N}}_0\right)\to y^i\in ℂ$$
141	96 140	mulcld	$$⊢\left(\left(\phi \wedge y\in S\right)\wedge i\in {\mathbb{N}}_0\right)\to if\left(i=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(i\right)\right)y^i\in ℂ$$
142	7	a1i	$$⊢\left(\phi \wedge y\in S\right)\to 0\in {\mathbb{N}}_0$$
143	19	adantlr	$$⊢\left(\left(\phi \wedge y\in S\right)\wedge k\in {\mathbb{N}}_0\right)\to if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)\in ℂ$$
144		expcl	$$⊢\left(y\in ℂ\wedge k\in {\mathbb{N}}_0\right)\to y^k\in ℂ$$
145	138 144	sylan	$$⊢\left(\left(\phi \wedge y\in S\right)\wedge k\in {\mathbb{N}}_0\right)\to y^k\in ℂ$$
146	143 145	mulcld	$$⊢\left(\left(\phi \wedge y\in S\right)\wedge k\in {\mathbb{N}}_0\right)\to if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)y^k\in ℂ$$
147	146	fmpttd	$$⊢\left(\phi \wedge y\in S\right)\to \left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)y^k\right):{\mathbb{N}}_0⟶ℂ$$
148	147	ffvelcdmda	$$⊢\left(\left(\phi \wedge y\in S\right)\wedge i\in {\mathbb{N}}_0\right)\to \left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)y^k\right)\left(i\right)\in ℂ$$
149	45	oveq1d	$$⊢\left(\phi \wedge i\in \mathbb{N}\right)\to if\left(i=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(i\right)\right)y^i=A\left(i\right)y^i$$
150	32 134	syl	$$⊢\left(\phi \wedge i\in \mathbb{N}\right)\to \left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)y^k\right)\left(i\right)=if\left(i=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(i\right)\right)y^i$$
151	34 130	oveq12d	$$⊢k=i\to A\left(k\right)y^k=A\left(i\right)y^i$$
152		eqid	$$⊢\left(k\in {\mathbb{N}}_0⟼A\left(k\right)y^k\right)=\left(k\in {\mathbb{N}}_0⟼A\left(k\right)y^k\right)$$
153		ovex	$$⊢A\left(i\right)y^i\in \mathrm{V}$$
154	151 152 153	fvmpt	$$⊢i\in {\mathbb{N}}_0\to \left(k\in {\mathbb{N}}_0⟼A\left(k\right)y^k\right)\left(i\right)=A\left(i\right)y^i$$
155	32 154	syl	$$⊢\left(\phi \wedge i\in \mathbb{N}\right)\to \left(k\in {\mathbb{N}}_0⟼A\left(k\right)y^k\right)\left(i\right)=A\left(i\right)y^i$$
156	149 150 155	3eqtr4d	$$⊢\left(\phi \wedge i\in \mathbb{N}\right)\to \left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)y^k\right)\left(i\right)=\left(k\in {\mathbb{N}}_0⟼A\left(k\right)y^k\right)\left(i\right)$$
157	30 156	sylan2br	$$⊢\left(\phi \wedge i\in {\mathbb{Z}}_{\ge \left(0+1\right)}\right)\to \left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)y^k\right)\left(i\right)=\left(k\in {\mathbb{N}}_0⟼A\left(k\right)y^k\right)\left(i\right)$$
158	26 157	seqfeq	$$⊢\phi \to seq\left(0+1\right)\left(+,\left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)y^k\right)\right)=seq\left(0+1\right)\left(+,\left(k\in {\mathbb{N}}_0⟼A\left(k\right)y^k\right)\right)$$
159	158	adantr	$$⊢\left(\phi \wedge y\in S\right)\to seq\left(0+1\right)\left(+,\left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)y^k\right)\right)=seq\left(0+1\right)\left(+,\left(k\in {\mathbb{N}}_0⟼A\left(k\right)y^k\right)\right)$$
160	18	adantlr	$$⊢\left(\left(\phi \wedge y\in S\right)\wedge k\in {\mathbb{N}}_0\right)\to A\left(k\right)\in ℂ$$
161	160 145	mulcld	$$⊢\left(\left(\phi \wedge y\in S\right)\wedge k\in {\mathbb{N}}_0\right)\to A\left(k\right)y^k\in ℂ$$
162	161	fmpttd	$$⊢\left(\phi \wedge y\in S\right)\to \left(k\in {\mathbb{N}}_0⟼A\left(k\right)y^k\right):{\mathbb{N}}_0⟶ℂ$$
163	162	ffvelcdmda	$$⊢\left(\left(\phi \wedge y\in S\right)\wedge i\in {\mathbb{N}}_0\right)\to \left(k\in {\mathbb{N}}_0⟼A\left(k\right)y^k\right)\left(i\right)\in ℂ$$
164	154	adantl	$$⊢\left(\left(\phi \wedge y\in S\right)\wedge i\in {\mathbb{N}}_0\right)\to \left(k\in {\mathbb{N}}_0⟼A\left(k\right)y^k\right)\left(i\right)=A\left(i\right)y^i$$
165	95 140	mulcld	$$⊢\left(\left(\phi \wedge y\in S\right)\wedge i\in {\mathbb{N}}_0\right)\to A\left(i\right)y^i\in ℂ$$
166	1 2 3 4 5	abelthlem3	$$⊢\left(\phi \wedge y\in S\right)\to seq0\left(+,\left(k\in {\mathbb{N}}_0⟼A\left(k\right)y^k\right)\right)\in \mathrm{dom}⇝$$
167	11 90 164 165 166	isumclim2	$$⊢\left(\phi \wedge y\in S\right)\to seq0\left(+,\left(k\in {\mathbb{N}}_0⟼A\left(k\right)y^k\right)\right)⇝\sum _{i\in {\mathbb{N}}_0}A\left(i\right)y^i$$
168		fveq2	$$⊢n=i\to A\left(n\right)=A\left(i\right)$$
169		oveq2	$$⊢n=i\to x^n=x^i$$
170	168 169	oveq12d	$$⊢n=i\to A\left(n\right)x^n=A\left(i\right)x^i$$
171	170	cbvsumv	$$⊢\sum _{n\in {\mathbb{N}}_0}A\left(n\right)x^n=\sum _{i\in {\mathbb{N}}_0}A\left(i\right)x^i$$
172	124	oveq2d	$$⊢x=y\to A\left(i\right)x^i=A\left(i\right)y^i$$
173	172	sumeq2sdv	$$⊢x=y\to \sum _{i\in {\mathbb{N}}_0}A\left(i\right)x^i=\sum _{i\in {\mathbb{N}}_0}A\left(i\right)y^i$$
174	171 173	eqtrid	$$⊢x=y\to \sum _{n\in {\mathbb{N}}_0}A\left(n\right)x^n=\sum _{i\in {\mathbb{N}}_0}A\left(i\right)y^i$$
175		sumex	$$⊢\sum _{i\in {\mathbb{N}}_0}A\left(i\right)y^i\in \mathrm{V}$$
176	174 6 175	fvmpt	$$⊢y\in S\to F\left(y\right)=\sum _{i\in {\mathbb{N}}_0}A\left(i\right)y^i$$
177	176	adantl	$$⊢\left(\phi \wedge y\in S\right)\to F\left(y\right)=\sum _{i\in {\mathbb{N}}_0}A\left(i\right)y^i$$
178	167 177	breqtrrd	$$⊢\left(\phi \wedge y\in S\right)\to seq0\left(+,\left(k\in {\mathbb{N}}_0⟼A\left(k\right)y^k\right)\right)⇝F\left(y\right)$$
179	11 142 163 178	clim2ser	$$⊢\left(\phi \wedge y\in S\right)\to seq\left(0+1\right)\left(+,\left(k\in {\mathbb{N}}_0⟼A\left(k\right)y^k\right)\right)⇝\left(F\left(y\right)-seq0\left(+,\left(k\in {\mathbb{N}}_0⟼A\left(k\right)y^k\right)\right)\left(0\right)\right)$$
180		seq1	$$⊢0\in \mathbb{Z}\to seq0\left(+,\left(k\in {\mathbb{N}}_0⟼A\left(k\right)y^k\right)\right)\left(0\right)=\left(k\in {\mathbb{N}}_0⟼A\left(k\right)y^k\right)\left(0\right)$$
181	51 180	ax-mp	$$⊢seq0\left(+,\left(k\in {\mathbb{N}}_0⟼A\left(k\right)y^k\right)\right)\left(0\right)=\left(k\in {\mathbb{N}}_0⟼A\left(k\right)y^k\right)\left(0\right)$$
182		fveq2	$$⊢k=0\to A\left(k\right)=A\left(0\right)$$
183		oveq2	$$⊢k=0\to y^k=y^0$$
184	182 183	oveq12d	$$⊢k=0\to A\left(k\right)y^k=A\left(0\right)y^0$$
185		ovex	$$⊢A\left(0\right)y^0\in \mathrm{V}$$
186	184 152 185	fvmpt	$$⊢0\in {\mathbb{N}}_0\to \left(k\in {\mathbb{N}}_0⟼A\left(k\right)y^k\right)\left(0\right)=A\left(0\right)y^0$$
187	7 186	ax-mp	$$⊢\left(k\in {\mathbb{N}}_0⟼A\left(k\right)y^k\right)\left(0\right)=A\left(0\right)y^0$$
188	181 187	eqtri	$$⊢seq0\left(+,\left(k\in {\mathbb{N}}_0⟼A\left(k\right)y^k\right)\right)\left(0\right)=A\left(0\right)y^0$$
189	138	exp0d	$$⊢\left(\phi \wedge y\in S\right)\to y^0=1$$
190	189	oveq2d	$$⊢\left(\phi \wedge y\in S\right)\to A\left(0\right)y^0=A\left(0\right)\cdot 1$$
191	65	adantr	$$⊢\left(\phi \wedge y\in S\right)\to A\left(0\right)\in ℂ$$
192	191	mulridd	$$⊢\left(\phi \wedge y\in S\right)\to A\left(0\right)\cdot 1=A\left(0\right)$$
193	190 192	eqtrd	$$⊢\left(\phi \wedge y\in S\right)\to A\left(0\right)y^0=A\left(0\right)$$
194	188 193	eqtrid	$$⊢\left(\phi \wedge y\in S\right)\to seq0\left(+,\left(k\in {\mathbb{N}}_0⟼A\left(k\right)y^k\right)\right)\left(0\right)=A\left(0\right)$$
195	194	oveq2d	$$⊢\left(\phi \wedge y\in S\right)\to F\left(y\right)-seq0\left(+,\left(k\in {\mathbb{N}}_0⟼A\left(k\right)y^k\right)\right)\left(0\right)=F\left(y\right)-A\left(0\right)$$
196	179 195	breqtrd	$$⊢\left(\phi \wedge y\in S\right)\to seq\left(0+1\right)\left(+,\left(k\in {\mathbb{N}}_0⟼A\left(k\right)y^k\right)\right)⇝\left(F\left(y\right)-A\left(0\right)\right)$$
197	159 196	eqbrtrd	$$⊢\left(\phi \wedge y\in S\right)\to seq\left(0+1\right)\left(+,\left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)y^k\right)\right)⇝\left(F\left(y\right)-A\left(0\right)\right)$$
198	11 142 148 197	clim2ser2	$$⊢\left(\phi \wedge y\in S\right)\to seq0\left(+,\left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)y^k\right)\right)⇝\left(F\left(y\right)-A\left(0\right)+seq0\left(+,\left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)y^k\right)\right)\left(0\right)\right)$$
199		seq1	$$⊢0\in \mathbb{Z}\to seq0\left(+,\left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)y^k\right)\right)\left(0\right)=\left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)y^k\right)\left(0\right)$$
200	51 199	ax-mp	$$⊢seq0\left(+,\left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)y^k\right)\right)\left(0\right)=\left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)y^k\right)\left(0\right)$$
201	60 183	oveq12d	$$⊢k=0\to if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)y^k=\left(A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right)\right)y^0$$
202		ovex	$$⊢\left(A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right)\right)y^0\in \mathrm{V}$$
203	201 132 202	fvmpt	$$⊢0\in {\mathbb{N}}_0\to \left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)y^k\right)\left(0\right)=\left(A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right)\right)y^0$$
204	7 203	ax-mp	$$⊢\left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)y^k\right)\left(0\right)=\left(A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right)\right)y^0$$
205	200 204	eqtri	$$⊢seq0\left(+,\left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)y^k\right)\right)\left(0\right)=\left(A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right)\right)y^0$$
206	189	oveq2d	$$⊢\left(\phi \wedge y\in S\right)\to \left(A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right)\right)y^0=\left(A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right)\right)\cdot 1$$
207	15	adantr	$$⊢\left(\phi \wedge y\in S\right)\to \sum _{m\in {\mathbb{N}}_0}A\left(m\right)\in ℂ$$
208	191 207	subcld	$$⊢\left(\phi \wedge y\in S\right)\to A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right)\in ℂ$$
209	208	mulridd	$$⊢\left(\phi \wedge y\in S\right)\to \left(A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right)\right)\cdot 1=A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right)$$
210	206 209	eqtrd	$$⊢\left(\phi \wedge y\in S\right)\to \left(A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right)\right)y^0=A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right)$$
211	205 210	eqtrid	$$⊢\left(\phi \wedge y\in S\right)\to seq0\left(+,\left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)y^k\right)\right)\left(0\right)=A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right)$$
212	211	oveq2d	$$⊢\left(\phi \wedge y\in S\right)\to F\left(y\right)-A\left(0\right)+seq0\left(+,\left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)y^k\right)\right)\left(0\right)=\left(F\left(y\right)-A\left(0\right)\right)+A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right)$$
213	1 2 3 4 5 6	abelthlem4	$$⊢\phi \to F:S⟶ℂ$$
214	213	ffvelcdmda	$$⊢\left(\phi \wedge y\in S\right)\to F\left(y\right)\in ℂ$$
215	214 191 207	npncand	$$⊢\left(\phi \wedge y\in S\right)\to \left(F\left(y\right)-A\left(0\right)\right)+A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right)=F\left(y\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right)$$
216	212 215	eqtrd	$$⊢\left(\phi \wedge y\in S\right)\to F\left(y\right)-A\left(0\right)+seq0\left(+,\left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)y^k\right)\right)\left(0\right)=F\left(y\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right)$$
217	198 216	breqtrd	$$⊢\left(\phi \wedge y\in S\right)\to seq0\left(+,\left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)y^k\right)\right)⇝\left(F\left(y\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right)\right)$$
218	11 90 135 141 217	isumclim	$$⊢\left(\phi \wedge y\in S\right)\to \sum _{i\in {\mathbb{N}}_0}if\left(i=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(i\right)\right)y^i=F\left(y\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right)$$
219	129 218	eqtrd	$$⊢\left(\phi \wedge y\in S\right)\to \left(x\in S⟼\sum _{i\in {\mathbb{N}}_0}\left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)\right)\left(i\right)x^i\right)\left(y\right)=F\left(y\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right)$$
220	123 219	oveq12d	$$⊢\left(\phi \wedge y\in S\right)\to \left(x\in S⟼\sum _{i\in {\mathbb{N}}_0}\left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)\right)\left(i\right)x^i\right)\left(1\right)-\left(x\in S⟼\sum _{i\in {\mathbb{N}}_0}\left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)\right)\left(i\right)x^i\right)\left(y\right)=F\left(1\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right)-\left(F\left(y\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right)\right)$$
221	213	adantr	$$⊢\left(\phi \wedge y\in S\right)\to F:S⟶ℂ$$
222	221 78	ffvelcdmd	$$⊢\left(\phi \wedge y\in S\right)\to F\left(1\right)\in ℂ$$
223	222 214 207	nnncan2d	$$⊢\left(\phi \wedge y\in S\right)\to F\left(1\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right)-\left(F\left(y\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right)\right)=F\left(1\right)-F\left(y\right)$$
224	220 223	eqtrd	$$⊢\left(\phi \wedge y\in S\right)\to \left(x\in S⟼\sum _{i\in {\mathbb{N}}_0}\left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)\right)\left(i\right)x^i\right)\left(1\right)-\left(x\in S⟼\sum _{i\in {\mathbb{N}}_0}\left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)\right)\left(i\right)x^i\right)\left(y\right)=F\left(1\right)-F\left(y\right)$$
225	224	fveq2d	$$⊢\left(\phi \wedge y\in S\right)\to \left|\left(x\in S⟼\sum _{i\in {\mathbb{N}}_0}\left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)\right)\left(i\right)x^i\right)\left(1\right)-\left(x\in S⟼\sum _{i\in {\mathbb{N}}_0}\left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)\right)\left(i\right)x^i\right)\left(y\right)\right|=\left|F\left(1\right)-F\left(y\right)\right|$$
226	225	breq1d	$$⊢\left(\phi \wedge y\in S\right)\to \left(\left|\left(x\in S⟼\sum _{i\in {\mathbb{N}}_0}\left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)\right)\left(i\right)x^i\right)\left(1\right)-\left(x\in S⟼\sum _{i\in {\mathbb{N}}_0}\left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)\right)\left(i\right)x^i\right)\left(y\right)\right|<R\leftrightarrow \left|F\left(1\right)-F\left(y\right)\right|<R\right)$$
227	226	imbi2d	$$⊢\left(\phi \wedge y\in S\right)\to \left(\left(\left|1-y\right|<w\to \left|\left(x\in S⟼\sum _{i\in {\mathbb{N}}_0}\left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)\right)\left(i\right)x^i\right)\left(1\right)-\left(x\in S⟼\sum _{i\in {\mathbb{N}}_0}\left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)\right)\left(i\right)x^i\right)\left(y\right)\right|<R\right)\leftrightarrow \left(\left|1-y\right|<w\to \left|F\left(1\right)-F\left(y\right)\right|<R\right)\right)$$
228	227	ralbidva	$$⊢\phi \to \left(\forall y\in S\left(\left|1-y\right|<w\to \left|\left(x\in S⟼\sum _{i\in {\mathbb{N}}_0}\left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)\right)\left(i\right)x^i\right)\left(1\right)-\left(x\in S⟼\sum _{i\in {\mathbb{N}}_0}\left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)\right)\left(i\right)x^i\right)\left(y\right)\right|<R\right)\leftrightarrow \forall y\in S\left(\left|1-y\right|<w\to \left|F\left(1\right)-F\left(y\right)\right|<R\right)\right)$$
229	228	rexbidv	$$⊢\phi \to \left(\exists w\in {ℝ}^{+}\forall y\in S\left(\left|1-y\right|<w\to \left|\left(x\in S⟼\sum _{i\in {\mathbb{N}}_0}\left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)\right)\left(i\right)x^i\right)\left(1\right)-\left(x\in S⟼\sum _{i\in {\mathbb{N}}_0}\left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)\right)\left(i\right)x^i\right)\left(y\right)\right|<R\right)\leftrightarrow \exists w\in {ℝ}^{+}\forall y\in S\left(\left|1-y\right|<w\to \left|F\left(1\right)-F\left(y\right)\right|<R\right)\right)$$
230	229	adantr	$$⊢\left(\phi \wedge R\in {ℝ}^{+}\right)\to \left(\exists w\in {ℝ}^{+}\forall y\in S\left(\left|1-y\right|<w\to \left|\left(x\in S⟼\sum _{i\in {\mathbb{N}}_0}\left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)\right)\left(i\right)x^i\right)\left(1\right)-\left(x\in S⟼\sum _{i\in {\mathbb{N}}_0}\left(k\in {\mathbb{N}}_0⟼if\left(k=0,A\left(0\right)-\sum _{m\in {\mathbb{N}}_0}A\left(m\right),A\left(k\right)\right)\right)\left(i\right)x^i\right)\left(y\right)\right|<R\right)\leftrightarrow \exists w\in {ℝ}^{+}\forall y\in S\left(\left|1-y\right|<w\to \left|F\left(1\right)-F\left(y\right)\right|<R\right)\right)$$
231	75 230	mpbid	$$⊢\left(\phi \wedge R\in {ℝ}^{+}\right)\to \exists w\in {ℝ}^{+}\forall y\in S\left(\left|1-y\right|<w\to \left|F\left(1\right)-F\left(y\right)\right|<R\right)$$