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	$⊢ φ \to A : ℕ_{0} ⟶ ℂ$
	abelth.2	$⊢ φ \to seq 0 (+ A) \in dom ⇝$
	abelth.3	$⊢ φ \to M \in ℝ$
	abelth.4	$⊢ φ \to 0 \leq M$
	abelth.5	$⊢ S = \{z \in ℂ \| \|1 - z\| \leq M (1 - \|z\|)\}$
	abelth.6	$⊢ F = (x \in S ⟼ \sum_{n \in ℕ_{0}} A (n) x^{n})$
Assertion	abelthlem9	$⊢ (φ \land R \in ℝ^{+}) \to \exists w \in ℝ^{+} \forall y \in S (\|1 - y\| < w \to \|F (1) - F (y)\| < R)$

Proof

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

Metamath Proof Explorer

Theorem abelthlem9

Proof