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 25251

Description: Lemma for fta 25258: "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 13091	. . . . . 6 ⊢ (𝜑 → (0...(𝑁 − 1)) ∈ Fin)
3		ftalem.3	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆))
4		ftalem.1	. . . . . . . . . 10 ⊢ 𝐴 = (coeff‘𝐹)
5	4	coef3 24425	. . . . . . . . 9 ⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐴:ℕ₀⟶ℂ)
6	3, 5	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐴:ℕ₀⟶ℂ)
7		elfznn0 12751	. . . . . . . 8 ⊢ (𝑘 ∈ (0...(𝑁 − 1)) → 𝑘 ∈ ℕ₀)
8		ffvelrn 6621	. . . . . . . 8 ⊢ ((𝐴:ℕ₀⟶ℂ ∧ 𝑘 ∈ ℕ₀) → (𝐴‘𝑘) ∈ ℂ)
9	6, 7, 8	syl2an 589	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (𝐴‘𝑘) ∈ ℂ)
10	9	abscld 14583	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (abs‘(𝐴‘𝑘)) ∈ ℝ)
11	2, 10	fsumrecl 14872	. . . . 5 ⊢ (𝜑 → Σ𝑘 ∈ (0...(𝑁 − 1))(abs‘(𝐴‘𝑘)) ∈ ℝ)
12		ftalem1.5	. . . . 5 ⊢ (𝜑 → 𝐸 ∈ ℝ⁺)
13	11, 12	rerpdivcld 12212	. . . 4 ⊢ (𝜑 → (Σ𝑘 ∈ (0...(𝑁 − 1))(abs‘(𝐴‘𝑘)) / 𝐸) ∈ ℝ)
14	1, 13	syl5eqel 2863	. . 3 ⊢ (𝜑 → 𝑇 ∈ ℝ)
15		1re 10376	. . 3 ⊢ 1 ∈ ℝ
16		ifcl 4351	. . 3 ⊢ ((𝑇 ∈ ℝ ∧ 1 ∈ ℝ) → if(1 ≤ 𝑇, 𝑇, 1) ∈ ℝ)
17	14, 15, 16	sylancl 580	. 2 ⊢ (𝜑 → if(1 ≤ 𝑇, 𝑇, 1) ∈ ℝ)
18	3	adantr 474	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → 𝐹 ∈ (Poly‘𝑆))
19		simprl 761	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → 𝑥 ∈ ℂ)
20		ftalem.2	. . . . . . . . . . 11 ⊢ 𝑁 = (deg‘𝐹)
21	4, 20	coeid2 24432	. . . . . . . . . 10 ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑥 ∈ ℂ) → (𝐹‘𝑥) = Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑥↑𝑘)))
22	18, 19, 21	syl2anc 579	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → (𝐹‘𝑥) = Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑥↑𝑘)))
23		ftalem.4	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ ℕ)
24	23	nnnn0d 11702	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
25	24	adantr 474	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → 𝑁 ∈ ℕ₀)
26		nn0uz 12028	. . . . . . . . . . 11 ⊢ ℕ₀ = (ℤ_≥‘0)
27	25, 26	syl6eleq 2869	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → 𝑁 ∈ (ℤ_≥‘0))
28		elfznn0 12751	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ₀)
29	6	adantr 474	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → 𝐴:ℕ₀⟶ℂ)
30	29, 8	sylan 575	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) ∧ 𝑘 ∈ ℕ₀) → (𝐴‘𝑘) ∈ ℂ)
31		expcl 13196	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℂ ∧ 𝑘 ∈ ℕ₀) → (𝑥↑𝑘) ∈ ℂ)
32	19, 31	sylan 575	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) ∧ 𝑘 ∈ ℕ₀) → (𝑥↑𝑘) ∈ ℂ)
33	30, 32	mulcld 10397	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) ∧ 𝑘 ∈ ℕ₀) → ((𝐴‘𝑘) · (𝑥↑𝑘)) ∈ ℂ)
34	28, 33	sylan2 586	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) ∧ 𝑘 ∈ (0...𝑁)) → ((𝐴‘𝑘) · (𝑥↑𝑘)) ∈ ℂ)
35		fveq2 6446	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑁 → (𝐴‘𝑘) = (𝐴‘𝑁))
36		oveq2 6930	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑁 → (𝑥↑𝑘) = (𝑥↑𝑁))
37	35, 36	oveq12d 6940	. . . . . . . . . 10 ⊢ (𝑘 = 𝑁 → ((𝐴‘𝑘) · (𝑥↑𝑘)) = ((𝐴‘𝑁) · (𝑥↑𝑁)))
38	27, 34, 37	fsumm1 14887	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑥↑𝑘)) = (Σ𝑘 ∈ (0...(𝑁 − 1))((𝐴‘𝑘) · (𝑥↑𝑘)) + ((𝐴‘𝑁) · (𝑥↑𝑁))))
39	22, 38	eqtrd 2814	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → (𝐹‘𝑥) = (Σ𝑘 ∈ (0...(𝑁 − 1))((𝐴‘𝑘) · (𝑥↑𝑘)) + ((𝐴‘𝑁) · (𝑥↑𝑁))))
40	39	oveq1d 6937	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → ((𝐹‘𝑥) − ((𝐴‘𝑁) · (𝑥↑𝑁))) = ((Σ𝑘 ∈ (0...(𝑁 − 1))((𝐴‘𝑘) · (𝑥↑𝑘)) + ((𝐴‘𝑁) · (𝑥↑𝑁))) − ((𝐴‘𝑁) · (𝑥↑𝑁))))
41		fzfid 13091	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → (0...(𝑁 − 1)) ∈ Fin)
42	7, 33	sylan2 586	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((𝐴‘𝑘) · (𝑥↑𝑘)) ∈ ℂ)
43	41, 42	fsumcl 14871	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → Σ𝑘 ∈ (0...(𝑁 − 1))((𝐴‘𝑘) · (𝑥↑𝑘)) ∈ ℂ)
44	29, 25	ffvelrnd 6624	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → (𝐴‘𝑁) ∈ ℂ)
45	19, 25	expcld 13327	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → (𝑥↑𝑁) ∈ ℂ)
46	44, 45	mulcld 10397	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → ((𝐴‘𝑁) · (𝑥↑𝑁)) ∈ ℂ)
47	43, 46	pncand 10735	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → ((Σ𝑘 ∈ (0...(𝑁 − 1))((𝐴‘𝑘) · (𝑥↑𝑘)) + ((𝐴‘𝑁) · (𝑥↑𝑁))) − ((𝐴‘𝑁) · (𝑥↑𝑁))) = Σ𝑘 ∈ (0...(𝑁 − 1))((𝐴‘𝑘) · (𝑥↑𝑘)))
48	40, 47	eqtrd 2814	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → ((𝐹‘𝑥) − ((𝐴‘𝑁) · (𝑥↑𝑁))) = Σ𝑘 ∈ (0...(𝑁 − 1))((𝐴‘𝑘) · (𝑥↑𝑘)))
49	48	fveq2d 6450	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → (abs‘((𝐹‘𝑥) − ((𝐴‘𝑁) · (𝑥↑𝑁)))) = (abs‘Σ𝑘 ∈ (0...(𝑁 − 1))((𝐴‘𝑘) · (𝑥↑𝑘))))
50	43	abscld 14583	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → (abs‘Σ𝑘 ∈ (0...(𝑁 − 1))((𝐴‘𝑘) · (𝑥↑𝑘))) ∈ ℝ)
51	42	abscld 14583	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (abs‘((𝐴‘𝑘) · (𝑥↑𝑘))) ∈ ℝ)
52	41, 51	fsumrecl 14872	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → Σ𝑘 ∈ (0...(𝑁 − 1))(abs‘((𝐴‘𝑘) · (𝑥↑𝑘))) ∈ ℝ)
53	12	adantr 474	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → 𝐸 ∈ ℝ⁺)
54	53	rpred 12181	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → 𝐸 ∈ ℝ)
55	19	abscld 14583	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → (abs‘𝑥) ∈ ℝ)
56	55, 25	reexpcld 13344	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → ((abs‘𝑥)↑𝑁) ∈ ℝ)
57	54, 56	remulcld 10407	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → (𝐸 · ((abs‘𝑥)↑𝑁)) ∈ ℝ)
58	41, 42	fsumabs 14937	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → (abs‘Σ𝑘 ∈ (0...(𝑁 − 1))((𝐴‘𝑘) · (𝑥↑𝑘))) ≤ Σ𝑘 ∈ (0...(𝑁 − 1))(abs‘((𝐴‘𝑘) · (𝑥↑𝑘))))
59	11	adantr 474	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → Σ𝑘 ∈ (0...(𝑁 − 1))(abs‘(𝐴‘𝑘)) ∈ ℝ)
60	23	adantr 474	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → 𝑁 ∈ ℕ)
61		nnm1nn0 11685	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ₀)
62	60, 61	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → (𝑁 − 1) ∈ ℕ₀)
63	55, 62	reexpcld 13344	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → ((abs‘𝑥)↑(𝑁 − 1)) ∈ ℝ)
64	59, 63	remulcld 10407	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → (Σ𝑘 ∈ (0...(𝑁 − 1))(abs‘(𝐴‘𝑘)) · ((abs‘𝑥)↑(𝑁 − 1))) ∈ ℝ)
65	10	adantlr 705	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (abs‘(𝐴‘𝑘)) ∈ ℝ)
66	63	adantr 474	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((abs‘𝑥)↑(𝑁 − 1)) ∈ ℝ)
67	65, 66	remulcld 10407	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((abs‘(𝐴‘𝑘)) · ((abs‘𝑥)↑(𝑁 − 1))) ∈ ℝ)
68	30, 32	absmuld 14601	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) ∧ 𝑘 ∈ ℕ₀) → (abs‘((𝐴‘𝑘) · (𝑥↑𝑘))) = ((abs‘(𝐴‘𝑘)) · (abs‘(𝑥↑𝑘))))
69	7, 68	sylan2 586	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (abs‘((𝐴‘𝑘) · (𝑥↑𝑘))) = ((abs‘(𝐴‘𝑘)) · (abs‘(𝑥↑𝑘))))
70	7, 32	sylan2 586	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (𝑥↑𝑘) ∈ ℂ)
71	70	abscld 14583	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (abs‘(𝑥↑𝑘)) ∈ ℝ)
72	7, 30	sylan2 586	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (𝐴‘𝑘) ∈ ℂ)
73	72	absge0d 14591	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → 0 ≤ (abs‘(𝐴‘𝑘)))
74		absexp 14451	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℂ ∧ 𝑘 ∈ ℕ₀) → (abs‘(𝑥↑𝑘)) = ((abs‘𝑥)↑𝑘))
75	19, 7, 74	syl2an 589	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (abs‘(𝑥↑𝑘)) = ((abs‘𝑥)↑𝑘))
76	55	adantr 474	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (abs‘𝑥) ∈ ℝ)
77	15	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → 1 ∈ ℝ)
78	17	adantr 474	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → if(1 ≤ 𝑇, 𝑇, 1) ∈ ℝ)
79		max1 12328	. . . . . . . . . . . . . . . . . 18 ⊢ ((1 ∈ ℝ ∧ 𝑇 ∈ ℝ) → 1 ≤ if(1 ≤ 𝑇, 𝑇, 1))
80	15, 14, 79	sylancr 581	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 1 ≤ if(1 ≤ 𝑇, 𝑇, 1))
81	80	adantr 474	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → 1 ≤ if(1 ≤ 𝑇, 𝑇, 1))
82		simprr 763	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))
83	77, 78, 55, 81, 82	lelttrd 10534	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → 1 < (abs‘𝑥))
84	77, 55, 83	ltled 10524	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → 1 ≤ (abs‘𝑥))
85	84	adantr 474	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → 1 ≤ (abs‘𝑥))
86		elfzuz3 12656	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (0...(𝑁 − 1)) → (𝑁 − 1) ∈ (ℤ_≥‘𝑘))
87	86	adantl 475	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (𝑁 − 1) ∈ (ℤ_≥‘𝑘))
88	76, 85, 87	leexp2ad 13362	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((abs‘𝑥)↑𝑘) ≤ ((abs‘𝑥)↑(𝑁 − 1)))
89	75, 88	eqbrtrd 4908	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (abs‘(𝑥↑𝑘)) ≤ ((abs‘𝑥)↑(𝑁 − 1)))
90	71, 66, 65, 73, 89	lemul2ad 11318	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((abs‘(𝐴‘𝑘)) · (abs‘(𝑥↑𝑘))) ≤ ((abs‘(𝐴‘𝑘)) · ((abs‘𝑥)↑(𝑁 − 1))))
91	69, 90	eqbrtrd 4908	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (abs‘((𝐴‘𝑘) · (𝑥↑𝑘))) ≤ ((abs‘(𝐴‘𝑘)) · ((abs‘𝑥)↑(𝑁 − 1))))
92	41, 51, 67, 91	fsumle 14935	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → Σ𝑘 ∈ (0...(𝑁 − 1))(abs‘((𝐴‘𝑘) · (𝑥↑𝑘))) ≤ Σ𝑘 ∈ (0...(𝑁 − 1))((abs‘(𝐴‘𝑘)) · ((abs‘𝑥)↑(𝑁 − 1))))
93	63	recnd 10405	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → ((abs‘𝑥)↑(𝑁 − 1)) ∈ ℂ)
94	65	recnd 10405	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (abs‘(𝐴‘𝑘)) ∈ ℂ)
95	41, 93, 94	fsummulc1 14921	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → (Σ𝑘 ∈ (0...(𝑁 − 1))(abs‘(𝐴‘𝑘)) · ((abs‘𝑥)↑(𝑁 − 1))) = Σ𝑘 ∈ (0...(𝑁 − 1))((abs‘(𝐴‘𝑘)) · ((abs‘𝑥)↑(𝑁 − 1))))
96	92, 95	breqtrrd 4914	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → Σ𝑘 ∈ (0...(𝑁 − 1))(abs‘((𝐴‘𝑘) · (𝑥↑𝑘))) ≤ (Σ𝑘 ∈ (0...(𝑁 − 1))(abs‘(𝐴‘𝑘)) · ((abs‘𝑥)↑(𝑁 − 1))))
97	14	adantr 474	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → 𝑇 ∈ ℝ)
98		max2 12330	. . . . . . . . . . . . . 14 ⊢ ((1 ∈ ℝ ∧ 𝑇 ∈ ℝ) → 𝑇 ≤ if(1 ≤ 𝑇, 𝑇, 1))
99	15, 14, 98	sylancr 581	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑇 ≤ if(1 ≤ 𝑇, 𝑇, 1))
100	99	adantr 474	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → 𝑇 ≤ if(1 ≤ 𝑇, 𝑇, 1))
101	97, 78, 55, 100, 82	lelttrd 10534	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → 𝑇 < (abs‘𝑥))
102	1, 101	syl5eqbrr 4922	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → (Σ𝑘 ∈ (0...(𝑁 − 1))(abs‘(𝐴‘𝑘)) / 𝐸) < (abs‘𝑥))
103	59, 55, 53	ltdivmuld 12232	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → ((Σ𝑘 ∈ (0...(𝑁 − 1))(abs‘(𝐴‘𝑘)) / 𝐸) < (abs‘𝑥) ↔ Σ𝑘 ∈ (0...(𝑁 − 1))(abs‘(𝐴‘𝑘)) < (𝐸 · (abs‘𝑥))))
104	102, 103	mpbid 224	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → Σ𝑘 ∈ (0...(𝑁 − 1))(abs‘(𝐴‘𝑘)) < (𝐸 · (abs‘𝑥)))
105	54, 55	remulcld 10407	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → (𝐸 · (abs‘𝑥)) ∈ ℝ)
106	62	nn0zd 11832	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → (𝑁 − 1) ∈ ℤ)
107		0red 10380	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → 0 ∈ ℝ)
108		0lt1 10897	. . . . . . . . . . . . 13 ⊢ 0 < 1
109	108	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → 0 < 1)
110	107, 77, 55, 109, 83	lttrd 10537	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → 0 < (abs‘𝑥))
111		expgt0 13211	. . . . . . . . . . 11 ⊢ (((abs‘𝑥) ∈ ℝ ∧ (𝑁 − 1) ∈ ℤ ∧ 0 < (abs‘𝑥)) → 0 < ((abs‘𝑥)↑(𝑁 − 1)))
112	55, 106, 110, 111	syl3anc 1439	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → 0 < ((abs‘𝑥)↑(𝑁 − 1)))
113		ltmul1 11227	. . . . . . . . . 10 ⊢ ((Σ𝑘 ∈ (0...(𝑁 − 1))(abs‘(𝐴‘𝑘)) ∈ ℝ ∧ (𝐸 · (abs‘𝑥)) ∈ ℝ ∧ (((abs‘𝑥)↑(𝑁 − 1)) ∈ ℝ ∧ 0 < ((abs‘𝑥)↑(𝑁 − 1)))) → (Σ𝑘 ∈ (0...(𝑁 − 1))(abs‘(𝐴‘𝑘)) < (𝐸 · (abs‘𝑥)) ↔ (Σ𝑘 ∈ (0...(𝑁 − 1))(abs‘(𝐴‘𝑘)) · ((abs‘𝑥)↑(𝑁 − 1))) < ((𝐸 · (abs‘𝑥)) · ((abs‘𝑥)↑(𝑁 − 1)))))
114	59, 105, 63, 112, 113	syl112anc 1442	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → (Σ𝑘 ∈ (0...(𝑁 − 1))(abs‘(𝐴‘𝑘)) < (𝐸 · (abs‘𝑥)) ↔ (Σ𝑘 ∈ (0...(𝑁 − 1))(abs‘(𝐴‘𝑘)) · ((abs‘𝑥)↑(𝑁 − 1))) < ((𝐸 · (abs‘𝑥)) · ((abs‘𝑥)↑(𝑁 − 1)))))
115	104, 114	mpbid 224	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → (Σ𝑘 ∈ (0...(𝑁 − 1))(abs‘(𝐴‘𝑘)) · ((abs‘𝑥)↑(𝑁 − 1))) < ((𝐸 · (abs‘𝑥)) · ((abs‘𝑥)↑(𝑁 − 1))))
116	55	recnd 10405	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → (abs‘𝑥) ∈ ℂ)
117		expm1t 13206	. . . . . . . . . . . 12 ⊢ (((abs‘𝑥) ∈ ℂ ∧ 𝑁 ∈ ℕ) → ((abs‘𝑥)↑𝑁) = (((abs‘𝑥)↑(𝑁 − 1)) · (abs‘𝑥)))
118	116, 60, 117	syl2anc 579	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → ((abs‘𝑥)↑𝑁) = (((abs‘𝑥)↑(𝑁 − 1)) · (abs‘𝑥)))
119	93, 116	mulcomd 10398	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → (((abs‘𝑥)↑(𝑁 − 1)) · (abs‘𝑥)) = ((abs‘𝑥) · ((abs‘𝑥)↑(𝑁 − 1))))
120	118, 119	eqtrd 2814	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → ((abs‘𝑥)↑𝑁) = ((abs‘𝑥) · ((abs‘𝑥)↑(𝑁 − 1))))
121	120	oveq2d 6938	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → (𝐸 · ((abs‘𝑥)↑𝑁)) = (𝐸 · ((abs‘𝑥) · ((abs‘𝑥)↑(𝑁 − 1)))))
122	54	recnd 10405	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → 𝐸 ∈ ℂ)
123	122, 116, 93	mulassd 10400	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → ((𝐸 · (abs‘𝑥)) · ((abs‘𝑥)↑(𝑁 − 1))) = (𝐸 · ((abs‘𝑥) · ((abs‘𝑥)↑(𝑁 − 1)))))
124	121, 123	eqtr4d 2817	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → (𝐸 · ((abs‘𝑥)↑𝑁)) = ((𝐸 · (abs‘𝑥)) · ((abs‘𝑥)↑(𝑁 − 1))))
125	115, 124	breqtrrd 4914	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → (Σ𝑘 ∈ (0...(𝑁 − 1))(abs‘(𝐴‘𝑘)) · ((abs‘𝑥)↑(𝑁 − 1))) < (𝐸 · ((abs‘𝑥)↑𝑁)))
126	52, 64, 57, 96, 125	lelttrd 10534	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → Σ𝑘 ∈ (0...(𝑁 − 1))(abs‘((𝐴‘𝑘) · (𝑥↑𝑘))) < (𝐸 · ((abs‘𝑥)↑𝑁)))
127	50, 52, 57, 58, 126	lelttrd 10534	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → (abs‘Σ𝑘 ∈ (0...(𝑁 − 1))((𝐴‘𝑘) · (𝑥↑𝑘))) < (𝐸 · ((abs‘𝑥)↑𝑁)))
128	49, 127	eqbrtrd 4908	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥))) → (abs‘((𝐹‘𝑥) − ((𝐴‘𝑁) · (𝑥↑𝑁)))) < (𝐸 · ((abs‘𝑥)↑𝑁)))
129	128	expr 450	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥) → (abs‘((𝐹‘𝑥) − ((𝐴‘𝑁) · (𝑥↑𝑁)))) < (𝐸 · ((abs‘𝑥)↑𝑁))))
130	129	ralrimiva 3148	. 2 ⊢ (𝜑 → ∀𝑥 ∈ ℂ (if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥) → (abs‘((𝐹‘𝑥) − ((𝐴‘𝑁) · (𝑥↑𝑁)))) < (𝐸 · ((abs‘𝑥)↑𝑁))))
131		breq1 4889	. . 3 ⊢ (𝑟 = if(1 ≤ 𝑇, 𝑇, 1) → (𝑟 < (abs‘𝑥) ↔ if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥)))
132	131	rspceaimv 3519	. 2 ⊢ ((if(1 ≤ 𝑇, 𝑇, 1) ∈ ℝ ∧ ∀𝑥 ∈ ℂ (if(1 ≤ 𝑇, 𝑇, 1) < (abs‘𝑥) → (abs‘((𝐹‘𝑥) − ((𝐴‘𝑁) · (𝑥↑𝑁)))) < (𝐸 · ((abs‘𝑥)↑𝑁)))) → ∃𝑟 ∈ ℝ ∀𝑥 ∈ ℂ (𝑟 < (abs‘𝑥) → (abs‘((𝐹‘𝑥) − ((𝐴‘𝑁) · (𝑥↑𝑁)))) < (𝐸 · ((abs‘𝑥)↑𝑁))))
133	17, 130, 132	syl2anc 579	1 ⊢ (𝜑 → ∃𝑟 ∈ ℝ ∀𝑥 ∈ ℂ (𝑟 < (abs‘𝑥) → (abs‘((𝐹‘𝑥) − ((𝐴‘𝑁) · (𝑥↑𝑁)))) < (𝐸 · ((abs‘𝑥)↑𝑁))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 198 ∧ wa 386 = wceq 1601 ∈ wcel 2107 ∀wral 3090 ∃wrex 3091 ifcif 4307 class class class wbr 4886 ⟶wf 6131 ‘cfv 6135 (class class class)co 6922 ℂcc 10270 ℝcr 10271 0cc0 10272 1c1 10273 + caddc 10275 · cmul 10277 < clt 10411 ≤ cle 10412 − cmin 10606 / cdiv 11032 ℕcn 11374 ℕ₀cn0 11642 ℤcz 11728 ℤ_≥cuz 11992 ℝ⁺crp 12137 ...cfz 12643 ↑cexp 13178 abscabs 14381 Σcsu 14824 Polycply 24377 coeffccoe 24379 degcdgr 24380

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-8 2109 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-13 2334 ax-ext 2754 ax-rep 5006 ax-sep 5017 ax-nul 5025 ax-pow 5077 ax-pr 5138 ax-un 7226 ax-inf2 8835 ax-cnex 10328 ax-resscn 10329 ax-1cn 10330 ax-icn 10331 ax-addcl 10332 ax-addrcl 10333 ax-mulcl 10334 ax-mulrcl 10335 ax-mulcom 10336 ax-addass 10337 ax-mulass 10338 ax-distr 10339 ax-i2m1 10340 ax-1ne0 10341 ax-1rid 10342 ax-rnegex 10343 ax-rrecex 10344 ax-cnre 10345 ax-pre-lttri 10346 ax-pre-lttrn 10347 ax-pre-ltadd 10348 ax-pre-mulgt0 10349 ax-pre-sup 10350 ax-addf 10351

This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-3or 1072 df-3an 1073 df-tru 1605 df-fal 1615 df-ex 1824 df-nf 1828 df-sb 2012 df-mo 2551 df-eu 2587 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-ne 2970 df-nel 3076 df-ral 3095 df-rex 3096 df-reu 3097 df-rmo 3098 df-rab 3099 df-v 3400 df-sbc 3653 df-csb 3752 df-dif 3795 df-un 3797 df-in 3799 df-ss 3806 df-pss 3808 df-nul 4142 df-if 4308 df-pw 4381 df-sn 4399 df-pr 4401 df-tp 4403 df-op 4405 df-uni 4672 df-int 4711 df-iun 4755 df-br 4887 df-opab 4949 df-mpt 4966 df-tr 4988 df-id 5261 df-eprel 5266 df-po 5274 df-so 5275 df-fr 5314 df-se 5315 df-we 5316 df-xp 5361 df-rel 5362 df-cnv 5363 df-co 5364 df-dm 5365 df-rn 5366 df-res 5367 df-ima 5368 df-pred 5933 df-ord 5979 df-on 5980 df-lim 5981 df-suc 5982 df-iota 6099 df-fun 6137 df-fn 6138 df-f 6139 df-f1 6140 df-fo 6141 df-f1o 6142 df-fv 6143 df-isom 6144 df-riota 6883 df-ov 6925 df-oprab 6926 df-mpt2 6927 df-of 7174 df-om 7344 df-1st 7445 df-2nd 7446 df-wrecs 7689 df-recs 7751 df-rdg 7789 df-1o 7843 df-oadd 7847 df-er 8026 df-map 8142 df-pm 8143 df-en 8242 df-dom 8243 df-sdom 8244 df-fin 8245 df-sup 8636 df-inf 8637 df-oi 8704 df-card 9098 df-pnf 10413 df-mnf 10414 df-xr 10415 df-ltxr 10416 df-le 10417 df-sub 10608 df-neg 10609 df-div 11033 df-nn 11375 df-2 11438 df-3 11439 df-n0 11643 df-z 11729 df-uz 11993 df-rp 12138 df-ico 12493 df-fz 12644 df-fzo 12785 df-fl 12912 df-seq 13120 df-exp 13179 df-hash 13436 df-cj 14246 df-re 14247 df-im 14248 df-sqrt 14382 df-abs 14383 df-clim 14627 df-rlim 14628 df-sum 14825 df-0p 23874 df-ply 24381 df-coe 24383 df-dgr 24384

This theorem is referenced by: ftalem2 25252

W3C validator