Theorem abelthlem4

Description: Lemma for abelth . (Contributed by Mario Carneiro, 31-Mar-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	abelthlem4	$$⊢\phi \to F:S⟶ℂ$$

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		nn0uz	$$⊢{\mathbb{N}}_0={\mathbb{Z}}_{\ge 0}$$
8		0zd	$$⊢\left(\phi \wedge x\in S\right)\to 0\in \mathbb{Z}$$
9		fveq2	$$⊢m=n\to A\left(m\right)=A\left(n\right)$$
10		oveq2	$$⊢m=n\to x^m=x^n$$
11	9 10	oveq12d	$$⊢m=n\to A\left(m\right)x^m=A\left(n\right)x^n$$
12		eqid	$$⊢\left(m\in {\mathbb{N}}_0⟼A\left(m\right)x^m\right)=\left(m\in {\mathbb{N}}_0⟼A\left(m\right)x^m\right)$$
13		ovex	$$⊢A\left(n\right)x^n\in \mathrm{V}$$
14	11 12 13	fvmpt	$$⊢n\in {\mathbb{N}}_0\to \left(m\in {\mathbb{N}}_0⟼A\left(m\right)x^m\right)\left(n\right)=A\left(n\right)x^n$$
15	14	adantl	$$⊢\left(\left(\phi \wedge x\in S\right)\wedge n\in {\mathbb{N}}_0\right)\to \left(m\in {\mathbb{N}}_0⟼A\left(m\right)x^m\right)\left(n\right)=A\left(n\right)x^n$$
16	1	adantr	$$⊢\left(\phi \wedge x\in S\right)\to A:{\mathbb{N}}_0⟶ℂ$$
17	16	ffvelcdmda	$$⊢\left(\left(\phi \wedge x\in S\right)\wedge n\in {\mathbb{N}}_0\right)\to A\left(n\right)\in ℂ$$
18	5	ssrab3	$$⊢S\subseteq ℂ$$
19	18	a1i	$$⊢\phi \to S\subseteq ℂ$$
20	19	sselda	$$⊢\left(\phi \wedge x\in S\right)\to x\in ℂ$$
21		expcl	$$⊢\left(x\in ℂ\wedge n\in {\mathbb{N}}_0\right)\to x^n\in ℂ$$
22	20 21	sylan	$$⊢\left(\left(\phi \wedge x\in S\right)\wedge n\in {\mathbb{N}}_0\right)\to x^n\in ℂ$$
23	17 22	mulcld	$$⊢\left(\left(\phi \wedge x\in S\right)\wedge n\in {\mathbb{N}}_0\right)\to A\left(n\right)x^n\in ℂ$$
24	1 2 3 4 5	abelthlem3	$$⊢\left(\phi \wedge x\in S\right)\to seq0\left(+,\left(m\in {\mathbb{N}}_0⟼A\left(m\right)x^m\right)\right)\in \mathrm{dom}⇝$$
25	7 8 15 23 24	isumcl	$$⊢\left(\phi \wedge x\in S\right)\to \sum _{n\in {\mathbb{N}}_0}A\left(n\right)x^n\in ℂ$$
26	25 6	fmptd	$$⊢\phi \to F:S⟶ℂ$$