ftalem5

Description: Lemma for fta : Main proof. We have already shifted the minimum found in ftalem3 to zero by a change of variables, and now we show that the minimum value is zero. Expanding in a series about the minimum value, let K be the lowest term in the polynomial that is nonzero, and let T be a K -th root of -u F ( 0 ) / A ( K ) . Then an evaluation of F ( T X ) where X is a sufficiently small positive number yields F ( 0 ) for the first term and -u F ( 0 ) x. X ^ K for the K -th term, and all higher terms are bounded because X is small. Thus, abs ( F ( T X ) ) <_ abs ( F ( 0 ) ) ( 1 - X ^ K ) < abs ( F ( 0 ) ) , in contradiction to our choice of F ( 0 ) as the minimum. (Contributed by Mario Carneiro, 14-Sep-2014) (Revised by AV, 28-Sep-2020)

	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 ℕ$
	ftalem4.5	$⊢ φ \to F (0) \neq 0$
	ftalem4.6	$⊢ K = sup (\{n \in ℕ \| A (n) \neq 0\} ℝ <)$
	ftalem4.7	$⊢ T = {(- (\frac{F (0)}{A (K)}))}^{\frac{1}{K}}$
	ftalem4.8	$⊢ U = \frac{\|F (0)\|}{\sum_{k = K + 1}^{N} \|A (k) T^{k}\| + 1}$
	ftalem4.9	$⊢ X = if (1 \leq U, 1, U)$
