Theorem ftalem5 27120

Description: Lemma for fta 27123: Main proof. We have already shifted the minimum found in ftalem3 27118 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 27119	. . . . 5 ⊢ (𝜑 → ((𝐾 ∈ ℕ ∧ (𝐴‘𝐾) ≠ 0) ∧ (𝑇 ∈ ℂ ∧ 𝑈 ∈ ℝ+ ∧ 𝑋 ∈ ℝ+)))
11	10	simprd 495	. . . 4 ⊢ (𝜑 → (𝑇 ∈ ℂ ∧ 𝑈 ∈ ℝ+ ∧ 𝑋 ∈ ℝ+))
12	11	simp1d 1143	. . 3 ⊢ (𝜑 → 𝑇 ∈ ℂ)
13	11	simp3d 1145	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ ℝ+)
14	13	rpred 13077	. . . 4 ⊢ (𝜑 → 𝑋 ∈ ℝ)
15	14	recnd 11289	. . 3 ⊢ (𝜑 → 𝑋 ∈ ℂ)
16	12, 15	mulcld 11281	. 2 ⊢ (𝜑 → (𝑇 · 𝑋) ∈ ℂ)
17		plyf 26237	. . . . . 6 ⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐹:ℂ⟶ℂ)
18	3, 17	syl 17	. . . . 5 ⊢ (𝜑 → 𝐹:ℂ⟶ℂ)
19	18, 16	ffvelcdmd 7105	. . . 4 ⊢ (𝜑 → (𝐹‘(𝑇 · 𝑋)) ∈ ℂ)
20	19	abscld 15475	. . 3 ⊢ (𝜑 → (abs‘(𝐹‘(𝑇 · 𝑋))) ∈ ℝ)
21		0cn 11253	. . . . . . 7 ⊢ 0 ∈ ℂ
22		ffvelcdm 7101	. . . . . . 7 ⊢ ((𝐹:ℂ⟶ℂ ∧ 0 ∈ ℂ) → (𝐹‘0) ∈ ℂ)
23	18, 21, 22	sylancl 586	. . . . . 6 ⊢ (𝜑 → (𝐹‘0) ∈ ℂ)
24	23	abscld 15475	. . . . 5 ⊢ (𝜑 → (abs‘(𝐹‘0)) ∈ ℝ)
25	10	simpld 494	. . . . . . . . 9 ⊢ (𝜑 → (𝐾 ∈ ℕ ∧ (𝐴‘𝐾) ≠ 0))
26	25	simpld 494	. . . . . . . 8 ⊢ (𝜑 → 𝐾 ∈ ℕ)
27	26	nnnn0d 12587	. . . . . . 7 ⊢ (𝜑 → 𝐾 ∈ ℕ0)
28	14, 27	reexpcld 14203	. . . . . 6 ⊢ (𝜑 → (𝑋↑𝐾) ∈ ℝ)
29	24, 28	remulcld 11291	. . . . 5 ⊢ (𝜑 → ((abs‘(𝐹‘0)) · (𝑋↑𝐾)) ∈ ℝ)
30	24, 29	resubcld 11691	. . . 4 ⊢ (𝜑 → ((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋↑𝐾))) ∈ ℝ)
31		fzfid 14014	. . . . . 6 ⊢ (𝜑 → ((𝐾 + 1)...𝑁) ∈ Fin)
32	1	coef3 26271	. . . . . . . . 9 ⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐴:ℕ0⟶ℂ)
33	3, 32	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)
34		peano2nn0 12566	. . . . . . . . . 10 ⊢ (𝐾 ∈ ℕ0 → (𝐾 + 1) ∈ ℕ0)
35	27, 34	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝐾 + 1) ∈ ℕ0)
36		elfzuz 13560	. . . . . . . . 9 ⊢ (𝑘 ∈ ((𝐾 + 1)...𝑁) → 𝑘 ∈ (ℤ≥‘(𝐾 + 1)))
37		eluznn0 12959	. . . . . . . . 9 ⊢ (((𝐾 + 1) ∈ ℕ0 ∧ 𝑘 ∈ (ℤ≥‘(𝐾 + 1))) → 𝑘 ∈ ℕ0)
38	35, 36, 37	syl2an 596	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑘 ∈ ℕ0)
39		ffvelcdm 7101	. . . . . . . 8 ⊢ ((𝐴:ℕ0⟶ℂ ∧ 𝑘 ∈ ℕ0) → (𝐴‘𝑘) ∈ ℂ)
40	33, 38, 39	syl2an2r 685	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝐴‘𝑘) ∈ ℂ)
41	16	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑇 · 𝑋) ∈ ℂ)
42	41, 38	expcld 14186	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((𝑇 · 𝑋)↑𝑘) ∈ ℂ)
43	40, 42	mulcld 11281	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) ∈ ℂ)
44	31, 43	fsumcl 15769	. . . . 5 ⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) ∈ ℂ)
45	44	abscld 15475	. . . 4 ⊢ (𝜑 → (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) ∈ ℝ)
46	30, 45	readdcld 11290	. . 3 ⊢ (𝜑 → (((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋↑𝐾))) + (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))) ∈ ℝ)
47		fzfid 14014	. . . . . 6 ⊢ (𝜑 → (0...𝐾) ∈ Fin)
48		elfznn0 13660	. . . . . . . 8 ⊢ (𝑘 ∈ (0...𝐾) → 𝑘 ∈ ℕ0)
49	33, 48, 39	syl2an 596	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐾)) → (𝐴‘𝑘) ∈ ℂ)
50		expcl 14120	. . . . . . . 8 ⊢ (((𝑇 · 𝑋) ∈ ℂ ∧ 𝑘 ∈ ℕ0) → ((𝑇 · 𝑋)↑𝑘) ∈ ℂ)
51	16, 48, 50	syl2an 596	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐾)) → ((𝑇 · 𝑋)↑𝑘) ∈ ℂ)
52	49, 51	mulcld 11281	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐾)) → ((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) ∈ ℂ)
53	47, 52	fsumcl 15769	. . . . 5 ⊢ (𝜑 → Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) ∈ ℂ)
54	53, 44	abstrid 15495	. . . 4 ⊢ (𝜑 → (abs‘(Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) + Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))) ≤ ((abs‘Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) + (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))))
55	1, 2	coeid2 26278	. . . . . . 7 ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (𝑇 · 𝑋) ∈ ℂ) → (𝐹‘(𝑇 · 𝑋)) = Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))
56	3, 16, 55	syl2anc 584	. . . . . 6 ⊢ (𝜑 → (𝐹‘(𝑇 · 𝑋)) = Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))
57	26	nnred 12281	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ∈ ℝ)
58	57	ltp1d 12198	. . . . . . . 8 ⊢ (𝜑 → 𝐾 < (𝐾 + 1))
59		fzdisj 13591	. . . . . . . 8 ⊢ (𝐾 < (𝐾 + 1) → ((0...𝐾) ∩ ((𝐾 + 1)...𝑁)) = ∅)
60	58, 59	syl 17	. . . . . . 7 ⊢ (𝜑 → ((0...𝐾) ∩ ((𝐾 + 1)...𝑁)) = ∅)
61		ssrab2 4080	. . . . . . . . . . . 12 ⊢ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ⊆ ℕ
62		nnuz 12921	. . . . . . . . . . . 12 ⊢ ℕ = (ℤ≥‘1)
63	61, 62	sseqtri 4032	. . . . . . . . . . 11 ⊢ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ⊆ (ℤ≥‘1)
64		fveq2 6906	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑁 → (𝐴‘𝑛) = (𝐴‘𝑁))
65	64	neeq1d 3000	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑁 → ((𝐴‘𝑛) ≠ 0 ↔ (𝐴‘𝑁) ≠ 0))
66	4	nnne0d 12316	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ≠ 0)
67	2, 1	dgreq0 26305	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ (Poly‘𝑆) → (𝐹 = 0𝑝 ↔ (𝐴‘𝑁) = 0))
68	3, 67	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐹 = 0𝑝 ↔ (𝐴‘𝑁) = 0))
69		fveq2 6906	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 = 0𝑝 → (deg‘𝐹) = (deg‘0𝑝))
70		dgr0 26302	. . . . . . . . . . . . . . . . 17 ⊢ (deg‘0𝑝) = 0
71	69, 70	eqtrdi 2793	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 = 0𝑝 → (deg‘𝐹) = 0)
72	2, 71	eqtrid 2789	. . . . . . . . . . . . . . 15 ⊢ (𝐹 = 0𝑝 → 𝑁 = 0)
73	68, 72	biimtrrdi 254	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐴‘𝑁) = 0 → 𝑁 = 0))
74	73	necon3d 2961	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑁 ≠ 0 → (𝐴‘𝑁) ≠ 0))
75	66, 74	mpd 15	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴‘𝑁) ≠ 0)
76	65, 4, 75	elrabd 3694	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0})
77		infssuzle 12973	. . . . . . . . . . 11 ⊢ (({𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ⊆ (ℤ≥‘1) ∧ 𝑁 ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0}) → inf({𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0}, ℝ, < ) ≤ 𝑁)
78	63, 76, 77	sylancr 587	. . . . . . . . . 10 ⊢ (𝜑 → inf({𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0}, ℝ, < ) ≤ 𝑁)
79	6, 78	eqbrtrid 5178	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ≤ 𝑁)
80		nn0uz 12920	. . . . . . . . . . 11 ⊢ ℕ0 = (ℤ≥‘0)
81	27, 80	eleqtrdi 2851	. . . . . . . . . 10 ⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘0))
82	4	nnzd 12640	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ ℤ)
83		elfz5 13556	. . . . . . . . . 10 ⊢ ((𝐾 ∈ (ℤ≥‘0) ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (0...𝑁) ↔ 𝐾 ≤ 𝑁))
84	81, 82, 83	syl2anc 584	. . . . . . . . 9 ⊢ (𝜑 → (𝐾 ∈ (0...𝑁) ↔ 𝐾 ≤ 𝑁))
85	79, 84	mpbird 257	. . . . . . . 8 ⊢ (𝜑 → 𝐾 ∈ (0...𝑁))
86		fzsplit 13590	. . . . . . . 8 ⊢ (𝐾 ∈ (0...𝑁) → (0...𝑁) = ((0...𝐾) ∪ ((𝐾 + 1)...𝑁)))
87	85, 86	syl 17	. . . . . . 7 ⊢ (𝜑 → (0...𝑁) = ((0...𝐾) ∪ ((𝐾 + 1)...𝑁)))
88		fzfid 14014	. . . . . . 7 ⊢ (𝜑 → (0...𝑁) ∈ Fin)
89		elfznn0 13660	. . . . . . . . 9 ⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0)
90	33, 89, 39	syl2an 596	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝐴‘𝑘) ∈ ℂ)
91	16, 89, 50	syl2an 596	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝑇 · 𝑋)↑𝑘) ∈ ℂ)
92	90, 91	mulcld 11281	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) ∈ ℂ)
93	60, 87, 88, 92	fsumsplit 15777	. . . . . 6 ⊢ (𝜑 → Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = (Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) + Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))))
94	56, 93	eqtrd 2777	. . . . 5 ⊢ (𝜑 → (𝐹‘(𝑇 · 𝑋)) = (Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) + Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))))
95	94	fveq2d 6910	. . . 4 ⊢ (𝜑 → (abs‘(𝐹‘(𝑇 · 𝑋))) = (abs‘(Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) + Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))))
96	1	coefv0 26287	. . . . . . . . . . . . 13 ⊢ (𝐹 ∈ (Poly‘𝑆) → (𝐹‘0) = (𝐴‘0))
97	3, 96	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹‘0) = (𝐴‘0))
98	97	eqcomd 2743	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴‘0) = (𝐹‘0))
99	16	exp0d 14180	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑇 · 𝑋)↑0) = 1)
100	98, 99	oveq12d 7449	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴‘0) · ((𝑇 · 𝑋)↑0)) = ((𝐹‘0) · 1))
101	23	mulridd 11278	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐹‘0) · 1) = (𝐹‘0))
102	100, 101	eqtrd 2777	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴‘0) · ((𝑇 · 𝑋)↑0)) = (𝐹‘0))
103		1e0p1 12775	. . . . . . . . . . . . 13 ⊢ 1 = (0 + 1)
104	103	oveq1i 7441	. . . . . . . . . . . 12 ⊢ (1...𝐾) = ((0 + 1)...𝐾)
105	104	sumeq1i 15733	. . . . . . . . . . 11 ⊢ Σ𝑘 ∈ (1...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = Σ𝑘 ∈ ((0 + 1)...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))
106	26, 62	eleqtrdi 2851	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘1))
107		elfznn 13593	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ (1...𝐾) → 𝑘 ∈ ℕ)
108	107	nnnn0d 12587	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (1...𝐾) → 𝑘 ∈ ℕ0)
109	33, 108, 39	syl2an 596	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐾)) → (𝐴‘𝑘) ∈ ℂ)
110	16, 108, 50	syl2an 596	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐾)) → ((𝑇 · 𝑋)↑𝑘) ∈ ℂ)
111	109, 110	mulcld 11281	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐾)) → ((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) ∈ ℂ)
112		fveq2 6906	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝐾 → (𝐴‘𝑘) = (𝐴‘𝐾))
113		oveq2 7439	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝐾 → ((𝑇 · 𝑋)↑𝑘) = ((𝑇 · 𝑋)↑𝐾))
114	112, 113	oveq12d 7449	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝐾 → ((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = ((𝐴‘𝐾) · ((𝑇 · 𝑋)↑𝐾)))
115	106, 111, 114	fsumm1 15787	. . . . . . . . . . 11 ⊢ (𝜑 → Σ𝑘 ∈ (1...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = (Σ𝑘 ∈ (1...(𝐾 − 1))((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) + ((𝐴‘𝐾) · ((𝑇 · 𝑋)↑𝐾))))
116	105, 115	eqtr3id 2791	. . . . . . . . . 10 ⊢ (𝜑 → Σ𝑘 ∈ ((0 + 1)...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = (Σ𝑘 ∈ (1...(𝐾 − 1))((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) + ((𝐴‘𝐾) · ((𝑇 · 𝑋)↑𝐾))))
117		elfznn 13593	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 ∈ (1...(𝐾 − 1)) → 𝑘 ∈ ℕ)
118	117	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → 𝑘 ∈ ℕ)
119	118	nnred 12281	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → 𝑘 ∈ ℝ)
120	57	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → 𝐾 ∈ ℝ)
121		peano2rem 11576	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐾 ∈ ℝ → (𝐾 − 1) ∈ ℝ)
122	120, 121	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → (𝐾 − 1) ∈ ℝ)
123		elfzle2 13568	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ (1...(𝐾 − 1)) → 𝑘 ≤ (𝐾 − 1))
124	123	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → 𝑘 ≤ (𝐾 − 1))
125	120	ltm1d 12200	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → (𝐾 − 1) < 𝐾)
126	119, 122, 120, 124, 125	lelttrd 11419	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → 𝑘 < 𝐾)
127	119, 120	ltnled 11408	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → (𝑘 < 𝐾 ↔ ¬ 𝐾 ≤ 𝑘))
128	126, 127	mpbid 232	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → ¬ 𝐾 ≤ 𝑘)
129		infssuzle 12973	. . . . . . . . . . . . . . . . . . 19 ⊢ (({𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ⊆ (ℤ≥‘1) ∧ 𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0}) → inf({𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0}, ℝ, < ) ≤ 𝑘)
130	6, 129	eqbrtrid 5178	. . . . . . . . . . . . . . . . . 18 ⊢ (({𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ⊆ (ℤ≥‘1) ∧ 𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0}) → 𝐾 ≤ 𝑘)
131	63, 130	mpan 690	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} → 𝐾 ≤ 𝑘)
132	128, 131	nsyl 140	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → ¬ 𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0})
133		fveq2 6906	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 𝑘 → (𝐴‘𝑛) = (𝐴‘𝑘))
134	133	neeq1d 3000	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑘 → ((𝐴‘𝑛) ≠ 0 ↔ (𝐴‘𝑘) ≠ 0))
135	134	elrab3 3693	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ℕ → (𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ↔ (𝐴‘𝑘) ≠ 0))
136	118, 135	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → (𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ↔ (𝐴‘𝑘) ≠ 0))
137	136	necon2bbid 2984	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → ((𝐴‘𝑘) = 0 ↔ ¬ 𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0}))
138	132, 137	mpbird 257	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → (𝐴‘𝑘) = 0)
139	138	oveq1d 7446	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → ((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = (0 · ((𝑇 · 𝑋)↑𝑘)))
140	117	nnnn0d 12587	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ (1...(𝐾 − 1)) → 𝑘 ∈ ℕ0)
141	16, 140, 50	syl2an 596	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → ((𝑇 · 𝑋)↑𝑘) ∈ ℂ)
142	141	mul02d 11459	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → (0 · ((𝑇 · 𝑋)↑𝑘)) = 0)
143	139, 142	eqtrd 2777	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → ((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = 0)
144	143	sumeq2dv 15738	. . . . . . . . . . . 12 ⊢ (𝜑 → Σ𝑘 ∈ (1...(𝐾 − 1))((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = Σ𝑘 ∈ (1...(𝐾 − 1))0)
145		fzfi 14013	. . . . . . . . . . . . . 14 ⊢ (1...(𝐾 − 1)) ∈ Fin
146	145	olci 867	. . . . . . . . . . . . 13 ⊢ ((1...(𝐾 − 1)) ⊆ (ℤ≥‘1) ∨ (1...(𝐾 − 1)) ∈ Fin)
147		sumz 15758	. . . . . . . . . . . . 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 2793	. . . . . . . . . . 11 ⊢ (𝜑 → Σ𝑘 ∈ (1...(𝐾 − 1))((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = 0)
150	12, 15, 27	mulexpd 14201	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑇 · 𝑋)↑𝐾) = ((𝑇↑𝐾) · (𝑋↑𝐾)))
151	150	oveq2d 7447	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐴‘𝐾) · ((𝑇 · 𝑋)↑𝐾)) = ((𝐴‘𝐾) · ((𝑇↑𝐾) · (𝑋↑𝐾))))
152	33, 27	ffvelcdmd 7105	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐴‘𝐾) ∈ ℂ)
153	12, 27	expcld 14186	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑇↑𝐾) ∈ ℂ)
154	28	recnd 11289	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑋↑𝐾) ∈ ℂ)
155	152, 153, 154	mulassd 11284	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐴‘𝐾) · (𝑇↑𝐾)) · (𝑋↑𝐾)) = ((𝐴‘𝐾) · ((𝑇↑𝐾) · (𝑋↑𝐾))))
156	151, 155	eqtr4d 2780	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐴‘𝐾) · ((𝑇 · 𝑋)↑𝐾)) = (((𝐴‘𝐾) · (𝑇↑𝐾)) · (𝑋↑𝐾)))
157	7	oveq1i 7441	. . . . . . . . . . . . . . . 16 ⊢ (𝑇↑𝐾) = ((-((𝐹‘0) / (𝐴‘𝐾))↑𝑐(1 / 𝐾))↑𝐾)
158	57	recnd 11289	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐾 ∈ ℂ)
159	26	nnne0d 12316	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐾 ≠ 0)
160	158, 159	recid2d 12039	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((1 / 𝐾) · 𝐾) = 1)
161	160	oveq2d 7447	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (-((𝐹‘0) / (𝐴‘𝐾))↑𝑐((1 / 𝐾) · 𝐾)) = (-((𝐹‘0) / (𝐴‘𝐾))↑𝑐1))
162	25	simprd 495	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐴‘𝐾) ≠ 0)
163	23, 152, 162	divcld 12043	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐹‘0) / (𝐴‘𝐾)) ∈ ℂ)
164	163	negcld 11607	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → -((𝐹‘0) / (𝐴‘𝐾)) ∈ ℂ)
165	26	nnrecred 12317	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (1 / 𝐾) ∈ ℝ)
166	165	recnd 11289	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (1 / 𝐾) ∈ ℂ)
167	164, 166, 27	cxpmul2d 26751	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (-((𝐹‘0) / (𝐴‘𝐾))↑𝑐((1 / 𝐾) · 𝐾)) = ((-((𝐹‘0) / (𝐴‘𝐾))↑𝑐(1 / 𝐾))↑𝐾))
168	164	cxp1d 26748	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (-((𝐹‘0) / (𝐴‘𝐾))↑𝑐1) = -((𝐹‘0) / (𝐴‘𝐾)))
169	161, 167, 168	3eqtr3d 2785	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((-((𝐹‘0) / (𝐴‘𝐾))↑𝑐(1 / 𝐾))↑𝐾) = -((𝐹‘0) / (𝐴‘𝐾)))
170	157, 169	eqtrid 2789	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑇↑𝐾) = -((𝐹‘0) / (𝐴‘𝐾)))
171	170	oveq2d 7447	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐴‘𝐾) · (𝑇↑𝐾)) = ((𝐴‘𝐾) · -((𝐹‘0) / (𝐴‘𝐾))))
172	152, 163	mulneg2d 11717	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐴‘𝐾) · -((𝐹‘0) / (𝐴‘𝐾))) = -((𝐴‘𝐾) · ((𝐹‘0) / (𝐴‘𝐾))))
173	23, 152, 162	divcan2d 12045	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐴‘𝐾) · ((𝐹‘0) / (𝐴‘𝐾))) = (𝐹‘0))
174	173	negeqd 11502	. . . . . . . . . . . . . 14 ⊢ (𝜑 → -((𝐴‘𝐾) · ((𝐹‘0) / (𝐴‘𝐾))) = -(𝐹‘0))
175	171, 172, 174	3eqtrd 2781	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐴‘𝐾) · (𝑇↑𝐾)) = -(𝐹‘0))
176	175	oveq1d 7446	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐴‘𝐾) · (𝑇↑𝐾)) · (𝑋↑𝐾)) = (-(𝐹‘0) · (𝑋↑𝐾)))
177	23, 154	mulneg1d 11716	. . . . . . . . . . . 12 ⊢ (𝜑 → (-(𝐹‘0) · (𝑋↑𝐾)) = -((𝐹‘0) · (𝑋↑𝐾)))
178	156, 176, 177	3eqtrd 2781	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴‘𝐾) · ((𝑇 · 𝑋)↑𝐾)) = -((𝐹‘0) · (𝑋↑𝐾)))
179	149, 178	oveq12d 7449	. . . . . . . . . 10 ⊢ (𝜑 → (Σ𝑘 ∈ (1...(𝐾 − 1))((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) + ((𝐴‘𝐾) · ((𝑇 · 𝑋)↑𝐾))) = (0 + -((𝐹‘0) · (𝑋↑𝐾))))
180	23, 154	mulcld 11281	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐹‘0) · (𝑋↑𝐾)) ∈ ℂ)
181	180	negcld 11607	. . . . . . . . . . 11 ⊢ (𝜑 → -((𝐹‘0) · (𝑋↑𝐾)) ∈ ℂ)
182	181	addlidd 11462	. . . . . . . . . 10 ⊢ (𝜑 → (0 + -((𝐹‘0) · (𝑋↑𝐾))) = -((𝐹‘0) · (𝑋↑𝐾)))
183	116, 179, 182	3eqtrd 2781	. . . . . . . . 9 ⊢ (𝜑 → Σ𝑘 ∈ ((0 + 1)...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = -((𝐹‘0) · (𝑋↑𝐾)))
184	102, 183	oveq12d 7449	. . . . . . . 8 ⊢ (𝜑 → (((𝐴‘0) · ((𝑇 · 𝑋)↑0)) + Σ𝑘 ∈ ((0 + 1)...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) = ((𝐹‘0) + -((𝐹‘0) · (𝑋↑𝐾))))
185		fveq2 6906	. . . . . . . . . 10 ⊢ (𝑘 = 0 → (𝐴‘𝑘) = (𝐴‘0))
186		oveq2 7439	. . . . . . . . . 10 ⊢ (𝑘 = 0 → ((𝑇 · 𝑋)↑𝑘) = ((𝑇 · 𝑋)↑0))
187	185, 186	oveq12d 7449	. . . . . . . . 9 ⊢ (𝑘 = 0 → ((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = ((𝐴‘0) · ((𝑇 · 𝑋)↑0)))
188	81, 52, 187	fsum1p 15789	. . . . . . . 8 ⊢ (𝜑 → Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = (((𝐴‘0) · ((𝑇 · 𝑋)↑0)) + Σ𝑘 ∈ ((0 + 1)...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))))
189	101	oveq1d 7446	. . . . . . . . 9 ⊢ (𝜑 → (((𝐹‘0) · 1) − ((𝐹‘0) · (𝑋↑𝐾))) = ((𝐹‘0) − ((𝐹‘0) · (𝑋↑𝐾))))
190		1cnd 11256	. . . . . . . . . 10 ⊢ (𝜑 → 1 ∈ ℂ)
191	23, 190, 154	subdid 11719	. . . . . . . . 9 ⊢ (𝜑 → ((𝐹‘0) · (1 − (𝑋↑𝐾))) = (((𝐹‘0) · 1) − ((𝐹‘0) · (𝑋↑𝐾))))
192	23, 180	negsubd 11626	. . . . . . . . 9 ⊢ (𝜑 → ((𝐹‘0) + -((𝐹‘0) · (𝑋↑𝐾))) = ((𝐹‘0) − ((𝐹‘0) · (𝑋↑𝐾))))
193	189, 191, 192	3eqtr4d 2787	. . . . . . . 8 ⊢ (𝜑 → ((𝐹‘0) · (1 − (𝑋↑𝐾))) = ((𝐹‘0) + -((𝐹‘0) · (𝑋↑𝐾))))
194	184, 188, 193	3eqtr4d 2787	. . . . . . 7 ⊢ (𝜑 → Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = ((𝐹‘0) · (1 − (𝑋↑𝐾))))
195	194	fveq2d 6910	. . . . . 6 ⊢ (𝜑 → (abs‘Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) = (abs‘((𝐹‘0) · (1 − (𝑋↑𝐾)))))
196		1re 11261	. . . . . . . . 9 ⊢ 1 ∈ ℝ
197		resubcl 11573	. . . . . . . . 9 ⊢ ((1 ∈ ℝ ∧ (𝑋↑𝐾) ∈ ℝ) → (1 − (𝑋↑𝐾)) ∈ ℝ)
198	196, 28, 197	sylancr 587	. . . . . . . 8 ⊢ (𝜑 → (1 − (𝑋↑𝐾)) ∈ ℝ)
199	198	recnd 11289	. . . . . . 7 ⊢ (𝜑 → (1 − (𝑋↑𝐾)) ∈ ℂ)
200	23, 199	absmuld 15493	. . . . . 6 ⊢ (𝜑 → (abs‘((𝐹‘0) · (1 − (𝑋↑𝐾)))) = ((abs‘(𝐹‘0)) · (abs‘(1 − (𝑋↑𝐾)))))
201	13	rpge0d 13081	. . . . . . . . . . 11 ⊢ (𝜑 → 0 ≤ 𝑋)
202	11	simp2d 1144	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑈 ∈ ℝ+)
203	202	rpred 13077	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑈 ∈ ℝ)
204		min1 13231	. . . . . . . . . . . . 13 ⊢ ((1 ∈ ℝ ∧ 𝑈 ∈ ℝ) → if(1 ≤ 𝑈, 1, 𝑈) ≤ 1)
205	196, 203, 204	sylancr 587	. . . . . . . . . . . 12 ⊢ (𝜑 → if(1 ≤ 𝑈, 1, 𝑈) ≤ 1)
206	9, 205	eqbrtrid 5178	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑋 ≤ 1)
207		exple1 14216	. . . . . . . . . . 11 ⊢ (((𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ∧ 𝑋 ≤ 1) ∧ 𝐾 ∈ ℕ0) → (𝑋↑𝐾) ≤ 1)
208	14, 201, 206, 27, 207	syl31anc 1375	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋↑𝐾) ≤ 1)
209		subge0 11776	. . . . . . . . . . 11 ⊢ ((1 ∈ ℝ ∧ (𝑋↑𝐾) ∈ ℝ) → (0 ≤ (1 − (𝑋↑𝐾)) ↔ (𝑋↑𝐾) ≤ 1))
210	196, 28, 209	sylancr 587	. . . . . . . . . 10 ⊢ (𝜑 → (0 ≤ (1 − (𝑋↑𝐾)) ↔ (𝑋↑𝐾) ≤ 1))
211	208, 210	mpbird 257	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ (1 − (𝑋↑𝐾)))
212	198, 211	absidd 15461	. . . . . . . 8 ⊢ (𝜑 → (abs‘(1 − (𝑋↑𝐾))) = (1 − (𝑋↑𝐾)))
213	212	oveq2d 7447	. . . . . . 7 ⊢ (𝜑 → ((abs‘(𝐹‘0)) · (abs‘(1 − (𝑋↑𝐾)))) = ((abs‘(𝐹‘0)) · (1 − (𝑋↑𝐾))))
214	24	recnd 11289	. . . . . . . 8 ⊢ (𝜑 → (abs‘(𝐹‘0)) ∈ ℂ)
215	214, 190, 154	subdid 11719	. . . . . . 7 ⊢ (𝜑 → ((abs‘(𝐹‘0)) · (1 − (𝑋↑𝐾))) = (((abs‘(𝐹‘0)) · 1) − ((abs‘(𝐹‘0)) · (𝑋↑𝐾))))
216	214	mulridd 11278	. . . . . . . 8 ⊢ (𝜑 → ((abs‘(𝐹‘0)) · 1) = (abs‘(𝐹‘0)))
217	216	oveq1d 7446	. . . . . . 7 ⊢ (𝜑 → (((abs‘(𝐹‘0)) · 1) − ((abs‘(𝐹‘0)) · (𝑋↑𝐾))) = ((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋↑𝐾))))
218	213, 215, 217	3eqtrd 2781	. . . . . 6 ⊢ (𝜑 → ((abs‘(𝐹‘0)) · (abs‘(1 − (𝑋↑𝐾)))) = ((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋↑𝐾))))
219	195, 200, 218	3eqtrrd 2782	. . . . 5 ⊢ (𝜑 → ((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋↑𝐾))) = (abs‘Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))))
220	219	oveq1d 7446	. . . 4 ⊢ (𝜑 → (((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋↑𝐾))) + (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))) = ((abs‘Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) + (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))))
221	54, 95, 220	3brtr4d 5175	. . 3 ⊢ (𝜑 → (abs‘(𝐹‘(𝑇 · 𝑋))) ≤ (((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋↑𝐾))) + (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))))
222	43	abscld 15475	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) ∈ ℝ)
223	31, 222	fsumrecl 15770	. . . . . 6 ⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) ∈ ℝ)
224	31, 43	fsumabs 15837	. . . . . 6 ⊢ (𝜑 → (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) ≤ Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))))
225		expcl 14120	. . . . . . . . . . . 12 ⊢ ((𝑇 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (𝑇↑𝑘) ∈ ℂ)
226	12, 38, 225	syl2an2r 685	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑇↑𝑘) ∈ ℂ)
227	40, 226	mulcld 11281	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((𝐴‘𝑘) · (𝑇↑𝑘)) ∈ ℂ)
228	227	abscld 15475	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) ∈ ℝ)
229	31, 228	fsumrecl 15770	. . . . . . . 8 ⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) ∈ ℝ)
230	14, 35	reexpcld 14203	. . . . . . . 8 ⊢ (𝜑 → (𝑋↑(𝐾 + 1)) ∈ ℝ)
231	229, 230	remulcld 11291	. . . . . . 7 ⊢ (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1))) ∈ ℝ)
232	230	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑋↑(𝐾 + 1)) ∈ ℝ)
233	228, 232	remulcld 11291	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1))) ∈ ℝ)
234	12	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑇 ∈ ℂ)
235	15	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑋 ∈ ℂ)
236	234, 235, 38	mulexpd 14201	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((𝑇 · 𝑋)↑𝑘) = ((𝑇↑𝑘) · (𝑋↑𝑘)))
237	236	oveq2d 7447	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = ((𝐴‘𝑘) · ((𝑇↑𝑘) · (𝑋↑𝑘))))
238	14	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑋 ∈ ℝ)
239	238, 38	reexpcld 14203	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑋↑𝑘) ∈ ℝ)
240	239	recnd 11289	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑋↑𝑘) ∈ ℂ)
241	40, 226, 240	mulassd 11284	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (((𝐴‘𝑘) · (𝑇↑𝑘)) · (𝑋↑𝑘)) = ((𝐴‘𝑘) · ((𝑇↑𝑘) · (𝑋↑𝑘))))
242	237, 241	eqtr4d 2780	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = (((𝐴‘𝑘) · (𝑇↑𝑘)) · (𝑋↑𝑘)))
243	242	fveq2d 6910	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) = (abs‘(((𝐴‘𝑘) · (𝑇↑𝑘)) · (𝑋↑𝑘))))
244	227, 240	absmuld 15493	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘(((𝐴‘𝑘) · (𝑇↑𝑘)) · (𝑋↑𝑘))) = ((abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (abs‘(𝑋↑𝑘))))
245		elfzelz 13564	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ((𝐾 + 1)...𝑁) → 𝑘 ∈ ℤ)
246		rpexpcl 14121	. . . . . . . . . . . . . . 15 ⊢ ((𝑋 ∈ ℝ+ ∧ 𝑘 ∈ ℤ) → (𝑋↑𝑘) ∈ ℝ+)
247	13, 245, 246	syl2an 596	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑋↑𝑘) ∈ ℝ+)
248	247	rpge0d 13081	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 0 ≤ (𝑋↑𝑘))
249	239, 248	absidd 15461	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘(𝑋↑𝑘)) = (𝑋↑𝑘))
250	249	oveq2d 7447	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (abs‘(𝑋↑𝑘))) = ((abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑𝑘)))
251	243, 244, 250	3eqtrd 2781	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) = ((abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑𝑘)))
252	227	absge0d 15483	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 0 ≤ (abs‘((𝐴‘𝑘) · (𝑇↑𝑘))))
253	35	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝐾 + 1) ∈ ℕ0)
254	36	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑘 ∈ (ℤ≥‘(𝐾 + 1)))
255	201	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 0 ≤ 𝑋)
256	206	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑋 ≤ 1)
257	238, 253, 254, 255, 256	leexp2rd 14294	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑋↑𝑘) ≤ (𝑋↑(𝐾 + 1)))
258	239, 232, 228, 252, 257	lemul2ad 12208	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑𝑘)) ≤ ((abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1))))
259	251, 258	eqbrtrd 5165	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) ≤ ((abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1))))
260	31, 222, 233, 259	fsumle 15835	. . . . . . . 8 ⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) ≤ Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1))))
261	230	recnd 11289	. . . . . . . . 9 ⊢ (𝜑 → (𝑋↑(𝐾 + 1)) ∈ ℂ)
262	228	recnd 11289	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) ∈ ℂ)
263	31, 261, 262	fsummulc1 15821	. . . . . . . 8 ⊢ (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1))) = Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1))))
264	260, 263	breqtrrd 5171	. . . . . . 7 ⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) ≤ (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1))))
265	15, 27	expp1d 14187	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑋↑(𝐾 + 1)) = ((𝑋↑𝐾) · 𝑋))
266	154, 15	mulcomd 11282	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑋↑𝐾) · 𝑋) = (𝑋 · (𝑋↑𝐾)))
267	265, 266	eqtrd 2777	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋↑(𝐾 + 1)) = (𝑋 · (𝑋↑𝐾)))
268	267	oveq2d 7447	. . . . . . . . 9 ⊢ (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1))) = (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋 · (𝑋↑𝐾))))
269	229	recnd 11289	. . . . . . . . . 10 ⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) ∈ ℂ)
270	269, 15, 154	mulassd 11284	. . . . . . . . 9 ⊢ (𝜑 → ((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · 𝑋) · (𝑋↑𝐾)) = (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋 · (𝑋↑𝐾))))
271	268, 270	eqtr4d 2780	. . . . . . . 8 ⊢ (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1))) = ((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · 𝑋) · (𝑋↑𝐾)))
272	229, 14	remulcld 11291	. . . . . . . . 9 ⊢ (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · 𝑋) ∈ ℝ)
273		nnssz 12635	. . . . . . . . . . . 12 ⊢ ℕ ⊆ ℤ
274	61, 273	sstri 3993	. . . . . . . . . . 11 ⊢ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ⊆ ℤ
275	76	ne0d 4342	. . . . . . . . . . . . 13 ⊢ (𝜑 → {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ≠ ∅)
276		infssuzcl 12974	. . . . . . . . . . . . 13 ⊢ (({𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ⊆ (ℤ≥‘1) ∧ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ≠ ∅) → inf({𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0}, ℝ, < ) ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0})
277	63, 275, 276	sylancr 587	. . . . . . . . . . . 12 ⊢ (𝜑 → inf({𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0}, ℝ, < ) ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0})
278	6, 277	eqeltrid 2845	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐾 ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0})
279	274, 278	sselid 3981	. . . . . . . . . 10 ⊢ (𝜑 → 𝐾 ∈ ℤ)
280	13, 279	rpexpcld 14286	. . . . . . . . 9 ⊢ (𝜑 → (𝑋↑𝐾) ∈ ℝ+)
281		peano2re 11434	. . . . . . . . . . . 12 ⊢ (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) ∈ ℝ → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1) ∈ ℝ)
282	229, 281	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1) ∈ ℝ)
283	282, 14	remulcld 11291	. . . . . . . . . 10 ⊢ (𝜑 → ((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1) · 𝑋) ∈ ℝ)
284	229	ltp1d 12198	. . . . . . . . . . 11 ⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) < (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1))
285	229, 282, 13, 284	ltmul1dd 13132	. . . . . . . . . 10 ⊢ (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · 𝑋) < ((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1) · 𝑋))
286		min2 13232	. . . . . . . . . . . . . 14 ⊢ ((1 ∈ ℝ ∧ 𝑈 ∈ ℝ) → if(1 ≤ 𝑈, 1, 𝑈) ≤ 𝑈)
287	196, 203, 286	sylancr 587	. . . . . . . . . . . . 13 ⊢ (𝜑 → if(1 ≤ 𝑈, 1, 𝑈) ≤ 𝑈)
288	9, 287	eqbrtrid 5178	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑋 ≤ 𝑈)
289	288, 8	breqtrdi 5184	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑋 ≤ ((abs‘(𝐹‘0)) / (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1)))
290		0red 11264	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 ∈ ℝ)
291	31, 228, 252	fsumge0 15831	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 ≤ Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))))
292	290, 229, 282, 291, 284	lelttrd 11419	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 < (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1))
293		lemuldiv2 12149	. . . . . . . . . . . 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 1376	. . . . . . . . . . 11 ⊢ (𝜑 → (((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1) · 𝑋) ≤ (abs‘(𝐹‘0)) ↔ 𝑋 ≤ ((abs‘(𝐹‘0)) / (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1))))
295	289, 294	mpbird 257	. . . . . . . . . 10 ⊢ (𝜑 → ((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1) · 𝑋) ≤ (abs‘(𝐹‘0)))
296	272, 283, 24, 285, 295	ltletrd 11421	. . . . . . . . 9 ⊢ (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · 𝑋) < (abs‘(𝐹‘0)))
297	272, 24, 280, 296	ltmul1dd 13132	. . . . . . . 8 ⊢ (𝜑 → ((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · 𝑋) · (𝑋↑𝐾)) < ((abs‘(𝐹‘0)) · (𝑋↑𝐾)))
298	271, 297	eqbrtrd 5165	. . . . . . 7 ⊢ (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1))) < ((abs‘(𝐹‘0)) · (𝑋↑𝐾)))
299	223, 231, 29, 264, 298	lelttrd 11419	. . . . . 6 ⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) < ((abs‘(𝐹‘0)) · (𝑋↑𝐾)))
300	45, 223, 29, 224, 299	lelttrd 11419	. . . . 5 ⊢ (𝜑 → (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) < ((abs‘(𝐹‘0)) · (𝑋↑𝐾)))
301	45, 29, 24, 300	ltsub2dd 11876	. . . 4 ⊢ (𝜑 → ((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋↑𝐾))) < ((abs‘(𝐹‘0)) − (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))))
302	30, 45, 24	ltaddsubd 11863	. . . 4 ⊢ (𝜑 → ((((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋↑𝐾))) + (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))) < (abs‘(𝐹‘0)) ↔ ((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋↑𝐾))) < ((abs‘(𝐹‘0)) − (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))))))
303	301, 302	mpbird 257	. . 3 ⊢ (𝜑 → (((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋↑𝐾))) + (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))) < (abs‘(𝐹‘0)))
304	20, 46, 24, 221, 303	lelttrd 11419	. 2 ⊢ (𝜑 → (abs‘(𝐹‘(𝑇 · 𝑋))) < (abs‘(𝐹‘0)))
305		2fveq3 6911	. . . 4 ⊢ (𝑥 = (𝑇 · 𝑋) → (abs‘(𝐹‘𝑥)) = (abs‘(𝐹‘(𝑇 · 𝑋))))
306	305	breq1d 5153	. . 3 ⊢ (𝑥 = (𝑇 · 𝑋) → ((abs‘(𝐹‘𝑥)) < (abs‘(𝐹‘0)) ↔ (abs‘(𝐹‘(𝑇 · 𝑋))) < (abs‘(𝐹‘0))))
307	306	rspcev 3622	. 2 ⊢ (((𝑇 · 𝑋) ∈ ℂ ∧ (abs‘(𝐹‘(𝑇 · 𝑋))) < (abs‘(𝐹‘0))) → ∃𝑥 ∈ ℂ (abs‘(𝐹‘𝑥)) < (abs‘(𝐹‘0)))
308	16, 304, 307	syl2anc 584	1 ⊢ (𝜑 → ∃𝑥 ∈ ℂ (abs‘(𝐹‘𝑥)) < (abs‘(𝐹‘0)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 848   ∧ w3a 1087   = wceq 1540   ∈ wcel 2108   ≠ wne 2940  ∃wrex 3070  {crab 3436   ∪ cun 3949   ∩ cin 3950   ⊆ wss 3951  ∅c0 4333  ifcif 4525   class class class wbr 5143  ⟶wf 6557  ‘cfv 6561  (class class class)co 7431  Fincfn 8985  infcinf 9481  ℂcc 11153  ℝcr 11154  0cc0 11155  1c1 11156   + caddc 11158   · cmul 11160   < clt 11295   ≤ cle 11296   − cmin 11492  -cneg 11493   / cdiv 11920  ℕcn 12266  ℕ₀cn0 12526  ℤcz 12613  ℤ_≥cuz 12878  ℝ⁺crp 13034  ...cfz 13547  ↑cexp 14102  abscabs 15273  Σcsu 15722  0_𝑝c0p 25704  Polycply 26223  coeffccoe 26225  degcdgr 26226  ↑_𝑐ccxp 26597

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-inf2 9681  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232  ax-pre-sup 11233  ax-addf 11234

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-tp 4631  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-iin 4994  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-se 5638  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-isom 6570  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-of 7697  df-om 7888  df-1st 8014  df-2nd 8015  df-supp 8186  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-2o 8507  df-er 8745  df-map 8868  df-pm 8869  df-ixp 8938  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-fsupp 9402  df-fi 9451  df-sup 9482  df-inf 9483  df-oi 9550  df-card 9979  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-div 11921  df-nn 12267  df-2 12329  df-3 12330  df-4 12331  df-5 12332  df-6 12333  df-7 12334  df-8 12335  df-9 12336  df-n0 12527  df-z 12614  df-dec 12734  df-uz 12879  df-q 12991  df-rp 13035  df-xneg 13154  df-xadd 13155  df-xmul 13156  df-ioo 13391  df-ioc 13392  df-ico 13393  df-icc 13394  df-fz 13548  df-fzo 13695  df-fl 13832  df-mod 13910  df-seq 14043  df-exp 14103  df-fac 14313  df-bc 14342  df-hash 14370  df-shft 15106  df-cj 15138  df-re 15139  df-im 15140  df-sqrt 15274  df-abs 15275  df-limsup 15507  df-clim 15524  df-rlim 15525  df-sum 15723  df-ef 16103  df-sin 16105  df-cos 16106  df-pi 16108  df-struct 17184  df-sets 17201  df-slot 17219  df-ndx 17231  df-base 17248  df-ress 17275  df-plusg 17310  df-mulr 17311  df-starv 17312  df-sca 17313  df-vsca 17314  df-ip 17315  df-tset 17316  df-ple 17317  df-ds 17319  df-unif 17320  df-hom 17321  df-cco 17322  df-rest 17467  df-topn 17468  df-0g 17486  df-gsum 17487  df-topgen 17488  df-pt 17489  df-prds 17492  df-xrs 17547  df-qtop 17552  df-imas 17553  df-xps 17555  df-mre 17629  df-mrc 17630  df-acs 17632  df-mgm 18653  df-sgrp 18732  df-mnd 18748  df-submnd 18797  df-mulg 19086  df-cntz 19335  df-cmn 19800  df-psmet 21356  df-xmet 21357  df-met 21358  df-bl 21359  df-mopn 21360  df-fbas 21361  df-fg 21362  df-cnfld 21365  df-top 22900  df-topon 22917  df-topsp 22939  df-bases 22953  df-cld 23027  df-ntr 23028  df-cls 23029  df-nei 23106  df-lp 23144  df-perf 23145  df-cn 23235  df-cnp 23236  df-haus 23323  df-tx 23570  df-hmeo 23763  df-fil 23854  df-fm 23946  df-flim 23947  df-flf 23948  df-xms 24330  df-ms 24331  df-tms 24332  df-cncf 24904  df-0p 25705  df-limc 25901  df-dv 25902  df-ply 26227  df-coe 26229  df-dgr 26230  df-log 26598  df-cxp 26599

This theorem is referenced by:  ftalem6  27121