ftalem1 - Metamath Proof Explorer

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

Theorem ftalem1 27409

Description: Lemma for fta 27416: "growth lemma". There exists some 𝑟 such that 𝐹 is arbitrarily close in proportion to its dominant term. (Contributed by Mario Carneiro, 14-Sep-2014.)

**Hypotheses**
Ref	Expression
ftalem.1	⊢ 𝐴 = (coeff‘𝐹)
ftalem.2	⊢ 𝑁 = (deg‘𝐹)
ftalem.3	⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆))
ftalem.4	⊢ (𝜑 → 𝑁 ∈ ℕ)
ftalem1.5	⊢ (𝜑 → 𝐸 ∈ ℝ⁺)
ftalem1.6	⊢ 𝑇 = (Σ𝑘 ∈ (0...(𝑁 − 1))(abs‘(𝐴‘𝑘)) / 𝐸)

**Assertion**
Ref	Expression
ftalem1	⊢ (𝜑 → ∃𝑟 ∈ ℝ ∀𝑥 ∈ ℂ (𝑟 < (abs‘𝑥) → (abs‘((𝐹‘𝑥) − ((𝐴‘𝑁) · (𝑥↑𝑁)))) < (𝐸 · ((abs‘𝑥)↑𝑁))))

Distinct variable groups: 𝑘,𝑟,𝑥,𝐴 𝐸,𝑟 𝑘,𝑁,𝑟,𝑥 𝑘,𝐹,𝑟,𝑥 𝜑,𝑘,𝑥 𝑆,𝑘 𝑇,𝑘,𝑟,𝑥 Allowed substitution hints: 𝜑(𝑟) 𝑆(𝑥, 𝑟) 𝐸(𝑥, 𝑘)

