ftalem5 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > ftalem5		Structured version Visualization version GIF version

Theorem ftalem5 26571

Description: Lemma for fta 26574: Main proof. We have already shifted the minimum found in ftalem3 26569 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 26570	. . . . 5 ⊢ (𝜑 → ((𝐾 ∈ ℕ ∧ (𝐴‘𝐾) ≠ 0) ∧ (𝑇 ∈ ℂ ∧ 𝑈 ∈ ℝ⁺ ∧ 𝑋 ∈ ℝ⁺)))
11	10	simprd 497	. . . 4 ⊢ (𝜑 → (𝑇 ∈ ℂ ∧ 𝑈 ∈ ℝ⁺ ∧ 𝑋 ∈ ℝ⁺))
12	11	simp1d 1143	. . 3 ⊢ (𝜑 → 𝑇 ∈ ℂ)
13	11	simp3d 1145	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ ℝ⁺)
14	13	rpred 13013	. . . 4 ⊢ (𝜑 → 𝑋 ∈ ℝ)
15	14	recnd 11239	. . 3 ⊢ (𝜑 → 𝑋 ∈ ℂ)
16	12, 15	mulcld 11231	. 2 ⊢ (𝜑 → (𝑇 · 𝑋) ∈ ℂ)
17		plyf 25704	. . . . . 6 ⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐹:ℂ⟶ℂ)
18	3, 17	syl 17	. . . . 5 ⊢ (𝜑 → 𝐹:ℂ⟶ℂ)
19	18, 16	ffvelcdmd 7085	. . . 4 ⊢ (𝜑 → (𝐹‘(𝑇 · 𝑋)) ∈ ℂ)
20	19	abscld 15380	. . 3 ⊢ (𝜑 → (abs‘(𝐹‘(𝑇 · 𝑋))) ∈ ℝ)
21		0cn 11203	. . . . . . 7 ⊢ 0 ∈ ℂ
22		ffvelcdm 7081	. . . . . . 7 ⊢ ((𝐹:ℂ⟶ℂ ∧ 0 ∈ ℂ) → (𝐹‘0) ∈ ℂ)
23	18, 21, 22	sylancl 587	. . . . . 6 ⊢ (𝜑 → (𝐹‘0) ∈ ℂ)
24	23	abscld 15380	. . . . 5 ⊢ (𝜑 → (abs‘(𝐹‘0)) ∈ ℝ)
25	10	simpld 496	. . . . . . . . 9 ⊢ (𝜑 → (𝐾 ∈ ℕ ∧ (𝐴‘𝐾) ≠ 0))
26	25	simpld 496	. . . . . . . 8 ⊢ (𝜑 → 𝐾 ∈ ℕ)
27	26	nnnn0d 12529	. . . . . . 7 ⊢ (𝜑 → 𝐾 ∈ ℕ₀)
28	14, 27	reexpcld 14125	. . . . . 6 ⊢ (𝜑 → (𝑋↑𝐾) ∈ ℝ)
29	24, 28	remulcld 11241	. . . . 5 ⊢ (𝜑 → ((abs‘(𝐹‘0)) · (𝑋↑𝐾)) ∈ ℝ)
30	24, 29	resubcld 11639	. . . 4 ⊢ (𝜑 → ((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋↑𝐾))) ∈ ℝ)
31		fzfid 13935	. . . . . 6 ⊢ (𝜑 → ((𝐾 + 1)...𝑁) ∈ Fin)
32	1	coef3 25738	. . . . . . . . 9 ⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐴:ℕ₀⟶ℂ)
33	3, 32	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐴:ℕ₀⟶ℂ)
34		peano2nn0 12509	. . . . . . . . . 10 ⊢ (𝐾 ∈ ℕ₀ → (𝐾 + 1) ∈ ℕ₀)
35	27, 34	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝐾 + 1) ∈ ℕ₀)
36		elfzuz 13494	. . . . . . . . 9 ⊢ (𝑘 ∈ ((𝐾 + 1)...𝑁) → 𝑘 ∈ (ℤ_≥‘(𝐾 + 1)))
37		eluznn0 12898	. . . . . . . . 9 ⊢ (((𝐾 + 1) ∈ ℕ₀ ∧ 𝑘 ∈ (ℤ_≥‘(𝐾 + 1))) → 𝑘 ∈ ℕ₀)
38	35, 36, 37	syl2an 597	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑘 ∈ ℕ₀)
39		ffvelcdm 7081	. . . . . . . 8 ⊢ ((𝐴:ℕ₀⟶ℂ ∧ 𝑘 ∈ ℕ₀) → (𝐴‘𝑘) ∈ ℂ)
40	33, 38, 39	syl2an2r 684	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝐴‘𝑘) ∈ ℂ)
41	16	adantr 482	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑇 · 𝑋) ∈ ℂ)
42	41, 38	expcld 14108	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((𝑇 · 𝑋)↑𝑘) ∈ ℂ)
43	40, 42	mulcld 11231	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) ∈ ℂ)
44	31, 43	fsumcl 15676	. . . . 5 ⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) ∈ ℂ)
45	44	abscld 15380	. . . 4 ⊢ (𝜑 → (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) ∈ ℝ)
46	30, 45	readdcld 11240	. . 3 ⊢ (𝜑 → (((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋↑𝐾))) + (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))) ∈ ℝ)
47		fzfid 13935	. . . . . 6 ⊢ (𝜑 → (0...𝐾) ∈ Fin)
48		elfznn0 13591	. . . . . . . 8 ⊢ (𝑘 ∈ (0...𝐾) → 𝑘 ∈ ℕ₀)
49	33, 48, 39	syl2an 597	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐾)) → (𝐴‘𝑘) ∈ ℂ)
50		expcl 14042	. . . . . . . 8 ⊢ (((𝑇 · 𝑋) ∈ ℂ ∧ 𝑘 ∈ ℕ₀) → ((𝑇 · 𝑋)↑𝑘) ∈ ℂ)
51	16, 48, 50	syl2an 597	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐾)) → ((𝑇 · 𝑋)↑𝑘) ∈ ℂ)
52	49, 51	mulcld 11231	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐾)) → ((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) ∈ ℂ)
53	47, 52	fsumcl 15676	. . . . 5 ⊢ (𝜑 → Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) ∈ ℂ)
54	53, 44	abstrid 15400	. . . 4 ⊢ (𝜑 → (abs‘(Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) + Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))) ≤ ((abs‘Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) + (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))))
55	1, 2	coeid2 25745	. . . . . . 7 ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (𝑇 · 𝑋) ∈ ℂ) → (𝐹‘(𝑇 · 𝑋)) = Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))
56	3, 16, 55	syl2anc 585	. . . . . 6 ⊢ (𝜑 → (𝐹‘(𝑇 · 𝑋)) = Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))
57	26	nnred 12224	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ∈ ℝ)
58	57	ltp1d 12141	. . . . . . . 8 ⊢ (𝜑 → 𝐾 < (𝐾 + 1))
59		fzdisj 13525	. . . . . . . 8 ⊢ (𝐾 < (𝐾 + 1) → ((0...𝐾) ∩ ((𝐾 + 1)...𝑁)) = ∅)
60	58, 59	syl 17	. . . . . . 7 ⊢ (𝜑 → ((0...𝐾) ∩ ((𝐾 + 1)...𝑁)) = ∅)
61		ssrab2 4077	. . . . . . . . . . . 12 ⊢ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ⊆ ℕ
62		nnuz 12862	. . . . . . . . . . . 12 ⊢ ℕ = (ℤ_≥‘1)
63	61, 62	sseqtri 4018	. . . . . . . . . . 11 ⊢ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ⊆ (ℤ_≥‘1)
64		fveq2 6889	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑁 → (𝐴‘𝑛) = (𝐴‘𝑁))
65	64	neeq1d 3001	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑁 → ((𝐴‘𝑛) ≠ 0 ↔ (𝐴‘𝑁) ≠ 0))
66	4	nnne0d 12259	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ≠ 0)
67	2, 1	dgreq0 25771	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ (Poly‘𝑆) → (𝐹 = 0_𝑝 ↔ (𝐴‘𝑁) = 0))
68	3, 67	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐹 = 0_𝑝 ↔ (𝐴‘𝑁) = 0))
69		fveq2 6889	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 = 0_𝑝 → (deg‘𝐹) = (deg‘0_𝑝))
70		dgr0 25768	. . . . . . . . . . . . . . . . 17 ⊢ (deg‘0_𝑝) = 0
71	69, 70	eqtrdi 2789	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 = 0_𝑝 → (deg‘𝐹) = 0)
72	2, 71	eqtrid 2785	. . . . . . . . . . . . . . 15 ⊢ (𝐹 = 0_𝑝 → 𝑁 = 0)
73	68, 72	syl6bir 254	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐴‘𝑁) = 0 → 𝑁 = 0))
74	73	necon3d 2962	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑁 ≠ 0 → (𝐴‘𝑁) ≠ 0))
75	66, 74	mpd 15	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴‘𝑁) ≠ 0)
76	65, 4, 75	elrabd 3685	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0})
77		infssuzle 12912	. . . . . . . . . . 11 ⊢ (({𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ⊆ (ℤ_≥‘1) ∧ 𝑁 ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0}) → inf({𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0}, ℝ, < ) ≤ 𝑁)
78	63, 76, 77	sylancr 588	. . . . . . . . . 10 ⊢ (𝜑 → inf({𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0}, ℝ, < ) ≤ 𝑁)
79	6, 78	eqbrtrid 5183	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ≤ 𝑁)
80		nn0uz 12861	. . . . . . . . . . 11 ⊢ ℕ₀ = (ℤ_≥‘0)
81	27, 80	eleqtrdi 2844	. . . . . . . . . 10 ⊢ (𝜑 → 𝐾 ∈ (ℤ_≥‘0))
82	4	nnzd 12582	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ ℤ)
83		elfz5 13490	. . . . . . . . . 10 ⊢ ((𝐾 ∈ (ℤ_≥‘0) ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (0...𝑁) ↔ 𝐾 ≤ 𝑁))
84	81, 82, 83	syl2anc 585	. . . . . . . . 9 ⊢ (𝜑 → (𝐾 ∈ (0...𝑁) ↔ 𝐾 ≤ 𝑁))
85	79, 84	mpbird 257	. . . . . . . 8 ⊢ (𝜑 → 𝐾 ∈ (0...𝑁))
86		fzsplit 13524	. . . . . . . 8 ⊢ (𝐾 ∈ (0...𝑁) → (0...𝑁) = ((0...𝐾) ∪ ((𝐾 + 1)...𝑁)))
87	85, 86	syl 17	. . . . . . 7 ⊢ (𝜑 → (0...𝑁) = ((0...𝐾) ∪ ((𝐾 + 1)...𝑁)))
88		fzfid 13935	. . . . . . 7 ⊢ (𝜑 → (0...𝑁) ∈ Fin)
89		elfznn0 13591	. . . . . . . . 9 ⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ₀)
90	33, 89, 39	syl2an 597	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝐴‘𝑘) ∈ ℂ)
91	16, 89, 50	syl2an 597	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝑇 · 𝑋)↑𝑘) ∈ ℂ)
92	90, 91	mulcld 11231	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) ∈ ℂ)
93	60, 87, 88, 92	fsumsplit 15684	. . . . . 6 ⊢ (𝜑 → Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = (Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) + Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))))
94	56, 93	eqtrd 2773	. . . . 5 ⊢ (𝜑 → (𝐹‘(𝑇 · 𝑋)) = (Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) + Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))))
95	94	fveq2d 6893	. . . 4 ⊢ (𝜑 → (abs‘(𝐹‘(𝑇 · 𝑋))) = (abs‘(Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) + Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))))
96	1	coefv0 25754	. . . . . . . . . . . . 13 ⊢ (𝐹 ∈ (Poly‘𝑆) → (𝐹‘0) = (𝐴‘0))
97	3, 96	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹‘0) = (𝐴‘0))
98	97	eqcomd 2739	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴‘0) = (𝐹‘0))
99	16	exp0d 14102	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑇 · 𝑋)↑0) = 1)
100	98, 99	oveq12d 7424	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴‘0) · ((𝑇 · 𝑋)↑0)) = ((𝐹‘0) · 1))
101	23	mulridd 11228	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐹‘0) · 1) = (𝐹‘0))
102	100, 101	eqtrd 2773	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴‘0) · ((𝑇 · 𝑋)↑0)) = (𝐹‘0))
103		1e0p1 12716	. . . . . . . . . . . . 13 ⊢ 1 = (0 + 1)
104	103	oveq1i 7416	. . . . . . . . . . . 12 ⊢ (1...𝐾) = ((0 + 1)...𝐾)
105	104	sumeq1i 15641	. . . . . . . . . . 11 ⊢ Σ𝑘 ∈ (1...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = Σ𝑘 ∈ ((0 + 1)...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))
106	26, 62	eleqtrdi 2844	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐾 ∈ (ℤ_≥‘1))
107		elfznn 13527	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ (1...𝐾) → 𝑘 ∈ ℕ)
108	107	nnnn0d 12529	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (1...𝐾) → 𝑘 ∈ ℕ₀)
109	33, 108, 39	syl2an 597	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐾)) → (𝐴‘𝑘) ∈ ℂ)
110	16, 108, 50	syl2an 597	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐾)) → ((𝑇 · 𝑋)↑𝑘) ∈ ℂ)
111	109, 110	mulcld 11231	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐾)) → ((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) ∈ ℂ)
112		fveq2 6889	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝐾 → (𝐴‘𝑘) = (𝐴‘𝐾))
113		oveq2 7414	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝐾 → ((𝑇 · 𝑋)↑𝑘) = ((𝑇 · 𝑋)↑𝐾))
114	112, 113	oveq12d 7424	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝐾 → ((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = ((𝐴‘𝐾) · ((𝑇 · 𝑋)↑𝐾)))
115	106, 111, 114	fsumm1 15694	. . . . . . . . . . 11 ⊢ (𝜑 → Σ𝑘 ∈ (1...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = (Σ𝑘 ∈ (1...(𝐾 − 1))((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) + ((𝐴‘𝐾) · ((𝑇 · 𝑋)↑𝐾))))
116	105, 115	eqtr3id 2787	. . . . . . . . . 10 ⊢ (𝜑 → Σ𝑘 ∈ ((0 + 1)...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = (Σ𝑘 ∈ (1...(𝐾 − 1))((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) + ((𝐴‘𝐾) · ((𝑇 · 𝑋)↑𝐾))))
117		elfznn 13527	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 ∈ (1...(𝐾 − 1)) → 𝑘 ∈ ℕ)
118	117	adantl 483	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → 𝑘 ∈ ℕ)
119	118	nnred 12224	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → 𝑘 ∈ ℝ)
120	57	adantr 482	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → 𝐾 ∈ ℝ)
121		peano2rem 11524	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐾 ∈ ℝ → (𝐾 − 1) ∈ ℝ)
122	120, 121	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → (𝐾 − 1) ∈ ℝ)
123		elfzle2 13502	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ (1...(𝐾 − 1)) → 𝑘 ≤ (𝐾 − 1))
124	123	adantl 483	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → 𝑘 ≤ (𝐾 − 1))
125	120	ltm1d 12143	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → (𝐾 − 1) < 𝐾)
126	119, 122, 120, 124, 125	lelttrd 11369	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → 𝑘 < 𝐾)
127	119, 120	ltnled 11358	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → (𝑘 < 𝐾 ↔ ¬ 𝐾 ≤ 𝑘))
128	126, 127	mpbid 231	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → ¬ 𝐾 ≤ 𝑘)
129		infssuzle 12912	. . . . . . . . . . . . . . . . . . 19 ⊢ (({𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ⊆ (ℤ_≥‘1) ∧ 𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0}) → inf({𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0}, ℝ, < ) ≤ 𝑘)
130	6, 129	eqbrtrid 5183	. . . . . . . . . . . . . . . . . 18 ⊢ (({𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ⊆ (ℤ_≥‘1) ∧ 𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0}) → 𝐾 ≤ 𝑘)
131	63, 130	mpan 689	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} → 𝐾 ≤ 𝑘)
132	128, 131	nsyl 140	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → ¬ 𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0})
133		fveq2 6889	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 𝑘 → (𝐴‘𝑛) = (𝐴‘𝑘))
134	133	neeq1d 3001	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑘 → ((𝐴‘𝑛) ≠ 0 ↔ (𝐴‘𝑘) ≠ 0))
135	134	elrab3 3684	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ℕ → (𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ↔ (𝐴‘𝑘) ≠ 0))
136	118, 135	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → (𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ↔ (𝐴‘𝑘) ≠ 0))
137	136	necon2bbid 2985	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → ((𝐴‘𝑘) = 0 ↔ ¬ 𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0}))
138	132, 137	mpbird 257	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → (𝐴‘𝑘) = 0)
139	138	oveq1d 7421	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → ((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = (0 · ((𝑇 · 𝑋)↑𝑘)))
140	117	nnnn0d 12529	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ (1...(𝐾 − 1)) → 𝑘 ∈ ℕ₀)
141	16, 140, 50	syl2an 597	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → ((𝑇 · 𝑋)↑𝑘) ∈ ℂ)
142	141	mul02d 11409	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → (0 · ((𝑇 · 𝑋)↑𝑘)) = 0)
143	139, 142	eqtrd 2773	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → ((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = 0)
144	143	sumeq2dv 15646	. . . . . . . . . . . 12 ⊢ (𝜑 → Σ𝑘 ∈ (1...(𝐾 − 1))((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = Σ𝑘 ∈ (1...(𝐾 − 1))0)
145		fzfi 13934	. . . . . . . . . . . . . 14 ⊢ (1...(𝐾 − 1)) ∈ Fin
146	145	olci 865	. . . . . . . . . . . . 13 ⊢ ((1...(𝐾 − 1)) ⊆ (ℤ_≥‘1) ∨ (1...(𝐾 − 1)) ∈ Fin)
147		sumz 15665	. . . . . . . . . . . . 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 2789	. . . . . . . . . . 11 ⊢ (𝜑 → Σ𝑘 ∈ (1...(𝐾 − 1))((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = 0)
150	12, 15, 27	mulexpd 14123	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑇 · 𝑋)↑𝐾) = ((𝑇↑𝐾) · (𝑋↑𝐾)))
151	150	oveq2d 7422	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐴‘𝐾) · ((𝑇 · 𝑋)↑𝐾)) = ((𝐴‘𝐾) · ((𝑇↑𝐾) · (𝑋↑𝐾))))
152	33, 27	ffvelcdmd 7085	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐴‘𝐾) ∈ ℂ)
153	12, 27	expcld 14108	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑇↑𝐾) ∈ ℂ)
154	28	recnd 11239	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑋↑𝐾) ∈ ℂ)
155	152, 153, 154	mulassd 11234	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐴‘𝐾) · (𝑇↑𝐾)) · (𝑋↑𝐾)) = ((𝐴‘𝐾) · ((𝑇↑𝐾) · (𝑋↑𝐾))))
156	151, 155	eqtr4d 2776	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐴‘𝐾) · ((𝑇 · 𝑋)↑𝐾)) = (((𝐴‘𝐾) · (𝑇↑𝐾)) · (𝑋↑𝐾)))
157	7	oveq1i 7416	. . . . . . . . . . . . . . . 16 ⊢ (𝑇↑𝐾) = ((-((𝐹‘0) / (𝐴‘𝐾))↑_𝑐(1 / 𝐾))↑𝐾)
158	57	recnd 11239	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐾 ∈ ℂ)
159	26	nnne0d 12259	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐾 ≠ 0)
160	158, 159	recid2d 11983	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((1 / 𝐾) · 𝐾) = 1)
161	160	oveq2d 7422	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (-((𝐹‘0) / (𝐴‘𝐾))↑_𝑐((1 / 𝐾) · 𝐾)) = (-((𝐹‘0) / (𝐴‘𝐾))↑_𝑐1))
162	25	simprd 497	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐴‘𝐾) ≠ 0)
163	23, 152, 162	divcld 11987	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐹‘0) / (𝐴‘𝐾)) ∈ ℂ)
164	163	negcld 11555	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → -((𝐹‘0) / (𝐴‘𝐾)) ∈ ℂ)
165	26	nnrecred 12260	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (1 / 𝐾) ∈ ℝ)
166	165	recnd 11239	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (1 / 𝐾) ∈ ℂ)
167	164, 166, 27	cxpmul2d 26209	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (-((𝐹‘0) / (𝐴‘𝐾))↑_𝑐((1 / 𝐾) · 𝐾)) = ((-((𝐹‘0) / (𝐴‘𝐾))↑_𝑐(1 / 𝐾))↑𝐾))
168	164	cxp1d 26206	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (-((𝐹‘0) / (𝐴‘𝐾))↑_𝑐1) = -((𝐹‘0) / (𝐴‘𝐾)))
169	161, 167, 168	3eqtr3d 2781	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((-((𝐹‘0) / (𝐴‘𝐾))↑_𝑐(1 / 𝐾))↑𝐾) = -((𝐹‘0) / (𝐴‘𝐾)))
170	157, 169	eqtrid 2785	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑇↑𝐾) = -((𝐹‘0) / (𝐴‘𝐾)))
171	170	oveq2d 7422	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐴‘𝐾) · (𝑇↑𝐾)) = ((𝐴‘𝐾) · -((𝐹‘0) / (𝐴‘𝐾))))
172	152, 163	mulneg2d 11665	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐴‘𝐾) · -((𝐹‘0) / (𝐴‘𝐾))) = -((𝐴‘𝐾) · ((𝐹‘0) / (𝐴‘𝐾))))
173	23, 152, 162	divcan2d 11989	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐴‘𝐾) · ((𝐹‘0) / (𝐴‘𝐾))) = (𝐹‘0))
174	173	negeqd 11451	. . . . . . . . . . . . . 14 ⊢ (𝜑 → -((𝐴‘𝐾) · ((𝐹‘0) / (𝐴‘𝐾))) = -(𝐹‘0))
175	171, 172, 174	3eqtrd 2777	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐴‘𝐾) · (𝑇↑𝐾)) = -(𝐹‘0))
176	175	oveq1d 7421	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐴‘𝐾) · (𝑇↑𝐾)) · (𝑋↑𝐾)) = (-(𝐹‘0) · (𝑋↑𝐾)))
177	23, 154	mulneg1d 11664	. . . . . . . . . . . 12 ⊢ (𝜑 → (-(𝐹‘0) · (𝑋↑𝐾)) = -((𝐹‘0) · (𝑋↑𝐾)))
178	156, 176, 177	3eqtrd 2777	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴‘𝐾) · ((𝑇 · 𝑋)↑𝐾)) = -((𝐹‘0) · (𝑋↑𝐾)))
179	149, 178	oveq12d 7424	. . . . . . . . . 10 ⊢ (𝜑 → (Σ𝑘 ∈ (1...(𝐾 − 1))((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) + ((𝐴‘𝐾) · ((𝑇 · 𝑋)↑𝐾))) = (0 + -((𝐹‘0) · (𝑋↑𝐾))))
180	23, 154	mulcld 11231	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐹‘0) · (𝑋↑𝐾)) ∈ ℂ)
181	180	negcld 11555	. . . . . . . . . . 11 ⊢ (𝜑 → -((𝐹‘0) · (𝑋↑𝐾)) ∈ ℂ)
182	181	addlidd 11412	. . . . . . . . . 10 ⊢ (𝜑 → (0 + -((𝐹‘0) · (𝑋↑𝐾))) = -((𝐹‘0) · (𝑋↑𝐾)))
183	116, 179, 182	3eqtrd 2777	. . . . . . . . 9 ⊢ (𝜑 → Σ𝑘 ∈ ((0 + 1)...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = -((𝐹‘0) · (𝑋↑𝐾)))
184	102, 183	oveq12d 7424	. . . . . . . 8 ⊢ (𝜑 → (((𝐴‘0) · ((𝑇 · 𝑋)↑0)) + Σ𝑘 ∈ ((0 + 1)...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) = ((𝐹‘0) + -((𝐹‘0) · (𝑋↑𝐾))))
185		fveq2 6889	. . . . . . . . . 10 ⊢ (𝑘 = 0 → (𝐴‘𝑘) = (𝐴‘0))
186		oveq2 7414	. . . . . . . . . 10 ⊢ (𝑘 = 0 → ((𝑇 · 𝑋)↑𝑘) = ((𝑇 · 𝑋)↑0))
187	185, 186	oveq12d 7424	. . . . . . . . 9 ⊢ (𝑘 = 0 → ((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = ((𝐴‘0) · ((𝑇 · 𝑋)↑0)))
188	81, 52, 187	fsum1p 15696	. . . . . . . 8 ⊢ (𝜑 → Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = (((𝐴‘0) · ((𝑇 · 𝑋)↑0)) + Σ𝑘 ∈ ((0 + 1)...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))))
189	101	oveq1d 7421	. . . . . . . . 9 ⊢ (𝜑 → (((𝐹‘0) · 1) − ((𝐹‘0) · (𝑋↑𝐾))) = ((𝐹‘0) − ((𝐹‘0) · (𝑋↑𝐾))))
190		1cnd 11206	. . . . . . . . . 10 ⊢ (𝜑 → 1 ∈ ℂ)
191	23, 190, 154	subdid 11667	. . . . . . . . 9 ⊢ (𝜑 → ((𝐹‘0) · (1 − (𝑋↑𝐾))) = (((𝐹‘0) · 1) − ((𝐹‘0) · (𝑋↑𝐾))))
192	23, 180	negsubd 11574	. . . . . . . . 9 ⊢ (𝜑 → ((𝐹‘0) + -((𝐹‘0) · (𝑋↑𝐾))) = ((𝐹‘0) − ((𝐹‘0) · (𝑋↑𝐾))))
193	189, 191, 192	3eqtr4d 2783	. . . . . . . 8 ⊢ (𝜑 → ((𝐹‘0) · (1 − (𝑋↑𝐾))) = ((𝐹‘0) + -((𝐹‘0) · (𝑋↑𝐾))))
194	184, 188, 193	3eqtr4d 2783	. . . . . . 7 ⊢ (𝜑 → Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = ((𝐹‘0) · (1 − (𝑋↑𝐾))))
195	194	fveq2d 6893	. . . . . 6 ⊢ (𝜑 → (abs‘Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) = (abs‘((𝐹‘0) · (1 − (𝑋↑𝐾)))))
196		1re 11211	. . . . . . . . 9 ⊢ 1 ∈ ℝ
197		resubcl 11521	. . . . . . . . 9 ⊢ ((1 ∈ ℝ ∧ (𝑋↑𝐾) ∈ ℝ) → (1 − (𝑋↑𝐾)) ∈ ℝ)
198	196, 28, 197	sylancr 588	. . . . . . . 8 ⊢ (𝜑 → (1 − (𝑋↑𝐾)) ∈ ℝ)
199	198	recnd 11239	. . . . . . 7 ⊢ (𝜑 → (1 − (𝑋↑𝐾)) ∈ ℂ)
200	23, 199	absmuld 15398	. . . . . 6 ⊢ (𝜑 → (abs‘((𝐹‘0) · (1 − (𝑋↑𝐾)))) = ((abs‘(𝐹‘0)) · (abs‘(1 − (𝑋↑𝐾)))))
201	13	rpge0d 13017	. . . . . . . . . . 11 ⊢ (𝜑 → 0 ≤ 𝑋)
202	11	simp2d 1144	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑈 ∈ ℝ⁺)
203	202	rpred 13013	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑈 ∈ ℝ)
204		min1 13165	. . . . . . . . . . . . 13 ⊢ ((1 ∈ ℝ ∧ 𝑈 ∈ ℝ) → if(1 ≤ 𝑈, 1, 𝑈) ≤ 1)
205	196, 203, 204	sylancr 588	. . . . . . . . . . . 12 ⊢ (𝜑 → if(1 ≤ 𝑈, 1, 𝑈) ≤ 1)
206	9, 205	eqbrtrid 5183	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑋 ≤ 1)
207		exple1 14138	. . . . . . . . . . 11 ⊢ (((𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ∧ 𝑋 ≤ 1) ∧ 𝐾 ∈ ℕ₀) → (𝑋↑𝐾) ≤ 1)
208	14, 201, 206, 27, 207	syl31anc 1374	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋↑𝐾) ≤ 1)
209		subge0 11724	. . . . . . . . . . 11 ⊢ ((1 ∈ ℝ ∧ (𝑋↑𝐾) ∈ ℝ) → (0 ≤ (1 − (𝑋↑𝐾)) ↔ (𝑋↑𝐾) ≤ 1))
210	196, 28, 209	sylancr 588	. . . . . . . . . 10 ⊢ (𝜑 → (0 ≤ (1 − (𝑋↑𝐾)) ↔ (𝑋↑𝐾) ≤ 1))
211	208, 210	mpbird 257	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ (1 − (𝑋↑𝐾)))
212	198, 211	absidd 15366	. . . . . . . 8 ⊢ (𝜑 → (abs‘(1 − (𝑋↑𝐾))) = (1 − (𝑋↑𝐾)))
213	212	oveq2d 7422	. . . . . . 7 ⊢ (𝜑 → ((abs‘(𝐹‘0)) · (abs‘(1 − (𝑋↑𝐾)))) = ((abs‘(𝐹‘0)) · (1 − (𝑋↑𝐾))))
214	24	recnd 11239	. . . . . . . 8 ⊢ (𝜑 → (abs‘(𝐹‘0)) ∈ ℂ)
215	214, 190, 154	subdid 11667	. . . . . . 7 ⊢ (𝜑 → ((abs‘(𝐹‘0)) · (1 − (𝑋↑𝐾))) = (((abs‘(𝐹‘0)) · 1) − ((abs‘(𝐹‘0)) · (𝑋↑𝐾))))
216	214	mulridd 11228	. . . . . . . 8 ⊢ (𝜑 → ((abs‘(𝐹‘0)) · 1) = (abs‘(𝐹‘0)))
217	216	oveq1d 7421	. . . . . . 7 ⊢ (𝜑 → (((abs‘(𝐹‘0)) · 1) − ((abs‘(𝐹‘0)) · (𝑋↑𝐾))) = ((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋↑𝐾))))
218	213, 215, 217	3eqtrd 2777	. . . . . 6 ⊢ (𝜑 → ((abs‘(𝐹‘0)) · (abs‘(1 − (𝑋↑𝐾)))) = ((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋↑𝐾))))
219	195, 200, 218	3eqtrrd 2778	. . . . 5 ⊢ (𝜑 → ((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋↑𝐾))) = (abs‘Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))))
220	219	oveq1d 7421	. . . 4 ⊢ (𝜑 → (((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋↑𝐾))) + (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))) = ((abs‘Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) + (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))))
221	54, 95, 220	3brtr4d 5180	. . 3 ⊢ (𝜑 → (abs‘(𝐹‘(𝑇 · 𝑋))) ≤ (((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋↑𝐾))) + (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))))
222	43	abscld 15380	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) ∈ ℝ)
223	31, 222	fsumrecl 15677	. . . . . 6 ⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) ∈ ℝ)
224	31, 43	fsumabs 15744	. . . . . 6 ⊢ (𝜑 → (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) ≤ Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))))
225		expcl 14042	. . . . . . . . . . . 12 ⊢ ((𝑇 ∈ ℂ ∧ 𝑘 ∈ ℕ₀) → (𝑇↑𝑘) ∈ ℂ)
226	12, 38, 225	syl2an2r 684	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑇↑𝑘) ∈ ℂ)
227	40, 226	mulcld 11231	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((𝐴‘𝑘) · (𝑇↑𝑘)) ∈ ℂ)
228	227	abscld 15380	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) ∈ ℝ)
229	31, 228	fsumrecl 15677	. . . . . . . 8 ⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) ∈ ℝ)
230	14, 35	reexpcld 14125	. . . . . . . 8 ⊢ (𝜑 → (𝑋↑(𝐾 + 1)) ∈ ℝ)
231	229, 230	remulcld 11241	. . . . . . 7 ⊢ (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1))) ∈ ℝ)
232	230	adantr 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑋↑(𝐾 + 1)) ∈ ℝ)
233	228, 232	remulcld 11241	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1))) ∈ ℝ)
234	12	adantr 482	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑇 ∈ ℂ)
235	15	adantr 482	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑋 ∈ ℂ)
236	234, 235, 38	mulexpd 14123	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((𝑇 · 𝑋)↑𝑘) = ((𝑇↑𝑘) · (𝑋↑𝑘)))
237	236	oveq2d 7422	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = ((𝐴‘𝑘) · ((𝑇↑𝑘) · (𝑋↑𝑘))))
238	14	adantr 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑋 ∈ ℝ)
239	238, 38	reexpcld 14125	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑋↑𝑘) ∈ ℝ)
240	239	recnd 11239	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑋↑𝑘) ∈ ℂ)
241	40, 226, 240	mulassd 11234	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (((𝐴‘𝑘) · (𝑇↑𝑘)) · (𝑋↑𝑘)) = ((𝐴‘𝑘) · ((𝑇↑𝑘) · (𝑋↑𝑘))))
242	237, 241	eqtr4d 2776	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = (((𝐴‘𝑘) · (𝑇↑𝑘)) · (𝑋↑𝑘)))
243	242	fveq2d 6893	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) = (abs‘(((𝐴‘𝑘) · (𝑇↑𝑘)) · (𝑋↑𝑘))))
244	227, 240	absmuld 15398	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘(((𝐴‘𝑘) · (𝑇↑𝑘)) · (𝑋↑𝑘))) = ((abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (abs‘(𝑋↑𝑘))))
245		elfzelz 13498	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ((𝐾 + 1)...𝑁) → 𝑘 ∈ ℤ)
246		rpexpcl 14043	. . . . . . . . . . . . . . 15 ⊢ ((𝑋 ∈ ℝ⁺ ∧ 𝑘 ∈ ℤ) → (𝑋↑𝑘) ∈ ℝ⁺)
247	13, 245, 246	syl2an 597	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑋↑𝑘) ∈ ℝ⁺)
248	247	rpge0d 13017	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 0 ≤ (𝑋↑𝑘))
249	239, 248	absidd 15366	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘(𝑋↑𝑘)) = (𝑋↑𝑘))
250	249	oveq2d 7422	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (abs‘(𝑋↑𝑘))) = ((abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑𝑘)))
251	243, 244, 250	3eqtrd 2777	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) = ((abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑𝑘)))
252	227	absge0d 15388	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 0 ≤ (abs‘((𝐴‘𝑘) · (𝑇↑𝑘))))
253	35	adantr 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝐾 + 1) ∈ ℕ₀)
254	36	adantl 483	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑘 ∈ (ℤ_≥‘(𝐾 + 1)))
255	201	adantr 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 0 ≤ 𝑋)
256	206	adantr 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑋 ≤ 1)
257	238, 253, 254, 255, 256	leexp2rd 14215	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑋↑𝑘) ≤ (𝑋↑(𝐾 + 1)))
258	239, 232, 228, 252, 257	lemul2ad 12151	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑𝑘)) ≤ ((abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1))))
259	251, 258	eqbrtrd 5170	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) ≤ ((abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1))))
260	31, 222, 233, 259	fsumle 15742	. . . . . . . 8 ⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) ≤ Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1))))
261	230	recnd 11239	. . . . . . . . 9 ⊢ (𝜑 → (𝑋↑(𝐾 + 1)) ∈ ℂ)
262	228	recnd 11239	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) ∈ ℂ)
263	31, 261, 262	fsummulc1 15728	. . . . . . . 8 ⊢ (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1))) = Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1))))
264	260, 263	breqtrrd 5176	. . . . . . 7 ⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) ≤ (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1))))
265	15, 27	expp1d 14109	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑋↑(𝐾 + 1)) = ((𝑋↑𝐾) · 𝑋))
266	154, 15	mulcomd 11232	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑋↑𝐾) · 𝑋) = (𝑋 · (𝑋↑𝐾)))
267	265, 266	eqtrd 2773	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋↑(𝐾 + 1)) = (𝑋 · (𝑋↑𝐾)))
268	267	oveq2d 7422	. . . . . . . . 9 ⊢ (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1))) = (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋 · (𝑋↑𝐾))))
269	229	recnd 11239	. . . . . . . . . 10 ⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) ∈ ℂ)
270	269, 15, 154	mulassd 11234	. . . . . . . . 9 ⊢ (𝜑 → ((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · 𝑋) · (𝑋↑𝐾)) = (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋 · (𝑋↑𝐾))))
271	268, 270	eqtr4d 2776	. . . . . . . 8 ⊢ (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1))) = ((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · 𝑋) · (𝑋↑𝐾)))
272	229, 14	remulcld 11241	. . . . . . . . 9 ⊢ (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · 𝑋) ∈ ℝ)
273		nnssz 12577	. . . . . . . . . . . 12 ⊢ ℕ ⊆ ℤ
274	61, 273	sstri 3991	. . . . . . . . . . 11 ⊢ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ⊆ ℤ
275	76	ne0d 4335	. . . . . . . . . . . . 13 ⊢ (𝜑 → {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ≠ ∅)
276		infssuzcl 12913	. . . . . . . . . . . . 13 ⊢ (({𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ⊆ (ℤ_≥‘1) ∧ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ≠ ∅) → inf({𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0}, ℝ, < ) ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0})
277	63, 275, 276	sylancr 588	. . . . . . . . . . . 12 ⊢ (𝜑 → inf({𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0}, ℝ, < ) ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0})
278	6, 277	eqeltrid 2838	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐾 ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0})
279	274, 278	sselid 3980	. . . . . . . . . 10 ⊢ (𝜑 → 𝐾 ∈ ℤ)
280	13, 279	rpexpcld 14207	. . . . . . . . 9 ⊢ (𝜑 → (𝑋↑𝐾) ∈ ℝ⁺)
281		peano2re 11384	. . . . . . . . . . . 12 ⊢ (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) ∈ ℝ → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1) ∈ ℝ)
282	229, 281	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1) ∈ ℝ)
283	282, 14	remulcld 11241	. . . . . . . . . 10 ⊢ (𝜑 → ((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1) · 𝑋) ∈ ℝ)
284	229	ltp1d 12141	. . . . . . . . . . 11 ⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) < (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1))
285	229, 282, 13, 284	ltmul1dd 13068	. . . . . . . . . 10 ⊢ (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · 𝑋) < ((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1) · 𝑋))
286		min2 13166	. . . . . . . . . . . . . 14 ⊢ ((1 ∈ ℝ ∧ 𝑈 ∈ ℝ) → if(1 ≤ 𝑈, 1, 𝑈) ≤ 𝑈)
287	196, 203, 286	sylancr 588	. . . . . . . . . . . . 13 ⊢ (𝜑 → if(1 ≤ 𝑈, 1, 𝑈) ≤ 𝑈)
288	9, 287	eqbrtrid 5183	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑋 ≤ 𝑈)
289	288, 8	breqtrdi 5189	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑋 ≤ ((abs‘(𝐹‘0)) / (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1)))
290		0red 11214	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 ∈ ℝ)
291	31, 228, 252	fsumge0 15738	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 ≤ Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))))
292	290, 229, 282, 291, 284	lelttrd 11369	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 < (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1))
293		lemuldiv2 12092	. . . . . . . . . . . 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 1375	. . . . . . . . . . 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 11371	. . . . . . . . 9 ⊢ (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · 𝑋) < (abs‘(𝐹‘0)))
297	272, 24, 280, 296	ltmul1dd 13068	. . . . . . . 8 ⊢ (𝜑 → ((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · 𝑋) · (𝑋↑𝐾)) < ((abs‘(𝐹‘0)) · (𝑋↑𝐾)))
298	271, 297	eqbrtrd 5170	. . . . . . 7 ⊢ (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1))) < ((abs‘(𝐹‘0)) · (𝑋↑𝐾)))
299	223, 231, 29, 264, 298	lelttrd 11369	. . . . . 6 ⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) < ((abs‘(𝐹‘0)) · (𝑋↑𝐾)))
300	45, 223, 29, 224, 299	lelttrd 11369	. . . . 5 ⊢ (𝜑 → (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) < ((abs‘(𝐹‘0)) · (𝑋↑𝐾)))
301	45, 29, 24, 300	ltsub2dd 11824	. . . 4 ⊢ (𝜑 → ((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋↑𝐾))) < ((abs‘(𝐹‘0)) − (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))))
302	30, 45, 24	ltaddsubd 11811	. . . 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 11369	. 2 ⊢ (𝜑 → (abs‘(𝐹‘(𝑇 · 𝑋))) < (abs‘(𝐹‘0)))
305		2fveq3 6894	. . . 4 ⊢ (𝑥 = (𝑇 · 𝑋) → (abs‘(𝐹‘𝑥)) = (abs‘(𝐹‘(𝑇 · 𝑋))))
306	305	breq1d 5158	. . 3 ⊢ (𝑥 = (𝑇 · 𝑋) → ((abs‘(𝐹‘𝑥)) < (abs‘(𝐹‘0)) ↔ (abs‘(𝐹‘(𝑇 · 𝑋))) < (abs‘(𝐹‘0))))
307	306	rspcev 3613	. 2 ⊢ (((𝑇 · 𝑋) ∈ ℂ ∧ (abs‘(𝐹‘(𝑇 · 𝑋))) < (abs‘(𝐹‘0))) → ∃𝑥 ∈ ℂ (abs‘(𝐹‘𝑥)) < (abs‘(𝐹‘0)))
308	16, 304, 307	syl2anc 585	1 ⊢ (𝜑 → ∃𝑥 ∈ ℂ (abs‘(𝐹‘𝑥)) < (abs‘(𝐹‘0)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 397 ∨ wo 846 ∧ w3a 1088 = wceq 1542 ∈ wcel 2107 ≠ wne 2941 ∃wrex 3071 {crab 3433 ∪ cun 3946 ∩ cin 3947 ⊆ wss 3948 ∅c0 4322 ifcif 4528 class class class wbr 5148 ⟶wf 6537 ‘cfv 6541 (class class class)co 7406 Fincfn 8936 infcinf 9433 ℂcc 11105 ℝcr 11106 0cc0 11107 1c1 11108 + caddc 11110 · cmul 11112 < clt 11245 ≤ cle 11246 − cmin 11441 -cneg 11442 / cdiv 11868 ℕcn 12209 ℕ₀cn0 12469 ℤcz 12555 ℤ_≥cuz 12819 ℝ⁺crp 12971 ...cfz 13481 ↑cexp 14024 abscabs 15178 Σcsu 15629 0_𝑝c0p 25178 Polycply 25690 coeffccoe 25692 degcdgr 25693 ↑_𝑐ccxp 26056

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-rep 5285 ax-sep 5299 ax-nul 5306 ax-pow 5363 ax-pr 5427 ax-un 7722 ax-inf2 9633 ax-cnex 11163 ax-resscn 11164 ax-1cn 11165 ax-icn 11166 ax-addcl 11167 ax-addrcl 11168 ax-mulcl 11169 ax-mulrcl 11170 ax-mulcom 11171 ax-addass 11172 ax-mulass 11173 ax-distr 11174 ax-i2m1 11175 ax-1ne0 11176 ax-1rid 11177 ax-rnegex 11178 ax-rrecex 11179 ax-cnre 11180 ax-pre-lttri 11181 ax-pre-lttrn 11182 ax-pre-ltadd 11183 ax-pre-mulgt0 11184 ax-pre-sup 11185 ax-addf 11186 ax-mulf 11187

This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rmo 3377 df-reu 3378 df-rab 3434 df-v 3477 df-sbc 3778 df-csb 3894 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-pss 3967 df-nul 4323 df-if 4529 df-pw 4604 df-sn 4629 df-pr 4631 df-tp 4633 df-op 4635 df-uni 4909 df-int 4951 df-iun 4999 df-iin 5000 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5574 df-eprel 5580 df-po 5588 df-so 5589 df-fr 5631 df-se 5632 df-we 5633 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-pred 6298 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6493 df-fun 6543 df-fn 6544 df-f 6545 df-f1 6546 df-fo 6547 df-f1o 6548 df-fv 6549 df-isom 6550 df-riota 7362 df-ov 7409 df-oprab 7410 df-mpo 7411 df-of 7667 df-om 7853 df-1st 7972 df-2nd 7973 df-supp 8144 df-frecs 8263 df-wrecs 8294 df-recs 8368 df-rdg 8407 df-1o 8463 df-2o 8464 df-er 8700 df-map 8819 df-pm 8820 df-ixp 8889 df-en 8937 df-dom 8938 df-sdom 8939 df-fin 8940 df-fsupp 9359 df-fi 9403 df-sup 9434 df-inf 9435 df-oi 9502 df-card 9931 df-pnf 11247 df-mnf 11248 df-xr 11249 df-ltxr 11250 df-le 11251 df-sub 11443 df-neg 11444 df-div 11869 df-nn 12210 df-2 12272 df-3 12273 df-4 12274 df-5 12275 df-6 12276 df-7 12277 df-8 12278 df-9 12279 df-n0 12470 df-z 12556 df-dec 12675 df-uz 12820 df-q 12930 df-rp 12972 df-xneg 13089 df-xadd 13090 df-xmul 13091 df-ioo 13325 df-ioc 13326 df-ico 13327 df-icc 13328 df-fz 13482 df-fzo 13625 df-fl 13754 df-mod 13832 df-seq 13964 df-exp 14025 df-fac 14231 df-bc 14260 df-hash 14288 df-shft 15011 df-cj 15043 df-re 15044 df-im 15045 df-sqrt 15179 df-abs 15180 df-limsup 15412 df-clim 15429 df-rlim 15430 df-sum 15630 df-ef 16008 df-sin 16010 df-cos 16011 df-pi 16013 df-struct 17077 df-sets 17094 df-slot 17112 df-ndx 17124 df-base 17142 df-ress 17171 df-plusg 17207 df-mulr 17208 df-starv 17209 df-sca 17210 df-vsca 17211 df-ip 17212 df-tset 17213 df-ple 17214 df-ds 17216 df-unif 17217 df-hom 17218 df-cco 17219 df-rest 17365 df-topn 17366 df-0g 17384 df-gsum 17385 df-topgen 17386 df-pt 17387 df-prds 17390 df-xrs 17445 df-qtop 17450 df-imas 17451 df-xps 17453 df-mre 17527 df-mrc 17528 df-acs 17530 df-mgm 18558 df-sgrp 18607 df-mnd 18623 df-submnd 18669 df-mulg 18946 df-cntz 19176 df-cmn 19645 df-psmet 20929 df-xmet 20930 df-met 20931 df-bl 20932 df-mopn 20933 df-fbas 20934 df-fg 20935 df-cnfld 20938 df-top 22388 df-topon 22405 df-topsp 22427 df-bases 22441 df-cld 22515 df-ntr 22516 df-cls 22517 df-nei 22594 df-lp 22632 df-perf 22633 df-cn 22723 df-cnp 22724 df-haus 22811 df-tx 23058 df-hmeo 23251 df-fil 23342 df-fm 23434 df-flim 23435 df-flf 23436 df-xms 23818 df-ms 23819 df-tms 23820 df-cncf 24386 df-0p 25179 df-limc 25375 df-dv 25376 df-ply 25694 df-coe 25696 df-dgr 25697 df-log 26057 df-cxp 26058

This theorem is referenced by: ftalem6 26572

W3C validator