Theorem ftalem5 27272

Description: Lemma for fta 27275: Main proof. We have already shifted the minimum found in ftalem3 27270 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 27271	. . . . 5 ⊢ (𝜑 → ((𝐾 ∈ ℕ ∧ (𝐴‘𝐾) ≠ 0) ∧ (𝑇 ∈ ℂ ∧ 𝑈 ∈ ℝ+ ∧ 𝑋 ∈ ℝ+)))
11	10	simprd 501	. . . 4 ⊢ (𝜑 → (𝑇 ∈ ℂ ∧ 𝑈 ∈ ℝ+ ∧ 𝑋 ∈ ℝ+))
12	11	simp1d 1160	. . 3 ⊢ (𝜑 → 𝑇 ∈ ℂ)
13	11	simp3d 1162	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ ℝ+)
14	13	rpred 13072	. . . 4 ⊢ (𝜑 → 𝑋 ∈ ℝ)
15	14	recnd 11248	. . 3 ⊢ (𝜑 → 𝑋 ∈ ℂ)
16	12, 15	mulcld 11240	. 2 ⊢ (𝜑 → (𝑇 · 𝑋) ∈ ℂ)
17		plyf 26386	. . . . . 6 ⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐹:ℂ⟶ℂ)
18	3, 17	syl 18	. . . . 5 ⊢ (𝜑 → 𝐹:ℂ⟶ℂ)
19	18, 16	ffvelcdmd 7084	. . . 4 ⊢ (𝜑 → (𝐹‘(𝑇 · 𝑋)) ∈ ℂ)
20	19	abscld 15510	. . 3 ⊢ (𝜑 → (abs‘(𝐹‘(𝑇 · 𝑋))) ∈ ℝ)
21		0cn 11209	. . . . . . 7 ⊢ 0 ∈ ℂ
22		ffvelcdm 7080	. . . . . . 7 ⊢ ((𝐹:ℂ⟶ℂ ∧ 0 ∈ ℂ) → (𝐹‘0) ∈ ℂ)
23	18, 21, 22	sylancl 598	. . . . . 6 ⊢ (𝜑 → (𝐹‘0) ∈ ℂ)
24	23	abscld 15510	. . . . 5 ⊢ (𝜑 → (abs‘(𝐹‘0)) ∈ ℝ)
25	10	simpld 500	. . . . . . . . 9 ⊢ (𝜑 → (𝐾 ∈ ℕ ∧ (𝐴‘𝐾) ≠ 0))
26	25	simpld 500	. . . . . . . 8 ⊢ (𝜑 → 𝐾 ∈ ℕ)
27	26	nnnn0d 12576	. . . . . . 7 ⊢ (𝜑 → 𝐾 ∈ ℕ0)
28	14, 27	reexpcld 14213	. . . . . 6 ⊢ (𝜑 → (𝑋↑𝐾) ∈ ℝ)
29	24, 28	remulcld 11250	. . . . 5 ⊢ (𝜑 → ((abs‘(𝐹‘0)) · (𝑋↑𝐾)) ∈ ℝ)
30	24, 29	resubcld 11653	. . . 4 ⊢ (𝜑 → ((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋↑𝐾))) ∈ ℝ)
31		fzfid 14023	. . . . . 6 ⊢ (𝜑 → ((𝐾 + 1)...𝑁) ∈ Fin)
32	1	coef3 26420	. . . . . . . . 9 ⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐴:ℕ0⟶ℂ)
33	3, 32	syl 18	. . . . . . . 8 ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)
34		peano2nn0 12555	. . . . . . . . . 10 ⊢ (𝐾 ∈ ℕ0 → (𝐾 + 1) ∈ ℕ0)
35	27, 34	syl 18	. . . . . . . . 9 ⊢ (𝜑 → (𝐾 + 1) ∈ ℕ0)
36		elfzuz 13560	. . . . . . . . 9 ⊢ (𝑘 ∈ ((𝐾 + 1)...𝑁) → 𝑘 ∈ (ℤ≥‘(𝐾 + 1)))
37		eluznn0 12953	. . . . . . . . 9 ⊢ (((𝐾 + 1) ∈ ℕ0 ∧ 𝑘 ∈ (ℤ≥‘(𝐾 + 1))) → 𝑘 ∈ ℕ0)
38	35, 36, 37	syl2an 608	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑘 ∈ ℕ0)
39		ffvelcdm 7080	. . . . . . . 8 ⊢ ((𝐴:ℕ0⟶ℂ ∧ 𝑘 ∈ ℕ0) → (𝐴‘𝑘) ∈ ℂ)
40	33, 38, 39	syl2an2r 698	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝐴‘𝑘) ∈ ℂ)
41	16	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑇 · 𝑋) ∈ ℂ)
42	41, 38	expcld 14196	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((𝑇 · 𝑋)↑𝑘) ∈ ℂ)
43	40, 42	mulcld 11240	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) ∈ ℂ)
44	31, 43	fsumcl 15803	. . . . 5 ⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) ∈ ℂ)
45	44	abscld 15510	. . . 4 ⊢ (𝜑 → (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) ∈ ℝ)
46	30, 45	readdcld 11249	. . 3 ⊢ (𝜑 → (((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋↑𝐾))) + (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))) ∈ ℝ)
47		fzfid 14023	. . . . . 6 ⊢ (𝜑 → (0...𝐾) ∈ Fin)
48		elfznn0 13661	. . . . . . . 8 ⊢ (𝑘 ∈ (0...𝐾) → 𝑘 ∈ ℕ0)
49	33, 48, 39	syl2an 608	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐾)) → (𝐴‘𝑘) ∈ ℂ)
50		expcl 14129	. . . . . . . 8 ⊢ (((𝑇 · 𝑋) ∈ ℂ ∧ 𝑘 ∈ ℕ0) → ((𝑇 · 𝑋)↑𝑘) ∈ ℂ)
51	16, 48, 50	syl2an 608	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐾)) → ((𝑇 · 𝑋)↑𝑘) ∈ ℂ)
52	49, 51	mulcld 11240	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐾)) → ((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) ∈ ℂ)
53	47, 52	fsumcl 15803	. . . . 5 ⊢ (𝜑 → Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) ∈ ℂ)
54	53, 44	abstrid 15530	. . . 4 ⊢ (𝜑 → (abs‘(Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) + Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))) ≤ ((abs‘Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) + (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))))
55	1, 2	coeid2 26427	. . . . . . 7 ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (𝑇 · 𝑋) ∈ ℂ) → (𝐹‘(𝑇 · 𝑋)) = Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))
56	3, 16, 55	syl2anc 596	. . . . . 6 ⊢ (𝜑 → (𝐹‘(𝑇 · 𝑋)) = Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))
57	26	nnred 12259	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ∈ ℝ)
58	57	ltp1d 12156	. . . . . . . 8 ⊢ (𝜑 → 𝐾 < (𝐾 + 1))
59		fzdisj 13592	. . . . . . . 8 ⊢ (𝐾 < (𝐾 + 1) → ((0...𝐾) ∩ ((𝐾 + 1)...𝑁)) = ∅)
60	58, 59	syl 18	. . . . . . 7 ⊢ (𝜑 → ((0...𝐾) ∩ ((𝐾 + 1)...𝑁)) = ∅)
61		ssrab2 4035	. . . . . . . . . . . 12 ⊢ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ⊆ ℕ
62		nnuz 12913	. . . . . . . . . . . 12 ⊢ ℕ = (ℤ≥‘1)
63	61, 62	sseqtri 3986	. . . . . . . . . . 11 ⊢ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ⊆ (ℤ≥‘1)
64		fveq2 6885	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑁 → (𝐴‘𝑛) = (𝐴‘𝑁))
65	64	neeq1d 3019	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑁 → ((𝐴‘𝑛) ≠ 0 ↔ (𝐴‘𝑁) ≠ 0))
66	4	nnne0d 12297	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ≠ 0)
67	2, 1	dgreq0 26453	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ (Poly‘𝑆) → (𝐹 = 0𝑝 ↔ (𝐴‘𝑁) = 0))
68	3, 67	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐹 = 0𝑝 ↔ (𝐴‘𝑁) = 0))
69		fveq2 6885	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 = 0𝑝 → (deg‘𝐹) = (deg‘0𝑝))
70		dgr0 26450	. . . . . . . . . . . . . . . . 17 ⊢ (deg‘0𝑝) = 0
71	69, 70	eqtrdi 2816	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 = 0𝑝 → (deg‘𝐹) = 0)
72	2, 71	eqtrid 2812	. . . . . . . . . . . . . . 15 ⊢ (𝐹 = 0𝑝 → 𝑁 = 0)
73	68, 72	biimtrrdi 257	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐴‘𝑁) = 0 → 𝑁 = 0))
74	73	necon3d 2981	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑁 ≠ 0 → (𝐴‘𝑁) ≠ 0))
75	66, 74	mpd 16	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴‘𝑁) ≠ 0)
76	65, 4, 75	elrabd 3654	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0})
77		infssuzle 12967	. . . . . . . . . . 11 ⊢ (({𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ⊆ (ℤ≥‘1) ∧ 𝑁 ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0}) → inf({𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0}, ℝ, < ) ≤ 𝑁)
78	63, 76, 77	sylancr 599	. . . . . . . . . 10 ⊢ (𝜑 → inf({𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0}, ℝ, < ) ≤ 𝑁)
79	6, 78	eqbrtrid 5148	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ≤ 𝑁)
80		nn0uz 12912	. . . . . . . . . . 11 ⊢ ℕ0 = (ℤ≥‘0)
81	27, 80	eleqtrdi 2875	. . . . . . . . . 10 ⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘0))
82	4	nnzd 12628	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ ℤ)
83		elfz5 13556	. . . . . . . . . 10 ⊢ ((𝐾 ∈ (ℤ≥‘0) ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (0...𝑁) ↔ 𝐾 ≤ 𝑁))
84	81, 82, 83	syl2anc 596	. . . . . . . . 9 ⊢ (𝜑 → (𝐾 ∈ (0...𝑁) ↔ 𝐾 ≤ 𝑁))
85	79, 84	mpbird 260	. . . . . . . 8 ⊢ (𝜑 → 𝐾 ∈ (0...𝑁))
86		fzsplit 13591	. . . . . . . 8 ⊢ (𝐾 ∈ (0...𝑁) → (0...𝑁) = ((0...𝐾) ∪ ((𝐾 + 1)...𝑁)))
87	85, 86	syl 18	. . . . . . 7 ⊢ (𝜑 → (0...𝑁) = ((0...𝐾) ∪ ((𝐾 + 1)...𝑁)))
88		fzfid 14023	. . . . . . 7 ⊢ (𝜑 → (0...𝑁) ∈ Fin)
89		elfznn0 13661	. . . . . . . . 9 ⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0)
90	33, 89, 39	syl2an 608	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝐴‘𝑘) ∈ ℂ)
91	16, 89, 50	syl2an 608	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝑇 · 𝑋)↑𝑘) ∈ ℂ)
92	90, 91	mulcld 11240	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) ∈ ℂ)
93	60, 87, 88, 92	fsumsplit 15811	. . . . . 6 ⊢ (𝜑 → Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = (Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) + Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))))
94	56, 93	eqtrd 2800	. . . . 5 ⊢ (𝜑 → (𝐹‘(𝑇 · 𝑋)) = (Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) + Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))))
95	94	fveq2d 6889	. . . 4 ⊢ (𝜑 → (abs‘(𝐹‘(𝑇 · 𝑋))) = (abs‘(Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) + Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))))
96	1	coefv0 26436	. . . . . . . . . . . . 13 ⊢ (𝐹 ∈ (Poly‘𝑆) → (𝐹‘0) = (𝐴‘0))
97	3, 96	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹‘0) = (𝐴‘0))
98	97	eqcomd 2771	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴‘0) = (𝐹‘0))
99	16	exp0d 14190	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑇 · 𝑋)↑0) = 1)
100	98, 99	oveq12d 7434	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴‘0) · ((𝑇 · 𝑋)↑0)) = ((𝐹‘0) · 1))
101	23	mulridd 11237	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐹‘0) · 1) = (𝐹‘0))
102	100, 101	eqtrd 2800	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴‘0) · ((𝑇 · 𝑋)↑0)) = (𝐹‘0))
103		1e0p1 12770	. . . . . . . . . . . . 13 ⊢ 1 = (0 + 1)
104	103	oveq1i 7426	. . . . . . . . . . . 12 ⊢ (1...𝐾) = ((0 + 1)...𝐾)
105	104	sumeq1i 15768	. . . . . . . . . . 11 ⊢ Σ𝑘 ∈ (1...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = Σ𝑘 ∈ ((0 + 1)...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))
106	26, 62	eleqtrdi 2875	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘1))
107		elfznn 13594	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ (1...𝐾) → 𝑘 ∈ ℕ)
108	107	nnnn0d 12576	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (1...𝐾) → 𝑘 ∈ ℕ0)
109	33, 108, 39	syl2an 608	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐾)) → (𝐴‘𝑘) ∈ ℂ)
110	16, 108, 50	syl2an 608	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐾)) → ((𝑇 · 𝑋)↑𝑘) ∈ ℂ)
111	109, 110	mulcld 11240	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐾)) → ((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) ∈ ℂ)
112		fveq2 6885	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝐾 → (𝐴‘𝑘) = (𝐴‘𝐾))
113		oveq2 7424	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝐾 → ((𝑇 · 𝑋)↑𝑘) = ((𝑇 · 𝑋)↑𝐾))
114	112, 113	oveq12d 7434	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝐾 → ((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = ((𝐴‘𝐾) · ((𝑇 · 𝑋)↑𝐾)))
115	106, 111, 114	fsumm1 15821	. . . . . . . . . . 11 ⊢ (𝜑 → Σ𝑘 ∈ (1...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = (Σ𝑘 ∈ (1...(𝐾 − 1))((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) + ((𝐴‘𝐾) · ((𝑇 · 𝑋)↑𝐾))))
116	105, 115	eqtr3id 2814	. . . . . . . . . 10 ⊢ (𝜑 → Σ𝑘 ∈ ((0 + 1)...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = (Σ𝑘 ∈ (1...(𝐾 − 1))((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) + ((𝐴‘𝐾) · ((𝑇 · 𝑋)↑𝐾))))
117		elfznn 13594	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 ∈ (1...(𝐾 − 1)) → 𝑘 ∈ ℕ)
118	117	adantl 487	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → 𝑘 ∈ ℕ)
119	118	nnred 12259	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → 𝑘 ∈ ℝ)
120	57	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → 𝐾 ∈ ℝ)
121		peano2rem 11536	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐾 ∈ ℝ → (𝐾 − 1) ∈ ℝ)
122	120, 121	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → (𝐾 − 1) ∈ ℝ)
123		elfzle2 13568	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ (1...(𝐾 − 1)) → 𝑘 ≤ (𝐾 − 1))
124	123	adantl 487	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → 𝑘 ≤ (𝐾 − 1))
125	120	ltm1d 12158	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → (𝐾 − 1) < 𝐾)
126	119, 122, 120, 124, 125	lelttrd 11379	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → 𝑘 < 𝐾)
127	119, 120	ltnled 11368	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → (𝑘 < 𝐾 ↔ ¬ 𝐾 ≤ 𝑘))
128	126, 127	mpbid 235	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → ¬ 𝐾 ≤ 𝑘)
129		infssuzle 12967	. . . . . . . . . . . . . . . . . . 19 ⊢ (({𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ⊆ (ℤ≥‘1) ∧ 𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0}) → inf({𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0}, ℝ, < ) ≤ 𝑘)
130	6, 129	eqbrtrid 5148	. . . . . . . . . . . . . . . . . 18 ⊢ (({𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ⊆ (ℤ≥‘1) ∧ 𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0}) → 𝐾 ≤ 𝑘)
131	63, 130	mpan 703	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} → 𝐾 ≤ 𝑘)
132	128, 131	nsyl 141	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → ¬ 𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0})
133		fveq2 6885	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 𝑘 → (𝐴‘𝑛) = (𝐴‘𝑘))
134	133	neeq1d 3019	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑘 → ((𝐴‘𝑛) ≠ 0 ↔ (𝐴‘𝑘) ≠ 0))
135	134	elrab3 3653	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ℕ → (𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ↔ (𝐴‘𝑘) ≠ 0))
136	118, 135	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → (𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ↔ (𝐴‘𝑘) ≠ 0))
137	136	necon2bbid 3003	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → ((𝐴‘𝑘) = 0 ↔ ¬ 𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0}))
138	132, 137	mpbird 260	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → (𝐴‘𝑘) = 0)
139	138	oveq1d 7431	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → ((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = (0 · ((𝑇 · 𝑋)↑𝑘)))
140	117	nnnn0d 12576	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ (1...(𝐾 − 1)) → 𝑘 ∈ ℕ0)
141	16, 140, 50	syl2an 608	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → ((𝑇 · 𝑋)↑𝑘) ∈ ℂ)
142	141	mul02d 11419	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → (0 · ((𝑇 · 𝑋)↑𝑘)) = 0)
143	139, 142	eqtrd 2800	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → ((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = 0)
144	143	sumeq2dv 15773	. . . . . . . . . . . 12 ⊢ (𝜑 → Σ𝑘 ∈ (1...(𝐾 − 1))((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = Σ𝑘 ∈ (1...(𝐾 − 1))0)
145		fzfi 14022	. . . . . . . . . . . . . 14 ⊢ (1...(𝐾 − 1)) ∈ Fin
146	145	olci 880	. . . . . . . . . . . . 13 ⊢ ((1...(𝐾 − 1)) ⊆ (ℤ≥‘1) ∨ (1...(𝐾 − 1)) ∈ Fin)
147		sumz 15792	. . . . . . . . . . . . 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 2816	. . . . . . . . . . 11 ⊢ (𝜑 → Σ𝑘 ∈ (1...(𝐾 − 1))((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = 0)
150	12, 15, 27	mulexpd 14211	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑇 · 𝑋)↑𝐾) = ((𝑇↑𝐾) · (𝑋↑𝐾)))
151	150	oveq2d 7432	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐴‘𝐾) · ((𝑇 · 𝑋)↑𝐾)) = ((𝐴‘𝐾) · ((𝑇↑𝐾) · (𝑋↑𝐾))))
152	33, 27	ffvelcdmd 7084	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐴‘𝐾) ∈ ℂ)
153	12, 27	expcld 14196	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑇↑𝐾) ∈ ℂ)
154	28	recnd 11248	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑋↑𝐾) ∈ ℂ)
155	152, 153, 154	mulassd 11243	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐴‘𝐾) · (𝑇↑𝐾)) · (𝑋↑𝐾)) = ((𝐴‘𝐾) · ((𝑇↑𝐾) · (𝑋↑𝐾))))
156	151, 155	eqtr4d 2803	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐴‘𝐾) · ((𝑇 · 𝑋)↑𝐾)) = (((𝐴‘𝐾) · (𝑇↑𝐾)) · (𝑋↑𝐾)))
157	7	oveq1i 7426	. . . . . . . . . . . . . . . 16 ⊢ (𝑇↑𝐾) = ((-((𝐹‘0) / (𝐴‘𝐾))↑𝑐(1 / 𝐾))↑𝐾)
158	57	recnd 11248	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐾 ∈ ℂ)
159	26	nnne0d 12297	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐾 ≠ 0)
160	158, 159	recid2d 11998	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((1 / 𝐾) · 𝐾) = 1)
161	160	oveq2d 7432	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (-((𝐹‘0) / (𝐴‘𝐾))↑𝑐((1 / 𝐾) · 𝐾)) = (-((𝐹‘0) / (𝐴‘𝐾))↑𝑐1))
162	25	simprd 501	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐴‘𝐾) ≠ 0)
163	23, 152, 162	divcld 12002	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐹‘0) / (𝐴‘𝐾)) ∈ ℂ)
164	163	negcld 11567	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → -((𝐹‘0) / (𝐴‘𝐾)) ∈ ℂ)
165	26	nnrecred 12298	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (1 / 𝐾) ∈ ℝ)
166	165	recnd 11248	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (1 / 𝐾) ∈ ℂ)
167	164, 166, 27	cxpmul2d 26905	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (-((𝐹‘0) / (𝐴‘𝐾))↑𝑐((1 / 𝐾) · 𝐾)) = ((-((𝐹‘0) / (𝐴‘𝐾))↑𝑐(1 / 𝐾))↑𝐾))
168	164	cxp1d 26902	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (-((𝐹‘0) / (𝐴‘𝐾))↑𝑐1) = -((𝐹‘0) / (𝐴‘𝐾)))
169	161, 167, 168	3eqtr3d 2808	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((-((𝐹‘0) / (𝐴‘𝐾))↑𝑐(1 / 𝐾))↑𝐾) = -((𝐹‘0) / (𝐴‘𝐾)))
170	157, 169	eqtrid 2812	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑇↑𝐾) = -((𝐹‘0) / (𝐴‘𝐾)))
171	170	oveq2d 7432	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐴‘𝐾) · (𝑇↑𝐾)) = ((𝐴‘𝐾) · -((𝐹‘0) / (𝐴‘𝐾))))
172	152, 163	mulneg2d 11679	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐴‘𝐾) · -((𝐹‘0) / (𝐴‘𝐾))) = -((𝐴‘𝐾) · ((𝐹‘0) / (𝐴‘𝐾))))
173	23, 152, 162	divcan2d 12004	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐴‘𝐾) · ((𝐹‘0) / (𝐴‘𝐾))) = (𝐹‘0))
174	173	negeqd 11462	. . . . . . . . . . . . . 14 ⊢ (𝜑 → -((𝐴‘𝐾) · ((𝐹‘0) / (𝐴‘𝐾))) = -(𝐹‘0))
175	171, 172, 174	3eqtrd 2804	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐴‘𝐾) · (𝑇↑𝐾)) = -(𝐹‘0))
176	175	oveq1d 7431	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐴‘𝐾) · (𝑇↑𝐾)) · (𝑋↑𝐾)) = (-(𝐹‘0) · (𝑋↑𝐾)))
177	23, 154	mulneg1d 11678	. . . . . . . . . . . 12 ⊢ (𝜑 → (-(𝐹‘0) · (𝑋↑𝐾)) = -((𝐹‘0) · (𝑋↑𝐾)))
178	156, 176, 177	3eqtrd 2804	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴‘𝐾) · ((𝑇 · 𝑋)↑𝐾)) = -((𝐹‘0) · (𝑋↑𝐾)))
179	149, 178	oveq12d 7434	. . . . . . . . . 10 ⊢ (𝜑 → (Σ𝑘 ∈ (1...(𝐾 − 1))((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) + ((𝐴‘𝐾) · ((𝑇 · 𝑋)↑𝐾))) = (0 + -((𝐹‘0) · (𝑋↑𝐾))))
180	23, 154	mulcld 11240	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐹‘0) · (𝑋↑𝐾)) ∈ ℂ)
181	180	negcld 11567	. . . . . . . . . . 11 ⊢ (𝜑 → -((𝐹‘0) · (𝑋↑𝐾)) ∈ ℂ)
182	181	addlidd 11422	. . . . . . . . . 10 ⊢ (𝜑 → (0 + -((𝐹‘0) · (𝑋↑𝐾))) = -((𝐹‘0) · (𝑋↑𝐾)))
183	116, 179, 182	3eqtrd 2804	. . . . . . . . 9 ⊢ (𝜑 → Σ𝑘 ∈ ((0 + 1)...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = -((𝐹‘0) · (𝑋↑𝐾)))
184	102, 183	oveq12d 7434	. . . . . . . 8 ⊢ (𝜑 → (((𝐴‘0) · ((𝑇 · 𝑋)↑0)) + Σ𝑘 ∈ ((0 + 1)...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) = ((𝐹‘0) + -((𝐹‘0) · (𝑋↑𝐾))))
185		fveq2 6885	. . . . . . . . . 10 ⊢ (𝑘 = 0 → (𝐴‘𝑘) = (𝐴‘0))
186		oveq2 7424	. . . . . . . . . 10 ⊢ (𝑘 = 0 → ((𝑇 · 𝑋)↑𝑘) = ((𝑇 · 𝑋)↑0))
187	185, 186	oveq12d 7434	. . . . . . . . 9 ⊢ (𝑘 = 0 → ((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = ((𝐴‘0) · ((𝑇 · 𝑋)↑0)))
188	81, 52, 187	fsum1p 15823	. . . . . . . 8 ⊢ (𝜑 → Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = (((𝐴‘0) · ((𝑇 · 𝑋)↑0)) + Σ𝑘 ∈ ((0 + 1)...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))))
189	101	oveq1d 7431	. . . . . . . . 9 ⊢ (𝜑 → (((𝐹‘0) · 1) − ((𝐹‘0) · (𝑋↑𝐾))) = ((𝐹‘0) − ((𝐹‘0) · (𝑋↑𝐾))))
190		1cnd 11213	. . . . . . . . . 10 ⊢ (𝜑 → 1 ∈ ℂ)
191	23, 190, 154	subdid 11681	. . . . . . . . 9 ⊢ (𝜑 → ((𝐹‘0) · (1 − (𝑋↑𝐾))) = (((𝐹‘0) · 1) − ((𝐹‘0) · (𝑋↑𝐾))))
192	23, 180	negsubd 11586	. . . . . . . . 9 ⊢ (𝜑 → ((𝐹‘0) + -((𝐹‘0) · (𝑋↑𝐾))) = ((𝐹‘0) − ((𝐹‘0) · (𝑋↑𝐾))))
193	189, 191, 192	3eqtr4d 2810	. . . . . . . 8 ⊢ (𝜑 → ((𝐹‘0) · (1 − (𝑋↑𝐾))) = ((𝐹‘0) + -((𝐹‘0) · (𝑋↑𝐾))))
194	184, 188, 193	3eqtr4d 2810	. . . . . . 7 ⊢ (𝜑 → Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = ((𝐹‘0) · (1 − (𝑋↑𝐾))))
195	194	fveq2d 6889	. . . . . 6 ⊢ (𝜑 → (abs‘Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) = (abs‘((𝐹‘0) · (1 − (𝑋↑𝐾)))))
196		1re 11219	. . . . . . . . 9 ⊢ 1 ∈ ℝ
197		resubcl 11533	. . . . . . . . 9 ⊢ ((1 ∈ ℝ ∧ (𝑋↑𝐾) ∈ ℝ) → (1 − (𝑋↑𝐾)) ∈ ℝ)
198	196, 28, 197	sylancr 599	. . . . . . . 8 ⊢ (𝜑 → (1 − (𝑋↑𝐾)) ∈ ℝ)
199	198	recnd 11248	. . . . . . 7 ⊢ (𝜑 → (1 − (𝑋↑𝐾)) ∈ ℂ)
200	23, 199	absmuld 15528	. . . . . 6 ⊢ (𝜑 → (abs‘((𝐹‘0) · (1 − (𝑋↑𝐾)))) = ((abs‘(𝐹‘0)) · (abs‘(1 − (𝑋↑𝐾)))))
201	13	rpge0d 13076	. . . . . . . . . . 11 ⊢ (𝜑 → 0 ≤ 𝑋)
202	11	simp2d 1161	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑈 ∈ ℝ+)
203	202	rpred 13072	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑈 ∈ ℝ)
204		min1 13227	. . . . . . . . . . . . 13 ⊢ ((1 ∈ ℝ ∧ 𝑈 ∈ ℝ) → if(1 ≤ 𝑈, 1, 𝑈) ≤ 1)
205	196, 203, 204	sylancr 599	. . . . . . . . . . . 12 ⊢ (𝜑 → if(1 ≤ 𝑈, 1, 𝑈) ≤ 1)
206	9, 205	eqbrtrid 5148	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑋 ≤ 1)
207		exple1 14227	. . . . . . . . . . 11 ⊢ (((𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ∧ 𝑋 ≤ 1) ∧ 𝐾 ∈ ℕ0) → (𝑋↑𝐾) ≤ 1)
208	14, 201, 206, 27, 207	syl31anc 1400	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋↑𝐾) ≤ 1)
209		subge0 11738	. . . . . . . . . . 11 ⊢ ((1 ∈ ℝ ∧ (𝑋↑𝐾) ∈ ℝ) → (0 ≤ (1 − (𝑋↑𝐾)) ↔ (𝑋↑𝐾) ≤ 1))
210	196, 28, 209	sylancr 599	. . . . . . . . . 10 ⊢ (𝜑 → (0 ≤ (1 − (𝑋↑𝐾)) ↔ (𝑋↑𝐾) ≤ 1))
211	208, 210	mpbird 260	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ (1 − (𝑋↑𝐾)))
212	198, 211	absidd 15494	. . . . . . . 8 ⊢ (𝜑 → (abs‘(1 − (𝑋↑𝐾))) = (1 − (𝑋↑𝐾)))
213	212	oveq2d 7432	. . . . . . 7 ⊢ (𝜑 → ((abs‘(𝐹‘0)) · (abs‘(1 − (𝑋↑𝐾)))) = ((abs‘(𝐹‘0)) · (1 − (𝑋↑𝐾))))
214	24	recnd 11248	. . . . . . . 8 ⊢ (𝜑 → (abs‘(𝐹‘0)) ∈ ℂ)
215	214, 190, 154	subdid 11681	. . . . . . 7 ⊢ (𝜑 → ((abs‘(𝐹‘0)) · (1 − (𝑋↑𝐾))) = (((abs‘(𝐹‘0)) · 1) − ((abs‘(𝐹‘0)) · (𝑋↑𝐾))))
216	214	mulridd 11237	. . . . . . . 8 ⊢ (𝜑 → ((abs‘(𝐹‘0)) · 1) = (abs‘(𝐹‘0)))
217	216	oveq1d 7431	. . . . . . 7 ⊢ (𝜑 → (((abs‘(𝐹‘0)) · 1) − ((abs‘(𝐹‘0)) · (𝑋↑𝐾))) = ((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋↑𝐾))))
218	213, 215, 217	3eqtrd 2804	. . . . . 6 ⊢ (𝜑 → ((abs‘(𝐹‘0)) · (abs‘(1 − (𝑋↑𝐾)))) = ((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋↑𝐾))))
219	195, 200, 218	3eqtrrd 2805	. . . . 5 ⊢ (𝜑 → ((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋↑𝐾))) = (abs‘Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))))
220	219	oveq1d 7431	. . . 4 ⊢ (𝜑 → (((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋↑𝐾))) + (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))) = ((abs‘Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) + (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))))
221	54, 95, 220	3brtr4d 5145	. . 3 ⊢ (𝜑 → (abs‘(𝐹‘(𝑇 · 𝑋))) ≤ (((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋↑𝐾))) + (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))))
222	43	abscld 15510	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) ∈ ℝ)
223	31, 222	fsumrecl 15804	. . . . . 6 ⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) ∈ ℝ)
224	31, 43	fsumabs 15872	. . . . . 6 ⊢ (𝜑 → (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) ≤ Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))))
225		expcl 14129	. . . . . . . . . . . 12 ⊢ ((𝑇 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (𝑇↑𝑘) ∈ ℂ)
226	12, 38, 225	syl2an2r 698	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑇↑𝑘) ∈ ℂ)
227	40, 226	mulcld 11240	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((𝐴‘𝑘) · (𝑇↑𝑘)) ∈ ℂ)
228	227	abscld 15510	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) ∈ ℝ)
229	31, 228	fsumrecl 15804	. . . . . . . 8 ⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) ∈ ℝ)
230	14, 35	reexpcld 14213	. . . . . . . 8 ⊢ (𝜑 → (𝑋↑(𝐾 + 1)) ∈ ℝ)
231	229, 230	remulcld 11250	. . . . . . 7 ⊢ (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1))) ∈ ℝ)
232	230	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑋↑(𝐾 + 1)) ∈ ℝ)
233	228, 232	remulcld 11250	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1))) ∈ ℝ)
234	12	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑇 ∈ ℂ)
235	15	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑋 ∈ ℂ)
236	234, 235, 38	mulexpd 14211	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((𝑇 · 𝑋)↑𝑘) = ((𝑇↑𝑘) · (𝑋↑𝑘)))
237	236	oveq2d 7432	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = ((𝐴‘𝑘) · ((𝑇↑𝑘) · (𝑋↑𝑘))))
238	14	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑋 ∈ ℝ)
239	238, 38	reexpcld 14213	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑋↑𝑘) ∈ ℝ)
240	239	recnd 11248	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑋↑𝑘) ∈ ℂ)
241	40, 226, 240	mulassd 11243	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (((𝐴‘𝑘) · (𝑇↑𝑘)) · (𝑋↑𝑘)) = ((𝐴‘𝑘) · ((𝑇↑𝑘) · (𝑋↑𝑘))))
242	237, 241	eqtr4d 2803	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = (((𝐴‘𝑘) · (𝑇↑𝑘)) · (𝑋↑𝑘)))
243	242	fveq2d 6889	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) = (abs‘(((𝐴‘𝑘) · (𝑇↑𝑘)) · (𝑋↑𝑘))))
244	227, 240	absmuld 15528	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘(((𝐴‘𝑘) · (𝑇↑𝑘)) · (𝑋↑𝑘))) = ((abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (abs‘(𝑋↑𝑘))))
245		elfzelz 13564	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ((𝐾 + 1)...𝑁) → 𝑘 ∈ ℤ)
246		rpexpcl 14130	. . . . . . . . . . . . . . 15 ⊢ ((𝑋 ∈ ℝ+ ∧ 𝑘 ∈ ℤ) → (𝑋↑𝑘) ∈ ℝ+)
247	13, 245, 246	syl2an 608	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑋↑𝑘) ∈ ℝ+)
248	247	rpge0d 13076	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 0 ≤ (𝑋↑𝑘))
249	239, 248	absidd 15494	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘(𝑋↑𝑘)) = (𝑋↑𝑘))
250	249	oveq2d 7432	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (abs‘(𝑋↑𝑘))) = ((abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑𝑘)))
251	243, 244, 250	3eqtrd 2804	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) = ((abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑𝑘)))
252	227	absge0d 15518	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 0 ≤ (abs‘((𝐴‘𝑘) · (𝑇↑𝑘))))
253	35	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝐾 + 1) ∈ ℕ0)
254	36	adantl 487	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑘 ∈ (ℤ≥‘(𝐾 + 1)))
255	201	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 0 ≤ 𝑋)
256	206	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑋 ≤ 1)
257	238, 253, 254, 255, 256	leexp2rd 14305	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑋↑𝑘) ≤ (𝑋↑(𝐾 + 1)))
258	239, 232, 228, 252, 257	lemul2ad 12166	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑𝑘)) ≤ ((abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1))))
259	251, 258	eqbrtrd 5135	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) ≤ ((abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1))))
260	31, 222, 233, 259	fsumle 15870	. . . . . . . 8 ⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) ≤ Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1))))
261	230	recnd 11248	. . . . . . . . 9 ⊢ (𝜑 → (𝑋↑(𝐾 + 1)) ∈ ℂ)
262	228	recnd 11248	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) ∈ ℂ)
263	31, 261, 262	fsummulc1 15855	. . . . . . . 8 ⊢ (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1))) = Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1))))
264	260, 263	breqtrrd 5141	. . . . . . 7 ⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) ≤ (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1))))
265	15, 27	expp1d 14197	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑋↑(𝐾 + 1)) = ((𝑋↑𝐾) · 𝑋))
266	154, 15	mulcomd 11241	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑋↑𝐾) · 𝑋) = (𝑋 · (𝑋↑𝐾)))
267	265, 266	eqtrd 2800	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋↑(𝐾 + 1)) = (𝑋 · (𝑋↑𝐾)))
268	267	oveq2d 7432	. . . . . . . . 9 ⊢ (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1))) = (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋 · (𝑋↑𝐾))))
269	229	recnd 11248	. . . . . . . . . 10 ⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) ∈ ℂ)
270	269, 15, 154	mulassd 11243	. . . . . . . . 9 ⊢ (𝜑 → ((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · 𝑋) · (𝑋↑𝐾)) = (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋 · (𝑋↑𝐾))))
271	268, 270	eqtr4d 2803	. . . . . . . 8 ⊢ (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1))) = ((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · 𝑋) · (𝑋↑𝐾)))
272	229, 14	remulcld 11250	. . . . . . . . 9 ⊢ (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · 𝑋) ∈ ℝ)
273		nnssz 12624	. . . . . . . . . . . 12 ⊢ ℕ ⊆ ℤ
274	61, 273	sstri 3947	. . . . . . . . . . 11 ⊢ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ⊆ ℤ
275	76	ne0d 4295	. . . . . . . . . . . . 13 ⊢ (𝜑 → {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ≠ ∅)
276		infssuzcl 12968	. . . . . . . . . . . . 13 ⊢ (({𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ⊆ (ℤ≥‘1) ∧ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ≠ ∅) → inf({𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0}, ℝ, < ) ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0})
277	63, 275, 276	sylancr 599	. . . . . . . . . . . 12 ⊢ (𝜑 → inf({𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0}, ℝ, < ) ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0})
278	6, 277	eqeltrid 2869	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐾 ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0})
279	274, 278	sselid 3936	. . . . . . . . . 10 ⊢ (𝜑 → 𝐾 ∈ ℤ)
280	13, 279	rpexpcld 14297	. . . . . . . . 9 ⊢ (𝜑 → (𝑋↑𝐾) ∈ ℝ+)
281		peano2re 11394	. . . . . . . . . . . 12 ⊢ (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) ∈ ℝ → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1) ∈ ℝ)
282	229, 281	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1) ∈ ℝ)
283	282, 14	remulcld 11250	. . . . . . . . . 10 ⊢ (𝜑 → ((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1) · 𝑋) ∈ ℝ)
284	229	ltp1d 12156	. . . . . . . . . . 11 ⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) < (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1))
285	229, 282, 13, 284	ltmul1dd 13127	. . . . . . . . . 10 ⊢ (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · 𝑋) < ((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1) · 𝑋))
286		min2 13228	. . . . . . . . . . . . . 14 ⊢ ((1 ∈ ℝ ∧ 𝑈 ∈ ℝ) → if(1 ≤ 𝑈, 1, 𝑈) ≤ 𝑈)
287	196, 203, 286	sylancr 599	. . . . . . . . . . . . 13 ⊢ (𝜑 → if(1 ≤ 𝑈, 1, 𝑈) ≤ 𝑈)
288	9, 287	eqbrtrid 5148	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑋 ≤ 𝑈)
289	288, 8	breqtrdi 5154	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑋 ≤ ((abs‘(𝐹‘0)) / (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1)))
290		0red 11222	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 ∈ ℝ)
291	31, 228, 252	fsumge0 15866	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 ≤ Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))))
292	290, 229, 282, 291, 284	lelttrd 11379	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 < (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1))
293		lemuldiv2 12107	. . . . . . . . . . . 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 1401	. . . . . . . . . . 11 ⊢ (𝜑 → (((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1) · 𝑋) ≤ (abs‘(𝐹‘0)) ↔ 𝑋 ≤ ((abs‘(𝐹‘0)) / (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1))))
295	289, 294	mpbird 260	. . . . . . . . . 10 ⊢ (𝜑 → ((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1) · 𝑋) ≤ (abs‘(𝐹‘0)))
296	272, 283, 24, 285, 295	ltletrd 11381	. . . . . . . . 9 ⊢ (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · 𝑋) < (abs‘(𝐹‘0)))
297	272, 24, 280, 296	ltmul1dd 13127	. . . . . . . 8 ⊢ (𝜑 → ((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · 𝑋) · (𝑋↑𝐾)) < ((abs‘(𝐹‘0)) · (𝑋↑𝐾)))
298	271, 297	eqbrtrd 5135	. . . . . . 7 ⊢ (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1))) < ((abs‘(𝐹‘0)) · (𝑋↑𝐾)))
299	223, 231, 29, 264, 298	lelttrd 11379	. . . . . 6 ⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) < ((abs‘(𝐹‘0)) · (𝑋↑𝐾)))
300	45, 223, 29, 224, 299	lelttrd 11379	. . . . 5 ⊢ (𝜑 → (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) < ((abs‘(𝐹‘0)) · (𝑋↑𝐾)))
301	45, 29, 24, 300	ltsub2dd 11838	. . . 4 ⊢ (𝜑 → ((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋↑𝐾))) < ((abs‘(𝐹‘0)) − (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))))
302	30, 45, 24	ltaddsubd 11825	. . . 4 ⊢ (𝜑 → ((((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋↑𝐾))) + (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))) < (abs‘(𝐹‘0)) ↔ ((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋↑𝐾))) < ((abs‘(𝐹‘0)) − (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))))))
303	301, 302	mpbird 260	. . 3 ⊢ (𝜑 → (((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋↑𝐾))) + (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))) < (abs‘(𝐹‘0)))
304	20, 46, 24, 221, 303	lelttrd 11379	. 2 ⊢ (𝜑 → (abs‘(𝐹‘(𝑇 · 𝑋))) < (abs‘(𝐹‘0)))
305		2fveq3 6890	. . . 4 ⊢ (𝑥 = (𝑇 · 𝑋) → (abs‘(𝐹‘𝑥)) = (abs‘(𝐹‘(𝑇 · 𝑋))))
306	305	breq1d 5121	. . 3 ⊢ (𝑥 = (𝑇 · 𝑋) → ((abs‘(𝐹‘𝑥)) < (abs‘(𝐹‘0)) ↔ (abs‘(𝐹‘(𝑇 · 𝑋))) < (abs‘(𝐹‘0))))
307	306	rspcev 3583	. 2 ⊢ (((𝑇 · 𝑋) ∈ ℂ ∧ (abs‘(𝐹‘(𝑇 · 𝑋))) < (abs‘(𝐹‘0))) → ∃𝑥 ∈ ℂ (abs‘(𝐹‘𝑥)) < (abs‘(𝐹‘0)))
308	16, 304, 307	syl2anc 596	1 ⊢ (𝜑 → ∃𝑥 ∈ ℂ (abs‘(𝐹‘𝑥)) < (abs‘(𝐹‘0)))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   ∧ w3a 1103   = wceq 1570   ∈ wcel 2146   ≠ wne 2960  ∃wrex 3091  {crab 3418   ∪ cun 3904   ∩ cin 3905   ⊆ wss 3906  ∅c0 4286  ifcif 4489   class class class wbr 5111  ⟶wf 6536  ‘cfv 6540  (class class class)co 7416  Fincfn 8945  infcinf 9404  ℂcc 11109  ℝcr 11110  0cc0 11111  1c1 11112   + caddc 11114   · cmul 11116   < clt 11254   ≤ cle 11255   − cmin 11452  -cneg 11453   / cdiv 11882  ℕcn 12244  ℕ₀cn0 12515  ℤcz 12602  ℤ_≥cuz 12874  ℝ⁺crp 13028  ...cfz 13547  ↑cexp 14111  abscabs 15305  Σcsu 15757  0_𝑝c0p 25859  Polycply 26372  coeffccoe 26374  degcdgr 26375  ↑_𝑐ccxp 26751

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-rep 5240  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7738  ax-inf2 9613  ax-cnex 11167  ax-resscn 11168  ax-1cn 11169  ax-icn 11170  ax-addcl 11171  ax-addrcl 11172  ax-mulcl 11173  ax-mulrcl 11174  ax-mulcom 11175  ax-addass 11176  ax-mulass 11177  ax-distr 11178  ax-i2m1 11179  ax-1ne0 11180  ax-1rid 11181  ax-rnegex 11182  ax-rrecex 11183  ax-cnre 11184  ax-pre-lttri 11185  ax-pre-lttrn 11186  ax-pre-ltadd 11187  ax-pre-mulgt0 11188  ax-pre-sup 11189  ax-addf 11190

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3067  df-ral 3082  df-rex 3092  df-rmo 3371  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-tp 4596  df-op 4598  df-uni 4875  df-int 4915  df-iun 4960  df-iin 4961  df-br 5112  df-opab 5176  df-mpt 5195  df-tr 5221  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-se 5617  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6306  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-isom 6549  df-riota 7373  df-ov 7419  df-oprab 7420  df-mpo 7421  df-of 7680  df-om 7865  df-1st 7988  df-2nd 7989  df-supp 8159  df-frecs 8280  df-wrecs 8311  df-recs 8360  df-rdg 8399  df-1o 8455  df-2o 8456  df-er 8696  df-map 8828  df-pm 8829  df-ixp 8898  df-en 8946  df-dom 8947  df-sdom 8948  df-fin 8949  df-fsupp 9325  df-fi 9374  df-sup 9405  df-inf 9406  df-oi 9475  df-card 9937  df-pnf 11256  df-mnf 11257  df-xr 11258  df-ltxr 11259  df-le 11260  df-sub 11454  df-neg 11455  df-div 11883  df-nn 12245  df-2 12314  df-3 12315  df-4 12316  df-5 12317  df-6 12318  df-7 12319  df-8 12320  df-9 12321  df-n0 12516  df-z 12603  df-dec 12724  df-uz 12875  df-q 12985  df-rp 13029  df-xneg 13149  df-xadd 13150  df-xmul 13151  df-ioo 13388  df-ioc 13389  df-ico 13390  df-icc 13391  df-fz 13548  df-fzo 13696  df-fl 13839  df-mod 13917  df-seq 14052  df-exp 14112  df-fac 14324  df-bc 14353  df-hash 14381  df-shft 15124  df-cj 15170  df-re 15171  df-im 15172  df-sqrt 15306  df-abs 15307  df-limsup 15542  df-clim 15559  df-rlim 15560  df-sum 15758  df-ef 16139  df-sin 16141  df-cos 16142  df-pi 16144  df-struct 17225  df-sets 17242  df-slot 17260  df-ndx 17272  df-base 17288  df-ress 17309  df-plusg 17341  df-mulr 17342  df-starv 17343  df-sca 17344  df-vsca 17345  df-ip 17346  df-tset 17347  df-ple 17348  df-ds 17350  df-unif 17351  df-hom 17352  df-cco 17353  df-rest 17493  df-topn 17494  df-0g 17512  df-gsum 17513  df-topgen 17514  df-pt 17515  df-prds 17518  df-xrs 17574  df-qtop 17579  df-imas 17580  df-xps 17582  df-mre 17656  df-mrc 17657  df-acs 17659  df-mgm 18716  df-sgrp 18799  df-mnd 18815  df-submnd 18866  df-mulg 19158  df-cntz 19411  df-cmn 19876  df-psmet 21544  df-xmet 21545  df-met 21546  df-bl 21547  df-mopn 21548  df-fbas 21549  df-fg 21550  df-cnfld 21553  df-top 23081  df-topon 23098  df-topsp 23120  df-bases 23133  df-cld 23206  df-ntr 23207  df-cls 23208  df-nei 23285  df-lp 23323  df-perf 23324  df-cn 23414  df-cnp 23415  df-haus 23502  df-tx 23750  df-hmeo 23943  df-fil 24034  df-fm 24126  df-flim 24127  df-flf 24128  df-xms 24508  df-ms 24509  df-tms 24510  df-cncf 25068  df-0p 25860  df-limc 26056  df-dv 26057  df-ply 26376  df-coe 26378  df-dgr 26379  df-log 26752  df-cxp 26753

This theorem is used by:  ftalem6  27273