Theorem ftalem5 27101

Description: Lemma for fta 27104: Main proof. We have already shifted the minimum found in ftalem3 27099 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 27100	. . . . 5 ⊢ (𝜑 → ((𝐾 ∈ ℕ ∧ (𝐴‘𝐾) ≠ 0) ∧ (𝑇 ∈ ℂ ∧ 𝑈 ∈ ℝ+ ∧ 𝑋 ∈ ℝ+)))
11	10	simprd 494	. . . 4 ⊢ (𝜑 → (𝑇 ∈ ℂ ∧ 𝑈 ∈ ℝ+ ∧ 𝑋 ∈ ℝ+))
12	11	simp1d 1139	. . 3 ⊢ (𝜑 → 𝑇 ∈ ℂ)
13	11	simp3d 1141	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ ℝ+)
14	13	rpred 13063	. . . 4 ⊢ (𝜑 → 𝑋 ∈ ℝ)
15	14	recnd 11282	. . 3 ⊢ (𝜑 → 𝑋 ∈ ℂ)
16	12, 15	mulcld 11274	. 2 ⊢ (𝜑 → (𝑇 · 𝑋) ∈ ℂ)
17		plyf 26221	. . . . . 6 ⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐹:ℂ⟶ℂ)
18	3, 17	syl 17	. . . . 5 ⊢ (𝜑 → 𝐹:ℂ⟶ℂ)
19	18, 16	ffvelcdmd 7090	. . . 4 ⊢ (𝜑 → (𝐹‘(𝑇 · 𝑋)) ∈ ℂ)
20	19	abscld 15435	. . 3 ⊢ (𝜑 → (abs‘(𝐹‘(𝑇 · 𝑋))) ∈ ℝ)
21		0cn 11246	. . . . . . 7 ⊢ 0 ∈ ℂ
22		ffvelcdm 7086	. . . . . . 7 ⊢ ((𝐹:ℂ⟶ℂ ∧ 0 ∈ ℂ) → (𝐹‘0) ∈ ℂ)
23	18, 21, 22	sylancl 584	. . . . . 6 ⊢ (𝜑 → (𝐹‘0) ∈ ℂ)
24	23	abscld 15435	. . . . 5 ⊢ (𝜑 → (abs‘(𝐹‘0)) ∈ ℝ)
25	10	simpld 493	. . . . . . . . 9 ⊢ (𝜑 → (𝐾 ∈ ℕ ∧ (𝐴‘𝐾) ≠ 0))
26	25	simpld 493	. . . . . . . 8 ⊢ (𝜑 → 𝐾 ∈ ℕ)
27	26	nnnn0d 12577	. . . . . . 7 ⊢ (𝜑 → 𝐾 ∈ ℕ0)
28	14, 27	reexpcld 14175	. . . . . 6 ⊢ (𝜑 → (𝑋↑𝐾) ∈ ℝ)
29	24, 28	remulcld 11284	. . . . 5 ⊢ (𝜑 → ((abs‘(𝐹‘0)) · (𝑋↑𝐾)) ∈ ℝ)
30	24, 29	resubcld 11682	. . . 4 ⊢ (𝜑 → ((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋↑𝐾))) ∈ ℝ)
31		fzfid 13986	. . . . . 6 ⊢ (𝜑 → ((𝐾 + 1)...𝑁) ∈ Fin)
32	1	coef3 26255	. . . . . . . . 9 ⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐴:ℕ0⟶ℂ)
33	3, 32	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)
34		peano2nn0 12557	. . . . . . . . . 10 ⊢ (𝐾 ∈ ℕ0 → (𝐾 + 1) ∈ ℕ0)
35	27, 34	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝐾 + 1) ∈ ℕ0)
36		elfzuz 13544	. . . . . . . . 9 ⊢ (𝑘 ∈ ((𝐾 + 1)...𝑁) → 𝑘 ∈ (ℤ≥‘(𝐾 + 1)))
37		eluznn0 12946	. . . . . . . . 9 ⊢ (((𝐾 + 1) ∈ ℕ0 ∧ 𝑘 ∈ (ℤ≥‘(𝐾 + 1))) → 𝑘 ∈ ℕ0)
38	35, 36, 37	syl2an 594	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑘 ∈ ℕ0)
39		ffvelcdm 7086	. . . . . . . 8 ⊢ ((𝐴:ℕ0⟶ℂ ∧ 𝑘 ∈ ℕ0) → (𝐴‘𝑘) ∈ ℂ)
40	33, 38, 39	syl2an2r 683	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝐴‘𝑘) ∈ ℂ)
41	16	adantr 479	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑇 · 𝑋) ∈ ℂ)
42	41, 38	expcld 14158	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((𝑇 · 𝑋)↑𝑘) ∈ ℂ)
43	40, 42	mulcld 11274	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) ∈ ℂ)
44	31, 43	fsumcl 15731	. . . . 5 ⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) ∈ ℂ)
45	44	abscld 15435	. . . 4 ⊢ (𝜑 → (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) ∈ ℝ)
46	30, 45	readdcld 11283	. . 3 ⊢ (𝜑 → (((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋↑𝐾))) + (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))) ∈ ℝ)
47		fzfid 13986	. . . . . 6 ⊢ (𝜑 → (0...𝐾) ∈ Fin)
48		elfznn0 13641	. . . . . . . 8 ⊢ (𝑘 ∈ (0...𝐾) → 𝑘 ∈ ℕ0)
49	33, 48, 39	syl2an 594	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐾)) → (𝐴‘𝑘) ∈ ℂ)
50		expcl 14092	. . . . . . . 8 ⊢ (((𝑇 · 𝑋) ∈ ℂ ∧ 𝑘 ∈ ℕ0) → ((𝑇 · 𝑋)↑𝑘) ∈ ℂ)
51	16, 48, 50	syl2an 594	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐾)) → ((𝑇 · 𝑋)↑𝑘) ∈ ℂ)
52	49, 51	mulcld 11274	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐾)) → ((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) ∈ ℂ)
53	47, 52	fsumcl 15731	. . . . 5 ⊢ (𝜑 → Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) ∈ ℂ)
54	53, 44	abstrid 15455	. . . 4 ⊢ (𝜑 → (abs‘(Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) + Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))) ≤ ((abs‘Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) + (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))))
55	1, 2	coeid2 26262	. . . . . . 7 ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (𝑇 · 𝑋) ∈ ℂ) → (𝐹‘(𝑇 · 𝑋)) = Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))
56	3, 16, 55	syl2anc 582	. . . . . 6 ⊢ (𝜑 → (𝐹‘(𝑇 · 𝑋)) = Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))
57	26	nnred 12272	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ∈ ℝ)
58	57	ltp1d 12189	. . . . . . . 8 ⊢ (𝜑 → 𝐾 < (𝐾 + 1))
59		fzdisj 13575	. . . . . . . 8 ⊢ (𝐾 < (𝐾 + 1) → ((0...𝐾) ∩ ((𝐾 + 1)...𝑁)) = ∅)
60	58, 59	syl 17	. . . . . . 7 ⊢ (𝜑 → ((0...𝐾) ∩ ((𝐾 + 1)...𝑁)) = ∅)
61		ssrab2 4075	. . . . . . . . . . . 12 ⊢ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ⊆ ℕ
62		nnuz 12910	. . . . . . . . . . . 12 ⊢ ℕ = (ℤ≥‘1)
63	61, 62	sseqtri 4017	. . . . . . . . . . 11 ⊢ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ⊆ (ℤ≥‘1)
64		fveq2 6892	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑁 → (𝐴‘𝑛) = (𝐴‘𝑁))
65	64	neeq1d 2990	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑁 → ((𝐴‘𝑛) ≠ 0 ↔ (𝐴‘𝑁) ≠ 0))
66	4	nnne0d 12307	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ≠ 0)
67	2, 1	dgreq0 26289	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ (Poly‘𝑆) → (𝐹 = 0𝑝 ↔ (𝐴‘𝑁) = 0))
68	3, 67	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐹 = 0𝑝 ↔ (𝐴‘𝑁) = 0))
69		fveq2 6892	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 = 0𝑝 → (deg‘𝐹) = (deg‘0𝑝))
70		dgr0 26286	. . . . . . . . . . . . . . . . 17 ⊢ (deg‘0𝑝) = 0
71	69, 70	eqtrdi 2782	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 = 0𝑝 → (deg‘𝐹) = 0)
72	2, 71	eqtrid 2778	. . . . . . . . . . . . . . 15 ⊢ (𝐹 = 0𝑝 → 𝑁 = 0)
73	68, 72	biimtrrdi 253	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐴‘𝑁) = 0 → 𝑁 = 0))
74	73	necon3d 2951	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑁 ≠ 0 → (𝐴‘𝑁) ≠ 0))
75	66, 74	mpd 15	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴‘𝑁) ≠ 0)
76	65, 4, 75	elrabd 3684	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0})
77		infssuzle 12960	. . . . . . . . . . 11 ⊢ (({𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ⊆ (ℤ≥‘1) ∧ 𝑁 ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0}) → inf({𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0}, ℝ, < ) ≤ 𝑁)
78	63, 76, 77	sylancr 585	. . . . . . . . . 10 ⊢ (𝜑 → inf({𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0}, ℝ, < ) ≤ 𝑁)
79	6, 78	eqbrtrid 5180	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ≤ 𝑁)
80		nn0uz 12909	. . . . . . . . . . 11 ⊢ ℕ0 = (ℤ≥‘0)
81	27, 80	eleqtrdi 2836	. . . . . . . . . 10 ⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘0))
82	4	nnzd 12630	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ ℤ)
83		elfz5 13540	. . . . . . . . . 10 ⊢ ((𝐾 ∈ (ℤ≥‘0) ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (0...𝑁) ↔ 𝐾 ≤ 𝑁))
84	81, 82, 83	syl2anc 582	. . . . . . . . 9 ⊢ (𝜑 → (𝐾 ∈ (0...𝑁) ↔ 𝐾 ≤ 𝑁))
85	79, 84	mpbird 256	. . . . . . . 8 ⊢ (𝜑 → 𝐾 ∈ (0...𝑁))
86		fzsplit 13574	. . . . . . . 8 ⊢ (𝐾 ∈ (0...𝑁) → (0...𝑁) = ((0...𝐾) ∪ ((𝐾 + 1)...𝑁)))
87	85, 86	syl 17	. . . . . . 7 ⊢ (𝜑 → (0...𝑁) = ((0...𝐾) ∪ ((𝐾 + 1)...𝑁)))
88		fzfid 13986	. . . . . . 7 ⊢ (𝜑 → (0...𝑁) ∈ Fin)
89		elfznn0 13641	. . . . . . . . 9 ⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0)
90	33, 89, 39	syl2an 594	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝐴‘𝑘) ∈ ℂ)
91	16, 89, 50	syl2an 594	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝑇 · 𝑋)↑𝑘) ∈ ℂ)
92	90, 91	mulcld 11274	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) ∈ ℂ)
93	60, 87, 88, 92	fsumsplit 15739	. . . . . 6 ⊢ (𝜑 → Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = (Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) + Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))))
94	56, 93	eqtrd 2766	. . . . 5 ⊢ (𝜑 → (𝐹‘(𝑇 · 𝑋)) = (Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) + Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))))
95	94	fveq2d 6896	. . . 4 ⊢ (𝜑 → (abs‘(𝐹‘(𝑇 · 𝑋))) = (abs‘(Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) + Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))))
96	1	coefv0 26271	. . . . . . . . . . . . 13 ⊢ (𝐹 ∈ (Poly‘𝑆) → (𝐹‘0) = (𝐴‘0))
97	3, 96	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹‘0) = (𝐴‘0))
98	97	eqcomd 2732	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴‘0) = (𝐹‘0))
99	16	exp0d 14152	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑇 · 𝑋)↑0) = 1)
100	98, 99	oveq12d 7433	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴‘0) · ((𝑇 · 𝑋)↑0)) = ((𝐹‘0) · 1))
101	23	mulridd 11271	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐹‘0) · 1) = (𝐹‘0))
102	100, 101	eqtrd 2766	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴‘0) · ((𝑇 · 𝑋)↑0)) = (𝐹‘0))
103		1e0p1 12764	. . . . . . . . . . . . 13 ⊢ 1 = (0 + 1)
104	103	oveq1i 7425	. . . . . . . . . . . 12 ⊢ (1...𝐾) = ((0 + 1)...𝐾)
105	104	sumeq1i 15696	. . . . . . . . . . 11 ⊢ Σ𝑘 ∈ (1...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = Σ𝑘 ∈ ((0 + 1)...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))
106	26, 62	eleqtrdi 2836	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘1))
107		elfznn 13577	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ (1...𝐾) → 𝑘 ∈ ℕ)
108	107	nnnn0d 12577	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (1...𝐾) → 𝑘 ∈ ℕ0)
109	33, 108, 39	syl2an 594	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐾)) → (𝐴‘𝑘) ∈ ℂ)
110	16, 108, 50	syl2an 594	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐾)) → ((𝑇 · 𝑋)↑𝑘) ∈ ℂ)
111	109, 110	mulcld 11274	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐾)) → ((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) ∈ ℂ)
112		fveq2 6892	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝐾 → (𝐴‘𝑘) = (𝐴‘𝐾))
113		oveq2 7423	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝐾 → ((𝑇 · 𝑋)↑𝑘) = ((𝑇 · 𝑋)↑𝐾))
114	112, 113	oveq12d 7433	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝐾 → ((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = ((𝐴‘𝐾) · ((𝑇 · 𝑋)↑𝐾)))
115	106, 111, 114	fsumm1 15749	. . . . . . . . . . 11 ⊢ (𝜑 → Σ𝑘 ∈ (1...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = (Σ𝑘 ∈ (1...(𝐾 − 1))((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) + ((𝐴‘𝐾) · ((𝑇 · 𝑋)↑𝐾))))
116	105, 115	eqtr3id 2780	. . . . . . . . . 10 ⊢ (𝜑 → Σ𝑘 ∈ ((0 + 1)...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = (Σ𝑘 ∈ (1...(𝐾 − 1))((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) + ((𝐴‘𝐾) · ((𝑇 · 𝑋)↑𝐾))))
117		elfznn 13577	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 ∈ (1...(𝐾 − 1)) → 𝑘 ∈ ℕ)
118	117	adantl 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → 𝑘 ∈ ℕ)
119	118	nnred 12272	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → 𝑘 ∈ ℝ)
120	57	adantr 479	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → 𝐾 ∈ ℝ)
121		peano2rem 11567	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐾 ∈ ℝ → (𝐾 − 1) ∈ ℝ)
122	120, 121	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → (𝐾 − 1) ∈ ℝ)
123		elfzle2 13552	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ (1...(𝐾 − 1)) → 𝑘 ≤ (𝐾 − 1))
124	123	adantl 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → 𝑘 ≤ (𝐾 − 1))
125	120	ltm1d 12191	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → (𝐾 − 1) < 𝐾)
126	119, 122, 120, 124, 125	lelttrd 11412	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → 𝑘 < 𝐾)
127	119, 120	ltnled 11401	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → (𝑘 < 𝐾 ↔ ¬ 𝐾 ≤ 𝑘))
128	126, 127	mpbid 231	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → ¬ 𝐾 ≤ 𝑘)
129		infssuzle 12960	. . . . . . . . . . . . . . . . . . 19 ⊢ (({𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ⊆ (ℤ≥‘1) ∧ 𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0}) → inf({𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0}, ℝ, < ) ≤ 𝑘)
130	6, 129	eqbrtrid 5180	. . . . . . . . . . . . . . . . . 18 ⊢ (({𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ⊆ (ℤ≥‘1) ∧ 𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0}) → 𝐾 ≤ 𝑘)
131	63, 130	mpan 688	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} → 𝐾 ≤ 𝑘)
132	128, 131	nsyl 140	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → ¬ 𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0})
133		fveq2 6892	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 𝑘 → (𝐴‘𝑛) = (𝐴‘𝑘))
134	133	neeq1d 2990	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑘 → ((𝐴‘𝑛) ≠ 0 ↔ (𝐴‘𝑘) ≠ 0))
135	134	elrab3 3683	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ℕ → (𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ↔ (𝐴‘𝑘) ≠ 0))
136	118, 135	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → (𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ↔ (𝐴‘𝑘) ≠ 0))
137	136	necon2bbid 2974	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → ((𝐴‘𝑘) = 0 ↔ ¬ 𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0}))
138	132, 137	mpbird 256	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → (𝐴‘𝑘) = 0)
139	138	oveq1d 7430	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → ((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = (0 · ((𝑇 · 𝑋)↑𝑘)))
140	117	nnnn0d 12577	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ (1...(𝐾 − 1)) → 𝑘 ∈ ℕ0)
141	16, 140, 50	syl2an 594	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → ((𝑇 · 𝑋)↑𝑘) ∈ ℂ)
142	141	mul02d 11452	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → (0 · ((𝑇 · 𝑋)↑𝑘)) = 0)
143	139, 142	eqtrd 2766	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → ((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = 0)
144	143	sumeq2dv 15701	. . . . . . . . . . . 12 ⊢ (𝜑 → Σ𝑘 ∈ (1...(𝐾 − 1))((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = Σ𝑘 ∈ (1...(𝐾 − 1))0)
145		fzfi 13985	. . . . . . . . . . . . . 14 ⊢ (1...(𝐾 − 1)) ∈ Fin
146	145	olci 864	. . . . . . . . . . . . 13 ⊢ ((1...(𝐾 − 1)) ⊆ (ℤ≥‘1) ∨ (1...(𝐾 − 1)) ∈ Fin)
147		sumz 15720	. . . . . . . . . . . . 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 2782	. . . . . . . . . . 11 ⊢ (𝜑 → Σ𝑘 ∈ (1...(𝐾 − 1))((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = 0)
150	12, 15, 27	mulexpd 14173	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑇 · 𝑋)↑𝐾) = ((𝑇↑𝐾) · (𝑋↑𝐾)))
151	150	oveq2d 7431	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐴‘𝐾) · ((𝑇 · 𝑋)↑𝐾)) = ((𝐴‘𝐾) · ((𝑇↑𝐾) · (𝑋↑𝐾))))
152	33, 27	ffvelcdmd 7090	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐴‘𝐾) ∈ ℂ)
153	12, 27	expcld 14158	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑇↑𝐾) ∈ ℂ)
154	28	recnd 11282	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑋↑𝐾) ∈ ℂ)
155	152, 153, 154	mulassd 11277	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐴‘𝐾) · (𝑇↑𝐾)) · (𝑋↑𝐾)) = ((𝐴‘𝐾) · ((𝑇↑𝐾) · (𝑋↑𝐾))))
156	151, 155	eqtr4d 2769	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐴‘𝐾) · ((𝑇 · 𝑋)↑𝐾)) = (((𝐴‘𝐾) · (𝑇↑𝐾)) · (𝑋↑𝐾)))
157	7	oveq1i 7425	. . . . . . . . . . . . . . . 16 ⊢ (𝑇↑𝐾) = ((-((𝐹‘0) / (𝐴‘𝐾))↑𝑐(1 / 𝐾))↑𝐾)
158	57	recnd 11282	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐾 ∈ ℂ)
159	26	nnne0d 12307	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐾 ≠ 0)
160	158, 159	recid2d 12030	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((1 / 𝐾) · 𝐾) = 1)
161	160	oveq2d 7431	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (-((𝐹‘0) / (𝐴‘𝐾))↑𝑐((1 / 𝐾) · 𝐾)) = (-((𝐹‘0) / (𝐴‘𝐾))↑𝑐1))
162	25	simprd 494	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐴‘𝐾) ≠ 0)
163	23, 152, 162	divcld 12034	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐹‘0) / (𝐴‘𝐾)) ∈ ℂ)
164	163	negcld 11598	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → -((𝐹‘0) / (𝐴‘𝐾)) ∈ ℂ)
165	26	nnrecred 12308	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (1 / 𝐾) ∈ ℝ)
166	165	recnd 11282	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (1 / 𝐾) ∈ ℂ)
167	164, 166, 27	cxpmul2d 26732	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (-((𝐹‘0) / (𝐴‘𝐾))↑𝑐((1 / 𝐾) · 𝐾)) = ((-((𝐹‘0) / (𝐴‘𝐾))↑𝑐(1 / 𝐾))↑𝐾))
168	164	cxp1d 26729	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (-((𝐹‘0) / (𝐴‘𝐾))↑𝑐1) = -((𝐹‘0) / (𝐴‘𝐾)))
169	161, 167, 168	3eqtr3d 2774	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((-((𝐹‘0) / (𝐴‘𝐾))↑𝑐(1 / 𝐾))↑𝐾) = -((𝐹‘0) / (𝐴‘𝐾)))
170	157, 169	eqtrid 2778	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑇↑𝐾) = -((𝐹‘0) / (𝐴‘𝐾)))
171	170	oveq2d 7431	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐴‘𝐾) · (𝑇↑𝐾)) = ((𝐴‘𝐾) · -((𝐹‘0) / (𝐴‘𝐾))))
172	152, 163	mulneg2d 11708	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐴‘𝐾) · -((𝐹‘0) / (𝐴‘𝐾))) = -((𝐴‘𝐾) · ((𝐹‘0) / (𝐴‘𝐾))))
173	23, 152, 162	divcan2d 12036	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐴‘𝐾) · ((𝐹‘0) / (𝐴‘𝐾))) = (𝐹‘0))
174	173	negeqd 11494	. . . . . . . . . . . . . 14 ⊢ (𝜑 → -((𝐴‘𝐾) · ((𝐹‘0) / (𝐴‘𝐾))) = -(𝐹‘0))
175	171, 172, 174	3eqtrd 2770	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐴‘𝐾) · (𝑇↑𝐾)) = -(𝐹‘0))
176	175	oveq1d 7430	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐴‘𝐾) · (𝑇↑𝐾)) · (𝑋↑𝐾)) = (-(𝐹‘0) · (𝑋↑𝐾)))
177	23, 154	mulneg1d 11707	. . . . . . . . . . . 12 ⊢ (𝜑 → (-(𝐹‘0) · (𝑋↑𝐾)) = -((𝐹‘0) · (𝑋↑𝐾)))
178	156, 176, 177	3eqtrd 2770	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴‘𝐾) · ((𝑇 · 𝑋)↑𝐾)) = -((𝐹‘0) · (𝑋↑𝐾)))
179	149, 178	oveq12d 7433	. . . . . . . . . 10 ⊢ (𝜑 → (Σ𝑘 ∈ (1...(𝐾 − 1))((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) + ((𝐴‘𝐾) · ((𝑇 · 𝑋)↑𝐾))) = (0 + -((𝐹‘0) · (𝑋↑𝐾))))
180	23, 154	mulcld 11274	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐹‘0) · (𝑋↑𝐾)) ∈ ℂ)
181	180	negcld 11598	. . . . . . . . . . 11 ⊢ (𝜑 → -((𝐹‘0) · (𝑋↑𝐾)) ∈ ℂ)
182	181	addlidd 11455	. . . . . . . . . 10 ⊢ (𝜑 → (0 + -((𝐹‘0) · (𝑋↑𝐾))) = -((𝐹‘0) · (𝑋↑𝐾)))
183	116, 179, 182	3eqtrd 2770	. . . . . . . . 9 ⊢ (𝜑 → Σ𝑘 ∈ ((0 + 1)...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = -((𝐹‘0) · (𝑋↑𝐾)))
184	102, 183	oveq12d 7433	. . . . . . . 8 ⊢ (𝜑 → (((𝐴‘0) · ((𝑇 · 𝑋)↑0)) + Σ𝑘 ∈ ((0 + 1)...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) = ((𝐹‘0) + -((𝐹‘0) · (𝑋↑𝐾))))
185		fveq2 6892	. . . . . . . . . 10 ⊢ (𝑘 = 0 → (𝐴‘𝑘) = (𝐴‘0))
186		oveq2 7423	. . . . . . . . . 10 ⊢ (𝑘 = 0 → ((𝑇 · 𝑋)↑𝑘) = ((𝑇 · 𝑋)↑0))
187	185, 186	oveq12d 7433	. . . . . . . . 9 ⊢ (𝑘 = 0 → ((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = ((𝐴‘0) · ((𝑇 · 𝑋)↑0)))
188	81, 52, 187	fsum1p 15751	. . . . . . . 8 ⊢ (𝜑 → Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = (((𝐴‘0) · ((𝑇 · 𝑋)↑0)) + Σ𝑘 ∈ ((0 + 1)...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))))
189	101	oveq1d 7430	. . . . . . . . 9 ⊢ (𝜑 → (((𝐹‘0) · 1) − ((𝐹‘0) · (𝑋↑𝐾))) = ((𝐹‘0) − ((𝐹‘0) · (𝑋↑𝐾))))
190		1cnd 11249	. . . . . . . . . 10 ⊢ (𝜑 → 1 ∈ ℂ)
191	23, 190, 154	subdid 11710	. . . . . . . . 9 ⊢ (𝜑 → ((𝐹‘0) · (1 − (𝑋↑𝐾))) = (((𝐹‘0) · 1) − ((𝐹‘0) · (𝑋↑𝐾))))
192	23, 180	negsubd 11617	. . . . . . . . 9 ⊢ (𝜑 → ((𝐹‘0) + -((𝐹‘0) · (𝑋↑𝐾))) = ((𝐹‘0) − ((𝐹‘0) · (𝑋↑𝐾))))
193	189, 191, 192	3eqtr4d 2776	. . . . . . . 8 ⊢ (𝜑 → ((𝐹‘0) · (1 − (𝑋↑𝐾))) = ((𝐹‘0) + -((𝐹‘0) · (𝑋↑𝐾))))
194	184, 188, 193	3eqtr4d 2776	. . . . . . 7 ⊢ (𝜑 → Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = ((𝐹‘0) · (1 − (𝑋↑𝐾))))
195	194	fveq2d 6896	. . . . . 6 ⊢ (𝜑 → (abs‘Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) = (abs‘((𝐹‘0) · (1 − (𝑋↑𝐾)))))
196		1re 11254	. . . . . . . . 9 ⊢ 1 ∈ ℝ
197		resubcl 11564	. . . . . . . . 9 ⊢ ((1 ∈ ℝ ∧ (𝑋↑𝐾) ∈ ℝ) → (1 − (𝑋↑𝐾)) ∈ ℝ)
198	196, 28, 197	sylancr 585	. . . . . . . 8 ⊢ (𝜑 → (1 − (𝑋↑𝐾)) ∈ ℝ)
199	198	recnd 11282	. . . . . . 7 ⊢ (𝜑 → (1 − (𝑋↑𝐾)) ∈ ℂ)
200	23, 199	absmuld 15453	. . . . . 6 ⊢ (𝜑 → (abs‘((𝐹‘0) · (1 − (𝑋↑𝐾)))) = ((abs‘(𝐹‘0)) · (abs‘(1 − (𝑋↑𝐾)))))
201	13	rpge0d 13067	. . . . . . . . . . 11 ⊢ (𝜑 → 0 ≤ 𝑋)
202	11	simp2d 1140	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑈 ∈ ℝ+)
203	202	rpred 13063	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑈 ∈ ℝ)
204		min1 13215	. . . . . . . . . . . . 13 ⊢ ((1 ∈ ℝ ∧ 𝑈 ∈ ℝ) → if(1 ≤ 𝑈, 1, 𝑈) ≤ 1)
205	196, 203, 204	sylancr 585	. . . . . . . . . . . 12 ⊢ (𝜑 → if(1 ≤ 𝑈, 1, 𝑈) ≤ 1)
206	9, 205	eqbrtrid 5180	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑋 ≤ 1)
207		exple1 14188	. . . . . . . . . . 11 ⊢ (((𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ∧ 𝑋 ≤ 1) ∧ 𝐾 ∈ ℕ0) → (𝑋↑𝐾) ≤ 1)
208	14, 201, 206, 27, 207	syl31anc 1370	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋↑𝐾) ≤ 1)
209		subge0 11767	. . . . . . . . . . 11 ⊢ ((1 ∈ ℝ ∧ (𝑋↑𝐾) ∈ ℝ) → (0 ≤ (1 − (𝑋↑𝐾)) ↔ (𝑋↑𝐾) ≤ 1))
210	196, 28, 209	sylancr 585	. . . . . . . . . 10 ⊢ (𝜑 → (0 ≤ (1 − (𝑋↑𝐾)) ↔ (𝑋↑𝐾) ≤ 1))
211	208, 210	mpbird 256	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ (1 − (𝑋↑𝐾)))
212	198, 211	absidd 15421	. . . . . . . 8 ⊢ (𝜑 → (abs‘(1 − (𝑋↑𝐾))) = (1 − (𝑋↑𝐾)))
213	212	oveq2d 7431	. . . . . . 7 ⊢ (𝜑 → ((abs‘(𝐹‘0)) · (abs‘(1 − (𝑋↑𝐾)))) = ((abs‘(𝐹‘0)) · (1 − (𝑋↑𝐾))))
214	24	recnd 11282	. . . . . . . 8 ⊢ (𝜑 → (abs‘(𝐹‘0)) ∈ ℂ)
215	214, 190, 154	subdid 11710	. . . . . . 7 ⊢ (𝜑 → ((abs‘(𝐹‘0)) · (1 − (𝑋↑𝐾))) = (((abs‘(𝐹‘0)) · 1) − ((abs‘(𝐹‘0)) · (𝑋↑𝐾))))
216	214	mulridd 11271	. . . . . . . 8 ⊢ (𝜑 → ((abs‘(𝐹‘0)) · 1) = (abs‘(𝐹‘0)))
217	216	oveq1d 7430	. . . . . . 7 ⊢ (𝜑 → (((abs‘(𝐹‘0)) · 1) − ((abs‘(𝐹‘0)) · (𝑋↑𝐾))) = ((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋↑𝐾))))
218	213, 215, 217	3eqtrd 2770	. . . . . 6 ⊢ (𝜑 → ((abs‘(𝐹‘0)) · (abs‘(1 − (𝑋↑𝐾)))) = ((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋↑𝐾))))
219	195, 200, 218	3eqtrrd 2771	. . . . 5 ⊢ (𝜑 → ((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋↑𝐾))) = (abs‘Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))))
220	219	oveq1d 7430	. . . 4 ⊢ (𝜑 → (((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋↑𝐾))) + (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))) = ((abs‘Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) + (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))))
221	54, 95, 220	3brtr4d 5177	. . 3 ⊢ (𝜑 → (abs‘(𝐹‘(𝑇 · 𝑋))) ≤ (((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋↑𝐾))) + (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))))
222	43	abscld 15435	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) ∈ ℝ)
223	31, 222	fsumrecl 15732	. . . . . 6 ⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) ∈ ℝ)
224	31, 43	fsumabs 15799	. . . . . 6 ⊢ (𝜑 → (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) ≤ Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))))
225		expcl 14092	. . . . . . . . . . . 12 ⊢ ((𝑇 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (𝑇↑𝑘) ∈ ℂ)
226	12, 38, 225	syl2an2r 683	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑇↑𝑘) ∈ ℂ)
227	40, 226	mulcld 11274	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((𝐴‘𝑘) · (𝑇↑𝑘)) ∈ ℂ)
228	227	abscld 15435	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) ∈ ℝ)
229	31, 228	fsumrecl 15732	. . . . . . . 8 ⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) ∈ ℝ)
230	14, 35	reexpcld 14175	. . . . . . . 8 ⊢ (𝜑 → (𝑋↑(𝐾 + 1)) ∈ ℝ)
231	229, 230	remulcld 11284	. . . . . . 7 ⊢ (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1))) ∈ ℝ)
232	230	adantr 479	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑋↑(𝐾 + 1)) ∈ ℝ)
233	228, 232	remulcld 11284	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1))) ∈ ℝ)
234	12	adantr 479	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑇 ∈ ℂ)
235	15	adantr 479	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑋 ∈ ℂ)
236	234, 235, 38	mulexpd 14173	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((𝑇 · 𝑋)↑𝑘) = ((𝑇↑𝑘) · (𝑋↑𝑘)))
237	236	oveq2d 7431	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = ((𝐴‘𝑘) · ((𝑇↑𝑘) · (𝑋↑𝑘))))
238	14	adantr 479	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑋 ∈ ℝ)
239	238, 38	reexpcld 14175	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑋↑𝑘) ∈ ℝ)
240	239	recnd 11282	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑋↑𝑘) ∈ ℂ)
241	40, 226, 240	mulassd 11277	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (((𝐴‘𝑘) · (𝑇↑𝑘)) · (𝑋↑𝑘)) = ((𝐴‘𝑘) · ((𝑇↑𝑘) · (𝑋↑𝑘))))
242	237, 241	eqtr4d 2769	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = (((𝐴‘𝑘) · (𝑇↑𝑘)) · (𝑋↑𝑘)))
243	242	fveq2d 6896	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) = (abs‘(((𝐴‘𝑘) · (𝑇↑𝑘)) · (𝑋↑𝑘))))
244	227, 240	absmuld 15453	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘(((𝐴‘𝑘) · (𝑇↑𝑘)) · (𝑋↑𝑘))) = ((abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (abs‘(𝑋↑𝑘))))
245		elfzelz 13548	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ((𝐾 + 1)...𝑁) → 𝑘 ∈ ℤ)
246		rpexpcl 14093	. . . . . . . . . . . . . . 15 ⊢ ((𝑋 ∈ ℝ+ ∧ 𝑘 ∈ ℤ) → (𝑋↑𝑘) ∈ ℝ+)
247	13, 245, 246	syl2an 594	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑋↑𝑘) ∈ ℝ+)
248	247	rpge0d 13067	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 0 ≤ (𝑋↑𝑘))
249	239, 248	absidd 15421	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘(𝑋↑𝑘)) = (𝑋↑𝑘))
250	249	oveq2d 7431	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (abs‘(𝑋↑𝑘))) = ((abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑𝑘)))
251	243, 244, 250	3eqtrd 2770	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) = ((abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑𝑘)))
252	227	absge0d 15443	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 0 ≤ (abs‘((𝐴‘𝑘) · (𝑇↑𝑘))))
253	35	adantr 479	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝐾 + 1) ∈ ℕ0)
254	36	adantl 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑘 ∈ (ℤ≥‘(𝐾 + 1)))
255	201	adantr 479	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 0 ≤ 𝑋)
256	206	adantr 479	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑋 ≤ 1)
257	238, 253, 254, 255, 256	leexp2rd 14266	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑋↑𝑘) ≤ (𝑋↑(𝐾 + 1)))
258	239, 232, 228, 252, 257	lemul2ad 12199	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑𝑘)) ≤ ((abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1))))
259	251, 258	eqbrtrd 5167	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) ≤ ((abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1))))
260	31, 222, 233, 259	fsumle 15797	. . . . . . . 8 ⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) ≤ Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1))))
261	230	recnd 11282	. . . . . . . . 9 ⊢ (𝜑 → (𝑋↑(𝐾 + 1)) ∈ ℂ)
262	228	recnd 11282	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) ∈ ℂ)
263	31, 261, 262	fsummulc1 15783	. . . . . . . 8 ⊢ (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1))) = Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1))))
264	260, 263	breqtrrd 5173	. . . . . . 7 ⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) ≤ (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1))))
265	15, 27	expp1d 14159	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑋↑(𝐾 + 1)) = ((𝑋↑𝐾) · 𝑋))
266	154, 15	mulcomd 11275	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑋↑𝐾) · 𝑋) = (𝑋 · (𝑋↑𝐾)))
267	265, 266	eqtrd 2766	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋↑(𝐾 + 1)) = (𝑋 · (𝑋↑𝐾)))
268	267	oveq2d 7431	. . . . . . . . 9 ⊢ (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1))) = (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋 · (𝑋↑𝐾))))
269	229	recnd 11282	. . . . . . . . . 10 ⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) ∈ ℂ)
270	269, 15, 154	mulassd 11277	. . . . . . . . 9 ⊢ (𝜑 → ((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · 𝑋) · (𝑋↑𝐾)) = (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋 · (𝑋↑𝐾))))
271	268, 270	eqtr4d 2769	. . . . . . . 8 ⊢ (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1))) = ((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · 𝑋) · (𝑋↑𝐾)))
272	229, 14	remulcld 11284	. . . . . . . . 9 ⊢ (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · 𝑋) ∈ ℝ)
273		nnssz 12625	. . . . . . . . . . . 12 ⊢ ℕ ⊆ ℤ
274	61, 273	sstri 3990	. . . . . . . . . . 11 ⊢ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ⊆ ℤ
275	76	ne0d 4337	. . . . . . . . . . . . 13 ⊢ (𝜑 → {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ≠ ∅)
276		infssuzcl 12961	. . . . . . . . . . . . 13 ⊢ (({𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ⊆ (ℤ≥‘1) ∧ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ≠ ∅) → inf({𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0}, ℝ, < ) ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0})
277	63, 275, 276	sylancr 585	. . . . . . . . . . . 12 ⊢ (𝜑 → inf({𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0}, ℝ, < ) ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0})
278	6, 277	eqeltrid 2830	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐾 ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0})
279	274, 278	sselid 3978	. . . . . . . . . 10 ⊢ (𝜑 → 𝐾 ∈ ℤ)
280	13, 279	rpexpcld 14258	. . . . . . . . 9 ⊢ (𝜑 → (𝑋↑𝐾) ∈ ℝ+)
281		peano2re 11427	. . . . . . . . . . . 12 ⊢ (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) ∈ ℝ → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1) ∈ ℝ)
282	229, 281	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1) ∈ ℝ)
283	282, 14	remulcld 11284	. . . . . . . . . 10 ⊢ (𝜑 → ((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1) · 𝑋) ∈ ℝ)
284	229	ltp1d 12189	. . . . . . . . . . 11 ⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) < (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1))
285	229, 282, 13, 284	ltmul1dd 13118	. . . . . . . . . 10 ⊢ (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · 𝑋) < ((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1) · 𝑋))
286		min2 13216	. . . . . . . . . . . . . 14 ⊢ ((1 ∈ ℝ ∧ 𝑈 ∈ ℝ) → if(1 ≤ 𝑈, 1, 𝑈) ≤ 𝑈)
287	196, 203, 286	sylancr 585	. . . . . . . . . . . . 13 ⊢ (𝜑 → if(1 ≤ 𝑈, 1, 𝑈) ≤ 𝑈)
288	9, 287	eqbrtrid 5180	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑋 ≤ 𝑈)
289	288, 8	breqtrdi 5186	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑋 ≤ ((abs‘(𝐹‘0)) / (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1)))
290		0red 11257	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 ∈ ℝ)
291	31, 228, 252	fsumge0 15793	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 ≤ Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))))
292	290, 229, 282, 291, 284	lelttrd 11412	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 < (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1))
293		lemuldiv2 12140	. . . . . . . . . . . 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 1371	. . . . . . . . . . 11 ⊢ (𝜑 → (((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1) · 𝑋) ≤ (abs‘(𝐹‘0)) ↔ 𝑋 ≤ ((abs‘(𝐹‘0)) / (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1))))
295	289, 294	mpbird 256	. . . . . . . . . 10 ⊢ (𝜑 → ((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1) · 𝑋) ≤ (abs‘(𝐹‘0)))
296	272, 283, 24, 285, 295	ltletrd 11414	. . . . . . . . 9 ⊢ (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · 𝑋) < (abs‘(𝐹‘0)))
297	272, 24, 280, 296	ltmul1dd 13118	. . . . . . . 8 ⊢ (𝜑 → ((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · 𝑋) · (𝑋↑𝐾)) < ((abs‘(𝐹‘0)) · (𝑋↑𝐾)))
298	271, 297	eqbrtrd 5167	. . . . . . 7 ⊢ (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1))) < ((abs‘(𝐹‘0)) · (𝑋↑𝐾)))
299	223, 231, 29, 264, 298	lelttrd 11412	. . . . . 6 ⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) < ((abs‘(𝐹‘0)) · (𝑋↑𝐾)))
300	45, 223, 29, 224, 299	lelttrd 11412	. . . . 5 ⊢ (𝜑 → (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) < ((abs‘(𝐹‘0)) · (𝑋↑𝐾)))
301	45, 29, 24, 300	ltsub2dd 11867	. . . 4 ⊢ (𝜑 → ((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋↑𝐾))) < ((abs‘(𝐹‘0)) − (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))))
302	30, 45, 24	ltaddsubd 11854	. . . 4 ⊢ (𝜑 → ((((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋↑𝐾))) + (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))) < (abs‘(𝐹‘0)) ↔ ((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋↑𝐾))) < ((abs‘(𝐹‘0)) − (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))))))
303	301, 302	mpbird 256	. . 3 ⊢ (𝜑 → (((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋↑𝐾))) + (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))) < (abs‘(𝐹‘0)))
304	20, 46, 24, 221, 303	lelttrd 11412	. 2 ⊢ (𝜑 → (abs‘(𝐹‘(𝑇 · 𝑋))) < (abs‘(𝐹‘0)))
305		2fveq3 6897	. . . 4 ⊢ (𝑥 = (𝑇 · 𝑋) → (abs‘(𝐹‘𝑥)) = (abs‘(𝐹‘(𝑇 · 𝑋))))
306	305	breq1d 5155	. . 3 ⊢ (𝑥 = (𝑇 · 𝑋) → ((abs‘(𝐹‘𝑥)) < (abs‘(𝐹‘0)) ↔ (abs‘(𝐹‘(𝑇 · 𝑋))) < (abs‘(𝐹‘0))))
307	306	rspcev 3609	. 2 ⊢ (((𝑇 · 𝑋) ∈ ℂ ∧ (abs‘(𝐹‘(𝑇 · 𝑋))) < (abs‘(𝐹‘0))) → ∃𝑥 ∈ ℂ (abs‘(𝐹‘𝑥)) < (abs‘(𝐹‘0)))
308	16, 304, 307	syl2anc 582	1 ⊢ (𝜑 → ∃𝑥 ∈ ℂ (abs‘(𝐹‘𝑥)) < (abs‘(𝐹‘0)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 394   ∨ wo 845   ∧ w3a 1084   = wceq 1534   ∈ wcel 2099   ≠ wne 2930  ∃wrex 3060  {crab 3420   ∪ cun 3946   ∩ cin 3947   ⊆ wss 3948  ∅c0 4324  ifcif 4525   class class class wbr 5145  ⟶wf 6541  ‘cfv 6545  (class class class)co 7415  Fincfn 8965  infcinf 9476  ℂcc 11146  ℝcr 11147  0cc0 11148  1c1 11149   + caddc 11151   · cmul 11153   < clt 11288   ≤ cle 11289   − cmin 11484  -cneg 11485   / cdiv 11911  ℕcn 12257  ℕ₀cn0 12517  ℤcz 12603  ℤ_≥cuz 12867  ℝ⁺crp 13021  ...cfz 13531  ↑cexp 14074  abscabs 15233  Σcsu 15684  0_𝑝c0p 25685  Polycply 26207  coeffccoe 26209  degcdgr 26210  ↑_𝑐ccxp 26578

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-rep 5282  ax-sep 5296  ax-nul 5303  ax-pow 5361  ax-pr 5425  ax-un 7737  ax-inf2 9676  ax-cnex 11204  ax-resscn 11205  ax-1cn 11206  ax-icn 11207  ax-addcl 11208  ax-addrcl 11209  ax-mulcl 11210  ax-mulrcl 11211  ax-mulcom 11212  ax-addass 11213  ax-mulass 11214  ax-distr 11215  ax-i2m1 11216  ax-1ne0 11217  ax-1rid 11218  ax-rnegex 11219  ax-rrecex 11220  ax-cnre 11221  ax-pre-lttri 11222  ax-pre-lttrn 11223  ax-pre-ltadd 11224  ax-pre-mulgt0 11225  ax-pre-sup 11226  ax-addf 11227

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3365  df-reu 3366  df-rab 3421  df-v 3466  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3968  df-nul 4325  df-if 4526  df-pw 4601  df-sn 4626  df-pr 4628  df-tp 4630  df-op 4632  df-uni 4908  df-int 4949  df-iun 4997  df-iin 4998  df-br 5146  df-opab 5208  df-mpt 5229  df-tr 5263  df-id 5572  df-eprel 5578  df-po 5586  df-so 5587  df-fr 5629  df-se 5630  df-we 5631  df-xp 5680  df-rel 5681  df-cnv 5682  df-co 5683  df-dm 5684  df-rn 5685  df-res 5686  df-ima 5687  df-pred 6304  df-ord 6370  df-on 6371  df-lim 6372  df-suc 6373  df-iota 6497  df-fun 6547  df-fn 6548  df-f 6549  df-f1 6550  df-fo 6551  df-f1o 6552  df-fv 6553  df-isom 6554  df-riota 7371  df-ov 7418  df-oprab 7419  df-mpo 7420  df-of 7681  df-om 7868  df-1st 7994  df-2nd 7995  df-supp 8166  df-frecs 8287  df-wrecs 8318  df-recs 8392  df-rdg 8431  df-1o 8487  df-2o 8488  df-er 8725  df-map 8848  df-pm 8849  df-ixp 8918  df-en 8966  df-dom 8967  df-sdom 8968  df-fin 8969  df-fsupp 9398  df-fi 9446  df-sup 9477  df-inf 9478  df-oi 9545  df-card 9974  df-pnf 11290  df-mnf 11291  df-xr 11292  df-ltxr 11293  df-le 11294  df-sub 11486  df-neg 11487  df-div 11912  df-nn 12258  df-2 12320  df-3 12321  df-4 12322  df-5 12323  df-6 12324  df-7 12325  df-8 12326  df-9 12327  df-n0 12518  df-z 12604  df-dec 12723  df-uz 12868  df-q 12978  df-rp 13022  df-xneg 13139  df-xadd 13140  df-xmul 13141  df-ioo 13375  df-ioc 13376  df-ico 13377  df-icc 13378  df-fz 13532  df-fzo 13675  df-fl 13805  df-mod 13883  df-seq 14015  df-exp 14075  df-fac 14285  df-bc 14314  df-hash 14342  df-shft 15066  df-cj 15098  df-re 15099  df-im 15100  df-sqrt 15234  df-abs 15235  df-limsup 15467  df-clim 15484  df-rlim 15485  df-sum 15685  df-ef 16063  df-sin 16065  df-cos 16066  df-pi 16068  df-struct 17143  df-sets 17160  df-slot 17178  df-ndx 17190  df-base 17208  df-ress 17237  df-plusg 17273  df-mulr 17274  df-starv 17275  df-sca 17276  df-vsca 17277  df-ip 17278  df-tset 17279  df-ple 17280  df-ds 17282  df-unif 17283  df-hom 17284  df-cco 17285  df-rest 17431  df-topn 17432  df-0g 17450  df-gsum 17451  df-topgen 17452  df-pt 17453  df-prds 17456  df-xrs 17511  df-qtop 17516  df-imas 17517  df-xps 17519  df-mre 17593  df-mrc 17594  df-acs 17596  df-mgm 18627  df-sgrp 18706  df-mnd 18722  df-submnd 18768  df-mulg 19057  df-cntz 19306  df-cmn 19775  df-psmet 21330  df-xmet 21331  df-met 21332  df-bl 21333  df-mopn 21334  df-fbas 21335  df-fg 21336  df-cnfld 21339  df-top 22883  df-topon 22900  df-topsp 22922  df-bases 22936  df-cld 23010  df-ntr 23011  df-cls 23012  df-nei 23089  df-lp 23127  df-perf 23128  df-cn 23218  df-cnp 23219  df-haus 23306  df-tx 23553  df-hmeo 23746  df-fil 23837  df-fm 23929  df-flim 23930  df-flf 23931  df-xms 24313  df-ms 24314  df-tms 24315  df-cncf 24885  df-0p 25686  df-limc 25882  df-dv 25883  df-ply 26211  df-coe 26213  df-dgr 26214  df-log 26579  df-cxp 26580

This theorem is referenced by:  ftalem6  27102