ftalem2

Description: Lemma for fta . There exists some r such that F has magnitude greater than F ( 0 ) outside the closed ball B(0,r). (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 ℕ$
	ftalem2.5	$⊢ U = if (if (1 \leq s, s, 1) \leq T, T, if (1 \leq s, s, 1))$
	ftalem2.6	$⊢ T = \frac{\|F (0)\|}{\frac{\|A (N)\|}{2}}$
Assertion	ftalem2	$⊢ φ \to \exists r \in ℝ^{+} \forall x \in ℂ (r < \|x\| \to \|F (0)\| < \|F (x)\|)$

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		ftalem2.5	$⊢ U = if (if (1 \leq s, s, 1) \leq T, T, if (1 \leq s, s, 1))$
6		ftalem2.6	$⊢ T = \frac{\|F (0)\|}{\frac{\|A (N)\|}{2}}$
7	1	coef3	$⊢ F \in Poly (S) \to A : ℕ_{0} ⟶ ℂ$
8	3 7	syl	$⊢ φ \to A : ℕ_{0} ⟶ ℂ$
9	4	nnnn0d	$⊢ φ \to N \in ℕ_{0}$
10	8 9	ffvelrnd	$⊢ φ \to A (N) \in ℂ$
11	4	nnne0d	$⊢ φ \to N \neq 0$
12	2 1	dgreq0	$⊢ F \in Poly (S) \to (F = 0_{𝑝} \leftrightarrow A (N) = 0)$
13		fveq2	$⊢ F = 0_{𝑝} \to \deg (F) = \deg (0_{𝑝})$
14		dgr0	$⊢ \deg (0_{𝑝}) = 0$
15	13 14	eqtrdi	$⊢ F = 0_{𝑝} \to \deg (F) = 0$
16	2 15	eqtrid	$⊢ F = 0_{𝑝} \to N = 0$
17	12 16	syl6bir	$⊢ F \in Poly (S) \to (A (N) = 0 \to N = 0)$
18	3 17	syl	$⊢ φ \to (A (N) = 0 \to N = 0)$
19	18	necon3d	$⊢ φ \to (N \neq 0 \to A (N) \neq 0)$
20	11 19	mpd	$⊢ φ \to A (N) \neq 0$
21	10 20	absrpcld	$⊢ φ \to \|A (N)\| \in ℝ^{+}$
22	21	rphalfcld	$⊢ φ \to \frac{\|A (N)\|}{2} \in ℝ^{+}$
23		2fveq3	$⊢ n = k \to \|A (n)\| = \|A (k)\|$
24	23	cbvsumv	$⊢ \sum_{n = 0}^{N - 1} \|A (n)\| = \sum_{k = 0}^{N - 1} \|A (k)\|$
25	24	oveq1i	$⊢ \frac{\sum_{n = 0}^{N - 1} \|A (n)\|}{\frac{\|A (N)\|}{2}} = \frac{\sum_{k = 0}^{N - 1} \|A (k)\|}{\frac{\|A (N)\|}{2}}$
26	1 2 3 4 22 25	ftalem1	$⊢ φ \to \exists s \in ℝ \forall x \in ℂ (s < \|x\| \to \|F (x) - A (N) x^{N}\| < (\frac{\|A (N)\|}{2}) {\|x\|}^{N})$
27		plyf	$⊢ F \in Poly (S) \to F : ℂ ⟶ ℂ$
28	3 27	syl	$⊢ φ \to F : ℂ ⟶ ℂ$
29		0cn	$⊢ 0 \in ℂ$
30		ffvelrn	$⊢ (F : ℂ ⟶ ℂ \land 0 \in ℂ) \to F (0) \in ℂ$
31	28 29 30	sylancl	$⊢ φ \to F (0) \in ℂ$
32	31	abscld	$⊢ φ \to \|F (0)\| \in ℝ$
33	32 22	rerpdivcld	$⊢ φ \to \frac{\|F (0)\|}{\frac{\|A (N)\|}{2}} \in ℝ$
34	6 33	eqeltrid	$⊢ φ \to T \in ℝ$
35	34	adantr	$⊢ (φ \land s \in ℝ) \to T \in ℝ$
36		simpr	$⊢ (φ \land s \in ℝ) \to s \in ℝ$
37		1re	$⊢ 1 \in ℝ$
38		ifcl	$⊢ (s \in ℝ \land 1 \in ℝ) \to if (1 \leq s, s, 1) \in ℝ$
39	36 37 38	sylancl	$⊢ (φ \land s \in ℝ) \to if (1 \leq s, s, 1) \in ℝ$
40	35 39	ifcld	$⊢ (φ \land s \in ℝ) \to if (if (1 \leq s, s, 1) \leq T, T, if (1 \leq s, s, 1)) \in ℝ$
41	5 40	eqeltrid	$⊢ (φ \land s \in ℝ) \to U \in ℝ$
42		0red	$⊢ (φ \land s \in ℝ) \to 0 \in ℝ$
43		1red	$⊢ (φ \land s \in ℝ) \to 1 \in ℝ$
44		0lt1	$⊢ 0 < 1$
45	44	a1i	$⊢ (φ \land s \in ℝ) \to 0 < 1$
46		max1	$⊢ (1 \in ℝ \land s \in ℝ) \to 1 \leq if (1 \leq s, s, 1)$
47	37 36 46	sylancr	$⊢ (φ \land s \in ℝ) \to 1 \leq if (1 \leq s, s, 1)$
48		max1	$⊢ (if (1 \leq s, s, 1) \in ℝ \land T \in ℝ) \to if (1 \leq s, s, 1) \leq if (if (1 \leq s, s, 1) \leq T, T, if (1 \leq s, s, 1))$
49	39 35 48	syl2anc	$⊢ (φ \land s \in ℝ) \to if (1 \leq s, s, 1) \leq if (if (1 \leq s, s, 1) \leq T, T, if (1 \leq s, s, 1))$
50	49 5	breqtrrdi	$⊢ (φ \land s \in ℝ) \to if (1 \leq s, s, 1) \leq U$
51	43 39 41 47 50	letrd	$⊢ (φ \land s \in ℝ) \to 1 \leq U$
52	42 43 41 45 51	ltletrd	$⊢ (φ \land s \in ℝ) \to 0 < U$
53	41 52	elrpd	$⊢ (φ \land s \in ℝ) \to U \in ℝ^{+}$
54		max2	$⊢ (1 \in ℝ \land s \in ℝ) \to s \leq if (1 \leq s, s, 1)$
55	37 36 54	sylancr	$⊢ (φ \land s \in ℝ) \to s \leq if (1 \leq s, s, 1)$
56	36 39 41 55 50	letrd	$⊢ (φ \land s \in ℝ) \to s \leq U$
57	56	adantr	$⊢ ((φ \land s \in ℝ) \land x \in ℂ) \to s \leq U$
58		abscl	$⊢ x \in ℂ \to \|x\| \in ℝ$
59		lelttr	$⊢ (s \in ℝ \land U \in ℝ \land \|x\| \in ℝ) \to ((s \leq U \land U < \|x\|) \to s < \|x\|)$
60	36 41 58 59	syl2an3an	$⊢ ((φ \land s \in ℝ) \land x \in ℂ) \to ((s \leq U \land U < \|x\|) \to s < \|x\|)$
61	57 60	mpand	$⊢ ((φ \land s \in ℝ) \land x \in ℂ) \to (U < \|x\| \to s < \|x\|)$
62	61	imim1d	$⊢ ((φ \land s \in ℝ) \land x \in ℂ) \to ((s < \|x\| \to \|F (x) - A (N) x^{N}\| < (\frac{\|A (N)\|}{2}) {\|x\|}^{N}) \to (U < \|x\| \to \|F (x) - A (N) x^{N}\| < (\frac{\|A (N)\|}{2}) {\|x\|}^{N}))$
63	28	ad2antrr	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to F : ℂ ⟶ ℂ$
64		simprl	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to x \in ℂ$
65	63 64	ffvelrnd	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to F (x) \in ℂ$
66	10	ad2antrr	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to A (N) \in ℂ$
67	9	ad2antrr	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to N \in ℕ_{0}$
68	64 67	expcld	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to x^{N} \in ℂ$
69	66 68	mulcld	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to A (N) x^{N} \in ℂ$
70	65 69	subcld	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to F (x) - A (N) x^{N} \in ℂ$
71	70	abscld	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to \|F (x) - A (N) x^{N}\| \in ℝ$
72	69	abscld	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to \|A (N) x^{N}\| \in ℝ$
73	72	rehalfcld	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to \frac{\|A (N) x^{N}\|}{2} \in ℝ$
74	71 73 72	ltsub2d	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to (\|F (x) - A (N) x^{N}\| < \frac{\|A (N) x^{N}\|}{2} \leftrightarrow \|A (N) x^{N}\| - (\frac{\|A (N) x^{N}\|}{2}) < \|A (N) x^{N}\| - \|F (x) - A (N) x^{N}\|)$
75	66 68	absmuld	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to \|A (N) x^{N}\| = \|A (N)\| \|x^{N}\|$
76	64 67	absexpd	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to \|x^{N}\| = {\|x\|}^{N}$
77	76	oveq2d	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to \|A (N)\| \|x^{N}\| = \|A (N)\| {\|x\|}^{N}$
78	75 77	eqtrd	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to \|A (N) x^{N}\| = \|A (N)\| {\|x\|}^{N}$
79	78	oveq1d	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to \frac{\|A (N) x^{N}\|}{2} = \frac{\|A (N)\| {\|x\|}^{N}}{2}$
80	66	abscld	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to \|A (N)\| \in ℝ$
81	80	recnd	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to \|A (N)\| \in ℂ$
82	58	ad2antrl	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to \|x\| \in ℝ$
83	82 67	reexpcld	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to {\|x\|}^{N} \in ℝ$
84	83	recnd	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to {\|x\|}^{N} \in ℂ$
85		2cnd	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to 2 \in ℂ$
86		2ne0	$⊢ 2 \neq 0$
87	86	a1i	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to 2 \neq 0$
88	81 84 85 87	div23d	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to \frac{\|A (N)\| {\|x\|}^{N}}{2} = (\frac{\|A (N)\|}{2}) {\|x\|}^{N}$
89	79 88	eqtrd	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to \frac{\|A (N) x^{N}\|}{2} = (\frac{\|A (N)\|}{2}) {\|x\|}^{N}$
90	89	breq2d	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to (\|F (x) - A (N) x^{N}\| < \frac{\|A (N) x^{N}\|}{2} \leftrightarrow \|F (x) - A (N) x^{N}\| < (\frac{\|A (N)\|}{2}) {\|x\|}^{N})$
91	72	recnd	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to \|A (N) x^{N}\| \in ℂ$
92	91	2halvesd	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to (\frac{\|A (N) x^{N}\|}{2}) + (\frac{\|A (N) x^{N}\|}{2}) = \|A (N) x^{N}\|$
93	92	oveq1d	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to (\frac{\|A (N) x^{N}\|}{2}) + (\frac{\|A (N) x^{N}\|}{2}) - (\frac{\|A (N) x^{N}\|}{2}) = \|A (N) x^{N}\| - (\frac{\|A (N) x^{N}\|}{2})$
94	73	recnd	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to \frac{\|A (N) x^{N}\|}{2} \in ℂ$
95	94 94	pncand	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to (\frac{\|A (N) x^{N}\|}{2}) + (\frac{\|A (N) x^{N}\|}{2}) - (\frac{\|A (N) x^{N}\|}{2}) = \frac{\|A (N) x^{N}\|}{2}$
96	93 95	eqtr3d	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to \|A (N) x^{N}\| - (\frac{\|A (N) x^{N}\|}{2}) = \frac{\|A (N) x^{N}\|}{2}$
97	96	breq1d	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to (\|A (N) x^{N}\| - (\frac{\|A (N) x^{N}\|}{2}) < \|A (N) x^{N}\| - \|F (x) - A (N) x^{N}\| \leftrightarrow \frac{\|A (N) x^{N}\|}{2} < \|A (N) x^{N}\| - \|F (x) - A (N) x^{N}\|)$
98	74 90 97	3bitr3d	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to (\|F (x) - A (N) x^{N}\| < (\frac{\|A (N)\|}{2}) {\|x\|}^{N} \leftrightarrow \frac{\|A (N) x^{N}\|}{2} < \|A (N) x^{N}\| - \|F (x) - A (N) x^{N}\|)$
99	69 65	subcld	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to A (N) x^{N} - F (x) \in ℂ$
100	69 99	abs2difd	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to \|A (N) x^{N}\| - \|A (N) x^{N} - F (x)\| \leq \|A (N) x^{N} - (A (N) x^{N} - F (x))\|$
101	69 65	abssubd	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to \|A (N) x^{N} - F (x)\| = \|F (x) - A (N) x^{N}\|$
102	101	oveq2d	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to \|A (N) x^{N}\| - \|A (N) x^{N} - F (x)\| = \|A (N) x^{N}\| - \|F (x) - A (N) x^{N}\|$
103	69 65	nncand	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to A (N) x^{N} - (A (N) x^{N} - F (x)) = F (x)$
104	103	fveq2d	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to \|A (N) x^{N} - (A (N) x^{N} - F (x))\| = \|F (x)\|$
105	100 102 104	3brtr3d	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to \|A (N) x^{N}\| - \|F (x) - A (N) x^{N}\| \leq \|F (x)\|$
106	72 71	resubcld	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to \|A (N) x^{N}\| - \|F (x) - A (N) x^{N}\| \in ℝ$
107	65	abscld	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to \|F (x)\| \in ℝ$
108		ltletr	$⊢ (\frac{\|A (N) x^{N}\|}{2} \in ℝ \land \|A (N) x^{N}\| - \|F (x) - A (N) x^{N}\| \in ℝ \land \|F (x)\| \in ℝ) \to ((\frac{\|A (N) x^{N}\|}{2} < \|A (N) x^{N}\| - \|F (x) - A (N) x^{N}\| \land \|A (N) x^{N}\| - \|F (x) - A (N) x^{N}\| \leq \|F (x)\|) \to \frac{\|A (N) x^{N}\|}{2} < \|F (x)\|)$
109	73 106 107 108	syl3anc	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to ((\frac{\|A (N) x^{N}\|}{2} < \|A (N) x^{N}\| - \|F (x) - A (N) x^{N}\| \land \|A (N) x^{N}\| - \|F (x) - A (N) x^{N}\| \leq \|F (x)\|) \to \frac{\|A (N) x^{N}\|}{2} < \|F (x)\|)$
110	105 109	mpan2d	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to (\frac{\|A (N) x^{N}\|}{2} < \|A (N) x^{N}\| - \|F (x) - A (N) x^{N}\| \to \frac{\|A (N) x^{N}\|}{2} < \|F (x)\|)$
111	98 110	sylbid	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to (\|F (x) - A (N) x^{N}\| < (\frac{\|A (N)\|}{2}) {\|x\|}^{N} \to \frac{\|A (N) x^{N}\|}{2} < \|F (x)\|)$
112	32	ad2antrr	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to \|F (0)\| \in ℝ$
113	22	ad2antrr	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to \frac{\|A (N)\|}{2} \in ℝ^{+}$
114	113	rpred	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to \frac{\|A (N)\|}{2} \in ℝ$
115	114 82	remulcld	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to (\frac{\|A (N)\|}{2}) \|x\| \in ℝ$
116	89 73	eqeltrrd	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to (\frac{\|A (N)\|}{2}) {\|x\|}^{N} \in ℝ$
117	35	adantr	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to T \in ℝ$
118	41	adantr	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to U \in ℝ$
119		max2	$⊢ (if (1 \leq s, s, 1) \in ℝ \land T \in ℝ) \to T \leq if (if (1 \leq s, s, 1) \leq T, T, if (1 \leq s, s, 1))$
120	39 35 119	syl2anc	$⊢ (φ \land s \in ℝ) \to T \leq if (if (1 \leq s, s, 1) \leq T, T, if (1 \leq s, s, 1))$
121	120 5	breqtrrdi	$⊢ (φ \land s \in ℝ) \to T \leq U$
122	121	adantr	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to T \leq U$
123		simprr	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to U < \|x\|$
124	117 118 82 122 123	lelttrd	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to T < \|x\|$
125	6 124	eqbrtrrid	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to \frac{\|F (0)\|}{\frac{\|A (N)\|}{2}} < \|x\|$
126	112 82 113	ltdivmuld	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to (\frac{\|F (0)\|}{\frac{\|A (N)\|}{2}} < \|x\| \leftrightarrow \|F (0)\| < (\frac{\|A (N)\|}{2}) \|x\|)$
127	125 126	mpbid	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to \|F (0)\| < (\frac{\|A (N)\|}{2}) \|x\|$
128	82	recnd	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to \|x\| \in ℂ$
129	128	exp1d	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to {\|x\|}^{1} = \|x\|$
130		1red	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to 1 \in ℝ$
131	51	adantr	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to 1 \leq U$
132	130 118 82 131 123	lelttrd	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to 1 < \|x\|$
133	130 82 132	ltled	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to 1 \leq \|x\|$
134	4	ad2antrr	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to N \in ℕ$
135		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
136	134 135	eleqtrdi	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to N \in ℤ_{\geq 1}$
137	82 133 136	leexp2ad	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to {\|x\|}^{1} \leq {\|x\|}^{N}$
138	129 137	eqbrtrrd	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to \|x\| \leq {\|x\|}^{N}$
139	82 83 113	lemul2d	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to (\|x\| \leq {\|x\|}^{N} \leftrightarrow (\frac{\|A (N)\|}{2}) \|x\| \leq (\frac{\|A (N)\|}{2}) {\|x\|}^{N})$
140	138 139	mpbid	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to (\frac{\|A (N)\|}{2}) \|x\| \leq (\frac{\|A (N)\|}{2}) {\|x\|}^{N}$
141	112 115 116 127 140	ltletrd	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to \|F (0)\| < (\frac{\|A (N)\|}{2}) {\|x\|}^{N}$
142	141 89	breqtrrd	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to \|F (0)\| < \frac{\|A (N) x^{N}\|}{2}$
143		lttr	$⊢ (\|F (0)\| \in ℝ \land \frac{\|A (N) x^{N}\|}{2} \in ℝ \land \|F (x)\| \in ℝ) \to ((\|F (0)\| < \frac{\|A (N) x^{N}\|}{2} \land \frac{\|A (N) x^{N}\|}{2} < \|F (x)\|) \to \|F (0)\| < \|F (x)\|)$
144	112 73 107 143	syl3anc	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to ((\|F (0)\| < \frac{\|A (N) x^{N}\|}{2} \land \frac{\|A (N) x^{N}\|}{2} < \|F (x)\|) \to \|F (0)\| < \|F (x)\|)$
145	142 144	mpand	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to (\frac{\|A (N) x^{N}\|}{2} < \|F (x)\| \to \|F (0)\| < \|F (x)\|)$
146	111 145	syld	$⊢ ((φ \land s \in ℝ) \land (x \in ℂ \land U < \|x\|)) \to (\|F (x) - A (N) x^{N}\| < (\frac{\|A (N)\|}{2}) {\|x\|}^{N} \to \|F (0)\| < \|F (x)\|)$
147	146	expr	$⊢ ((φ \land s \in ℝ) \land x \in ℂ) \to (U < \|x\| \to (\|F (x) - A (N) x^{N}\| < (\frac{\|A (N)\|}{2}) {\|x\|}^{N} \to \|F (0)\| < \|F (x)\|))$
148	147	a2d	$⊢ ((φ \land s \in ℝ) \land x \in ℂ) \to ((U < \|x\| \to \|F (x) - A (N) x^{N}\| < (\frac{\|A (N)\|}{2}) {\|x\|}^{N}) \to (U < \|x\| \to \|F (0)\| < \|F (x)\|))$
149	62 148	syld	$⊢ ((φ \land s \in ℝ) \land x \in ℂ) \to ((s < \|x\| \to \|F (x) - A (N) x^{N}\| < (\frac{\|A (N)\|}{2}) {\|x\|}^{N}) \to (U < \|x\| \to \|F (0)\| < \|F (x)\|))$
150	149	ralimdva	$⊢ (φ \land s \in ℝ) \to (\forall x \in ℂ (s < \|x\| \to \|F (x) - A (N) x^{N}\| < (\frac{\|A (N)\|}{2}) {\|x\|}^{N}) \to \forall x \in ℂ (U < \|x\| \to \|F (0)\| < \|F (x)\|))$
151		breq1	$⊢ r = U \to (r < \|x\| \leftrightarrow U < \|x\|)$
152	151	rspceaimv	$⊢ (U \in ℝ^{+} \land \forall x \in ℂ (U < \|x\| \to \|F (0)\| < \|F (x)\|)) \to \exists r \in ℝ^{+} \forall x \in ℂ (r < \|x\| \to \|F (0)\| < \|F (x)\|)$
153	53 150 152	syl6an	$⊢ (φ \land s \in ℝ) \to (\forall x \in ℂ (s < \|x\| \to \|F (x) - A (N) x^{N}\| < (\frac{\|A (N)\|}{2}) {\|x\|}^{N}) \to \exists r \in ℝ^{+} \forall x \in ℂ (r < \|x\| \to \|F (0)\| < \|F (x)\|))$
154	153	rexlimdva	$⊢ φ \to (\exists s \in ℝ \forall x \in ℂ (s < \|x\| \to \|F (x) - A (N) x^{N}\| < (\frac{\|A (N)\|}{2}) {\|x\|}^{N}) \to \exists r \in ℝ^{+} \forall x \in ℂ (r < \|x\| \to \|F (0)\| < \|F (x)\|))$
155	26 154	mpd	$⊢ φ \to \exists r \in ℝ^{+} \forall x \in ℂ (r < \|x\| \to \|F (0)\| < \|F (x)\|)$

Metamath Proof Explorer

Theorem ftalem2

Proof