ftalem1

Description: Lemma for fta : "growth lemma". There exists some r such that F is arbitrarily close in proportion to its dominant term. (Contributed by Mario Carneiro, 14-Sep-2014)

	Ref	Expression
Hypotheses	ftalem.1	$⊢ A = coeff (F)$
	ftalem.2	$⊢ N = \deg (F)$
	ftalem.3	$⊢ φ \to F \in Poly (S)$
	ftalem.4	$⊢ φ \to N \in ℕ$
	ftalem1.5	$⊢ φ \to E \in ℝ^{+}$
	ftalem1.6	$⊢ T = \frac{\sum_{k = 0}^{N - 1} \|A (k)\|}{E}$
Assertion	ftalem1	$⊢ φ \to \exists r \in ℝ \forall x \in ℂ (r < \|x\| \to \|F (x) - A (N) x^{N}\| < E {\|x\|}^{N})$

Proof

Step	Hyp	Ref	Expression
1		ftalem.1	$⊢ A = coeff (F)$
2		ftalem.2	$⊢ N = \deg (F)$
3		ftalem.3	$⊢ φ \to F \in Poly (S)$
4		ftalem.4	$⊢ φ \to N \in ℕ$
5		ftalem1.5	$⊢ φ \to E \in ℝ^{+}$
6		ftalem1.6	$⊢ T = \frac{\sum_{k = 0}^{N - 1} \|A (k)\|}{E}$
7		fzfid	$⊢ φ \to (0 \dots N - 1) \in Fin$
8	1	coef3	$⊢ F \in Poly (S) \to A : ℕ_{0} ⟶ ℂ$
9	3 8	syl	$⊢ φ \to A : ℕ_{0} ⟶ ℂ$
10		elfznn0	$⊢ k \in (0 \dots N - 1) \to k \in ℕ_{0}$
11		ffvelcdm	$⊢ (A : ℕ_{0} ⟶ ℂ \land k \in ℕ_{0}) \to A (k) \in ℂ$
12	9 10 11	syl2an	$⊢ (φ \land k \in (0 \dots N - 1)) \to A (k) \in ℂ$
13	12	abscld	$⊢ (φ \land k \in (0 \dots N - 1)) \to \|A (k)\| \in ℝ$
14	7 13	fsumrecl	$⊢ φ \to \sum_{k = 0}^{N - 1} \|A (k)\| \in ℝ$
15	14 5	rerpdivcld	$⊢ φ \to \frac{\sum_{k = 0}^{N - 1} \|A (k)\|}{E} \in ℝ$
16	6 15	eqeltrid	$⊢ φ \to T \in ℝ$
17		1re	$⊢ 1 \in ℝ$
18		ifcl	$⊢ (T \in ℝ \land 1 \in ℝ) \to if (1 \leq T, T, 1) \in ℝ$
19	16 17 18	sylancl	$⊢ φ \to if (1 \leq T, T, 1) \in ℝ$
20		fzfid	$⊢ (φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \to (0 \dots N - 1) \in Fin$
21	9	adantr	$⊢ (φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \to A : ℕ_{0} ⟶ ℂ$
22	21 11	sylan	$⊢ ((φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \land k \in ℕ_{0}) \to A (k) \in ℂ$
23		simprl	$⊢ (φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \to x \in ℂ$
24		expcl	$⊢ (x \in ℂ \land k \in ℕ_{0}) \to x^{k} \in ℂ$
25	23 24	sylan	$⊢ ((φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \land k \in ℕ_{0}) \to x^{k} \in ℂ$
26	22 25	mulcld	$⊢ ((φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \land k \in ℕ_{0}) \to A (k) x^{k} \in ℂ$
27	10 26	sylan2	$⊢ ((φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \land k \in (0 \dots N - 1)) \to A (k) x^{k} \in ℂ$
28	20 27	fsumcl	$⊢ (φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \to \sum_{k = 0}^{N - 1} A (k) x^{k} \in ℂ$
29	4	nnnn0d	$⊢ φ \to N \in ℕ_{0}$
30	29	adantr	$⊢ (φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \to N \in ℕ_{0}$
31	21 30	ffvelcdmd	$⊢ (φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \to A (N) \in ℂ$
32	23 30	expcld	$⊢ (φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \to x^{N} \in ℂ$
33	31 32	mulcld	$⊢ (φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \to A (N) x^{N} \in ℂ$
34	3	adantr	$⊢ (φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \to F \in Poly (S)$
35	1 2	coeid2	$⊢ (F \in Poly (S) \land x \in ℂ) \to F (x) = \sum_{k = 0}^{N} A (k) x^{k}$
36	34 23 35	syl2anc	$⊢ (φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \to F (x) = \sum_{k = 0}^{N} A (k) x^{k}$
37		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
38	30 37	eleqtrdi	$⊢ (φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \to N \in ℤ_{\geq 0}$
39		elfznn0	$⊢ k \in (0 \dots N) \to k \in ℕ_{0}$
40	39 26	sylan2	$⊢ ((φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \land k \in (0 \dots N)) \to A (k) x^{k} \in ℂ$
41		fveq2	$⊢ k = N \to A (k) = A (N)$
42		oveq2	$⊢ k = N \to x^{k} = x^{N}$
43	41 42	oveq12d	$⊢ k = N \to A (k) x^{k} = A (N) x^{N}$
44	38 40 43	fsumm1	$⊢ (φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \to \sum_{k = 0}^{N} A (k) x^{k} = \sum_{k = 0}^{N - 1} A (k) x^{k} + A (N) x^{N}$
45	36 44	eqtrd	$⊢ (φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \to F (x) = \sum_{k = 0}^{N - 1} A (k) x^{k} + A (N) x^{N}$
46	28 33 45	mvrraddd	$⊢ (φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \to F (x) - A (N) x^{N} = \sum_{k = 0}^{N - 1} A (k) x^{k}$
47	46	fveq2d	$⊢ (φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \to \|F (x) - A (N) x^{N}\| = \|\sum_{k = 0}^{N - 1} A (k) x^{k}\|$
48	28	abscld	$⊢ (φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \to \|\sum_{k = 0}^{N - 1} A (k) x^{k}\| \in ℝ$
49	27	abscld	$⊢ ((φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \land k \in (0 \dots N - 1)) \to \|A (k) x^{k}\| \in ℝ$
50	20 49	fsumrecl	$⊢ (φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \to \sum_{k = 0}^{N - 1} \|A (k) x^{k}\| \in ℝ$
51	5	adantr	$⊢ (φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \to E \in ℝ^{+}$
52	51	rpred	$⊢ (φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \to E \in ℝ$
53	23	abscld	$⊢ (φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \to \|x\| \in ℝ$
54	53 30	reexpcld	$⊢ (φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \to {\|x\|}^{N} \in ℝ$
55	52 54	remulcld	$⊢ (φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \to E {\|x\|}^{N} \in ℝ$
56	20 27	fsumabs	$⊢ (φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \to \|\sum_{k = 0}^{N - 1} A (k) x^{k}\| \leq \sum_{k = 0}^{N - 1} \|A (k) x^{k}\|$
57	14	adantr	$⊢ (φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \to \sum_{k = 0}^{N - 1} \|A (k)\| \in ℝ$
58	4	adantr	$⊢ (φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \to N \in ℕ$
59		nnm1nn0	$⊢ N \in ℕ \to N - 1 \in ℕ_{0}$
60	58 59	syl	$⊢ (φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \to N - 1 \in ℕ_{0}$
61	53 60	reexpcld	$⊢ (φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \to {\|x\|}^{N - 1} \in ℝ$
62	57 61	remulcld	$⊢ (φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \to \sum_{k = 0}^{N - 1} \|A (k)\| {\|x\|}^{N - 1} \in ℝ$
63	13	adantlr	$⊢ ((φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \land k \in (0 \dots N - 1)) \to \|A (k)\| \in ℝ$
64	61	adantr	$⊢ ((φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \land k \in (0 \dots N - 1)) \to {\|x\|}^{N - 1} \in ℝ$
65	63 64	remulcld	$⊢ ((φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \land k \in (0 \dots N - 1)) \to \|A (k)\| {\|x\|}^{N - 1} \in ℝ$
66	22 25	absmuld	$⊢ ((φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \land k \in ℕ_{0}) \to \|A (k) x^{k}\| = \|A (k)\| \|x^{k}\|$
67	10 66	sylan2	$⊢ ((φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \land k \in (0 \dots N - 1)) \to \|A (k) x^{k}\| = \|A (k)\| \|x^{k}\|$
68	10 25	sylan2	$⊢ ((φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \land k \in (0 \dots N - 1)) \to x^{k} \in ℂ$
69	68	abscld	$⊢ ((φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \land k \in (0 \dots N - 1)) \to \|x^{k}\| \in ℝ$
70	10 22	sylan2	$⊢ ((φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \land k \in (0 \dots N - 1)) \to A (k) \in ℂ$
71	70	absge0d	$⊢ ((φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \land k \in (0 \dots N - 1)) \to 0 \leq \|A (k)\|$
72		absexp	$⊢ (x \in ℂ \land k \in ℕ_{0}) \to \|x^{k}\| = {\|x\|}^{k}$
73	23 10 72	syl2an	$⊢ ((φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \land k \in (0 \dots N - 1)) \to \|x^{k}\| = {\|x\|}^{k}$
74	53	adantr	$⊢ ((φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \land k \in (0 \dots N - 1)) \to \|x\| \in ℝ$
75	17	a1i	$⊢ (φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \to 1 \in ℝ$
76	19	adantr	$⊢ (φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \to if (1 \leq T, T, 1) \in ℝ$
77		max1	$⊢ (1 \in ℝ \land T \in ℝ) \to 1 \leq if (1 \leq T, T, 1)$
78	17 16 77	sylancr	$⊢ φ \to 1 \leq if (1 \leq T, T, 1)$
79	78	adantr	$⊢ (φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \to 1 \leq if (1 \leq T, T, 1)$
80		simprr	$⊢ (φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \to if (1 \leq T, T, 1) < \|x\|$
81	75 76 53 79 80	lelttrd	$⊢ (φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \to 1 < \|x\|$
82	75 53 81	ltled	$⊢ (φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \to 1 \leq \|x\|$
83	82	adantr	$⊢ ((φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \land k \in (0 \dots N - 1)) \to 1 \leq \|x\|$
84		elfzuz3	$⊢ k \in (0 \dots N - 1) \to N - 1 \in ℤ_{\geq k}$
85	84	adantl	$⊢ ((φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \land k \in (0 \dots N - 1)) \to N - 1 \in ℤ_{\geq k}$
86	74 83 85	leexp2ad	$⊢ ((φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \land k \in (0 \dots N - 1)) \to {\|x\|}^{k} \leq {\|x\|}^{N - 1}$
87	73 86	eqbrtrd	$⊢ ((φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \land k \in (0 \dots N - 1)) \to \|x^{k}\| \leq {\|x\|}^{N - 1}$
88	69 64 63 71 87	lemul2ad	$⊢ ((φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \land k \in (0 \dots N - 1)) \to \|A (k)\| \|x^{k}\| \leq \|A (k)\| {\|x\|}^{N - 1}$
89	67 88	eqbrtrd	$⊢ ((φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \land k \in (0 \dots N - 1)) \to \|A (k) x^{k}\| \leq \|A (k)\| {\|x\|}^{N - 1}$
90	20 49 65 89	fsumle	$⊢ (φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \to \sum_{k = 0}^{N - 1} \|A (k) x^{k}\| \leq \sum_{k = 0}^{N - 1} \|A (k)\| {\|x\|}^{N - 1}$
91	61	recnd	$⊢ (φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \to {\|x\|}^{N - 1} \in ℂ$
92	63	recnd	$⊢ ((φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \land k \in (0 \dots N - 1)) \to \|A (k)\| \in ℂ$
93	20 91 92	fsummulc1	$⊢ (φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \to \sum_{k = 0}^{N - 1} \|A (k)\| {\|x\|}^{N - 1} = \sum_{k = 0}^{N - 1} \|A (k)\| {\|x\|}^{N - 1}$
94	90 93	breqtrrd	$⊢ (φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \to \sum_{k = 0}^{N - 1} \|A (k) x^{k}\| \leq \sum_{k = 0}^{N - 1} \|A (k)\| {\|x\|}^{N - 1}$
95	16	adantr	$⊢ (φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \to T \in ℝ$
96		max2	$⊢ (1 \in ℝ \land T \in ℝ) \to T \leq if (1 \leq T, T, 1)$
97	17 16 96	sylancr	$⊢ φ \to T \leq if (1 \leq T, T, 1)$
98	97	adantr	$⊢ (φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \to T \leq if (1 \leq T, T, 1)$
99	95 76 53 98 80	lelttrd	$⊢ (φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \to T < \|x\|$
100	6 99	eqbrtrrid	$⊢ (φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \to \frac{\sum_{k = 0}^{N - 1} \|A (k)\|}{E} < \|x\|$
101	57 53 51	ltdivmuld	$⊢ (φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \to (\frac{\sum_{k = 0}^{N - 1} \|A (k)\|}{E} < \|x\| \leftrightarrow \sum_{k = 0}^{N - 1} \|A (k)\| < E \|x\|)$
102	100 101	mpbid	$⊢ (φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \to \sum_{k = 0}^{N - 1} \|A (k)\| < E \|x\|$
103	52 53	remulcld	$⊢ (φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \to E \|x\| \in ℝ$
104	60	nn0zd	$⊢ (φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \to N - 1 \in ℤ$
105		0red	$⊢ (φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \to 0 \in ℝ$
106		0lt1	$⊢ 0 < 1$
107	106	a1i	$⊢ (φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \to 0 < 1$
108	105 75 53 107 81	lttrd	$⊢ (φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \to 0 < \|x\|$
109		expgt0	$⊢ (\|x\| \in ℝ \land N - 1 \in ℤ \land 0 < \|x\|) \to 0 < {\|x\|}^{N - 1}$
110	53 104 108 109	syl3anc	$⊢ (φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \to 0 < {\|x\|}^{N - 1}$
111		ltmul1	$⊢ (\sum_{k = 0}^{N - 1} \|A (k)\| \in ℝ \land E \|x\| \in ℝ \land ({\|x\|}^{N - 1} \in ℝ \land 0 < {\|x\|}^{N - 1})) \to (\sum_{k = 0}^{N - 1} \|A (k)\| < E \|x\| \leftrightarrow \sum_{k = 0}^{N - 1} \|A (k)\| {\|x\|}^{N - 1} < E \|x\| {\|x\|}^{N - 1})$
112	57 103 61 110 111	syl112anc	$⊢ (φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \to (\sum_{k = 0}^{N - 1} \|A (k)\| < E \|x\| \leftrightarrow \sum_{k = 0}^{N - 1} \|A (k)\| {\|x\|}^{N - 1} < E \|x\| {\|x\|}^{N - 1})$
113	102 112	mpbid	$⊢ (φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \to \sum_{k = 0}^{N - 1} \|A (k)\| {\|x\|}^{N - 1} < E \|x\| {\|x\|}^{N - 1}$
114	53	recnd	$⊢ (φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \to \|x\| \in ℂ$
115		expm1t	$⊢ (\|x\| \in ℂ \land N \in ℕ) \to {\|x\|}^{N} = {\|x\|}^{N - 1} \|x\|$
116	114 58 115	syl2anc	$⊢ (φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \to {\|x\|}^{N} = {\|x\|}^{N - 1} \|x\|$
117	91 114	mulcomd	$⊢ (φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \to {\|x\|}^{N - 1} \|x\| = \|x\| {\|x\|}^{N - 1}$
118	116 117	eqtrd	$⊢ (φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \to {\|x\|}^{N} = \|x\| {\|x\|}^{N - 1}$
119	118	oveq2d	$⊢ (φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \to E {\|x\|}^{N} = E \|x\| {\|x\|}^{N - 1}$
120	52	recnd	$⊢ (φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \to E \in ℂ$
121	120 114 91	mulassd	$⊢ (φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \to E \|x\| {\|x\|}^{N - 1} = E \|x\| {\|x\|}^{N - 1}$
122	119 121	eqtr4d	$⊢ (φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \to E {\|x\|}^{N} = E \|x\| {\|x\|}^{N - 1}$
123	113 122	breqtrrd	$⊢ (φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \to \sum_{k = 0}^{N - 1} \|A (k)\| {\|x\|}^{N - 1} < E {\|x\|}^{N}$
124	50 62 55 94 123	lelttrd	$⊢ (φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \to \sum_{k = 0}^{N - 1} \|A (k) x^{k}\| < E {\|x\|}^{N}$
125	48 50 55 56 124	lelttrd	$⊢ (φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \to \|\sum_{k = 0}^{N - 1} A (k) x^{k}\| < E {\|x\|}^{N}$
126	47 125	eqbrtrd	$⊢ (φ \land (x \in ℂ \land if (1 \leq T, T, 1) < \|x\|)) \to \|F (x) - A (N) x^{N}\| < E {\|x\|}^{N}$
127	126	expr	$⊢ (φ \land x \in ℂ) \to (if (1 \leq T, T, 1) < \|x\| \to \|F (x) - A (N) x^{N}\| < E {\|x\|}^{N})$
128	127	ralrimiva	$⊢ φ \to \forall x \in ℂ (if (1 \leq T, T, 1) < \|x\| \to \|F (x) - A (N) x^{N}\| < E {\|x\|}^{N})$
129		breq1	$⊢ r = if (1 \leq T, T, 1) \to (r < \|x\| \leftrightarrow if (1 \leq T, T, 1) < \|x\|)$
130	129	rspceaimv	$⊢ (if (1 \leq T, T, 1) \in ℝ \land \forall x \in ℂ (if (1 \leq T, T, 1) < \|x\| \to \|F (x) - A (N) x^{N}\| < E {\|x\|}^{N})) \to \exists r \in ℝ \forall x \in ℂ (r < \|x\| \to \|F (x) - A (N) x^{N}\| < E {\|x\|}^{N})$
131	19 128 130	syl2anc	$⊢ φ \to \exists r \in ℝ \forall x \in ℂ (r < \|x\| \to \|F (x) - A (N) x^{N}\| < E {\|x\|}^{N})$

Metamath Proof Explorer

Theorem ftalem1

Proof