abelthlem6

	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})$
	abelth.7	$⊢ φ \to seq 0 (+ A) ⇝ 0$
	abelthlem6.1	$⊢ φ \to X \in (S ∖ \{1\})$
Assertion	abelthlem6	$⊢ φ \to F (X) = (1 - X) \sum_{n \in ℕ_{0}} seq 0 (+ A) (n) X^{n}$

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		abelth.7	$⊢ φ \to seq 0 (+ A) ⇝ 0$
8		abelthlem6.1	$⊢ φ \to X \in (S ∖ \{1\})$
9	8	eldifad	$⊢ φ \to X \in S$
10		oveq1	$⊢ x = X \to x^{n} = X^{n}$
11	10	oveq2d	$⊢ x = X \to A (n) x^{n} = A (n) X^{n}$
12	11	sumeq2sdv	$⊢ x = X \to \sum_{n \in ℕ_{0}} A (n) x^{n} = \sum_{n \in ℕ_{0}} A (n) X^{n}$
13		sumex	$⊢ \sum_{n \in ℕ_{0}} A (n) X^{n} \in V$
14	12 6 13	fvmpt	$⊢ X \in S \to F (X) = \sum_{n \in ℕ_{0}} A (n) X^{n}$
15	9 14	syl	$⊢ φ \to F (X) = \sum_{n \in ℕ_{0}} A (n) X^{n}$
16		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
17		0zd	$⊢ φ \to 0 \in ℤ$
18		fveq2	$⊢ k = n \to A (k) = A (n)$
19		oveq2	$⊢ k = n \to X^{k} = X^{n}$
20	18 19	oveq12d	$⊢ k = n \to A (k) X^{k} = A (n) X^{n}$
21		eqid	$⊢ (k \in ℕ_{0} ⟼ A (k) X^{k}) = (k \in ℕ_{0} ⟼ A (k) X^{k})$
22		ovex	$⊢ A (n) X^{n} \in V$
23	20 21 22	fvmpt	$⊢ n \in ℕ_{0} \to (k \in ℕ_{0} ⟼ A (k) X^{k}) (n) = A (n) X^{n}$
24	23	adantl	$⊢ (φ \land n \in ℕ_{0}) \to (k \in ℕ_{0} ⟼ A (k) X^{k}) (n) = A (n) X^{n}$
25	1	ffvelrnda	$⊢ (φ \land n \in ℕ_{0}) \to A (n) \in ℂ$
26	5	ssrab3	$⊢ S \subseteq ℂ$
27	26 9	sselid	$⊢ φ \to X \in ℂ$
28		expcl	$⊢ (X \in ℂ \land n \in ℕ_{0}) \to X^{n} \in ℂ$
29	27 28	sylan	$⊢ (φ \land n \in ℕ_{0}) \to X^{n} \in ℂ$
30	25 29	mulcld	$⊢ (φ \land n \in ℕ_{0}) \to A (n) X^{n} \in ℂ$
31		fveq2	$⊢ k = n \to seq 0 (+ A) (k) = seq 0 (+ A) (n)$
32	31 19	oveq12d	$⊢ k = n \to seq 0 (+ A) (k) X^{k} = seq 0 (+ A) (n) X^{n}$
33		eqid	$⊢ (k \in ℕ_{0} ⟼ seq 0 (+ A) (k) X^{k}) = (k \in ℕ_{0} ⟼ seq 0 (+ A) (k) X^{k})$
34		ovex	$⊢ seq 0 (+ A) (n) X^{n} \in V$
35	32 33 34	fvmpt	$⊢ n \in ℕ_{0} \to (k \in ℕ_{0} ⟼ seq 0 (+ A) (k) X^{k}) (n) = seq 0 (+ A) (n) X^{n}$
36	35	adantl	$⊢ (φ \land n \in ℕ_{0}) \to (k \in ℕ_{0} ⟼ seq 0 (+ A) (k) X^{k}) (n) = seq 0 (+ A) (n) X^{n}$
37	16 17 25	serf	$⊢ φ \to seq 0 (+ A) : ℕ_{0} ⟶ ℂ$
38	37	ffvelrnda	$⊢ (φ \land n \in ℕ_{0}) \to seq 0 (+ A) (n) \in ℂ$
39	38 29	mulcld	$⊢ (φ \land n \in ℕ_{0}) \to seq 0 (+ A) (n) X^{n} \in ℂ$
40	1 2 3 4 5	abelthlem2	$⊢ φ \to (1 \in S \land S ∖ \{1\} \subseteq 0 ball (abs \circ -) 1)$
41	40	simprd	$⊢ φ \to S ∖ \{1\} \subseteq 0 ball (abs \circ -) 1$
42	41 8	sseldd	$⊢ φ \to X \in (0 ball (abs \circ -) 1)$
43	1 2 3 4 5 6 7	abelthlem5	$⊢ (φ \land X \in (0 ball (abs \circ -) 1)) \to seq 0 (+ (k \in ℕ_{0} ⟼ seq 0 (+ A) (k) X^{k})) \in dom ⇝$
44	42 43	mpdan	$⊢ φ \to seq 0 (+ (k \in ℕ_{0} ⟼ seq 0 (+ A) (k) X^{k})) \in dom ⇝$
45	16 17 36 39 44	isumclim2	$⊢ φ \to seq 0 (+ (k \in ℕ_{0} ⟼ seq 0 (+ A) (k) X^{k})) ⇝ \sum_{n \in ℕ_{0}} seq 0 (+ A) (n) X^{n}$
46		seqex	$⊢ seq 0 (+ (k \in ℕ_{0} ⟼ A (k) X^{k})) \in V$
47	46	a1i	$⊢ φ \to seq 0 (+ (k \in ℕ_{0} ⟼ A (k) X^{k})) \in V$
48		0nn0	$⊢ 0 \in ℕ_{0}$
49	48	a1i	$⊢ φ \to 0 \in ℕ_{0}$
50		oveq1	$⊢ k = i \to k - 1 = i - 1$
51	50	oveq2d	$⊢ k = i \to (0 \dots k - 1) = (0 \dots i - 1)$
52	51	sumeq1d	$⊢ k = i \to \sum_{m = 0}^{k - 1} A (m) = \sum_{m = 0}^{i - 1} A (m)$
53		oveq2	$⊢ k = i \to X^{k} = X^{i}$
54	52 53	oveq12d	$⊢ k = i \to \sum_{m = 0}^{k - 1} A (m) X^{k} = \sum_{m = 0}^{i - 1} A (m) X^{i}$
55		eqid	$⊢ (k \in ℕ_{0} ⟼ \sum_{m = 0}^{k - 1} A (m) X^{k}) = (k \in ℕ_{0} ⟼ \sum_{m = 0}^{k - 1} A (m) X^{k})$
56		ovex	$⊢ \sum_{m = 0}^{i - 1} A (m) X^{i} \in V$
57	54 55 56	fvmpt	$⊢ i \in ℕ_{0} \to (k \in ℕ_{0} ⟼ \sum_{m = 0}^{k - 1} A (m) X^{k}) (i) = \sum_{m = 0}^{i - 1} A (m) X^{i}$
58	57	adantl	$⊢ (φ \land i \in ℕ_{0}) \to (k \in ℕ_{0} ⟼ \sum_{m = 0}^{k - 1} A (m) X^{k}) (i) = \sum_{m = 0}^{i - 1} A (m) X^{i}$
59		fzfid	$⊢ (φ \land i \in ℕ_{0}) \to (0 \dots i - 1) \in Fin$
60	1	adantr	$⊢ (φ \land i \in ℕ_{0}) \to A : ℕ_{0} ⟶ ℂ$
61		elfznn0	$⊢ m \in (0 \dots i - 1) \to m \in ℕ_{0}$
62		ffvelrn	$⊢ (A : ℕ_{0} ⟶ ℂ \land m \in ℕ_{0}) \to A (m) \in ℂ$
63	60 61 62	syl2an	$⊢ ((φ \land i \in ℕ_{0}) \land m \in (0 \dots i - 1)) \to A (m) \in ℂ$
64	59 63	fsumcl	$⊢ (φ \land i \in ℕ_{0}) \to \sum_{m = 0}^{i - 1} A (m) \in ℂ$
65		expcl	$⊢ (X \in ℂ \land i \in ℕ_{0}) \to X^{i} \in ℂ$
66	27 65	sylan	$⊢ (φ \land i \in ℕ_{0}) \to X^{i} \in ℂ$
67	64 66	mulcld	$⊢ (φ \land i \in ℕ_{0}) \to \sum_{m = 0}^{i - 1} A (m) X^{i} \in ℂ$
68	58 67	eqeltrd	$⊢ (φ \land i \in ℕ_{0}) \to (k \in ℕ_{0} ⟼ \sum_{m = 0}^{k - 1} A (m) X^{k}) (i) \in ℂ$
69	17	peano2zd	$⊢ φ \to 0 + 1 \in ℤ$
70		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
71		1e0p1	$⊢ 1 = 0 + 1$
72	71	fveq2i	$⊢ ℤ_{\geq 1} = ℤ_{\geq (0 + 1)}$
73	70 72	eqtri	$⊢ ℕ = ℤ_{\geq (0 + 1)}$
74	73	eleq2i	$⊢ n \in ℕ \leftrightarrow n \in ℤ_{\geq (0 + 1)}$
75		nnm1nn0	$⊢ n \in ℕ \to n - 1 \in ℕ_{0}$
76	75	adantl	$⊢ (φ \land n \in ℕ) \to n - 1 \in ℕ_{0}$
77		fveq2	$⊢ k = n - 1 \to seq 0 (+ A) (k) = seq 0 (+ A) (n - 1)$
78		oveq2	$⊢ k = n - 1 \to X^{k} = X^{n - 1}$
79	77 78	oveq12d	$⊢ k = n - 1 \to seq 0 (+ A) (k) X^{k} = seq 0 (+ A) (n - 1) X^{n - 1}$
80	79	oveq2d	$⊢ k = n - 1 \to X seq 0 (+ A) (k) X^{k} = X seq 0 (+ A) (n - 1) X^{n - 1}$
81		eqid	$⊢ (k \in ℕ_{0} ⟼ X seq 0 (+ A) (k) X^{k}) = (k \in ℕ_{0} ⟼ X seq 0 (+ A) (k) X^{k})$
82		ovex	$⊢ X seq 0 (+ A) (n - 1) X^{n - 1} \in V$
83	80 81 82	fvmpt	$⊢ n - 1 \in ℕ_{0} \to (k \in ℕ_{0} ⟼ X seq 0 (+ A) (k) X^{k}) (n - 1) = X seq 0 (+ A) (n - 1) X^{n - 1}$
84	76 83	syl	$⊢ (φ \land n \in ℕ) \to (k \in ℕ_{0} ⟼ X seq 0 (+ A) (k) X^{k}) (n - 1) = X seq 0 (+ A) (n - 1) X^{n - 1}$
85		ax-1cn	$⊢ 1 \in ℂ$
86		nncn	$⊢ n \in ℕ \to n \in ℂ$
87	86	adantl	$⊢ (φ \land n \in ℕ) \to n \in ℂ$
88		nn0ex	$⊢ ℕ_{0} \in V$
89	88	mptex	$⊢ (k \in ℕ_{0} ⟼ X seq 0 (+ A) (k) X^{k}) \in V$
90	89	shftval	$⊢ (1 \in ℂ \land n \in ℂ) \to ((k \in ℕ_{0} ⟼ X seq 0 (+ A) (k) X^{k}) shift 1) (n) = (k \in ℕ_{0} ⟼ X seq 0 (+ A) (k) X^{k}) (n - 1)$
91	85 87 90	sylancr	$⊢ (φ \land n \in ℕ) \to ((k \in ℕ_{0} ⟼ X seq 0 (+ A) (k) X^{k}) shift 1) (n) = (k \in ℕ_{0} ⟼ X seq 0 (+ A) (k) X^{k}) (n - 1)$
92		eqidd	$⊢ ((φ \land n \in ℕ) \land m \in (0 \dots n - 1)) \to A (m) = A (m)$
93	76 16	eleqtrdi	$⊢ (φ \land n \in ℕ) \to n - 1 \in ℤ_{\geq 0}$
94	1	adantr	$⊢ (φ \land n \in ℕ) \to A : ℕ_{0} ⟶ ℂ$
95		elfznn0	$⊢ m \in (0 \dots n - 1) \to m \in ℕ_{0}$
96	94 95 62	syl2an	$⊢ ((φ \land n \in ℕ) \land m \in (0 \dots n - 1)) \to A (m) \in ℂ$
97	92 93 96	fsumser	$⊢ (φ \land n \in ℕ) \to \sum_{m = 0}^{n - 1} A (m) = seq 0 (+ A) (n - 1)$
98		expm1t	$⊢ (X \in ℂ \land n \in ℕ) \to X^{n} = X^{n - 1} X$
99	27 98	sylan	$⊢ (φ \land n \in ℕ) \to X^{n} = X^{n - 1} X$
100	27	adantr	$⊢ (φ \land n \in ℕ) \to X \in ℂ$
101		expcl	$⊢ (X \in ℂ \land n - 1 \in ℕ_{0}) \to X^{n - 1} \in ℂ$
102	27 75 101	syl2an	$⊢ (φ \land n \in ℕ) \to X^{n - 1} \in ℂ$
103	100 102	mulcomd	$⊢ (φ \land n \in ℕ) \to X X^{n - 1} = X^{n - 1} X$
104	99 103	eqtr4d	$⊢ (φ \land n \in ℕ) \to X^{n} = X X^{n - 1}$
105	97 104	oveq12d	$⊢ (φ \land n \in ℕ) \to \sum_{m = 0}^{n - 1} A (m) X^{n} = seq 0 (+ A) (n - 1) X X^{n - 1}$
106		nnnn0	$⊢ n \in ℕ \to n \in ℕ_{0}$
107	106	adantl	$⊢ (φ \land n \in ℕ) \to n \in ℕ_{0}$
108		oveq1	$⊢ k = n \to k - 1 = n - 1$
109	108	oveq2d	$⊢ k = n \to (0 \dots k - 1) = (0 \dots n - 1)$
110	109	sumeq1d	$⊢ k = n \to \sum_{m = 0}^{k - 1} A (m) = \sum_{m = 0}^{n - 1} A (m)$
111	110 19	oveq12d	$⊢ k = n \to \sum_{m = 0}^{k - 1} A (m) X^{k} = \sum_{m = 0}^{n - 1} A (m) X^{n}$
112		ovex	$⊢ \sum_{m = 0}^{n - 1} A (m) X^{n} \in V$
113	111 55 112	fvmpt	$⊢ n \in ℕ_{0} \to (k \in ℕ_{0} ⟼ \sum_{m = 0}^{k - 1} A (m) X^{k}) (n) = \sum_{m = 0}^{n - 1} A (m) X^{n}$
114	107 113	syl	$⊢ (φ \land n \in ℕ) \to (k \in ℕ_{0} ⟼ \sum_{m = 0}^{k - 1} A (m) X^{k}) (n) = \sum_{m = 0}^{n - 1} A (m) X^{n}$
115		ffvelrn	$⊢ (seq 0 (+ A) : ℕ_{0} ⟶ ℂ \land n - 1 \in ℕ_{0}) \to seq 0 (+ A) (n - 1) \in ℂ$
116	37 75 115	syl2an	$⊢ (φ \land n \in ℕ) \to seq 0 (+ A) (n - 1) \in ℂ$
117	100 116 102	mul12d	$⊢ (φ \land n \in ℕ) \to X seq 0 (+ A) (n - 1) X^{n - 1} = seq 0 (+ A) (n - 1) X X^{n - 1}$
118	105 114 117	3eqtr4d	$⊢ (φ \land n \in ℕ) \to (k \in ℕ_{0} ⟼ \sum_{m = 0}^{k - 1} A (m) X^{k}) (n) = X seq 0 (+ A) (n - 1) X^{n - 1}$
119	84 91 118	3eqtr4d	$⊢ (φ \land n \in ℕ) \to ((k \in ℕ_{0} ⟼ X seq 0 (+ A) (k) X^{k}) shift 1) (n) = (k \in ℕ_{0} ⟼ \sum_{m = 0}^{k - 1} A (m) X^{k}) (n)$
120	74 119	sylan2br	$⊢ (φ \land n \in ℤ_{\geq (0 + 1)}) \to ((k \in ℕ_{0} ⟼ X seq 0 (+ A) (k) X^{k}) shift 1) (n) = (k \in ℕ_{0} ⟼ \sum_{m = 0}^{k - 1} A (m) X^{k}) (n)$
121	69 120	seqfeq	$⊢ φ \to seq (0 + 1) (+ ((k \in ℕ_{0} ⟼ X seq 0 (+ A) (k) X^{k}) shift 1)) = seq (0 + 1) (+ (k \in ℕ_{0} ⟼ \sum_{m = 0}^{k - 1} A (m) X^{k}))$
122		fveq2	$⊢ k = i \to seq 0 (+ A) (k) = seq 0 (+ A) (i)$
123	122 53	oveq12d	$⊢ k = i \to seq 0 (+ A) (k) X^{k} = seq 0 (+ A) (i) X^{i}$
124		ovex	$⊢ seq 0 (+ A) (i) X^{i} \in V$
125	123 33 124	fvmpt	$⊢ i \in ℕ_{0} \to (k \in ℕ_{0} ⟼ seq 0 (+ A) (k) X^{k}) (i) = seq 0 (+ A) (i) X^{i}$
126	125	adantl	$⊢ (φ \land i \in ℕ_{0}) \to (k \in ℕ_{0} ⟼ seq 0 (+ A) (k) X^{k}) (i) = seq 0 (+ A) (i) X^{i}$
127	37	ffvelrnda	$⊢ (φ \land i \in ℕ_{0}) \to seq 0 (+ A) (i) \in ℂ$
128	127 66	mulcld	$⊢ (φ \land i \in ℕ_{0}) \to seq 0 (+ A) (i) X^{i} \in ℂ$
129	126 128	eqeltrd	$⊢ (φ \land i \in ℕ_{0}) \to (k \in ℕ_{0} ⟼ seq 0 (+ A) (k) X^{k}) (i) \in ℂ$
130	123	oveq2d	$⊢ k = i \to X seq 0 (+ A) (k) X^{k} = X seq 0 (+ A) (i) X^{i}$
131		ovex	$⊢ X seq 0 (+ A) (i) X^{i} \in V$
132	130 81 131	fvmpt	$⊢ i \in ℕ_{0} \to (k \in ℕ_{0} ⟼ X seq 0 (+ A) (k) X^{k}) (i) = X seq 0 (+ A) (i) X^{i}$
133	132	adantl	$⊢ (φ \land i \in ℕ_{0}) \to (k \in ℕ_{0} ⟼ X seq 0 (+ A) (k) X^{k}) (i) = X seq 0 (+ A) (i) X^{i}$
134	126	oveq2d	$⊢ (φ \land i \in ℕ_{0}) \to X (k \in ℕ_{0} ⟼ seq 0 (+ A) (k) X^{k}) (i) = X seq 0 (+ A) (i) X^{i}$
135	133 134	eqtr4d	$⊢ (φ \land i \in ℕ_{0}) \to (k \in ℕ_{0} ⟼ X seq 0 (+ A) (k) X^{k}) (i) = X (k \in ℕ_{0} ⟼ seq 0 (+ A) (k) X^{k}) (i)$
136	16 17 27 45 129 135	isermulc2	$⊢ φ \to seq 0 (+ (k \in ℕ_{0} ⟼ X seq 0 (+ A) (k) X^{k})) ⇝ X \sum_{n \in ℕ_{0}} seq 0 (+ A) (n) X^{n}$
137		0z	$⊢ 0 \in ℤ$
138		1z	$⊢ 1 \in ℤ$
139	89	isershft	$⊢ (0 \in ℤ \land 1 \in ℤ) \to (seq 0 (+ (k \in ℕ_{0} ⟼ X seq 0 (+ A) (k) X^{k})) ⇝ X \sum_{n \in ℕ_{0}} seq 0 (+ A) (n) X^{n} \leftrightarrow seq (0 + 1) (+ ((k \in ℕ_{0} ⟼ X seq 0 (+ A) (k) X^{k}) shift 1)) ⇝ X \sum_{n \in ℕ_{0}} seq 0 (+ A) (n) X^{n})$
140	137 138 139	mp2an	$⊢ seq 0 (+ (k \in ℕ_{0} ⟼ X seq 0 (+ A) (k) X^{k})) ⇝ X \sum_{n \in ℕ_{0}} seq 0 (+ A) (n) X^{n} \leftrightarrow seq (0 + 1) (+ ((k \in ℕ_{0} ⟼ X seq 0 (+ A) (k) X^{k}) shift 1)) ⇝ X \sum_{n \in ℕ_{0}} seq 0 (+ A) (n) X^{n}$
141	136 140	sylib	$⊢ φ \to seq (0 + 1) (+ ((k \in ℕ_{0} ⟼ X seq 0 (+ A) (k) X^{k}) shift 1)) ⇝ X \sum_{n \in ℕ_{0}} seq 0 (+ A) (n) X^{n}$
142	121 141	eqbrtrrd	$⊢ φ \to seq (0 + 1) (+ (k \in ℕ_{0} ⟼ \sum_{m = 0}^{k - 1} A (m) X^{k})) ⇝ X \sum_{n \in ℕ_{0}} seq 0 (+ A) (n) X^{n}$
143	16 49 68 142	clim2ser2	$⊢ φ \to seq 0 (+ (k \in ℕ_{0} ⟼ \sum_{m = 0}^{k - 1} A (m) X^{k})) ⇝ (X \sum_{n \in ℕ_{0}} seq 0 (+ A) (n) X^{n} + seq 0 (+ (k \in ℕ_{0} ⟼ \sum_{m = 0}^{k - 1} A (m) X^{k})) (0))$
144		seq1	$⊢ 0 \in ℤ \to seq 0 (+ (k \in ℕ_{0} ⟼ \sum_{m = 0}^{k - 1} A (m) X^{k})) (0) = (k \in ℕ_{0} ⟼ \sum_{m = 0}^{k - 1} A (m) X^{k}) (0)$
145	137 144	ax-mp	$⊢ seq 0 (+ (k \in ℕ_{0} ⟼ \sum_{m = 0}^{k - 1} A (m) X^{k})) (0) = (k \in ℕ_{0} ⟼ \sum_{m = 0}^{k - 1} A (m) X^{k}) (0)$
146		oveq1	$⊢ k = 0 \to k - 1 = 0 - 1$
147	146	oveq2d	$⊢ k = 0 \to (0 \dots k - 1) = (0 \dots 0 - 1)$
148		risefall0lem	$⊢ (0 \dots 0 - 1) = \emptyset$
149	147 148	eqtrdi	$⊢ k = 0 \to (0 \dots k - 1) = \emptyset$
150	149	sumeq1d	$⊢ k = 0 \to \sum_{m = 0}^{k - 1} A (m) = \sum_{m \in \emptyset} A (m)$
151		sum0	$⊢ \sum_{m \in \emptyset} A (m) = 0$
152	150 151	eqtrdi	$⊢ k = 0 \to \sum_{m = 0}^{k - 1} A (m) = 0$
153		oveq2	$⊢ k = 0 \to X^{k} = X^{0}$
154	152 153	oveq12d	$⊢ k = 0 \to \sum_{m = 0}^{k - 1} A (m) X^{k} = 0 \cdot X^{0}$
155		ovex	$⊢ 0 \cdot X^{0} \in V$
156	154 55 155	fvmpt	$⊢ 0 \in ℕ_{0} \to (k \in ℕ_{0} ⟼ \sum_{m = 0}^{k - 1} A (m) X^{k}) (0) = 0 \cdot X^{0}$
157	48 156	ax-mp	$⊢ (k \in ℕ_{0} ⟼ \sum_{m = 0}^{k - 1} A (m) X^{k}) (0) = 0 \cdot X^{0}$
158	145 157	eqtri	$⊢ seq 0 (+ (k \in ℕ_{0} ⟼ \sum_{m = 0}^{k - 1} A (m) X^{k})) (0) = 0 \cdot X^{0}$
159		expcl	$⊢ (X \in ℂ \land 0 \in ℕ_{0}) \to X^{0} \in ℂ$
160	27 48 159	sylancl	$⊢ φ \to X^{0} \in ℂ$
161	160	mul02d	$⊢ φ \to 0 \cdot X^{0} = 0$
162	158 161	syl5eq	$⊢ φ \to seq 0 (+ (k \in ℕ_{0} ⟼ \sum_{m = 0}^{k - 1} A (m) X^{k})) (0) = 0$
163	162	oveq2d	$⊢ φ \to X \sum_{n \in ℕ_{0}} seq 0 (+ A) (n) X^{n} + seq 0 (+ (k \in ℕ_{0} ⟼ \sum_{m = 0}^{k - 1} A (m) X^{k})) (0) = X \sum_{n \in ℕ_{0}} seq 0 (+ A) (n) X^{n} + 0$
164	16 17 36 39 44	isumcl	$⊢ φ \to \sum_{n \in ℕ_{0}} seq 0 (+ A) (n) X^{n} \in ℂ$
165	27 164	mulcld	$⊢ φ \to X \sum_{n \in ℕ_{0}} seq 0 (+ A) (n) X^{n} \in ℂ$
166	165	addid1d	$⊢ φ \to X \sum_{n \in ℕ_{0}} seq 0 (+ A) (n) X^{n} + 0 = X \sum_{n \in ℕ_{0}} seq 0 (+ A) (n) X^{n}$
167	163 166	eqtrd	$⊢ φ \to X \sum_{n \in ℕ_{0}} seq 0 (+ A) (n) X^{n} + seq 0 (+ (k \in ℕ_{0} ⟼ \sum_{m = 0}^{k - 1} A (m) X^{k})) (0) = X \sum_{n \in ℕ_{0}} seq 0 (+ A) (n) X^{n}$
168	143 167	breqtrd	$⊢ φ \to seq 0 (+ (k \in ℕ_{0} ⟼ \sum_{m = 0}^{k - 1} A (m) X^{k})) ⇝ X \sum_{n \in ℕ_{0}} seq 0 (+ A) (n) X^{n}$
169	16 17 129	serf	$⊢ φ \to seq 0 (+ (k \in ℕ_{0} ⟼ seq 0 (+ A) (k) X^{k})) : ℕ_{0} ⟶ ℂ$
170	169	ffvelrnda	$⊢ (φ \land i \in ℕ_{0}) \to seq 0 (+ (k \in ℕ_{0} ⟼ seq 0 (+ A) (k) X^{k})) (i) \in ℂ$
171	16 17 68	serf	$⊢ φ \to seq 0 (+ (k \in ℕ_{0} ⟼ \sum_{m = 0}^{k - 1} A (m) X^{k})) : ℕ_{0} ⟶ ℂ$
172	171	ffvelrnda	$⊢ (φ \land i \in ℕ_{0}) \to seq 0 (+ (k \in ℕ_{0} ⟼ \sum_{m = 0}^{k - 1} A (m) X^{k})) (i) \in ℂ$
173		simpr	$⊢ (φ \land i \in ℕ_{0}) \to i \in ℕ_{0}$
174	173 16	eleqtrdi	$⊢ (φ \land i \in ℕ_{0}) \to i \in ℤ_{\geq 0}$
175		simpl	$⊢ (φ \land i \in ℕ_{0}) \to φ$
176		elfznn0	$⊢ n \in (0 \dots i) \to n \in ℕ_{0}$
177	36 39	eqeltrd	$⊢ (φ \land n \in ℕ_{0}) \to (k \in ℕ_{0} ⟼ seq 0 (+ A) (k) X^{k}) (n) \in ℂ$
178	175 176 177	syl2an	$⊢ ((φ \land i \in ℕ_{0}) \land n \in (0 \dots i)) \to (k \in ℕ_{0} ⟼ seq 0 (+ A) (k) X^{k}) (n) \in ℂ$
179	113	adantl	$⊢ (φ \land n \in ℕ_{0}) \to (k \in ℕ_{0} ⟼ \sum_{m = 0}^{k - 1} A (m) X^{k}) (n) = \sum_{m = 0}^{n - 1} A (m) X^{n}$
180		fzfid	$⊢ (φ \land n \in ℕ_{0}) \to (0 \dots n - 1) \in Fin$
181	1	adantr	$⊢ (φ \land n \in ℕ_{0}) \to A : ℕ_{0} ⟶ ℂ$
182	181 95 62	syl2an	$⊢ ((φ \land n \in ℕ_{0}) \land m \in (0 \dots n - 1)) \to A (m) \in ℂ$
183	180 182	fsumcl	$⊢ (φ \land n \in ℕ_{0}) \to \sum_{m = 0}^{n - 1} A (m) \in ℂ$
184	183 29	mulcld	$⊢ (φ \land n \in ℕ_{0}) \to \sum_{m = 0}^{n - 1} A (m) X^{n} \in ℂ$
185	179 184	eqeltrd	$⊢ (φ \land n \in ℕ_{0}) \to (k \in ℕ_{0} ⟼ \sum_{m = 0}^{k - 1} A (m) X^{k}) (n) \in ℂ$
186	175 176 185	syl2an	$⊢ ((φ \land i \in ℕ_{0}) \land n \in (0 \dots i)) \to (k \in ℕ_{0} ⟼ \sum_{m = 0}^{k - 1} A (m) X^{k}) (n) \in ℂ$
187		eqidd	$⊢ ((φ \land n \in ℕ_{0}) \land m \in (0 \dots n)) \to A (m) = A (m)$
188		simpr	$⊢ (φ \land n \in ℕ_{0}) \to n \in ℕ_{0}$
189	188 16	eleqtrdi	$⊢ (φ \land n \in ℕ_{0}) \to n \in ℤ_{\geq 0}$
190		elfznn0	$⊢ m \in (0 \dots n) \to m \in ℕ_{0}$
191	181 190 62	syl2an	$⊢ ((φ \land n \in ℕ_{0}) \land m \in (0 \dots n)) \to A (m) \in ℂ$
192	187 189 191	fsumser	$⊢ (φ \land n \in ℕ_{0}) \to \sum_{m = 0}^{n} A (m) = seq 0 (+ A) (n)$
193		fveq2	$⊢ m = n \to A (m) = A (n)$
194	189 191 193	fsumm1	$⊢ (φ \land n \in ℕ_{0}) \to \sum_{m = 0}^{n} A (m) = \sum_{m = 0}^{n - 1} A (m) + A (n)$
195	192 194	eqtr3d	$⊢ (φ \land n \in ℕ_{0}) \to seq 0 (+ A) (n) = \sum_{m = 0}^{n - 1} A (m) + A (n)$
196	195	oveq1d	$⊢ (φ \land n \in ℕ_{0}) \to seq 0 (+ A) (n) - \sum_{m = 0}^{n - 1} A (m) = \sum_{m = 0}^{n - 1} A (m) + A (n) - \sum_{m = 0}^{n - 1} A (m)$
197	183 25	pncan2d	$⊢ (φ \land n \in ℕ_{0}) \to \sum_{m = 0}^{n - 1} A (m) + A (n) - \sum_{m = 0}^{n - 1} A (m) = A (n)$
198	196 197	eqtr2d	$⊢ (φ \land n \in ℕ_{0}) \to A (n) = seq 0 (+ A) (n) - \sum_{m = 0}^{n - 1} A (m)$
199	198	oveq1d	$⊢ (φ \land n \in ℕ_{0}) \to A (n) X^{n} = (seq 0 (+ A) (n) - \sum_{m = 0}^{n - 1} A (m)) X^{n}$
200	38 183 29	subdird	$⊢ (φ \land n \in ℕ_{0}) \to (seq 0 (+ A) (n) - \sum_{m = 0}^{n - 1} A (m)) X^{n} = seq 0 (+ A) (n) X^{n} - \sum_{m = 0}^{n - 1} A (m) X^{n}$
201	199 200	eqtrd	$⊢ (φ \land n \in ℕ_{0}) \to A (n) X^{n} = seq 0 (+ A) (n) X^{n} - \sum_{m = 0}^{n - 1} A (m) X^{n}$
202	36 179	oveq12d	$⊢ (φ \land n \in ℕ_{0}) \to (k \in ℕ_{0} ⟼ seq 0 (+ A) (k) X^{k}) (n) - (k \in ℕ_{0} ⟼ \sum_{m = 0}^{k - 1} A (m) X^{k}) (n) = seq 0 (+ A) (n) X^{n} - \sum_{m = 0}^{n - 1} A (m) X^{n}$
203	201 24 202	3eqtr4d	$⊢ (φ \land n \in ℕ_{0}) \to (k \in ℕ_{0} ⟼ A (k) X^{k}) (n) = (k \in ℕ_{0} ⟼ seq 0 (+ A) (k) X^{k}) (n) - (k \in ℕ_{0} ⟼ \sum_{m = 0}^{k - 1} A (m) X^{k}) (n)$
204	175 176 203	syl2an	$⊢ ((φ \land i \in ℕ_{0}) \land n \in (0 \dots i)) \to (k \in ℕ_{0} ⟼ A (k) X^{k}) (n) = (k \in ℕ_{0} ⟼ seq 0 (+ A) (k) X^{k}) (n) - (k \in ℕ_{0} ⟼ \sum_{m = 0}^{k - 1} A (m) X^{k}) (n)$
205	174 178 186 204	sersub	$⊢ (φ \land i \in ℕ_{0}) \to seq 0 (+ (k \in ℕ_{0} ⟼ A (k) X^{k})) (i) = seq 0 (+ (k \in ℕ_{0} ⟼ seq 0 (+ A) (k) X^{k})) (i) - seq 0 (+ (k \in ℕ_{0} ⟼ \sum_{m = 0}^{k - 1} A (m) X^{k})) (i)$
206	16 17 45 47 168 170 172 205	climsub	$⊢ φ \to seq 0 (+ (k \in ℕ_{0} ⟼ A (k) X^{k})) ⇝ (\sum_{n \in ℕ_{0}} seq 0 (+ A) (n) X^{n} - X \sum_{n \in ℕ_{0}} seq 0 (+ A) (n) X^{n})$
207		1cnd	$⊢ φ \to 1 \in ℂ$
208	207 27 164	subdird	$⊢ φ \to (1 - X) \sum_{n \in ℕ_{0}} seq 0 (+ A) (n) X^{n} = 1 \sum_{n \in ℕ_{0}} seq 0 (+ A) (n) X^{n} - X \sum_{n \in ℕ_{0}} seq 0 (+ A) (n) X^{n}$
209	164	mulid2d	$⊢ φ \to 1 \sum_{n \in ℕ_{0}} seq 0 (+ A) (n) X^{n} = \sum_{n \in ℕ_{0}} seq 0 (+ A) (n) X^{n}$
210	209	oveq1d	$⊢ φ \to 1 \sum_{n \in ℕ_{0}} seq 0 (+ A) (n) X^{n} - X \sum_{n \in ℕ_{0}} seq 0 (+ A) (n) X^{n} = \sum_{n \in ℕ_{0}} seq 0 (+ A) (n) X^{n} - X \sum_{n \in ℕ_{0}} seq 0 (+ A) (n) X^{n}$
211	208 210	eqtrd	$⊢ φ \to (1 - X) \sum_{n \in ℕ_{0}} seq 0 (+ A) (n) X^{n} = \sum_{n \in ℕ_{0}} seq 0 (+ A) (n) X^{n} - X \sum_{n \in ℕ_{0}} seq 0 (+ A) (n) X^{n}$
212	206 211	breqtrrd	$⊢ φ \to seq 0 (+ (k \in ℕ_{0} ⟼ A (k) X^{k})) ⇝ (1 - X) \sum_{n \in ℕ_{0}} seq 0 (+ A) (n) X^{n}$
213	16 17 24 30 212	isumclim	$⊢ φ \to \sum_{n \in ℕ_{0}} A (n) X^{n} = (1 - X) \sum_{n \in ℕ_{0}} seq 0 (+ A) (n) X^{n}$
214	15 213	eqtrd	$⊢ φ \to F (X) = (1 - X) \sum_{n \in ℕ_{0}} seq 0 (+ A) (n) X^{n}$

Metamath Proof Explorer

Theorem abelthlem6

Proof