Theorem ftalem5 27252

Description: Lemma for fta 27255: Main proof. We have already shifted the minimum found in ftalem3 27250 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 𝐾 be the lowest term in the polynomial that is nonzero, and let 𝑇 be a 𝐾-th root of -𝐹(0) / 𝐴(𝐾). Then an evaluation of 𝐹(𝑇𝑋) where 𝑋 is a sufficiently small positive number yields 𝐹(0) for the first term and -𝐹(0) · 𝑋↑𝐾 for the 𝐾-th term, and all higher terms are bounded because 𝑋 is small. Thus, abs(𝐹(𝑇𝑋)) ≤ abs(𝐹(0))(1 − 𝑋↑𝐾) < abs(𝐹(0)), in contradiction to our choice of 𝐹(0) as the minimum. (Contributed by Mario Carneiro, 14-Sep-2014.) (Revised by AV, 28-Sep-2020.)

Hypotheses

Ref	Expression
ftalem.1	⊢ 𝐴 = (coeff‘𝐹)
ftalem.2	⊢ 𝑁 = (deg‘𝐹)
ftalem.3	⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆))
ftalem.4	⊢ (𝜑 → 𝑁 ∈ ℕ)
ftalem4.5	⊢ (𝜑 → (𝐹‘0) ≠ 0)
ftalem4.6	⊢ 𝐾 = inf({𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0}, ℝ, < )
ftalem4.7	⊢ 𝑇 = (-((𝐹‘0) / (𝐴‘𝐾))↑𝑐(1 / 𝐾))
ftalem4.8	⊢ 𝑈 = ((abs‘(𝐹‘0)) / (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1))
ftalem4.9	⊢ 𝑋 = if(1 ≤ 𝑈, 1, 𝑈)

Assertion

Ref	Expression
ftalem5	⊢ (𝜑 → ∃𝑥 ∈ ℂ (abs‘(𝐹‘𝑥)) < (abs‘(𝐹‘0)))

Distinct variable groups:   𝑘,𝑛,𝑥,𝐴   𝑘,𝐾,𝑛   𝑘,𝑁,𝑛,𝑥   𝑘,𝐹,𝑛,𝑥   𝜑,𝑘,𝑥   𝑆,𝑘   𝑇,𝑘,𝑥   𝑥,𝑈   𝑘,𝑋,𝑛,𝑥

Allowed substitution hints:   𝜑(𝑛)   𝑆(𝑥, 𝑛)   𝑇(𝑛)   𝑈(𝑘, 𝑛)   𝐾(𝑥)

Proof of Theorem ftalem5

