Theorem abelthlem7a

Description: Lemma for abelth . (Contributed by Mario Carneiro, 8-May-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)$$
	abelth.7	$$⊢\phi \to seq0\left(+,A\right)⇝0$$
	abelthlem6.1	$$⊢\phi \to X\in \left(S\setminus \left\{1\right\}\right)$$
Assertion	abelthlem7a	$$⊢\phi \to \left(X\in ℂ\wedge \left|1-X\right|\le M\left(1-\left|X\right|\right)\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		abelth.7	$$⊢\phi \to seq0\left(+,A\right)⇝0$$
8		abelthlem6.1	$$⊢\phi \to X\in \left(S\setminus \left\{1\right\}\right)$$
9	8	eldifad	$$⊢\phi \to X\in S$$
10		oveq2	$$⊢z=X\to 1-z=1-X$$
11	10	fveq2d	$$⊢z=X\to \left|1-z\right|=\left|1-X\right|$$
12		fveq2	$$⊢z=X\to \left|z\right|=\left|X\right|$$
13	12	oveq2d	$$⊢z=X\to 1-\left|z\right|=1-\left|X\right|$$
14	13	oveq2d	$$⊢z=X\to M\left(1-\left|z\right|\right)=M\left(1-\left|X\right|\right)$$
15	11 14	breq12d	$$⊢z=X\to \left(\left|1-z\right|\le M\left(1-\left|z\right|\right)\leftrightarrow \left|1-X\right|\le M\left(1-\left|X\right|\right)\right)$$
16	15 5	elrab2	$$⊢X\in S\leftrightarrow \left(X\in ℂ\wedge \left|1-X\right|\le M\left(1-\left|X\right|\right)\right)$$
17	9 16	sylib	$$⊢\phi \to \left(X\in ℂ\wedge \left|1-X\right|\le M\left(1-\left|X\right|\right)\right)$$