Assertion	ftalem5	$⊢ φ \to \exists x \in ℂ \|F (x)\| < \|F (0)\|$

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		ftalem4.5	$⊢ φ \to F (0) \neq 0$
6		ftalem4.6	$⊢ K = sup (\{n \in ℕ \| A (n) \neq 0\} ℝ <)$
7		ftalem4.7	$⊢ T = {(- (\frac{F (0)}{A (K)}))}^{\frac{1}{K}}$
8		ftalem4.8	$⊢ U = \frac{\|F (0)\|}{\sum_{k = K + 1}^{N} \|A (k) T^{k}\| + 1}$
9		ftalem4.9	$⊢ X = if (1 \leq U, 1, U)$
10	1 2 3 4 5 6 7 8 9	ftalem4	$⊢ φ \to ((K \in ℕ \land A (K) \neq 0) \land (T \in ℂ \land U \in ℝ^{+} \land X \in ℝ^{+}))$
11	10	simprd	$⊢ φ \to (T \in ℂ \land U \in ℝ^{+} \land X \in ℝ^{+})$
12	11	simp1d	$⊢ φ \to T \in ℂ$
13	11	simp3d	$⊢ φ \to X \in ℝ^{+}$
14	13	rpred	$⊢ φ \to X \in ℝ$
15	14	recnd	$⊢ φ \to X \in ℂ$
16	12 15	mulcld	$⊢ φ \to T X \in ℂ$
17		plyf	$⊢ F \in Poly (S) \to F : ℂ ⟶ ℂ$
18	3 17	syl	$⊢ φ \to F : ℂ ⟶ ℂ$
19	18 16	ffvelcdmd	$⊢ φ \to F (T X) \in ℂ$
20	19	abscld	$⊢ φ \to \|F (T X)\| \in ℝ$
21		0cn	$⊢ 0 \in ℂ$
22		ffvelcdm	$⊢ (F : ℂ ⟶ ℂ \land 0 \in ℂ) \to F (0) \in ℂ$
23	18 21 22	sylancl	$⊢ φ \to F (0) \in ℂ$
24	23	abscld	$⊢ φ \to \|F (0)\| \in ℝ$
25	10	simpld	$⊢ φ \to (K \in ℕ \land A (K) \neq 0)$
26	25	simpld	$⊢ φ \to K \in ℕ$
27	26	nnnn0d	$⊢ φ \to K \in ℕ_{0}$
28	14 27	reexpcld	$⊢ φ \to X^{K} \in ℝ$
29	24 28	remulcld	$⊢ φ \to \|F (0)\| X^{K} \in ℝ$
30	24 29	resubcld	$⊢ φ \to \|F (0)\| - \|F (0)\| X^{K} \in ℝ$
31		fzfid	$⊢ φ \to (K + 1 \dots N) \in Fin$
32	1	coef3	$⊢ F \in Poly (S) \to A : ℕ_{0} ⟶ ℂ$
33	3 32	syl	$⊢ φ \to A : ℕ_{0} ⟶ ℂ$
34		peano2nn0	$⊢ K \in ℕ_{0} \to K + 1 \in ℕ_{0}$
35	27 34	syl	$⊢ φ \to K + 1 \in ℕ_{0}$
36		elfzuz	$⊢ k \in (K + 1 \dots N) \to k \in ℤ_{\geq (K + 1)}$
37		eluznn0	$⊢ (K + 1 \in ℕ_{0} \land k \in ℤ_{\geq (K + 1)}) \to k \in ℕ_{0}$
38	35 36 37	syl2an	$⊢ (φ \land k \in (K + 1 \dots N)) \to k \in ℕ_{0}$
39		ffvelcdm	$⊢ (A : ℕ_{0} ⟶ ℂ \land k \in ℕ_{0}) \to A (k) \in ℂ$
40	33 38 39	syl2an2r	$⊢ (φ \land k \in (K + 1 \dots N)) \to A (k) \in ℂ$
41	16	adantr	$⊢ (φ \land k \in (K + 1 \dots N)) \to T X \in ℂ$
42	41 38	expcld	$⊢ (φ \land k \in (K + 1 \dots N)) \to {T X}^{k} \in ℂ$
43	40 42	mulcld	$⊢ (φ \land k \in (K + 1 \dots N)) \to A (k) {T X}^{k} \in ℂ$
44	31 43	fsumcl	$⊢ φ \to \sum_{k = K + 1}^{N} A (k) {T X}^{k} \in ℂ$
45	44	abscld	$⊢ φ \to \|\sum_{k = K + 1}^{N} A (k) {T X}^{k}\| \in ℝ$
46	30 45	readdcld	$⊢ φ \to \|F (0)\| - \|F (0)\| X^{K} + \|\sum_{k = K + 1}^{N} A (k) {T X}^{k}\| \in ℝ$
47		fzfid	$⊢ φ \to (0 \dots K) \in Fin$
48		elfznn0	$⊢ k \in (0 \dots K) \to k \in ℕ_{0}$
49	33 48 39	syl2an	$⊢ (φ \land k \in (0 \dots K)) \to A (k) \in ℂ$
50		expcl	$⊢ (T X \in ℂ \land k \in ℕ_{0}) \to {T X}^{k} \in ℂ$
51	16 48 50	syl2an	$⊢ (φ \land k \in (0 \dots K)) \to {T X}^{k} \in ℂ$
52	49 51	mulcld	$⊢ (φ \land k \in (0 \dots K)) \to A (k) {T X}^{k} \in ℂ$
53	47 52	fsumcl	$⊢ φ \to \sum_{k = 0}^{K} A (k) {T X}^{k} \in ℂ$
54	53 44	abstrid	$⊢ φ \to \|\sum_{k = 0}^{K} A (k) {T X}^{k} + \sum_{k = K + 1}^{N} A (k) {T X}^{k}\| \leq \|\sum_{k = 0}^{K} A (k) {T X}^{k}\| + \|\sum_{k = K + 1}^{N} A (k) {T X}^{k}\|$
55	1 2	coeid2	$⊢ (F \in Poly (S) \land T X \in ℂ) \to F (T X) = \sum_{k = 0}^{N} A (k) {T X}^{k}$
56	3 16 55	syl2anc	$⊢ φ \to F (T X) = \sum_{k = 0}^{N} A (k) {T X}^{k}$
57	26	nnred	$⊢ φ \to K \in ℝ$
58	57	ltp1d	$⊢ φ \to K < K + 1$
59		fzdisj	$⊢ K < K + 1 \to (0 \dots K) \cap (K + 1 \dots N) = \emptyset$
60	58 59	syl	$⊢ φ \to (0 \dots K) \cap (K + 1 \dots N) = \emptyset$
61		ssrab2	$⊢ \{n \in ℕ \| A (n) \neq 0\} \subseteq ℕ$
62		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
63	61 62	sseqtri	$⊢ \{n \in ℕ \| A (n) \neq 0\} \subseteq ℤ_{\geq 1}$
64		fveq2	$⊢ n = N \to A (n) = A (N)$
65	64	neeq1d	$⊢ n = N \to (A (n) \neq 0 \leftrightarrow A (N) \neq 0)$
66	4	nnne0d	$⊢ φ \to N \neq 0$
67	2 1	dgreq0	$⊢ F \in Poly (S) \to (F = 0_{𝑝} \leftrightarrow A (N) = 0)$
68	3 67	syl	$⊢ φ \to (F = 0_{𝑝} \leftrightarrow A (N) = 0)$
69		fveq2	$⊢ F = 0_{𝑝} \to \deg (F) = \deg (0_{𝑝})$
70		dgr0	$⊢ \deg (0_{𝑝}) = 0$
71	69 70	eqtrdi	$⊢ F = 0_{𝑝} \to \deg (F) = 0$
72	2 71	eqtrid	$⊢ F = 0_{𝑝} \to N = 0$
73	68 72	syl6bir	$⊢ φ \to (A (N) = 0 \to N = 0)$
74	73	necon3d	$⊢ φ \to (N \neq 0 \to A (N) \neq 0)$
75	66 74	mpd	$⊢ φ \to A (N) \neq 0$
76	65 4 75	elrabd	$⊢ φ \to N \in \{n \in ℕ \| A (n) \neq 0\}$
77		infssuzle	$⊢ (\{n \in ℕ \| A (n) \neq 0\} \subseteq ℤ_{\geq 1} \land N \in \{n \in ℕ \| A (n) \neq 0\}) \to sup (\{n \in ℕ \| A (n) \neq 0\} ℝ <) \leq N$
78	63 76 77	sylancr	$⊢ φ \to sup (\{n \in ℕ \| A (n) \neq 0\} ℝ <) \leq N$
79	6 78	eqbrtrid	$⊢ φ \to K \leq N$
80		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
81	27 80	eleqtrdi	$⊢ φ \to K \in ℤ_{\geq 0}$
82	4	nnzd	$⊢ φ \to N \in ℤ$
83		elfz5	$⊢ (K \in ℤ_{\geq 0} \land N \in ℤ) \to (K \in (0 \dots N) \leftrightarrow K \leq N)$
84	81 82 83	syl2anc	$⊢ φ \to (K \in (0 \dots N) \leftrightarrow K \leq N)$
85	79 84	mpbird	$⊢ φ \to K \in (0 \dots N)$
86		fzsplit	$⊢ K \in (0 \dots N) \to (0 \dots N) = (0 \dots K) \cup (K + 1 \dots N)$
87	85 86	syl	$⊢ φ \to (0 \dots N) = (0 \dots K) \cup (K + 1 \dots N)$
88		fzfid	$⊢ φ \to (0 \dots N) \in Fin$
89		elfznn0	$⊢ k \in (0 \dots N) \to k \in ℕ_{0}$
90	33 89 39	syl2an	$⊢ (φ \land k \in (0 \dots N)) \to A (k) \in ℂ$
91	16 89 50	syl2an	$⊢ (φ \land k \in (0 \dots N)) \to {T X}^{k} \in ℂ$
92	90 91	mulcld	$⊢ (φ \land k \in (0 \dots N)) \to A (k) {T X}^{k} \in ℂ$
93	60 87 88 92	fsumsplit	$⊢ φ \to \sum_{k = 0}^{N} A (k) {T X}^{k} = \sum_{k = 0}^{K} A (k) {T X}^{k} + \sum_{k = K + 1}^{N} A (k) {T X}^{k}$
94	56 93	eqtrd	$⊢ φ \to F (T X) = \sum_{k = 0}^{K} A (k) {T X}^{k} + \sum_{k = K + 1}^{N} A (k) {T X}^{k}$
95	94	fveq2d	$⊢ φ \to \|F (T X)\| = \|\sum_{k = 0}^{K} A (k) {T X}^{k} + \sum_{k = K + 1}^{N} A (k) {T X}^{k}\|$
96	1	coefv0	$⊢ F \in Poly (S) \to F (0) = A (0)$
97	3 96	syl	$⊢ φ \to F (0) = A (0)$
98	97	eqcomd	$⊢ φ \to A (0) = F (0)$
99	16	exp0d	$⊢ φ \to {T X}^{0} = 1$
100	98 99	oveq12d	$⊢ φ \to A (0) {T X}^{0} = F (0) \cdot 1$
101	23	mulridd	$⊢ φ \to F (0) \cdot 1 = F (0)$
102	100 101	eqtrd	$⊢ φ \to A (0) {T X}^{0} = F (0)$
103		1e0p1	$⊢ 1 = 0 + 1$
104	103	oveq1i	$⊢ (1 \dots K) = (0 + 1 \dots K)$
105	104	sumeq1i	$⊢ \sum_{k = 1}^{K} A (k) {T X}^{k} = \sum_{k = 0 + 1}^{K} A (k) {T X}^{k}$
106	26 62	eleqtrdi	$⊢ φ \to K \in ℤ_{\geq 1}$
107		elfznn	$⊢ k \in (1 \dots K) \to k \in ℕ$
108	107	nnnn0d	$⊢ k \in (1 \dots K) \to k \in ℕ_{0}$
109	33 108 39	syl2an	$⊢ (φ \land k \in (1 \dots K)) \to A (k) \in ℂ$
110	16 108 50	syl2an	$⊢ (φ \land k \in (1 \dots K)) \to {T X}^{k} \in ℂ$
111	109 110	mulcld	$⊢ (φ \land k \in (1 \dots K)) \to A (k) {T X}^{k} \in ℂ$
112		fveq2	$⊢ k = K \to A (k) = A (K)$
113		oveq2	$⊢ k = K \to {T X}^{k} = {T X}^{K}$
114	112 113	oveq12d	$⊢ k = K \to A (k) {T X}^{k} = A (K) {T X}^{K}$
115	106 111 114	fsumm1	$⊢ φ \to \sum_{k = 1}^{K} A (k) {T X}^{k} = \sum_{k = 1}^{K - 1} A (k) {T X}^{k} + A (K) {T X}^{K}$
116	105 115	eqtr3id	$⊢ φ \to \sum_{k = 0 + 1}^{K} A (k) {T X}^{k} = \sum_{k = 1}^{K - 1} A (k) {T X}^{k} + A (K) {T X}^{K}$
117		elfznn	$⊢ k \in (1 \dots K - 1) \to k \in ℕ$
118	117	adantl	$⊢ (φ \land k \in (1 \dots K - 1)) \to k \in ℕ$
119	118	nnred	$⊢ (φ \land k \in (1 \dots K - 1)) \to k \in ℝ$
120	57	adantr	$⊢ (φ \land k \in (1 \dots K - 1)) \to K \in ℝ$
121		peano2rem	$⊢ K \in ℝ \to K - 1 \in ℝ$
122	120 121	syl	$⊢ (φ \land k \in (1 \dots K - 1)) \to K - 1 \in ℝ$
123		elfzle2	$⊢ k \in (1 \dots K - 1) \to k \leq K - 1$
124	123	adantl	$⊢ (φ \land k \in (1 \dots K - 1)) \to k \leq K - 1$
125	120	ltm1d	$⊢ (φ \land k \in (1 \dots K - 1)) \to K - 1 < K$
126	119 122 120 124 125	lelttrd	$⊢ (φ \land k \in (1 \dots K - 1)) \to k < K$
127	119 120	ltnled	$⊢ (φ \land k \in (1 \dots K - 1)) \to (k < K \leftrightarrow \neg K \leq k)$
128	126 127	mpbid	$⊢ (φ \land k \in (1 \dots K - 1)) \to \neg K \leq k$
129		infssuzle	$⊢ (\{n \in ℕ \| A (n) \neq 0\} \subseteq ℤ_{\geq 1} \land k \in \{n \in ℕ \| A (n) \neq 0\}) \to sup (\{n \in ℕ \| A (n) \neq 0\} ℝ <) \leq k$
130	6 129	eqbrtrid	$⊢ (\{n \in ℕ \| A (n) \neq 0\} \subseteq ℤ_{\geq 1} \land k \in \{n \in ℕ \| A (n) \neq 0\}) \to K \leq k$
131	63 130	mpan	$⊢ k \in \{n \in ℕ \| A (n) \neq 0\} \to K \leq k$
132	128 131	nsyl	$⊢ (φ \land k \in (1 \dots K - 1)) \to \neg k \in \{n \in ℕ \| A (n) \neq 0\}$
133		fveq2	$⊢ n = k \to A (n) = A (k)$
134	133	neeq1d	$⊢ n = k \to (A (n) \neq 0 \leftrightarrow A (k) \neq 0)$
135	134	elrab3	$⊢ k \in ℕ \to (k \in \{n \in ℕ \| A (n) \neq 0\} \leftrightarrow A (k) \neq 0)$
136	118 135	syl	$⊢ (φ \land k \in (1 \dots K - 1)) \to (k \in \{n \in ℕ \| A (n) \neq 0\} \leftrightarrow A (k) \neq 0)$
137	136	necon2bbid	$⊢ (φ \land k \in (1 \dots K - 1)) \to (A (k) = 0 \leftrightarrow \neg k \in \{n \in ℕ \| A (n) \neq 0\})$
138	132 137	mpbird	$⊢ (φ \land k \in (1 \dots K - 1)) \to A (k) = 0$
139	138	oveq1d	$⊢ (φ \land k \in (1 \dots K - 1)) \to A (k) {T X}^{k} = 0 \cdot {T X}^{k}$
140	117	nnnn0d	$⊢ k \in (1 \dots K - 1) \to k \in ℕ_{0}$
141	16 140 50	syl2an	$⊢ (φ \land k \in (1 \dots K - 1)) \to {T X}^{k} \in ℂ$
142	141	mul02d	$⊢ (φ \land k \in (1 \dots K - 1)) \to 0 \cdot {T X}^{k} = 0$
143	139 142	eqtrd	$⊢ (φ \land k \in (1 \dots K - 1)) \to A (k) {T X}^{k} = 0$
144	143	sumeq2dv	$⊢ φ \to \sum_{k = 1}^{K - 1} A (k) {T X}^{k} = \sum_{k = 1}^{K - 1} 0$
145		fzfi	$⊢ (1 \dots K - 1) \in Fin$
146	145	olci	$⊢ ((1 \dots K - 1) \subseteq ℤ_{\geq 1} \lor (1 \dots K - 1) \in Fin)$
147		sumz	$⊢ ((1 \dots K - 1) \subseteq ℤ_{\geq 1} \lor (1 \dots K - 1) \in Fin) \to \sum_{k = 1}^{K - 1} 0 = 0$
148	146 147	ax-mp	$⊢ \sum_{k = 1}^{K - 1} 0 = 0$
149	144 148	eqtrdi	$⊢ φ \to \sum_{k = 1}^{K - 1} A (k) {T X}^{k} = 0$
150	12 15 27	mulexpd	$⊢ φ \to {T X}^{K} = T^{K} X^{K}$
151	150	oveq2d	$⊢ φ \to A (K) {T X}^{K} = A (K) T^{K} X^{K}$
152	33 27	ffvelcdmd	$⊢ φ \to A (K) \in ℂ$
153	12 27	expcld	$⊢ φ \to T^{K} \in ℂ$
154	28	recnd	$⊢ φ \to X^{K} \in ℂ$
155	152 153 154	mulassd	$⊢ φ \to A (K) T^{K} X^{K} = A (K) T^{K} X^{K}$
156	151 155	eqtr4d	$⊢ φ \to A (K) {T X}^{K} = A (K) T^{K} X^{K}$
157	7	oveq1i	$⊢ T^{K} = {({(- \frac{F (0)}{A (K)})}^{\frac{1}{K}})}^{K}$
158	57	recnd	$⊢ φ \to K \in ℂ$
159	26	nnne0d	$⊢ φ \to K \neq 0$
160	158 159	recid2d	$⊢ φ \to (\frac{1}{K}) K = 1$
161	160	oveq2d	$⊢ φ \to {(- (\frac{F (0)}{A (K)}))}^{(\frac{1}{K}) K} = {(- (\frac{F (0)}{A (K)}))}^{1}$
162	25	simprd	$⊢ φ \to A (K) \neq 0$
163	23 152 162	divcld	$⊢ φ \to \frac{F (0)}{A (K)} \in ℂ$
164	163	negcld	$⊢ φ \to - \frac{F (0)}{A (K)} \in ℂ$
165	26	nnrecred	$⊢ φ \to \frac{1}{K} \in ℝ$
166	165	recnd	$⊢ φ \to \frac{1}{K} \in ℂ$
167	164 166 27	cxpmul2d	$⊢ φ \to {(- (\frac{F (0)}{A (K)}))}^{(\frac{1}{K}) K} = {({(- \frac{F (0)}{A (K)})}^{\frac{1}{K}})}^{K}$
168	164	cxp1d	$⊢ φ \to {(- (\frac{F (0)}{A (K)}))}^{1} = - \frac{F (0)}{A (K)}$
169	161 167 168	3eqtr3d	$⊢ φ \to {({(- \frac{F (0)}{A (K)})}^{\frac{1}{K}})}^{K} = - \frac{F (0)}{A (K)}$
170	157 169	eqtrid	$⊢ φ \to T^{K} = - \frac{F (0)}{A (K)}$
171	170	oveq2d	$⊢ φ \to A (K) T^{K} = A (K) (- \frac{F (0)}{A (K)})$
172	152 163	mulneg2d	$⊢ φ \to A (K) (- \frac{F (0)}{A (K)}) = - A (K) (\frac{F (0)}{A (K)})$
173	23 152 162	divcan2d	$⊢ φ \to A (K) (\frac{F (0)}{A (K)}) = F (0)$
174	173	negeqd	$⊢ φ \to - A (K) (\frac{F (0)}{A (K)}) = - F (0)$
175	171 172 174	3eqtrd	$⊢ φ \to A (K) T^{K} = - F (0)$
176	175	oveq1d	$⊢ φ \to A (K) T^{K} X^{K} = (- F (0)) X^{K}$
177	23 154	mulneg1d	$⊢ φ \to (- F (0)) X^{K} = - F (0) X^{K}$
178	156 176 177	3eqtrd	$⊢ φ \to A (K) {T X}^{K} = - F (0) X^{K}$
179	149 178	oveq12d	$⊢ φ \to \sum_{k = 1}^{K - 1} A (k) {T X}^{k} + A (K) {T X}^{K} = 0 + (- F (0) X^{K})$
180	23 154	mulcld	$⊢ φ \to F (0) X^{K} \in ℂ$
181	180	negcld	$⊢ φ \to - F (0) X^{K} \in ℂ$
182	181	addlidd	$⊢ φ \to 0 + (- F (0) X^{K}) = - F (0) X^{K}$
183	116 179 182	3eqtrd	$⊢ φ \to \sum_{k = 0 + 1}^{K} A (k) {T X}^{k} = - F (0) X^{K}$
184	102 183	oveq12d	$⊢ φ \to A (0) {T X}^{0} + \sum_{k = 0 + 1}^{K} A (k) {T X}^{k} = F (0) + (- F (0) X^{K})$
185		fveq2	$⊢ k = 0 \to A (k) = A (0)$
186		oveq2	$⊢ k = 0 \to {T X}^{k} = {T X}^{0}$
187	185 186	oveq12d	$⊢ k = 0 \to A (k) {T X}^{k} = A (0) {T X}^{0}$
188	81 52 187	fsum1p	$⊢ φ \to \sum_{k = 0}^{K} A (k) {T X}^{k} = A (0) {T X}^{0} + \sum_{k = 0 + 1}^{K} A (k) {T X}^{k}$
189	101	oveq1d	$⊢ φ \to F (0) \cdot 1 - F (0) X^{K} = F (0) - F (0) X^{K}$
190		1cnd	$⊢ φ \to 1 \in ℂ$
191	23 190 154	subdid	$⊢ φ \to F (0) (1 - X^{K}) = F (0) \cdot 1 - F (0) X^{K}$
192	23 180	negsubd	$⊢ φ \to F (0) + (- F (0) X^{K}) = F (0) - F (0) X^{K}$
193	189 191 192	3eqtr4d	$⊢ φ \to F (0) (1 - X^{K}) = F (0) + (- F (0) X^{K})$
194	184 188 193	3eqtr4d	$⊢ φ \to \sum_{k = 0}^{K} A (k) {T X}^{k} = F (0) (1 - X^{K})$
195	194	fveq2d	$⊢ φ \to \|\sum_{k = 0}^{K} A (k) {T X}^{k}\| = \|F (0) (1 - X^{K})\|$
196		1re	$⊢ 1 \in ℝ$
197		resubcl	$⊢ (1 \in ℝ \land X^{K} \in ℝ) \to 1 - X^{K} \in ℝ$
198	196 28 197	sylancr	$⊢ φ \to 1 - X^{K} \in ℝ$
199	198	recnd	$⊢ φ \to 1 - X^{K} \in ℂ$
200	23 199	absmuld	$⊢ φ \to \|F (0) (1 - X^{K})\| = \|F (0)\| \|1 - X^{K}\|$
201	13	rpge0d	$⊢ φ \to 0 \leq X$
202	11	simp2d	$⊢ φ \to U \in ℝ^{+}$
203	202	rpred	$⊢ φ \to U \in ℝ$
204		min1	$⊢ (1 \in ℝ \land U \in ℝ) \to if (1 \leq U, 1, U) \leq 1$
205	196 203 204	sylancr	$⊢ φ \to if (1 \leq U, 1, U) \leq 1$
206	9 205	eqbrtrid	$⊢ φ \to X \leq 1$
207		exple1	$⊢ ((X \in ℝ \land 0 \leq X \land X \leq 1) \land K \in ℕ_{0}) \to X^{K} \leq 1$
208	14 201 206 27 207	syl31anc	$⊢ φ \to X^{K} \leq 1$
209		subge0	$⊢ (1 \in ℝ \land X^{K} \in ℝ) \to (0 \leq 1 - X^{K} \leftrightarrow X^{K} \leq 1)$
210	196 28 209	sylancr	$⊢ φ \to (0 \leq 1 - X^{K} \leftrightarrow X^{K} \leq 1)$
211	208 210	mpbird	$⊢ φ \to 0 \leq 1 - X^{K}$
212	198 211	absidd	$⊢ φ \to \|1 - X^{K}\| = 1 - X^{K}$
213	212	oveq2d	$⊢ φ \to \|F (0)\| \|1 - X^{K}\| = \|F (0)\| (1 - X^{K})$
214	24	recnd	$⊢ φ \to \|F (0)\| \in ℂ$
215	214 190 154	subdid	$⊢ φ \to \|F (0)\| (1 - X^{K}) = \|F (0)\| \cdot 1 - \|F (0)\| X^{K}$
216	214	mulridd	$⊢ φ \to \|F (0)\| \cdot 1 = \|F (0)\|$
217	216	oveq1d	$⊢ φ \to \|F (0)\| \cdot 1 - \|F (0)\| X^{K} = \|F (0)\| - \|F (0)\| X^{K}$
218	213 215 217	3eqtrd	$⊢ φ \to \|F (0)\| \|1 - X^{K}\| = \|F (0)\| - \|F (0)\| X^{K}$
219	195 200 218	3eqtrrd	$⊢ φ \to \|F (0)\| - \|F (0)\| X^{K} = \|\sum_{k = 0}^{K} A (k) {T X}^{k}\|$
220	219	oveq1d	$⊢ φ \to \|F (0)\| - \|F (0)\| X^{K} + \|\sum_{k = K + 1}^{N} A (k) {T X}^{k}\| = \|\sum_{k = 0}^{K} A (k) {T X}^{k}\| + \|\sum_{k = K + 1}^{N} A (k) {T X}^{k}\|$
221	54 95 220	3brtr4d	$⊢ φ \to \|F (T X)\| \leq \|F (0)\| - \|F (0)\| X^{K} + \|\sum_{k = K + 1}^{N} A (k) {T X}^{k}\|$
222	43	abscld	$⊢ (φ \land k \in (K + 1 \dots N)) \to \|A (k) {T X}^{k}\| \in ℝ$
223	31 222	fsumrecl	$⊢ φ \to \sum_{k = K + 1}^{N} \|A (k) {T X}^{k}\| \in ℝ$
224	31 43	fsumabs	$⊢ φ \to \|\sum_{k = K + 1}^{N} A (k) {T X}^{k}\| \leq \sum_{k = K + 1}^{N} \|A (k) {T X}^{k}\|$
225		expcl	$⊢ (T \in ℂ \land k \in ℕ_{0}) \to T^{k} \in ℂ$
226	12 38 225	syl2an2r	$⊢ (φ \land k \in (K + 1 \dots N)) \to T^{k} \in ℂ$
227	40 226	mulcld	$⊢ (φ \land k \in (K + 1 \dots N)) \to A (k) T^{k} \in ℂ$
228	227	abscld	$⊢ (φ \land k \in (K + 1 \dots N)) \to \|A (k) T^{k}\| \in ℝ$
229	31 228	fsumrecl	$⊢ φ \to \sum_{k = K + 1}^{N} \|A (k) T^{k}\| \in ℝ$
230	14 35	reexpcld	$⊢ φ \to X^{K + 1} \in ℝ$
231	229 230	remulcld	$⊢ φ \to \sum_{k = K + 1}^{N} \|A (k) T^{k}\| X^{K + 1} \in ℝ$
232	230	adantr	$⊢ (φ \land k \in (K + 1 \dots N)) \to X^{K + 1} \in ℝ$
233	228 232	remulcld	$⊢ (φ \land k \in (K + 1 \dots N)) \to \|A (k) T^{k}\| X^{K + 1} \in ℝ$
234	12	adantr	$⊢ (φ \land k \in (K + 1 \dots N)) \to T \in ℂ$
235	15	adantr	$⊢ (φ \land k \in (K + 1 \dots N)) \to X \in ℂ$
236	234 235 38	mulexpd	$⊢ (φ \land k \in (K + 1 \dots N)) \to {T X}^{k} = T^{k} X^{k}$
237	236	oveq2d	$⊢ (φ \land k \in (K + 1 \dots N)) \to A (k) {T X}^{k} = A (k) T^{k} X^{k}$
238	14	adantr	$⊢ (φ \land k \in (K + 1 \dots N)) \to X \in ℝ$
239	238 38	reexpcld	$⊢ (φ \land k \in (K + 1 \dots N)) \to X^{k} \in ℝ$
240	239	recnd	$⊢ (φ \land k \in (K + 1 \dots N)) \to X^{k} \in ℂ$
241	40 226 240	mulassd	$⊢ (φ \land k \in (K + 1 \dots N)) \to A (k) T^{k} X^{k} = A (k) T^{k} X^{k}$
242	237 241	eqtr4d	$⊢ (φ \land k \in (K + 1 \dots N)) \to A (k) {T X}^{k} = A (k) T^{k} X^{k}$
243	242	fveq2d	$⊢ (φ \land k \in (K + 1 \dots N)) \to \|A (k) {T X}^{k}\| = \|A (k) T^{k} X^{k}\|$
244	227 240	absmuld	$⊢ (φ \land k \in (K + 1 \dots N)) \to \|A (k) T^{k} X^{k}\| = \|A (k) T^{k}\| \|X^{k}\|$
245		elfzelz	$⊢ k \in (K + 1 \dots N) \to k \in ℤ$
246		rpexpcl	$⊢ (X \in ℝ^{+} \land k \in ℤ) \to X^{k} \in ℝ^{+}$
247	13 245 246	syl2an	$⊢ (φ \land k \in (K + 1 \dots N)) \to X^{k} \in ℝ^{+}$
248	247	rpge0d	$⊢ (φ \land k \in (K + 1 \dots N)) \to 0 \leq X^{k}$
249	239 248	absidd	$⊢ (φ \land k \in (K + 1 \dots N)) \to \|X^{k}\| = X^{k}$
250	249	oveq2d	$⊢ (φ \land k \in (K + 1 \dots N)) \to \|A (k) T^{k}\| \|X^{k}\| = \|A (k) T^{k}\| X^{k}$
251	243 244 250	3eqtrd	$⊢ (φ \land k \in (K + 1 \dots N)) \to \|A (k) {T X}^{k}\| = \|A (k) T^{k}\| X^{k}$
252	227	absge0d	$⊢ (φ \land k \in (K + 1 \dots N)) \to 0 \leq \|A (k) T^{k}\|$
253	35	adantr	$⊢ (φ \land k \in (K + 1 \dots N)) \to K + 1 \in ℕ_{0}$
254	36	adantl	$⊢ (φ \land k \in (K + 1 \dots N)) \to k \in ℤ_{\geq (K + 1)}$
255	201	adantr	$⊢ (φ \land k \in (K + 1 \dots N)) \to 0 \leq X$
256	206	adantr	$⊢ (φ \land k \in (K + 1 \dots N)) \to X \leq 1$
257	238 253 254 255 256	leexp2rd	$⊢ (φ \land k \in (K + 1 \dots N)) \to X^{k} \leq X^{K + 1}$
258	239 232 228 252 257	lemul2ad	$⊢ (φ \land k \in (K + 1 \dots N)) \to \|A (k) T^{k}\| X^{k} \leq \|A (k) T^{k}\| X^{K + 1}$
259	251 258	eqbrtrd	$⊢ (φ \land k \in (K + 1 \dots N)) \to \|A (k) {T X}^{k}\| \leq \|A (k) T^{k}\| X^{K + 1}$
260	31 222 233 259	fsumle	$⊢ φ \to \sum_{k = K + 1}^{N} \|A (k) {T X}^{k}\| \leq \sum_{k = K + 1}^{N} \|A (k) T^{k}\| X^{K + 1}$
261	230	recnd	$⊢ φ \to X^{K + 1} \in ℂ$
262	228	recnd	$⊢ (φ \land k \in (K + 1 \dots N)) \to \|A (k) T^{k}\| \in ℂ$
263	31 261 262	fsummulc1	$⊢ φ \to \sum_{k = K + 1}^{N} \|A (k) T^{k}\| X^{K + 1} = \sum_{k = K + 1}^{N} \|A (k) T^{k}\| X^{K + 1}$
264	260 263	breqtrrd	$⊢ φ \to \sum_{k = K + 1}^{N} \|A (k) {T X}^{k}\| \leq \sum_{k = K + 1}^{N} \|A (k) T^{k}\| X^{K + 1}$
265	15 27	expp1d	$⊢ φ \to X^{K + 1} = X^{K} X$
266	154 15	mulcomd	$⊢ φ \to X^{K} X = X X^{K}$
267	265 266	eqtrd	$⊢ φ \to X^{K + 1} = X X^{K}$
268	267	oveq2d	$⊢ φ \to \sum_{k = K + 1}^{N} \|A (k) T^{k}\| X^{K + 1} = \sum_{k = K + 1}^{N} \|A (k) T^{k}\| X X^{K}$
269	229	recnd	$⊢ φ \to \sum_{k = K + 1}^{N} \|A (k) T^{k}\| \in ℂ$
270	269 15 154	mulassd	$⊢ φ \to \sum_{k = K + 1}^{N} \|A (k) T^{k}\| X X^{K} = \sum_{k = K + 1}^{N} \|A (k) T^{k}\| X X^{K}$
271	268 270	eqtr4d	$⊢ φ \to \sum_{k = K + 1}^{N} \|A (k) T^{k}\| X^{K + 1} = \sum_{k = K + 1}^{N} \|A (k) T^{k}\| X X^{K}$
272	229 14	remulcld	$⊢ φ \to \sum_{k = K + 1}^{N} \|A (k) T^{k}\| X \in ℝ$
273		nnssz	$⊢ ℕ \subseteq ℤ$
274	61 273	sstri	$⊢ \{n \in ℕ \| A (n) \neq 0\} \subseteq ℤ$
275	76	ne0d	$⊢ φ \to \{n \in ℕ \| A (n) \neq 0\} \neq \emptyset$
276		infssuzcl	$⊢ (\{n \in ℕ \| A (n) \neq 0\} \subseteq ℤ_{\geq 1} \land \{n \in ℕ \| A (n) \neq 0\} \neq \emptyset) \to sup (\{n \in ℕ \| A (n) \neq 0\} ℝ <) \in \{n \in ℕ \| A (n) \neq 0\}$
277	63 275 276	sylancr	$⊢ φ \to sup (\{n \in ℕ \| A (n) \neq 0\} ℝ <) \in \{n \in ℕ \| A (n) \neq 0\}$
278	6 277	eqeltrid	$⊢ φ \to K \in \{n \in ℕ \| A (n) \neq 0\}$
279	274 278	sselid	$⊢ φ \to K \in ℤ$
280	13 279	rpexpcld	$⊢ φ \to X^{K} \in ℝ^{+}$
281		peano2re	$⊢ \sum_{k = K + 1}^{N} \|A (k) T^{k}\| \in ℝ \to \sum_{k = K + 1}^{N} \|A (k) T^{k}\| + 1 \in ℝ$
282	229 281	syl	$⊢ φ \to \sum_{k = K + 1}^{N} \|A (k) T^{k}\| + 1 \in ℝ$
283	282 14	remulcld	$⊢ φ \to (\sum_{k = K + 1}^{N} \|A (k) T^{k}\| + 1) X \in ℝ$
284	229	ltp1d	$⊢ φ \to \sum_{k = K + 1}^{N} \|A (k) T^{k}\| < \sum_{k = K + 1}^{N} \|A (k) T^{k}\| + 1$
285	229 282 13 284	ltmul1dd	$⊢ φ \to \sum_{k = K + 1}^{N} \|A (k) T^{k}\| X < (\sum_{k = K + 1}^{N} \|A (k) T^{k}\| + 1) X$
286		min2	$⊢ (1 \in ℝ \land U \in ℝ) \to if (1 \leq U, 1, U) \leq U$
287	196 203 286	sylancr	$⊢ φ \to if (1 \leq U, 1, U) \leq U$
288	9 287	eqbrtrid	$⊢ φ \to X \leq U$
289	288 8	breqtrdi	$⊢ φ \to X \leq \frac{\|F (0)\|}{\sum_{k = K + 1}^{N} \|A (k) T^{k}\| + 1}$
290		0red	$⊢ φ \to 0 \in ℝ$
291	31 228 252	fsumge0	$⊢ φ \to 0 \leq \sum_{k = K + 1}^{N} \|A (k) T^{k}\|$
292	290 229 282 291 284	lelttrd	$⊢ φ \to 0 < \sum_{k = K + 1}^{N} \|A (k) T^{k}\| + 1$
293		lemuldiv2	$⊢ (X \in ℝ \land \|F (0)\| \in ℝ \land (\sum_{k = K + 1}^{N} \|A (k) T^{k}\| + 1 \in ℝ \land 0 < \sum_{k = K + 1}^{N} \|A (k) T^{k}\| + 1)) \to ((\sum_{k = K + 1}^{N} \|A (k) T^{k}\| + 1) X \leq \|F (0)\| \leftrightarrow X \leq \frac{\|F (0)\|}{\sum_{k = K + 1}^{N} \|A (k) T^{k}\| + 1})$
294	14 24 282 292 293	syl112anc	$⊢ φ \to ((\sum_{k = K + 1}^{N} \|A (k) T^{k}\| + 1) X \leq \|F (0)\| \leftrightarrow X \leq \frac{\|F (0)\|}{\sum_{k = K + 1}^{N} \|A (k) T^{k}\| + 1})$
295	289 294	mpbird	$⊢ φ \to (\sum_{k = K + 1}^{N} \|A (k) T^{k}\| + 1) X \leq \|F (0)\|$
296	272 283 24 285 295	ltletrd	$⊢ φ \to \sum_{k = K + 1}^{N} \|A (k) T^{k}\| X < \|F (0)\|$
297	272 24 280 296	ltmul1dd	$⊢ φ \to \sum_{k = K + 1}^{N} \|A (k) T^{k}\| X X^{K} < \|F (0)\| X^{K}$
298	271 297	eqbrtrd	$⊢ φ \to \sum_{k = K + 1}^{N} \|A (k) T^{k}\| X^{K + 1} < \|F (0)\| X^{K}$
299	223 231 29 264 298	lelttrd	$⊢ φ \to \sum_{k = K + 1}^{N} \|A (k) {T X}^{k}\| < \|F (0)\| X^{K}$
300	45 223 29 224 299	lelttrd	$⊢ φ \to \|\sum_{k = K + 1}^{N} A (k) {T X}^{k}\| < \|F (0)\| X^{K}$
301	45 29 24 300	ltsub2dd	$⊢ φ \to \|F (0)\| - \|F (0)\| X^{K} < \|F (0)\| - \|\sum_{k = K + 1}^{N} A (k) {T X}^{k}\|$
302	30 45 24	ltaddsubd	$⊢ φ \to (\|F (0)\| - \|F (0)\| X^{K} + \|\sum_{k = K + 1}^{N} A (k) {T X}^{k}\| < \|F (0)\| \leftrightarrow \|F (0)\| - \|F (0)\| X^{K} < \|F (0)\| - \|\sum_{k = K + 1}^{N} A (k) {T X}^{k}\|)$
303	301 302	mpbird	$⊢ φ \to \|F (0)\| - \|F (0)\| X^{K} + \|\sum_{k = K + 1}^{N} A (k) {T X}^{k}\| < \|F (0)\|$
304	20 46 24 221 303	lelttrd	$⊢ φ \to \|F (T X)\| < \|F (0)\|$
305		2fveq3	$⊢ x = T X \to \|F (x)\| = \|F (T X)\|$
306	305	breq1d	$⊢ x = T X \to (\|F (x)\| < \|F (0)\| \leftrightarrow \|F (T X)\| < \|F (0)\|)$
307	306	rspcev	$⊢ (T X \in ℂ \land \|F (T X)\| < \|F (0)\|) \to \exists x \in ℂ \|F (x)\| < \|F (0)\|$
308	16 304 307	syl2anc	$⊢ φ \to \exists x \in ℂ \|F (x)\| < \|F (0)\|$

Metamath Proof Explorer

Theorem ftalem5

Proof