Step	Hyp	Ref	Expression
1		ftalem.1	. . . . . 6 ⊢ 𝐴 = (coeff‘𝐹)
2		ftalem.2	. . . . . 6 ⊢ 𝑁 = (deg‘𝐹)
3		ftalem.3	. . . . . 6 ⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆))
4		ftalem.4	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ ℕ)
5		ftalem4.5	. . . . . 6 ⊢ (𝜑 → (𝐹‘0) ≠ 0)
6		ftalem4.6	. . . . . 6 ⊢ 𝐾 = inf({𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0}, ℝ, < )
7		ftalem4.7	. . . . . 6 ⊢ 𝑇 = (-((𝐹‘0) / (𝐴‘𝐾))↑𝑐(1 / 𝐾))
8		ftalem4.8	. . . . . 6 ⊢ 𝑈 = ((abs‘(𝐹‘0)) / (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1))
9		ftalem4.9	. . . . . 6 ⊢ 𝑋 = if(1 ≤ 𝑈, 1, 𝑈)
10	1, 2, 3, 4, 5, 6, 7, 8, 9	ftalem4 27251	. . . . 5 ⊢ (𝜑 → ((𝐾 ∈ ℕ ∧ (𝐴‘𝐾) ≠ 0) ∧ (𝑇 ∈ ℂ ∧ 𝑈 ∈ ℝ+ ∧ 𝑋 ∈ ℝ+)))
11	10	simprd 500	. . . 4 ⊢ (𝜑 → (𝑇 ∈ ℂ ∧ 𝑈 ∈ ℝ+ ∧ 𝑋 ∈ ℝ+))
12	11	simp1d 1159	. . 3 ⊢ (𝜑 → 𝑇 ∈ ℂ)
13	11	simp3d 1161	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ ℝ+)
14	13	rpred 13066	. . . 4 ⊢ (𝜑 → 𝑋 ∈ ℝ)
15	14	recnd 11243	. . 3 ⊢ (𝜑 → 𝑋 ∈ ℂ)
16	12, 15	mulcld 11235	. 2 ⊢ (𝜑 → (𝑇 · 𝑋) ∈ ℂ)
17		plyf 26366	. . . . . 6 ⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐹:ℂ⟶ℂ)
18	3, 17	syl 18	. . . . 5 ⊢ (𝜑 → 𝐹:ℂ⟶ℂ)
19	18, 16	ffvelcdmd 7080	. . . 4 ⊢ (𝜑 → (𝐹‘(𝑇 · 𝑋)) ∈ ℂ)
20	19	abscld 15497	. . 3 ⊢ (𝜑 → (abs‘(𝐹‘(𝑇 · 𝑋))) ∈ ℝ)
21		0cn 11204	. . . . . . 7 ⊢ 0 ∈ ℂ
22		ffvelcdm 7076	. . . . . . 7 ⊢ ((𝐹:ℂ⟶ℂ ∧ 0 ∈ ℂ) → (𝐹‘0) ∈ ℂ)
23	18, 21, 22	sylancl 597	. . . . . 6 ⊢ (𝜑 → (𝐹‘0) ∈ ℂ)
24	23	abscld 15497	. . . . 5 ⊢ (𝜑 → (abs‘(𝐹‘0)) ∈ ℝ)
25	10	simpld 499	. . . . . . . . 9 ⊢ (𝜑 → (𝐾 ∈ ℕ ∧ (𝐴‘𝐾) ≠ 0))
26	25	simpld 499	. . . . . . . 8 ⊢ (𝜑 → 𝐾 ∈ ℕ)
27	26	nnnn0d 12571	. . . . . . 7 ⊢ (𝜑 → 𝐾 ∈ ℕ0)
28	14, 27	reexpcld 14206	. . . . . 6 ⊢ (𝜑 → (𝑋↑𝐾) ∈ ℝ)
29	24, 28	remulcld 11245	. . . . 5 ⊢ (𝜑 → ((abs‘(𝐹‘0)) · (𝑋↑𝐾)) ∈ ℝ)
30	24, 29	resubcld 11648	. . . 4 ⊢ (𝜑 → ((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋↑𝐾))) ∈ ℝ)
31		fzfid 14016	. . . . . 6 ⊢ (𝜑 → ((𝐾 + 1)...𝑁) ∈ Fin)
32	1	coef3 26400	. . . . . . . . 9 ⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐴:ℕ0⟶ℂ)
33	3, 32	syl 18	. . . . . . . 8 ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)
34		peano2nn0 12550	. . . . . . . . . 10 ⊢ (𝐾 ∈ ℕ0 → (𝐾 + 1) ∈ ℕ0)
35	27, 34	syl 18	. . . . . . . . 9 ⊢ (𝜑 → (𝐾 + 1) ∈ ℕ0)
36		elfzuz 13554	. . . . . . . . 9 ⊢ (𝑘 ∈ ((𝐾 + 1)...𝑁) → 𝑘 ∈ (ℤ≥‘(𝐾 + 1)))
37		eluznn0 12947	. . . . . . . . 9 ⊢ (((𝐾 + 1) ∈ ℕ0 ∧ 𝑘 ∈ (ℤ≥‘(𝐾 + 1))) → 𝑘 ∈ ℕ0)
38	35, 36, 37	syl2an 607	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑘 ∈ ℕ0)
39		ffvelcdm 7076	. . . . . . . 8 ⊢ ((𝐴:ℕ0⟶ℂ ∧ 𝑘 ∈ ℕ0) → (𝐴‘𝑘) ∈ ℂ)
40	33, 38, 39	syl2an2r 697	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝐴‘𝑘) ∈ ℂ)
41	16	adantr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑇 · 𝑋) ∈ ℂ)
42	41, 38	expcld 14189	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((𝑇 · 𝑋)↑𝑘) ∈ ℂ)
43	40, 42	mulcld 11235	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) ∈ ℂ)
44	31, 43	fsumcl 15791	. . . . 5 ⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) ∈ ℂ)
45	44	abscld 15497	. . . 4 ⊢ (𝜑 → (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) ∈ ℝ)
46	30, 45	readdcld 11244	. . 3 ⊢ (𝜑 → (((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋↑𝐾))) + (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))) ∈ ℝ)
47		fzfid 14016	. . . . . 6 ⊢ (𝜑 → (0...𝐾) ∈ Fin)
48		elfznn0 13655	. . . . . . . 8 ⊢ (𝑘 ∈ (0...𝐾) → 𝑘 ∈ ℕ0)
49	33, 48, 39	syl2an 607	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐾)) → (𝐴‘𝑘) ∈ ℂ)
50		expcl 14122	. . . . . . . 8 ⊢ (((𝑇 · 𝑋) ∈ ℂ ∧ 𝑘 ∈ ℕ0) → ((𝑇 · 𝑋)↑𝑘) ∈ ℂ)
51	16, 48, 50	syl2an 607	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐾)) → ((𝑇 · 𝑋)↑𝑘) ∈ ℂ)
52	49, 51	mulcld 11235	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐾)) → ((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) ∈ ℂ)
53	47, 52	fsumcl 15791	. . . . 5 ⊢ (𝜑 → Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) ∈ ℂ)
54	53, 44	abstrid 15517	. . . 4 ⊢ (𝜑 → (abs‘(Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) + Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))) ≤ ((abs‘Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) + (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))))
55	1, 2	coeid2 26407	. . . . . . 7 ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (𝑇 · 𝑋) ∈ ℂ) → (𝐹‘(𝑇 · 𝑋)) = Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))
56	3, 16, 55	syl2anc 595	. . . . . 6 ⊢ (𝜑 → (𝐹‘(𝑇 · 𝑋)) = Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))
57	26	nnred 12254	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ∈ ℝ)
58	57	ltp1d 12151	. . . . . . . 8 ⊢ (𝜑 → 𝐾 < (𝐾 + 1))
59		fzdisj 13586	. . . . . . . 8 ⊢ (𝐾 < (𝐾 + 1) → ((0...𝐾) ∩ ((𝐾 + 1)...𝑁)) = ∅)
60	58, 59	syl 18	. . . . . . 7 ⊢ (𝜑 → ((0...𝐾) ∩ ((𝐾 + 1)...𝑁)) = ∅)
61		ssrab2 4033	. . . . . . . . . . . 12 ⊢ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ⊆ ℕ
62		nnuz 12907	. . . . . . . . . . . 12 ⊢ ℕ = (ℤ≥‘1)
63	61, 62	sseqtri 3984	. . . . . . . . . . 11 ⊢ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ⊆ (ℤ≥‘1)
64		fveq2 6881	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑁 → (𝐴‘𝑛) = (𝐴‘𝑁))
65	64	neeq1d 3016	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑁 → ((𝐴‘𝑛) ≠ 0 ↔ (𝐴‘𝑁) ≠ 0))
66	4	nnne0d 12292	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ≠ 0)
67	2, 1	dgreq0 26433	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ (Poly‘𝑆) → (𝐹 = 0𝑝 ↔ (𝐴‘𝑁) = 0))
68	3, 67	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐹 = 0𝑝 ↔ (𝐴‘𝑁) = 0))
69		fveq2 6881	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 = 0𝑝 → (deg‘𝐹) = (deg‘0𝑝))
70		dgr0 26430	. . . . . . . . . . . . . . . . 17 ⊢ (deg‘0𝑝) = 0
71	69, 70	eqtrdi 2813	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 = 0𝑝 → (deg‘𝐹) = 0)
72	2, 71	eqtrid 2809	. . . . . . . . . . . . . . 15 ⊢ (𝐹 = 0𝑝 → 𝑁 = 0)
73	68, 72	biimtrrdi 257	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐴‘𝑁) = 0 → 𝑁 = 0))
74	73	necon3d 2978	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑁 ≠ 0 → (𝐴‘𝑁) ≠ 0))
75	66, 74	mpd 16	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴‘𝑁) ≠ 0)
76	65, 4, 75	elrabd 3651	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0})
77		infssuzle 12961	. . . . . . . . . . 11 ⊢ (({𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ⊆ (ℤ≥‘1) ∧ 𝑁 ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0}) → inf({𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0}, ℝ, < ) ≤ 𝑁)
78	63, 76, 77	sylancr 598	. . . . . . . . . 10 ⊢ (𝜑 → inf({𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0}, ℝ, < ) ≤ 𝑁)
79	6, 78	eqbrtrid 5145	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ≤ 𝑁)
80		nn0uz 12906	. . . . . . . . . . 11 ⊢ ℕ0 = (ℤ≥‘0)
81	27, 80	eleqtrdi 2872	. . . . . . . . . 10 ⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘0))
82	4	nnzd 12623	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ ℤ)
83		elfz5 13550	. . . . . . . . . 10 ⊢ ((𝐾 ∈ (ℤ≥‘0) ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (0...𝑁) ↔ 𝐾 ≤ 𝑁))
84	81, 82, 83	syl2anc 595	. . . . . . . . 9 ⊢ (𝜑 → (𝐾 ∈ (0...𝑁) ↔ 𝐾 ≤ 𝑁))
85	79, 84	mpbird 260	. . . . . . . 8 ⊢ (𝜑 → 𝐾 ∈ (0...𝑁))
86		fzsplit 13585	. . . . . . . 8 ⊢ (𝐾 ∈ (0...𝑁) → (0...𝑁) = ((0...𝐾) ∪ ((𝐾 + 1)...𝑁)))
87	85, 86	syl 18	. . . . . . 7 ⊢ (𝜑 → (0...𝑁) = ((0...𝐾) ∪ ((𝐾 + 1)...𝑁)))
88		fzfid 14016	. . . . . . 7 ⊢ (𝜑 → (0...𝑁) ∈ Fin)
89		elfznn0 13655	. . . . . . . . 9 ⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0)
90	33, 89, 39	syl2an 607	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝐴‘𝑘) ∈ ℂ)
91	16, 89, 50	syl2an 607	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝑇 · 𝑋)↑𝑘) ∈ ℂ)
92	90, 91	mulcld 11235	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) ∈ ℂ)
93	60, 87, 88, 92	fsumsplit 15799	. . . . . 6 ⊢ (𝜑 → Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = (Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) + Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))))
94	56, 93	eqtrd 2797	. . . . 5 ⊢ (𝜑 → (𝐹‘(𝑇 · 𝑋)) = (Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) + Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))))
95	94	fveq2d 6885	. . . 4 ⊢ (𝜑 → (abs‘(𝐹‘(𝑇 · 𝑋))) = (abs‘(Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) + Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))))
96	1	coefv0 26416	. . . . . . . . . . . . 13 ⊢ (𝐹 ∈ (Poly‘𝑆) → (𝐹‘0) = (𝐴‘0))
97	3, 96	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹‘0) = (𝐴‘0))
98	97	eqcomd 2768	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴‘0) = (𝐹‘0))
99	16	exp0d 14183	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑇 · 𝑋)↑0) = 1)
100	98, 99	oveq12d 7430	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴‘0) · ((𝑇 · 𝑋)↑0)) = ((𝐹‘0) · 1))
101	23	mulridd 11232	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐹‘0) · 1) = (𝐹‘0))
102	100, 101	eqtrd 2797	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴‘0) · ((𝑇 · 𝑋)↑0)) = (𝐹‘0))
103		1e0p1 12764	. . . . . . . . . . . . 13 ⊢ 1 = (0 + 1)
104	103	oveq1i 7422	. . . . . . . . . . . 12 ⊢ (1...𝐾) = ((0 + 1)...𝐾)
105	104	sumeq1i 15755	. . . . . . . . . . 11 ⊢ Σ𝑘 ∈ (1...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = Σ𝑘 ∈ ((0 + 1)...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))
106	26, 62	eleqtrdi 2872	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘1))
107		elfznn 13588	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ (1...𝐾) → 𝑘 ∈ ℕ)
108	107	nnnn0d 12571	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (1...𝐾) → 𝑘 ∈ ℕ0)
109	33, 108, 39	syl2an 607	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐾)) → (𝐴‘𝑘) ∈ ℂ)
110	16, 108, 50	syl2an 607	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐾)) → ((𝑇 · 𝑋)↑𝑘) ∈ ℂ)
111	109, 110	mulcld 11235	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐾)) → ((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) ∈ ℂ)
112		fveq2 6881	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝐾 → (𝐴‘𝑘) = (𝐴‘𝐾))
113		oveq2 7420	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝐾 → ((𝑇 · 𝑋)↑𝑘) = ((𝑇 · 𝑋)↑𝐾))
114	112, 113	oveq12d 7430	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝐾 → ((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = ((𝐴‘𝐾) · ((𝑇 · 𝑋)↑𝐾)))
115	106, 111, 114	fsumm1 15809	. . . . . . . . . . 11 ⊢ (𝜑 → Σ𝑘 ∈ (1...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = (Σ𝑘 ∈ (1...(𝐾 − 1))((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) + ((𝐴‘𝐾) · ((𝑇 · 𝑋)↑𝐾))))
116	105, 115	eqtr3id 2811	. . . . . . . . . 10 ⊢ (𝜑 → Σ𝑘 ∈ ((0 + 1)...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = (Σ𝑘 ∈ (1...(𝐾 − 1))((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) + ((𝐴‘𝐾) · ((𝑇 · 𝑋)↑𝐾))))
117		elfznn 13588	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 ∈ (1...(𝐾 − 1)) → 𝑘 ∈ ℕ)
118	117	adantl 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → 𝑘 ∈ ℕ)
119	118	nnred 12254	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → 𝑘 ∈ ℝ)
120	57	adantr 485	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → 𝐾 ∈ ℝ)
121		peano2rem 11531	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐾 ∈ ℝ → (𝐾 − 1) ∈ ℝ)
122	120, 121	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → (𝐾 − 1) ∈ ℝ)
123		elfzle2 13562	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ (1...(𝐾 − 1)) → 𝑘 ≤ (𝐾 − 1))
124	123	adantl 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → 𝑘 ≤ (𝐾 − 1))
125	120	ltm1d 12153	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → (𝐾 − 1) < 𝐾)
126	119, 122, 120, 124, 125	lelttrd 11374	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → 𝑘 < 𝐾)
127	119, 120	ltnled 11363	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → (𝑘 < 𝐾 ↔ ¬ 𝐾 ≤ 𝑘))
128	126, 127	mpbid 235	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → ¬ 𝐾 ≤ 𝑘)
129		infssuzle 12961	. . . . . . . . . . . . . . . . . . 19 ⊢ (({𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ⊆ (ℤ≥‘1) ∧ 𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0}) → inf({𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0}, ℝ, < ) ≤ 𝑘)
130	6, 129	eqbrtrid 5145	. . . . . . . . . . . . . . . . . 18 ⊢ (({𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ⊆ (ℤ≥‘1) ∧ 𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0}) → 𝐾 ≤ 𝑘)
131	63, 130	mpan 702	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} → 𝐾 ≤ 𝑘)
132	128, 131	nsyl 141	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → ¬ 𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0})
133		fveq2 6881	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 𝑘 → (𝐴‘𝑛) = (𝐴‘𝑘))
134	133	neeq1d 3016	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑘 → ((𝐴‘𝑛) ≠ 0 ↔ (𝐴‘𝑘) ≠ 0))
135	134	elrab3 3650	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ℕ → (𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ↔ (𝐴‘𝑘) ≠ 0))
136	118, 135	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → (𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ↔ (𝐴‘𝑘) ≠ 0))
137	136	necon2bbid 3000	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → ((𝐴‘𝑘) = 0 ↔ ¬ 𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0}))
138	132, 137	mpbird 260	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → (𝐴‘𝑘) = 0)
139	138	oveq1d 7427	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → ((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = (0 · ((𝑇 · 𝑋)↑𝑘)))
140	117	nnnn0d 12571	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ (1...(𝐾 − 1)) → 𝑘 ∈ ℕ0)
141	16, 140, 50	syl2an 607	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → ((𝑇 · 𝑋)↑𝑘) ∈ ℂ)
142	141	mul02d 11414	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → (0 · ((𝑇 · 𝑋)↑𝑘)) = 0)
143	139, 142	eqtrd 2797	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → ((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = 0)
144	143	sumeq2dv 15760	. . . . . . . . . . . 12 ⊢ (𝜑 → Σ𝑘 ∈ (1...(𝐾 − 1))((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = Σ𝑘 ∈ (1...(𝐾 − 1))0)
145		fzfi 14015	. . . . . . . . . . . . . 14 ⊢ (1...(𝐾 − 1)) ∈ Fin
146	145	olci 879	. . . . . . . . . . . . 13 ⊢ ((1...(𝐾 − 1)) ⊆ (ℤ≥‘1) ∨ (1...(𝐾 − 1)) ∈ Fin)
147		sumz 15780	. . . . . . . . . . . . 13 ⊢ (((1...(𝐾 − 1)) ⊆ (ℤ≥‘1) ∨ (1...(𝐾 − 1)) ∈ Fin) → Σ𝑘 ∈ (1...(𝐾 − 1))0 = 0)
148	146, 147	ax-mp 5	. . . . . . . . . . . 12 ⊢ Σ𝑘 ∈ (1...(𝐾 − 1))0 = 0
149	144, 148	eqtrdi 2813	. . . . . . . . . . 11 ⊢ (𝜑 → Σ𝑘 ∈ (1...(𝐾 − 1))((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = 0)
150	12, 15, 27	mulexpd 14204	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑇 · 𝑋)↑𝐾) = ((𝑇↑𝐾) · (𝑋↑𝐾)))
151	150	oveq2d 7428	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐴‘𝐾) · ((𝑇 · 𝑋)↑𝐾)) = ((𝐴‘𝐾) · ((𝑇↑𝐾) · (𝑋↑𝐾))))
152	33, 27	ffvelcdmd 7080	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐴‘𝐾) ∈ ℂ)
153	12, 27	expcld 14189	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑇↑𝐾) ∈ ℂ)
154	28	recnd 11243	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑋↑𝐾) ∈ ℂ)
155	152, 153, 154	mulassd 11238	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐴‘𝐾) · (𝑇↑𝐾)) · (𝑋↑𝐾)) = ((𝐴‘𝐾) · ((𝑇↑𝐾) · (𝑋↑𝐾))))
156	151, 155	eqtr4d 2800	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐴‘𝐾) · ((𝑇 · 𝑋)↑𝐾)) = (((𝐴‘𝐾) · (𝑇↑𝐾)) · (𝑋↑𝐾)))
157	7	oveq1i 7422	. . . . . . . . . . . . . . . 16 ⊢ (𝑇↑𝐾) = ((-((𝐹‘0) / (𝐴‘𝐾))↑𝑐(1 / 𝐾))↑𝐾)
158	57	recnd 11243	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐾 ∈ ℂ)
159	26	nnne0d 12292	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐾 ≠ 0)
160	158, 159	recid2d 11993	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((1 / 𝐾) · 𝐾) = 1)
161	160	oveq2d 7428	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (-((𝐹‘0) / (𝐴‘𝐾))↑𝑐((1 / 𝐾) · 𝐾)) = (-((𝐹‘0) / (𝐴‘𝐾))↑𝑐1))
162	25	simprd 500	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐴‘𝐾) ≠ 0)
163	23, 152, 162	divcld 11997	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐹‘0) / (𝐴‘𝐾)) ∈ ℂ)
164	163	negcld 11562	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → -((𝐹‘0) / (𝐴‘𝐾)) ∈ ℂ)
165	26	nnrecred 12293	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (1 / 𝐾) ∈ ℝ)
166	165	recnd 11243	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (1 / 𝐾) ∈ ℂ)
167	164, 166, 27	cxpmul2d 26885	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (-((𝐹‘0) / (𝐴‘𝐾))↑𝑐((1 / 𝐾) · 𝐾)) = ((-((𝐹‘0) / (𝐴‘𝐾))↑𝑐(1 / 𝐾))↑𝐾))
168	164	cxp1d 26882	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (-((𝐹‘0) / (𝐴‘𝐾))↑𝑐1) = -((𝐹‘0) / (𝐴‘𝐾)))
169	161, 167, 168	3eqtr3d 2805	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((-((𝐹‘0) / (𝐴‘𝐾))↑𝑐(1 / 𝐾))↑𝐾) = -((𝐹‘0) / (𝐴‘𝐾)))
170	157, 169	eqtrid 2809	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑇↑𝐾) = -((𝐹‘0) / (𝐴‘𝐾)))
171	170	oveq2d 7428	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐴‘𝐾) · (𝑇↑𝐾)) = ((𝐴‘𝐾) · -((𝐹‘0) / (𝐴‘𝐾))))
172	152, 163	mulneg2d 11674	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐴‘𝐾) · -((𝐹‘0) / (𝐴‘𝐾))) = -((𝐴‘𝐾) · ((𝐹‘0) / (𝐴‘𝐾))))
173	23, 152, 162	divcan2d 11999	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐴‘𝐾) · ((𝐹‘0) / (𝐴‘𝐾))) = (𝐹‘0))
174	173	negeqd 11457	. . . . . . . . . . . . . 14 ⊢ (𝜑 → -((𝐴‘𝐾) · ((𝐹‘0) / (𝐴‘𝐾))) = -(𝐹‘0))
175	171, 172, 174	3eqtrd 2801	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐴‘𝐾) · (𝑇↑𝐾)) = -(𝐹‘0))
176	175	oveq1d 7427	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐴‘𝐾) · (𝑇↑𝐾)) · (𝑋↑𝐾)) = (-(𝐹‘0) · (𝑋↑𝐾)))
177	23, 154	mulneg1d 11673	. . . . . . . . . . . 12 ⊢ (𝜑 → (-(𝐹‘0) · (𝑋↑𝐾)) = -((𝐹‘0) · (𝑋↑𝐾)))
178	156, 176, 177	3eqtrd 2801	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴‘𝐾) · ((𝑇 · 𝑋)↑𝐾)) = -((𝐹‘0) · (𝑋↑𝐾)))
179	149, 178	oveq12d 7430	. . . . . . . . . 10 ⊢ (𝜑 → (Σ𝑘 ∈ (1...(𝐾 − 1))((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) + ((𝐴‘𝐾) · ((𝑇 · 𝑋)↑𝐾))) = (0 + -((𝐹‘0) · (𝑋↑𝐾))))
180	23, 154	mulcld 11235	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐹‘0) · (𝑋↑𝐾)) ∈ ℂ)
181	180	negcld 11562	. . . . . . . . . . 11 ⊢ (𝜑 → -((𝐹‘0) · (𝑋↑𝐾)) ∈ ℂ)
182	181	addlidd 11417	. . . . . . . . . 10 ⊢ (𝜑 → (0 + -((𝐹‘0) · (𝑋↑𝐾))) = -((𝐹‘0) · (𝑋↑𝐾)))
183	116, 179, 182	3eqtrd 2801	. . . . . . . . 9 ⊢ (𝜑 → Σ𝑘 ∈ ((0 + 1)...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = -((𝐹‘0) · (𝑋↑𝐾)))
184	102, 183	oveq12d 7430	. . . . . . . 8 ⊢ (𝜑 → (((𝐴‘0) · ((𝑇 · 𝑋)↑0)) + Σ𝑘 ∈ ((0 + 1)...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) = ((𝐹‘0) + -((𝐹‘0) · (𝑋↑𝐾))))
185		fveq2 6881	. . . . . . . . . 10 ⊢ (𝑘 = 0 → (𝐴‘𝑘) = (𝐴‘0))
186		oveq2 7420	. . . . . . . . . 10 ⊢ (𝑘 = 0 → ((𝑇 · 𝑋)↑𝑘) = ((𝑇 · 𝑋)↑0))
187	185, 186	oveq12d 7430	. . . . . . . . 9 ⊢ (𝑘 = 0 → ((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = ((𝐴‘0) · ((𝑇 · 𝑋)↑0)))
188	81, 52, 187	fsum1p 15811	. . . . . . . 8 ⊢ (𝜑 → Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = (((𝐴‘0) · ((𝑇 · 𝑋)↑0)) + Σ𝑘 ∈ ((0 + 1)...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))))
189	101	oveq1d 7427	. . . . . . . . 9 ⊢ (𝜑 → (((𝐹‘0) · 1) − ((𝐹‘0) · (𝑋↑𝐾))) = ((𝐹‘0) − ((𝐹‘0) · (𝑋↑𝐾))))
190		1cnd 11208	. . . . . . . . . 10 ⊢ (𝜑 → 1 ∈ ℂ)
191	23, 190, 154	subdid 11676	. . . . . . . . 9 ⊢ (𝜑 → ((𝐹‘0) · (1 − (𝑋↑𝐾))) = (((𝐹‘0) · 1) − ((𝐹‘0) · (𝑋↑𝐾))))
192	23, 180	negsubd 11581	. . . . . . . . 9 ⊢ (𝜑 → ((𝐹‘0) + -((𝐹‘0) · (𝑋↑𝐾))) = ((𝐹‘0) − ((𝐹‘0) · (𝑋↑𝐾))))
193	189, 191, 192	3eqtr4d 2807	. . . . . . . 8 ⊢ (𝜑 → ((𝐹‘0) · (1 − (𝑋↑𝐾))) = ((𝐹‘0) + -((𝐹‘0) · (𝑋↑𝐾))))
194	184, 188, 193	3eqtr4d 2807	. . . . . . 7 ⊢ (𝜑 → Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = ((𝐹‘0) · (1 − (𝑋↑𝐾))))
195	194	fveq2d 6885	. . . . . 6 ⊢ (𝜑 → (abs‘Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) = (abs‘((𝐹‘0) · (1 − (𝑋↑𝐾)))))
196		1re 11214	. . . . . . . . 9 ⊢ 1 ∈ ℝ
197		resubcl 11528	. . . . . . . . 9 ⊢ ((1 ∈ ℝ ∧ (𝑋↑𝐾) ∈ ℝ) → (1 − (𝑋↑𝐾)) ∈ ℝ)
198	196, 28, 197	sylancr 598	. . . . . . . 8 ⊢ (𝜑 → (1 − (𝑋↑𝐾)) ∈ ℝ)
199	198	recnd 11243	. . . . . . 7 ⊢ (𝜑 → (1 − (𝑋↑𝐾)) ∈ ℂ)
200	23, 199	absmuld 15515	. . . . . 6 ⊢ (𝜑 → (abs‘((𝐹‘0) · (1 − (𝑋↑𝐾)))) = ((abs‘(𝐹‘0)) · (abs‘(1 − (𝑋↑𝐾)))))
201	13	rpge0d 13070	. . . . . . . . . . 11 ⊢ (𝜑 → 0 ≤ 𝑋)
202	11	simp2d 1160	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑈 ∈ ℝ+)
203	202	rpred 13066	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑈 ∈ ℝ)
204		min1 13221	. . . . . . . . . . . . 13 ⊢ ((1 ∈ ℝ ∧ 𝑈 ∈ ℝ) → if(1 ≤ 𝑈, 1, 𝑈) ≤ 1)
205	196, 203, 204	sylancr 598	. . . . . . . . . . . 12 ⊢ (𝜑 → if(1 ≤ 𝑈, 1, 𝑈) ≤ 1)
206	9, 205	eqbrtrid 5145	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑋 ≤ 1)
207		exple1 14220	. . . . . . . . . . 11 ⊢ (((𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ∧ 𝑋 ≤ 1) ∧ 𝐾 ∈ ℕ0) → (𝑋↑𝐾) ≤ 1)
208	14, 201, 206, 27, 207	syl31anc 1399	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋↑𝐾) ≤ 1)
209		subge0 11733	. . . . . . . . . . 11 ⊢ ((1 ∈ ℝ ∧ (𝑋↑𝐾) ∈ ℝ) → (0 ≤ (1 − (𝑋↑𝐾)) ↔ (𝑋↑𝐾) ≤ 1))
210	196, 28, 209	sylancr 598	. . . . . . . . . 10 ⊢ (𝜑 → (0 ≤ (1 − (𝑋↑𝐾)) ↔ (𝑋↑𝐾) ≤ 1))
211	208, 210	mpbird 260	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ (1 − (𝑋↑𝐾)))
212	198, 211	absidd 15481	. . . . . . . 8 ⊢ (𝜑 → (abs‘(1 − (𝑋↑𝐾))) = (1 − (𝑋↑𝐾)))
213	212	oveq2d 7428	. . . . . . 7 ⊢ (𝜑 → ((abs‘(𝐹‘0)) · (abs‘(1 − (𝑋↑𝐾)))) = ((abs‘(𝐹‘0)) · (1 − (𝑋↑𝐾))))
214	24	recnd 11243	. . . . . . . 8 ⊢ (𝜑 → (abs‘(𝐹‘0)) ∈ ℂ)
215	214, 190, 154	subdid 11676	. . . . . . 7 ⊢ (𝜑 → ((abs‘(𝐹‘0)) · (1 − (𝑋↑𝐾))) = (((abs‘(𝐹‘0)) · 1) − ((abs‘(𝐹‘0)) · (𝑋↑𝐾))))
216	214	mulridd 11232	. . . . . . . 8 ⊢ (𝜑 → ((abs‘(𝐹‘0)) · 1) = (abs‘(𝐹‘0)))
217	216	oveq1d 7427	. . . . . . 7 ⊢ (𝜑 → (((abs‘(𝐹‘0)) · 1) − ((abs‘(𝐹‘0)) · (𝑋↑𝐾))) = ((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋↑𝐾))))
218	213, 215, 217	3eqtrd 2801	. . . . . 6 ⊢ (𝜑 → ((abs‘(𝐹‘0)) · (abs‘(1 − (𝑋↑𝐾)))) = ((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋↑𝐾))))
219	195, 200, 218	3eqtrrd 2802	. . . . 5 ⊢ (𝜑 → ((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋↑𝐾))) = (abs‘Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))))
220	219	oveq1d 7427	. . . 4 ⊢ (𝜑 → (((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋↑𝐾))) + (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))) = ((abs‘Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) + (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))))
221	54, 95, 220	3brtr4d 5142	. . 3 ⊢ (𝜑 → (abs‘(𝐹‘(𝑇 · 𝑋))) ≤ (((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋↑𝐾))) + (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))))
222	43	abscld 15497	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) ∈ ℝ)
223	31, 222	fsumrecl 15792	. . . . . 6 ⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) ∈ ℝ)
224	31, 43	fsumabs 15860	. . . . . 6 ⊢ (𝜑 → (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) ≤ Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))))
225		expcl 14122	. . . . . . . . . . . 12 ⊢ ((𝑇 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (𝑇↑𝑘) ∈ ℂ)
226	12, 38, 225	syl2an2r 697	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑇↑𝑘) ∈ ℂ)
227	40, 226	mulcld 11235	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((𝐴‘𝑘) · (𝑇↑𝑘)) ∈ ℂ)
228	227	abscld 15497	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) ∈ ℝ)
229	31, 228	fsumrecl 15792	. . . . . . . 8 ⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) ∈ ℝ)
230	14, 35	reexpcld 14206	. . . . . . . 8 ⊢ (𝜑 → (𝑋↑(𝐾 + 1)) ∈ ℝ)
231	229, 230	remulcld 11245	. . . . . . 7 ⊢ (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1))) ∈ ℝ)
232	230	adantr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑋↑(𝐾 + 1)) ∈ ℝ)
233	228, 232	remulcld 11245	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1))) ∈ ℝ)
234	12	adantr 485	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑇 ∈ ℂ)
235	15	adantr 485	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑋 ∈ ℂ)
236	234, 235, 38	mulexpd 14204	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((𝑇 · 𝑋)↑𝑘) = ((𝑇↑𝑘) · (𝑋↑𝑘)))
237	236	oveq2d 7428	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = ((𝐴‘𝑘) · ((𝑇↑𝑘) · (𝑋↑𝑘))))
238	14	adantr 485	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑋 ∈ ℝ)
239	238, 38	reexpcld 14206	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑋↑𝑘) ∈ ℝ)
240	239	recnd 11243	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑋↑𝑘) ∈ ℂ)
241	40, 226, 240	mulassd 11238	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (((𝐴‘𝑘) · (𝑇↑𝑘)) · (𝑋↑𝑘)) = ((𝐴‘𝑘) · ((𝑇↑𝑘) · (𝑋↑𝑘))))
242	237, 241	eqtr4d 2800	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = (((𝐴‘𝑘) · (𝑇↑𝑘)) · (𝑋↑𝑘)))
243	242	fveq2d 6885	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) = (abs‘(((𝐴‘𝑘) · (𝑇↑𝑘)) · (𝑋↑𝑘))))
244	227, 240	absmuld 15515	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘(((𝐴‘𝑘) · (𝑇↑𝑘)) · (𝑋↑𝑘))) = ((abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (abs‘(𝑋↑𝑘))))
245		elfzelz 13558	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ((𝐾 + 1)...𝑁) → 𝑘 ∈ ℤ)
246		rpexpcl 14123	. . . . . . . . . . . . . . 15 ⊢ ((𝑋 ∈ ℝ+ ∧ 𝑘 ∈ ℤ) → (𝑋↑𝑘) ∈ ℝ+)
247	13, 245, 246	syl2an 607	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑋↑𝑘) ∈ ℝ+)
248	247	rpge0d 13070	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 0 ≤ (𝑋↑𝑘))
249	239, 248	absidd 15481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘(𝑋↑𝑘)) = (𝑋↑𝑘))
250	249	oveq2d 7428	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (abs‘(𝑋↑𝑘))) = ((abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑𝑘)))
251	243, 244, 250	3eqtrd 2801	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) = ((abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑𝑘)))
252	227	absge0d 15505	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 0 ≤ (abs‘((𝐴‘𝑘) · (𝑇↑𝑘))))
253	35	adantr 485	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝐾 + 1) ∈ ℕ0)
254	36	adantl 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑘 ∈ (ℤ≥‘(𝐾 + 1)))
255	201	adantr 485	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 0 ≤ 𝑋)
256	206	adantr 485	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑋 ≤ 1)
257	238, 253, 254, 255, 256	leexp2rd 14298	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑋↑𝑘) ≤ (𝑋↑(𝐾 + 1)))
258	239, 232, 228, 252, 257	lemul2ad 12161	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑𝑘)) ≤ ((abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1))))
259	251, 258	eqbrtrd 5132	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) ≤ ((abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1))))
260	31, 222, 233, 259	fsumle 15858	. . . . . . . 8 ⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) ≤ Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1))))
261	230	recnd 11243	. . . . . . . . 9 ⊢ (𝜑 → (𝑋↑(𝐾 + 1)) ∈ ℂ)
262	228	recnd 11243	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) ∈ ℂ)
263	31, 261, 262	fsummulc1 15843	. . . . . . . 8 ⊢ (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1))) = Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1))))
264	260, 263	breqtrrd 5138	. . . . . . 7 ⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) ≤ (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1))))
265	15, 27	expp1d 14190	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑋↑(𝐾 + 1)) = ((𝑋↑𝐾) · 𝑋))
266	154, 15	mulcomd 11236	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑋↑𝐾) · 𝑋) = (𝑋 · (𝑋↑𝐾)))
267	265, 266	eqtrd 2797	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋↑(𝐾 + 1)) = (𝑋 · (𝑋↑𝐾)))
268	267	oveq2d 7428	. . . . . . . . 9 ⊢ (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1))) = (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋 · (𝑋↑𝐾))))
269	229	recnd 11243	. . . . . . . . . 10 ⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) ∈ ℂ)
270	269, 15, 154	mulassd 11238	. . . . . . . . 9 ⊢ (𝜑 → ((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · 𝑋) · (𝑋↑𝐾)) = (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋 · (𝑋↑𝐾))))
271	268, 270	eqtr4d 2800	. . . . . . . 8 ⊢ (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1))) = ((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · 𝑋) · (𝑋↑𝐾)))
272	229, 14	remulcld 11245	. . . . . . . . 9 ⊢ (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · 𝑋) ∈ ℝ)
273		nnssz 12619	. . . . . . . . . . . 12 ⊢ ℕ ⊆ ℤ
274	61, 273	sstri 3945	. . . . . . . . . . 11 ⊢ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ⊆ ℤ
275	76	ne0d 4294	. . . . . . . . . . . . 13 ⊢ (𝜑 → {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ≠ ∅)
276		infssuzcl 12962	. . . . . . . . . . . . 13 ⊢ (({𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ⊆ (ℤ≥‘1) ∧ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ≠ ∅) → inf({𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0}, ℝ, < ) ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0})
277	63, 275, 276	sylancr 598	. . . . . . . . . . . 12 ⊢ (𝜑 → inf({𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0}, ℝ, < ) ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0})
278	6, 277	eqeltrid 2866	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐾 ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0})
279	274, 278	sselid 3934	. . . . . . . . . 10 ⊢ (𝜑 → 𝐾 ∈ ℤ)
280	13, 279	rpexpcld 14290	. . . . . . . . 9 ⊢ (𝜑 → (𝑋↑𝐾) ∈ ℝ+)
281		peano2re 11389	. . . . . . . . . . . 12 ⊢ (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) ∈ ℝ → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1) ∈ ℝ)
282	229, 281	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1) ∈ ℝ)
283	282, 14	remulcld 11245	. . . . . . . . . 10 ⊢ (𝜑 → ((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1) · 𝑋) ∈ ℝ)
284	229	ltp1d 12151	. . . . . . . . . . 11 ⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) < (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1))
285	229, 282, 13, 284	ltmul1dd 13121	. . . . . . . . . 10 ⊢ (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · 𝑋) < ((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1) · 𝑋))
286		min2 13222	. . . . . . . . . . . . . 14 ⊢ ((1 ∈ ℝ ∧ 𝑈 ∈ ℝ) → if(1 ≤ 𝑈, 1, 𝑈) ≤ 𝑈)
287	196, 203, 286	sylancr 598	. . . . . . . . . . . . 13 ⊢ (𝜑 → if(1 ≤ 𝑈, 1, 𝑈) ≤ 𝑈)
288	9, 287	eqbrtrid 5145	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑋 ≤ 𝑈)
289	288, 8	breqtrdi 5151	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑋 ≤ ((abs‘(𝐹‘0)) / (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1)))
290		0red 11217	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 ∈ ℝ)
291	31, 228, 252	fsumge0 15854	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 ≤ Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))))
292	290, 229, 282, 291, 284	lelttrd 11374	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 < (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1))
293		lemuldiv2 12102	. . . . . . . . . . . 12 ⊢ ((𝑋 ∈ ℝ ∧ (abs‘(𝐹‘0)) ∈ ℝ ∧ ((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1) ∈ ℝ ∧ 0 < (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1))) → (((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1) · 𝑋) ≤ (abs‘(𝐹‘0)) ↔ 𝑋 ≤ ((abs‘(𝐹‘0)) / (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1))))
294	14, 24, 282, 292, 293	syl112anc 1400	. . . . . . . . . . 11 ⊢ (𝜑 → (((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1) · 𝑋) ≤ (abs‘(𝐹‘0)) ↔ 𝑋 ≤ ((abs‘(𝐹‘0)) / (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1))))
295	289, 294	mpbird 260	. . . . . . . . . 10 ⊢ (𝜑 → ((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1) · 𝑋) ≤ (abs‘(𝐹‘0)))
296	272, 283, 24, 285, 295	ltletrd 11376	. . . . . . . . 9 ⊢ (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · 𝑋) < (abs‘(𝐹‘0)))
297	272, 24, 280, 296	ltmul1dd 13121	. . . . . . . 8 ⊢ (𝜑 → ((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · 𝑋) · (𝑋↑𝐾)) < ((abs‘(𝐹‘0)) · (𝑋↑𝐾)))
298	271, 297	eqbrtrd 5132	. . . . . . 7 ⊢ (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1))) < ((abs‘(𝐹‘0)) · (𝑋↑𝐾)))
299	223, 231, 29, 264, 298	lelttrd 11374	. . . . . 6 ⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) < ((abs‘(𝐹‘0)) · (𝑋↑𝐾)))
300	45, 223, 29, 224, 299	lelttrd 11374	. . . . 5 ⊢ (𝜑 → (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) < ((abs‘(𝐹‘0)) · (𝑋↑𝐾)))
301	45, 29, 24, 300	ltsub2dd 11833	. . . 4 ⊢ (𝜑 → ((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋↑𝐾))) < ((abs‘(𝐹‘0)) − (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))))
302	30, 45, 24	ltaddsubd 11820	. . . 4 ⊢ (𝜑 → ((((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋↑𝐾))) + (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))) < (abs‘(𝐹‘0)) ↔ ((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋↑𝐾))) < ((abs‘(𝐹‘0)) − (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))))))
303	301, 302	mpbird 260	. . 3 ⊢ (𝜑 → (((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋↑𝐾))) + (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))) < (abs‘(𝐹‘0)))
304	20, 46, 24, 221, 303	lelttrd 11374	. 2 ⊢ (𝜑 → (abs‘(𝐹‘(𝑇 · 𝑋))) < (abs‘(𝐹‘0)))
305		2fveq3 6886	. . . 4 ⊢ (𝑥 = (𝑇 · 𝑋) → (abs‘(𝐹‘𝑥)) = (abs‘(𝐹‘(𝑇 · 𝑋))))
306	305	breq1d 5118	. . 3 ⊢ (𝑥 = (𝑇 · 𝑋) → ((abs‘(𝐹‘𝑥)) < (abs‘(𝐹‘0)) ↔ (abs‘(𝐹‘(𝑇 · 𝑋))) < (abs‘(𝐹‘0))))
307	306	rspcev 3580	. 2 ⊢ (((𝑇 · 𝑋) ∈ ℂ ∧ (abs‘(𝐹‘(𝑇 · 𝑋))) < (abs‘(𝐹‘0))) → ∃𝑥 ∈ ℂ (abs‘(𝐹‘𝑥)) < (abs‘(𝐹‘0)))
308	16, 304, 307	syl2anc 595	1 ⊢ (𝜑 → ∃𝑥 ∈ ℂ (abs‘(𝐹‘𝑥)) < (abs‘(𝐹‘0)))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∨ wo 860   ∧ w3a 1102   = wceq 1569   ∈ wcel 2142   ≠ wne 2957  ∃wrex 3088  {crab 3415   ∪ cun 3902   ∩ cin 3903   ⊆ wss 3904  ∅c0 4285  ifcif 4486   class class class wbr 5108  ⟶wf 6532  ‘cfv 6536  (class class class)co 7412  Fincfn 8941  infcinf 9399  ℂcc 11104  ℝcr 11105  0cc0 11106  1c1 11107   + caddc 11109   · cmul 11111   < clt 11249   ≤ cle 11250   − cmin 11447  -cneg 11448   / cdiv 11877  ℕcn 12239  ℕ₀cn0 12510  ℤcz 12597  ℤ_≥cuz 12868  ℝ⁺crp 13022  ...cfz 13541  ↑cexp 14104  abscabs 15292  Σcsu 15744  0_𝑝c0p 25839  Polycply 26352  coeffccoe 26354  degcdgr 26355  ↑_𝑐ccxp 26731

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-rep 5237  ax-sep 5256  ax-nul 5268  ax-pow 5335  ax-pr 5403  ax-un 7734  ax-inf2 9608  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183  ax-pre-sup 11184  ax-addf 11185

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1103  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-nf 1813  df-sb 2096  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3064  df-ral 3079  df-rex 3089  df-rmo 3368  df-reu 3369  df-rab 3416  df-v 3456  df-sbc 3744  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4487  df-pw 4563  df-sn 4589  df-pr 4591  df-tp 4593  df-op 4595  df-uni 4872  df-int 4912  df-iun 4957  df-iin 4958  df-br 5109  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5555  df-eprel 5560  df-po 5568  df-so 5569  df-fr 5613  df-se 5614  df-we 5615  df-xp 5666  df-rel 5667  df-cnv 5668  df-co 5669  df-dm 5670  df-rn 5671  df-res 5672  df-ima 5673  df-pred 6302  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-isom 6545  df-riota 7369  df-ov 7415  df-oprab 7416  df-mpo 7417  df-of 7676  df-om 7861  df-1st 7984  df-2nd 7985  df-supp 8155  df-frecs 8276  df-wrecs 8307  df-recs 8356  df-rdg 8395  df-1o 8451  df-2o 8452  df-er 8692  df-map 8824  df-pm 8825  df-ixp 8894  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-fsupp 9320  df-fi 9369  df-sup 9400  df-inf 9401  df-oi 9470  df-card 9932  df-pnf 11251  df-mnf 11252  df-xr 11253  df-ltxr 11254  df-le 11255  df-sub 11449  df-neg 11450  df-div 11878  df-nn 12240  df-2 12309  df-3 12310  df-4 12311  df-5 12312  df-6 12313  df-7 12314  df-8 12315  df-9 12316  df-n0 12511  df-z 12598  df-dec 12718  df-uz 12869  df-q 12979  df-rp 13023  df-xneg 13143  df-xadd 13144  df-xmul 13145  df-ioo 13382  df-ioc 13383  df-ico 13384  df-icc 13385  df-fz 13542  df-fzo 13690  df-fl 13832  df-mod 13910  df-seq 14045  df-exp 14105  df-fac 14317  df-bc 14346  df-hash 14374  df-shft 15111  df-cj 15157  df-re 15158  df-im 15159  df-sqrt 15293  df-abs 15294  df-limsup 15529  df-clim 15546  df-rlim 15547  df-sum 15745  df-ef 16127  df-sin 16129  df-cos 16130  df-pi 16132  df-struct 17213  df-sets 17230  df-slot 17248  df-ndx 17260  df-base 17276  df-ress 17297  df-plusg 17329  df-mulr 17330  df-starv 17331  df-sca 17332  df-vsca 17333  df-ip 17334  df-tset 17335  df-ple 17336  df-ds 17338  df-unif 17339  df-hom 17340  df-cco 17341  df-rest 17481  df-topn 17482  df-0g 17500  df-gsum 17501  df-topgen 17502  df-pt 17503  df-prds 17506  df-xrs 17562  df-qtop 17567  df-imas 17568  df-xps 17570  df-mre 17644  df-mrc 17645  df-acs 17647  df-mgm 18704  df-sgrp 18783  df-mnd 18799  df-submnd 18848  df-mulg 19140  df-cntz 19393  df-cmn 19858  df-psmet 21525  df-xmet 21526  df-met 21527  df-bl 21528  df-mopn 21529  df-fbas 21530  df-fg 21531  df-cnfld 21534  df-top 23062  df-topon 23079  df-topsp 23101  df-bases 23114  df-cld 23187  df-ntr 23188  df-cls 23189  df-nei 23266  df-lp 23304  df-perf 23305  df-cn 23395  df-cnp 23396  df-haus 23483  df-tx 23730  df-hmeo 23923  df-fil 24014  df-fm 24106  df-flim 24107  df-flf 24108  df-xms 24488  df-ms 24489  df-tms 24490  df-cncf 25048  df-0p 25840  df-limc 26036  df-dv 26037  df-ply 26356  df-coe 26358  df-dgr 26359  df-log 26732  df-cxp 26733

This theorem is used by:  ftalem6  27253