**Proof of Theorem ftalem1**
Step	Hyp	Ref	Expression
1		ftalem1.6	. . . 4 ⊢ 𝑇 = (Σ𝑘 ∈ (0...(𝑁 − 1))(abs‘(𝐴‘𝑘)) / 𝐸)
2		fzfid 14123	. . . . . 6 ⊢ (𝜑 → (0...(𝑁 − 1)) ∈ Fin)
3		ftalem.3	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆))
4		ftalem.1	. . . . . . . . . 10 ⊢ 𝐴 = (coeff‘𝐹)
5	4	coef3 26560	. . . . . . . . 9 ⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐴:ℕ₀⟶ℂ)
6	3, 5	syl 18	. . . . . . . 8 ⊢ (𝜑 → 𝐴:ℕ₀⟶ℂ)
7		elfznn0 13761	. . . . . . . 8 ⊢ (𝑘 ∈ (0...(𝑁 − 1)) → 𝑘 ∈ ℕ₀)
8		ffvelcdm 7086	. . . . . . . 8 ⊢ ((𝐴:ℕ₀⟶ℂ ∧ 𝑘 ∈ ℕ₀) → (𝐴‘𝑘) ∈ ℂ)
9	6, 7, 8	syl2an 608	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (𝐴‘𝑘) ∈ ℂ)
10	9	abscld 15615	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (abs‘(𝐴‘𝑘)) ∈ ℝ)
11	2, 10	fsumrecl 15909	. . . . 5 ⊢ (𝜑 → Σ𝑘 ∈ (0...(𝑁 − 1))(abs‘(𝐴‘𝑘)) ∈ ℝ)
12		ftalem1.5	. . . . 5 ⊢ (𝜑 → 𝐸 ∈ ℝ⁺)
13	11, 12	rerpdivcld 13202	. . . 4 ⊢ (𝜑 → (Σ𝑘 ∈ (0...(𝑁 − 1))(abs‘(𝐴‘𝑘)) / 𝐸) ∈ ℝ)
14	1, 13	eqeltrid 2864	. . 3 ⊢ (𝜑 → 𝑇 ∈ ℝ)
15		1re 11315	. . 3 ⊢ 1 ∈ ℝ
16		ifcl 4527	. . 3 ⊢ ((𝑇 ∈ ℝ ∧ 1 ∈ ℝ) → if(1 ≤ 𝑇, 𝑇, 1) ∈ ℝ)
17	14, 15, 16	sylancl 598	. 2 ⊢ (𝜑 → if(1 ≤ 𝑇, 𝑇, 1) ∈ ℝ)
18		fzfid 14123	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → (0...(𝑁 − 1)) ∈ Fin)
19	6	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → 𝐴:ℕ₀⟶ℂ)
20	19, 8	sylan 592	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) ∧ 𝑘 ∈ ℕ₀) → (𝐴‘𝑘) ∈ ℂ)
21		simprl 783	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → 𝑥 ∈ ℂ)
22		expcl 14229	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℂ ∧ 𝑘 ∈ ℕ₀) → (𝑥↑𝑘) ∈ ℂ)
23	21, 22	sylan 592	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) ∧ 𝑘 ∈ ℕ₀) → (𝑥↑𝑘) ∈ ℂ)
24	20, 23	mulcld 11336	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) ∧ 𝑘 ∈ ℕ₀) → ((𝐴‘𝑘) · (𝑥↑𝑘)) ∈ ℂ)
25	7, 24	sylan2 605	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((𝐴‘𝑘) · (𝑥↑𝑘)) ∈ ℂ)
26	18, 25	fsumcl 15908	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → Σ𝑘 ∈ (0...(𝑁 − 1))((𝐴‘𝑘) · (𝑥↑𝑘)) ∈ ℂ)
27		ftalem.4	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ ℕ)
28	27	nnnn0d 12674	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
29	28	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → 𝑁 ∈ ℕ₀)
30	19, 29	ffvelcdmd 7090	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → (𝐴‘𝑁) ∈ ℂ)
31	21, 29	expcld 14296	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → (𝑥↑𝑁) ∈ ℂ)
32	30, 31	mulcld 11336	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → ((𝐴‘𝑁) · (𝑥↑𝑁)) ∈ ℂ)
33	3	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → 𝐹 ∈ (Poly‘𝑆))
34		ftalem.2	. . . . . . . . . 10 ⊢ 𝑁 = (deg‘𝐹)
35	4, 34	coeid2 26567	. . . . . . . . 9 ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑥 ∈ ℂ) → (𝐹‘𝑥) = Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑥↑𝑘)))
36	33, 21, 35	syl2anc 596	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → (𝐹‘𝑥) = Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑥↑𝑘)))
37		nn0uz 13010	. . . . . . . . . 10 ⊢ ℕ₀ = (ℤ_≥‘0)
38	29, 37	eleqtrdi 2870	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → 𝑁 ∈ (ℤ_≥‘0))
39		elfznn0 13761	. . . . . . . . . 10 ⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ₀)
40	39, 24	sylan2 605	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) ∧ 𝑘 ∈ (0...𝑁)) → ((𝐴‘𝑘) · (𝑥↑𝑘)) ∈ ℂ)
41		fveq2 6890	. . . . . . . . . 10 ⊢ (𝑘 = 𝑁 → (𝐴‘𝑘) = (𝐴‘𝑁))
42		oveq2 7432	. . . . . . . . . 10 ⊢ (𝑘 = 𝑁 → (𝑥↑𝑘) = (𝑥↑𝑁))
43	41, 42	oveq12d 7442	. . . . . . . . 9 ⊢ (𝑘 = 𝑁 → ((𝐴‘𝑘) · (𝑥↑𝑘)) = ((𝐴‘𝑁) · (𝑥↑𝑁)))
44	38, 40, 43	fsumm1 15926	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑥↑𝑘)) = (Σ𝑘 ∈ (0...(𝑁 − 1))((𝐴‘𝑘) · (𝑥↑𝑘)) + ((𝐴‘𝑁) · (𝑥↑𝑁))))
45	36, 44	eqtrd 2795	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → (𝐹‘𝑥) = (Σ𝑘 ∈ (0...(𝑁 − 1))((𝐴‘𝑘) · (𝑥↑𝑘)) + ((𝐴‘𝑁) · (𝑥↑𝑁))))
46	26, 32, 45	mvrraddd 11734	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → ((𝐹‘𝑥) − ((𝐴‘𝑁) · (𝑥↑𝑁))) = Σ𝑘 ∈ (0...(𝑁 − 1))((𝐴‘𝑘) · (𝑥↑𝑘)))
47	46	fveq2d 6894	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → (abs‘((𝐹‘𝑥) − ((𝐴‘𝑁) · (𝑥↑𝑁)))) = (abs‘Σ𝑘 ∈ (0...(𝑁 − 1))((𝐴‘𝑘) · (𝑥↑𝑘))))
48	26	abscld 15615	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → (abs‘Σ𝑘 ∈ (0...(𝑁 − 1))((𝐴‘𝑘) · (𝑥↑𝑘))) ∈ ℝ)
49	25	abscld 15615	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (abs‘((𝐴‘𝑘) · (𝑥↑𝑘))) ∈ ℝ)
50	18, 49	fsumrecl 15909	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → Σ𝑘 ∈ (0...(𝑁 − 1))(abs‘((𝐴‘𝑘) · (𝑥↑𝑘))) ∈ ℝ)
51	12	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → 𝐸 ∈ ℝ⁺)
52	51	rpred 13171	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → 𝐸 ∈ ℝ)
53	21	abscld 15615	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → (abs‘𝑥) ∈ ℝ)
54	53, 29	reexpcld 14313	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → ((abs‘𝑥)↑𝑁) ∈ ℝ)
55	52, 54	remulcld 11346	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → (𝐸 · ((abs‘𝑥)↑𝑁)) ∈ ℝ)
56	18, 25	fsumabs 15977	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → (abs‘Σ𝑘 ∈ (0...(𝑁 − 1))((𝐴‘𝑘) · (𝑥↑𝑘))) ≤ Σ𝑘 ∈ (0...(𝑁 − 1))(abs‘((𝐴‘𝑘) · (𝑥↑𝑘))))
57	11	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → Σ𝑘 ∈ (0...(𝑁 − 1))(abs‘(𝐴‘𝑘)) ∈ ℝ)
58	27	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → 𝑁 ∈ ℕ)
59		nnm1nn0 12654	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ₀)
60	58, 59	syl 18	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → (𝑁 − 1) ∈ ℕ₀)
61	53, 60	reexpcld 14313	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → ((abs‘𝑥)↑(𝑁 − 1)) ∈ ℝ)
62	57, 61	remulcld 11346	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → (Σ𝑘 ∈ (0...(𝑁 − 1))(abs‘(𝐴‘𝑘)) · ((abs‘𝑥)↑(𝑁 − 1))) ∈ ℝ)
63	10	adantlr 728	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (abs‘(𝐴‘𝑘)) ∈ ℝ)
64	61	adantr 486	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((abs‘𝑥)↑(𝑁 − 1)) ∈ ℝ)
65	63, 64	remulcld 11346	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((abs‘(𝐴‘𝑘)) · ((abs‘𝑥)↑(𝑁 − 1))) ∈ ℝ)
66	20, 23	absmuld 15633	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) ∧ 𝑘 ∈ ℕ₀) → (abs‘((𝐴‘𝑘) · (𝑥↑𝑘))) = ((abs‘(𝐴‘𝑘)) · (abs‘(𝑥↑𝑘))))
67	7, 66	sylan2 605	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (abs‘((𝐴‘𝑘) · (𝑥↑𝑘))) = ((abs‘(𝐴‘𝑘)) · (abs‘(𝑥↑𝑘))))
68	7, 23	sylan2 605	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (𝑥↑𝑘) ∈ ℂ)
69	68	abscld 15615	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (abs‘(𝑥↑𝑘)) ∈ ℝ)
70	7, 20	sylan2 605	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (𝐴‘𝑘) ∈ ℂ)
71	70	absge0d 15623	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → 0 ≤ (abs‘(𝐴‘𝑘)))
72		absexp 15480	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℂ ∧ 𝑘 ∈ ℕ₀) → (abs‘(𝑥↑𝑘)) = ((abs‘𝑥)↑𝑘))
73	21, 7, 72	syl2an 608	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (abs‘(𝑥↑𝑘)) = ((abs‘𝑥)↑𝑘))
74	53	adantr 486	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (abs‘𝑥) ∈ ℝ)
75	15	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → 1 ∈ ℝ)
76	17	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → if(1 ≤ 𝑇, 𝑇, 1) ∈ ℝ)
77		max1 13322	. . . . . . . . . . . . . . . . . 18 ⊢ ((1 ∈ ℝ ∧ 𝑇 ∈ ℝ) → 1 ≤ if(1 ≤ 𝑇, 𝑇, 1))
78	15, 14, 77	sylancr 599	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 1 ≤ if(1 ≤ 𝑇, 𝑇, 1))
79	78	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → 1 ≤ if(1 ≤ 𝑇, 𝑇, 1))
80		simprr 785	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))
81	75, 76, 53, 79, 80	lelttrd 11475	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → 1 < (abs‘𝑥))
82	75, 53, 81	ltled 11465	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → 1 ≤ (abs‘𝑥))
83	82	adantr 486	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → 1 ≤ (abs‘𝑥))
84		elfzuz3 13660	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (0...(𝑁 − 1)) → (𝑁 − 1) ∈ (ℤ_≥‘𝑘))
85	84	adantl 487	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (𝑁 − 1) ∈ (ℤ_≥‘𝑘))
86	74, 83, 85	leexp2ad 14405	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((abs‘𝑥)↑𝑘) ≤ ((abs‘𝑥)↑(𝑁 − 1)))
87	73, 86	eqbrtrd 5126	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (abs‘(𝑥↑𝑘)) ≤ ((abs‘𝑥)↑(𝑁 − 1)))
88	69, 64, 63, 71, 87	lemul2ad 12264	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((abs‘(𝐴‘𝑘)) · (abs‘(𝑥↑𝑘))) ≤ ((abs‘(𝐴‘𝑘)) · ((abs‘𝑥)↑(𝑁 − 1))))
89	67, 88	eqbrtrd 5126	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (abs‘((𝐴‘𝑘) · (𝑥↑𝑘))) ≤ ((abs‘(𝐴‘𝑘)) · ((abs‘𝑥)↑(𝑁 − 1))))
90	18, 49, 65, 89	fsumle 15975	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → Σ𝑘 ∈ (0...(𝑁 − 1))(abs‘((𝐴‘𝑘) · (𝑥↑𝑘))) ≤ Σ𝑘 ∈ (0...(𝑁 − 1))((abs‘(𝐴‘𝑘)) · ((abs‘𝑥)↑(𝑁 − 1))))
91	61	recnd 11344	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → ((abs‘𝑥)↑(𝑁 − 1)) ∈ ℂ)
92	63	recnd 11344	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (abs‘(𝐴‘𝑘)) ∈ ℂ)
93	18, 91, 92	fsummulc1 15960	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → (Σ𝑘 ∈ (0...(𝑁 − 1))(abs‘(𝐴‘𝑘)) · ((abs‘𝑥)↑(𝑁 − 1))) = Σ𝑘 ∈ (0...(𝑁 − 1))((abs‘(𝐴‘𝑘)) · ((abs‘𝑥)↑(𝑁 − 1))))
94	90, 93	breqtrrd 5132	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → Σ𝑘 ∈ (0...(𝑁 − 1))(abs‘((𝐴‘𝑘) · (𝑥↑𝑘))) ≤ (Σ𝑘 ∈ (0...(𝑁 − 1))(abs‘(𝐴‘𝑘)) · ((abs‘𝑥)↑(𝑁 − 1))))
95	14	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → 𝑇 ∈ ℝ)
96		max2 13324	. . . . . . . . . . . . . 14 ⊢ ((1 ∈ ℝ ∧ 𝑇 ∈ ℝ) → 𝑇 ≤ if(1 ≤ 𝑇, 𝑇, 1))
97	15, 14, 96	sylancr 599	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑇 ≤ if(1 ≤ 𝑇, 𝑇, 1))
98	97	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → 𝑇 ≤ if(1 ≤ 𝑇, 𝑇, 1))
99	95, 76, 53, 98, 80	lelttrd 11475	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → 𝑇 < (abs‘𝑥))
100	1, 99	eqbrtrrid 5140	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → (Σ𝑘 ∈ (0...(𝑁 − 1))(abs‘(𝐴‘𝑘)) / 𝐸) < (abs‘𝑥))
101	57, 53, 51	ltdivmuld 13222	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → ((Σ𝑘 ∈ (0...(𝑁 − 1))(abs‘(𝐴‘𝑘)) / 𝐸) < (abs‘𝑥) ↔ Σ𝑘 ∈ (0...(𝑁 − 1))(abs‘(𝐴‘𝑘)) < (𝐸 · (abs‘𝑥))))
102	100, 101	mpbid 235	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → Σ𝑘 ∈ (0...(𝑁 − 1))(abs‘(𝐴‘𝑘)) < (𝐸 · (abs‘𝑥)))
103	52, 53	remulcld 11346	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → (𝐸 · (abs‘𝑥)) ∈ ℝ)
104	60	nn0zd 12725	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → (𝑁 − 1) ∈ ℤ)
105		0red 11318	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → 0 ∈ ℝ)
106		0lt1 11845	. . . . . . . . . . . . 13 ⊢ 0 < 1
107	106	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → 0 < 1)
108	105, 75, 53, 107, 81	lttrd 11478	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → 0 < (abs‘𝑥))
109		expgt0 14245	. . . . . . . . . . 11 ⊢ (((abs‘𝑥) ∈ ℝ ∧ (𝑁 − 1) ∈ ℤ ∧ 0 < (abs‘𝑥)) → 0 < ((abs‘𝑥)↑(𝑁 − 1)))
110	53, 104, 108, 109	syl3anc 1398	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → 0 < ((abs‘𝑥)↑(𝑁 − 1)))
111		ltmul1 12174	. . . . . . . . . 10 ⊢ ((Σ𝑘 ∈ (0...(𝑁 − 1))(abs‘(𝐴‘𝑘)) ∈ ℝ ∧ (𝐸 · (abs‘𝑥)) ∈ ℝ ∧ (((abs‘𝑥)↑(𝑁 − 1)) ∈ ℝ ∧ 0 < ((abs‘𝑥)↑(𝑁 − 1)))) → (Σ𝑘 ∈ (0...(𝑁 − 1))(abs‘(𝐴‘𝑘)) < (𝐸 · (abs‘𝑥)) ↔ (Σ𝑘 ∈ (0...(𝑁 − 1))(abs‘(𝐴‘𝑘)) · ((abs‘𝑥)↑(𝑁 − 1))) < ((𝐸 · (abs‘𝑥)) · ((abs‘𝑥)↑(𝑁 − 1)))))
112	57, 103, 61, 110, 111	syl112anc 1401	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → (Σ𝑘 ∈ (0...(𝑁 − 1))(abs‘(𝐴‘𝑘)) < (𝐸 · (abs‘𝑥)) ↔ (Σ𝑘 ∈ (0...(𝑁 − 1))(abs‘(𝐴‘𝑘)) · ((abs‘𝑥)↑(𝑁 − 1))) < ((𝐸 · (abs‘𝑥)) · ((abs‘𝑥)↑(𝑁 − 1)))))
113	102, 112	mpbid 235	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → (Σ𝑘 ∈ (0...(𝑁 − 1))(abs‘(𝐴‘𝑘)) · ((abs‘𝑥)↑(𝑁 − 1))) < ((𝐸 · (abs‘𝑥)) · ((abs‘𝑥)↑(𝑁 − 1))))
114	53	recnd 11344	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → (abs‘𝑥) ∈ ℂ)
115		expm1t 14240	. . . . . . . . . . . 12 ⊢ (((abs‘𝑥) ∈ ℂ ∧ 𝑁 ∈ ℕ) → ((abs‘𝑥)↑𝑁) = (((abs‘𝑥)↑(𝑁 − 1)) · (abs‘𝑥)))
116	114, 58, 115	syl2anc 596	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → ((abs‘𝑥)↑𝑁) = (((abs‘𝑥)↑(𝑁 − 1)) · (abs‘𝑥)))
117	91, 114	mulcomd 11337	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → (((abs‘𝑥)↑(𝑁 − 1)) · (abs‘𝑥)) = ((abs‘𝑥) · ((abs‘𝑥)↑(𝑁 − 1))))
118	116, 117	eqtrd 2795	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → ((abs‘𝑥)↑𝑁) = ((abs‘𝑥) · ((abs‘𝑥)↑(𝑁 − 1))))
119	118	oveq2d 7440	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → (𝐸 · ((abs‘𝑥)↑𝑁)) = (𝐸 · ((abs‘𝑥) · ((abs‘𝑥)↑(𝑁 − 1)))))
120	52	recnd 11344	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → 𝐸 ∈ ℂ)
121	120, 114, 91	mulassd 11339	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → ((𝐸 · (abs‘𝑥)) · ((abs‘𝑥)↑(𝑁 − 1))) = (𝐸 · ((abs‘𝑥) · ((abs‘𝑥)↑(𝑁 − 1)))))
122	119, 121	eqtr4d 2798	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → (𝐸 · ((abs‘𝑥)↑𝑁)) = ((𝐸 · (abs‘𝑥)) · ((abs‘𝑥)↑(𝑁 − 1))))
123	113, 122	breqtrrd 5132	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → (Σ𝑘 ∈ (0...(𝑁 − 1))(abs‘(𝐴‘𝑘)) · ((abs‘𝑥)↑(𝑁 − 1))) < (𝐸 · ((abs‘𝑥)↑𝑁)))
124	50, 62, 55, 94, 123	lelttrd 11475	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → Σ𝑘 ∈ (0...(𝑁 − 1))(abs‘((𝐴‘𝑘) · (𝑥↑𝑘))) < (𝐸 · ((abs‘𝑥)↑𝑁)))
125	48, 50, 55, 56, 124	lelttrd 11475	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → (abs‘Σ𝑘 ∈ (0...(𝑁 − 1))((𝐴‘𝑘) · (𝑥↑𝑘))) < (𝐸 · ((abs‘𝑥)↑𝑁)))
126	47, 125	eqbrtrd 5126	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → (abs‘((𝐹‘𝑥) − ((𝐴‘𝑁) · (𝑥↑𝑁)))) < (𝐸 · ((abs‘𝑥)↑𝑁)))
127	126	expr 462	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥) → (abs‘((𝐹‘𝑥) − ((𝐴‘𝑁) · (𝑥↑𝑁)))) < (𝐸 · ((abs‘𝑥)↑𝑁))))
128	127	ralrimiva 3154	. 2 ⊢ (𝜑 → ∀𝑥 ∈ ℂ (if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥) → (abs‘((𝐹‘𝑥) − ((𝐴‘𝑁) · (𝑥↑𝑁)))) < (𝐸 · ((abs‘𝑥)↑𝑁))))
129		breq1 5105	. . 3 ⊢ (𝑟 = if(1 ≤ 𝑇, 𝑇, 1) → (𝑟 < (abs‘𝑥) ↔ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥)))
130	129	rspceaimv 3582	. 2 ⊢ ((if(1 ≤ 𝑇, 𝑇, 1) ∈ ℝ ∧ ∀𝑥 ∈ ℂ (if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥) → (abs‘((𝐹‘𝑥) − ((𝐴‘𝑁) · (𝑥↑𝑁)))) < (𝐸 · ((abs‘𝑥)↑𝑁)))) → ∃𝑟 ∈ ℝ ∀𝑥 ∈ ℂ (𝑟 < (abs‘𝑥) → (abs‘((𝐹‘𝑥) − ((𝐴‘𝑁) · (𝑥↑𝑁)))) < (𝐸 · ((abs‘𝑥)↑𝑁))))
131	17, 128, 130	syl2anc 596	1 ⊢ (𝜑 → ∃𝑟 ∈ ℝ ∀𝑥 ∈ ℂ (𝑟 < (abs‘𝑥) → (abs‘((𝐹‘𝑥) − ((𝐴‘𝑁) · (𝑥↑𝑁)))) < (𝐸 · ((abs‘𝑥)↑𝑁))))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1569 ∈ wcel 2144 ∀wral 3076 ∃wrex 3086 ifcif 4481 class class class wbr 5102 ⟶wf 6539 ‘cfv 6543 (class class class)co 7424 ℂcc 11205 ℝcr 11206 0cc0 11207 1c1 11208 + caddc 11210 · cmul 11212 < clt 11350 ≤ cle 11351 − cmin 11548 / cdiv 11980 ℕcn 12342 ℕ₀cn0 12613 ℤcz 12700 ℤ_≥cuz 12972 ℝ⁺crp 13127 ...cfz 13646 ↑cexp 14211 abscabs 15410 Σcsu 15862 Polycply 26511 coeffccoe 26513 degcdgr 26514

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5327 ax-pr 5391 ax-un 7755 ax-inf2 9649 ax-cnex 11263 ax-resscn 11264 ax-1cn 11265 ax-icn 11266 ax-addcl 11267 ax-addrcl 11268 ax-mulcl 11269 ax-mulrcl 11270 ax-mulcom 11271 ax-addass 11272 ax-mulass 11273 ax-distr 11274 ax-i2m1 11275 ax-1ne0 11276 ax-1rid 11277 ax-rnegex 11278 ax-rrecex 11279 ax-cnre 11280 ax-pre-lttri 11281 ax-pre-lttrn 11282 ax-pre-ltadd 11283 ax-pre-mulgt0 11284 ax-pre-sup 11285

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3848 df-ss 3897 df-pss 4013 df-dif 4046 df-in 4090 df-un 4150 df-nul 4278 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-op 4835 df-uni 4867 df-int 4907 df-iun 4952 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-se 5605 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6307 df-ord 6368 df-on 6369 df-lim 6370 df-suc 6371 df-iota 6497 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-isom 6552 df-riota 7381 df-ov 7427 df-oprab 7428 df-mpo 7429 df-of 7697 df-om 7882 df-1st 8005 df-2nd 8006 df-frecs 8307 df-wrecs 8338 df-recs 8387 df-rdg 8426 df-1o 8484 df-er 8725 df-map 8857 df-pm 8858 df-en 8982 df-dom 8983 df-sdom 8984 df-fin 8985 df-sup 9441 df-inf 9442 df-oi 9511 df-card 10027 df-pnf 11352 df-mnf 11353 df-xr 11354 df-ltxr 11355 df-le 11356 df-sub 11550 df-neg 11551 df-div 11981 df-nn 12343 df-2 12412 df-3 12413 df-n0 12614 df-z 12701 df-uz 12973 df-rp 13128 df-ico 13489 df-fz 13647 df-fzo 13796 df-fl 13939 df-seq 14152 df-exp 14212 df-hash 14482 df-cj 15275 df-re 15276 df-im 15277 df-sqrt 15411 df-abs 15412 df-clim 15664 df-rlim 15665 df-sum 15863 df-0p 26000 df-ply 26515 df-coe 26517 df-dgr 26518

This theorem is used by: ftalem2 27410

W3C validator