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

Theorem ftalem5 27101
Description: Lemma for fta 27104: Main proof. We have already shifted the minimum found in ftalem3 27099 to zero by a change of variables, and now we show that the minimum value is zero. Expanding in a series about the minimum value, let 𝐾 be the lowest term in the polynomial that is nonzero, and let 𝑇 be a 𝐾-th root of -𝐹(0) / 𝐴(𝐾). Then an evaluation of 𝐹(𝑇𝑋) where 𝑋 is a sufficiently small positive number yields 𝐹(0) for the first term and -𝐹(0) · 𝑋𝐾 for the 𝐾-th term, and all higher terms are bounded because 𝑋 is small. Thus, abs(𝐹(𝑇𝑋)) ≤ abs(𝐹(0))(1 − 𝑋𝐾) < abs(𝐹(0)), in contradiction to our choice of 𝐹(0) as the minimum. (Contributed by Mario Carneiro, 14-Sep-2014.) (Revised by AV, 28-Sep-2020.)
Hypotheses
Ref Expression
ftalem.1 𝐴 = (coeff‘𝐹)
ftalem.2 𝑁 = (deg‘𝐹)
ftalem.3 (𝜑𝐹 ∈ (Poly‘𝑆))
ftalem.4 (𝜑𝑁 ∈ ℕ)
ftalem4.5 (𝜑 → (𝐹‘0) ≠ 0)
ftalem4.6 𝐾 = inf({𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0}, ℝ, < )
ftalem4.7 𝑇 = (-((𝐹‘0) / (𝐴𝐾))↑𝑐(1 / 𝐾))
ftalem4.8 𝑈 = ((abs‘(𝐹‘0)) / (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) + 1))
ftalem4.9 𝑋 = if(1 ≤ 𝑈, 1, 𝑈)
Assertion
Ref Expression
ftalem5 (𝜑 → ∃𝑥 ∈ ℂ (abs‘(𝐹𝑥)) < (abs‘(𝐹‘0)))
Distinct variable groups:   𝑘,𝑛,𝑥,𝐴   𝑘,𝐾,𝑛   𝑘,𝑁,𝑛,𝑥   𝑘,𝐹,𝑛,𝑥   𝜑,𝑘,𝑥   𝑆,𝑘   𝑇,𝑘,𝑥   𝑥,𝑈   𝑘,𝑋,𝑛,𝑥
Allowed substitution hints:   𝜑(𝑛)   𝑆(𝑥,𝑛)   𝑇(𝑛)   𝑈(𝑘,𝑛)   𝐾(𝑥)

Proof of Theorem ftalem5
StepHypRef 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, 𝑈)
101, 2, 3, 4, 5, 6, 7, 8, 9ftalem4 27100 . . . . 5 (𝜑 → ((𝐾 ∈ ℕ ∧ (𝐴𝐾) ≠ 0) ∧ (𝑇 ∈ ℂ ∧ 𝑈 ∈ ℝ+𝑋 ∈ ℝ+)))
1110simprd 494 . . . 4 (𝜑 → (𝑇 ∈ ℂ ∧ 𝑈 ∈ ℝ+𝑋 ∈ ℝ+))
1211simp1d 1139 . . 3 (𝜑𝑇 ∈ ℂ)
1311simp3d 1141 . . . . 5 (𝜑𝑋 ∈ ℝ+)
1413rpred 13063 . . . 4 (𝜑𝑋 ∈ ℝ)
1514recnd 11282 . . 3 (𝜑𝑋 ∈ ℂ)
1612, 15mulcld 11274 . 2 (𝜑 → (𝑇 · 𝑋) ∈ ℂ)
17 plyf 26221 . . . . . 6 (𝐹 ∈ (Poly‘𝑆) → 𝐹:ℂ⟶ℂ)
183, 17syl 17 . . . . 5 (𝜑𝐹:ℂ⟶ℂ)
1918, 16ffvelcdmd 7090 . . . 4 (𝜑 → (𝐹‘(𝑇 · 𝑋)) ∈ ℂ)
2019abscld 15435 . . 3 (𝜑 → (abs‘(𝐹‘(𝑇 · 𝑋))) ∈ ℝ)
21 0cn 11246 . . . . . . 7 0 ∈ ℂ
22 ffvelcdm 7086 . . . . . . 7 ((𝐹:ℂ⟶ℂ ∧ 0 ∈ ℂ) → (𝐹‘0) ∈ ℂ)
2318, 21, 22sylancl 584 . . . . . 6 (𝜑 → (𝐹‘0) ∈ ℂ)
2423abscld 15435 . . . . 5 (𝜑 → (abs‘(𝐹‘0)) ∈ ℝ)
2510simpld 493 . . . . . . . . 9 (𝜑 → (𝐾 ∈ ℕ ∧ (𝐴𝐾) ≠ 0))
2625simpld 493 . . . . . . . 8 (𝜑𝐾 ∈ ℕ)
2726nnnn0d 12577 . . . . . . 7 (𝜑𝐾 ∈ ℕ0)
2814, 27reexpcld 14175 . . . . . 6 (𝜑 → (𝑋𝐾) ∈ ℝ)
2924, 28remulcld 11284 . . . . 5 (𝜑 → ((abs‘(𝐹‘0)) · (𝑋𝐾)) ∈ ℝ)
3024, 29resubcld 11682 . . . 4 (𝜑 → ((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋𝐾))) ∈ ℝ)
31 fzfid 13986 . . . . . 6 (𝜑 → ((𝐾 + 1)...𝑁) ∈ Fin)
321coef3 26255 . . . . . . . . 9 (𝐹 ∈ (Poly‘𝑆) → 𝐴:ℕ0⟶ℂ)
333, 32syl 17 . . . . . . . 8 (𝜑𝐴:ℕ0⟶ℂ)
34 peano2nn0 12557 . . . . . . . . . 10 (𝐾 ∈ ℕ0 → (𝐾 + 1) ∈ ℕ0)
3527, 34syl 17 . . . . . . . . 9 (𝜑 → (𝐾 + 1) ∈ ℕ0)
36 elfzuz 13544 . . . . . . . . 9 (𝑘 ∈ ((𝐾 + 1)...𝑁) → 𝑘 ∈ (ℤ‘(𝐾 + 1)))
37 eluznn0 12946 . . . . . . . . 9 (((𝐾 + 1) ∈ ℕ0𝑘 ∈ (ℤ‘(𝐾 + 1))) → 𝑘 ∈ ℕ0)
3835, 36, 37syl2an 594 . . . . . . . 8 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑘 ∈ ℕ0)
39 ffvelcdm 7086 . . . . . . . 8 ((𝐴:ℕ0⟶ℂ ∧ 𝑘 ∈ ℕ0) → (𝐴𝑘) ∈ ℂ)
4033, 38, 39syl2an2r 683 . . . . . . 7 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝐴𝑘) ∈ ℂ)
4116adantr 479 . . . . . . . 8 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑇 · 𝑋) ∈ ℂ)
4241, 38expcld 14158 . . . . . . 7 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((𝑇 · 𝑋)↑𝑘) ∈ ℂ)
4340, 42mulcld 11274 . . . . . 6 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) ∈ ℂ)
4431, 43fsumcl 15731 . . . . 5 (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) ∈ ℂ)
4544abscld 15435 . . . 4 (𝜑 → (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘))) ∈ ℝ)
4630, 45readdcld 11283 . . 3 (𝜑 → (((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋𝐾))) + (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)))) ∈ ℝ)
47 fzfid 13986 . . . . . 6 (𝜑 → (0...𝐾) ∈ Fin)
48 elfznn0 13641 . . . . . . . 8 (𝑘 ∈ (0...𝐾) → 𝑘 ∈ ℕ0)
4933, 48, 39syl2an 594 . . . . . . 7 ((𝜑𝑘 ∈ (0...𝐾)) → (𝐴𝑘) ∈ ℂ)
50 expcl 14092 . . . . . . . 8 (((𝑇 · 𝑋) ∈ ℂ ∧ 𝑘 ∈ ℕ0) → ((𝑇 · 𝑋)↑𝑘) ∈ ℂ)
5116, 48, 50syl2an 594 . . . . . . 7 ((𝜑𝑘 ∈ (0...𝐾)) → ((𝑇 · 𝑋)↑𝑘) ∈ ℂ)
5249, 51mulcld 11274 . . . . . 6 ((𝜑𝑘 ∈ (0...𝐾)) → ((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) ∈ ℂ)
5347, 52fsumcl 15731 . . . . 5 (𝜑 → Σ𝑘 ∈ (0...𝐾)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) ∈ ℂ)
5453, 44abstrid 15455 . . . 4 (𝜑 → (abs‘(Σ𝑘 ∈ (0...𝐾)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) + Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)))) ≤ ((abs‘Σ𝑘 ∈ (0...𝐾)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘))) + (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)))))
551, 2coeid2 26262 . . . . . . 7 ((𝐹 ∈ (Poly‘𝑆) ∧ (𝑇 · 𝑋) ∈ ℂ) → (𝐹‘(𝑇 · 𝑋)) = Σ𝑘 ∈ (0...𝑁)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)))
563, 16, 55syl2anc 582 . . . . . 6 (𝜑 → (𝐹‘(𝑇 · 𝑋)) = Σ𝑘 ∈ (0...𝑁)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)))
5726nnred 12272 . . . . . . . . 9 (𝜑𝐾 ∈ ℝ)
5857ltp1d 12189 . . . . . . . 8 (𝜑𝐾 < (𝐾 + 1))
59 fzdisj 13575 . . . . . . . 8 (𝐾 < (𝐾 + 1) → ((0...𝐾) ∩ ((𝐾 + 1)...𝑁)) = ∅)
6058, 59syl 17 . . . . . . 7 (𝜑 → ((0...𝐾) ∩ ((𝐾 + 1)...𝑁)) = ∅)
61 ssrab2 4075 . . . . . . . . . . . 12 {𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0} ⊆ ℕ
62 nnuz 12910 . . . . . . . . . . . 12 ℕ = (ℤ‘1)
6361, 62sseqtri 4017 . . . . . . . . . . 11 {𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0} ⊆ (ℤ‘1)
64 fveq2 6892 . . . . . . . . . . . . 13 (𝑛 = 𝑁 → (𝐴𝑛) = (𝐴𝑁))
6564neeq1d 2990 . . . . . . . . . . . 12 (𝑛 = 𝑁 → ((𝐴𝑛) ≠ 0 ↔ (𝐴𝑁) ≠ 0))
664nnne0d 12307 . . . . . . . . . . . . 13 (𝜑𝑁 ≠ 0)
672, 1dgreq0 26289 . . . . . . . . . . . . . . . 16 (𝐹 ∈ (Poly‘𝑆) → (𝐹 = 0𝑝 ↔ (𝐴𝑁) = 0))
683, 67syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (𝐹 = 0𝑝 ↔ (𝐴𝑁) = 0))
69 fveq2 6892 . . . . . . . . . . . . . . . . 17 (𝐹 = 0𝑝 → (deg‘𝐹) = (deg‘0𝑝))
70 dgr0 26286 . . . . . . . . . . . . . . . . 17 (deg‘0𝑝) = 0
7169, 70eqtrdi 2782 . . . . . . . . . . . . . . . 16 (𝐹 = 0𝑝 → (deg‘𝐹) = 0)
722, 71eqtrid 2778 . . . . . . . . . . . . . . 15 (𝐹 = 0𝑝𝑁 = 0)
7368, 72biimtrrdi 253 . . . . . . . . . . . . . 14 (𝜑 → ((𝐴𝑁) = 0 → 𝑁 = 0))
7473necon3d 2951 . . . . . . . . . . . . 13 (𝜑 → (𝑁 ≠ 0 → (𝐴𝑁) ≠ 0))
7566, 74mpd 15 . . . . . . . . . . . 12 (𝜑 → (𝐴𝑁) ≠ 0)
7665, 4, 75elrabd 3684 . . . . . . . . . . 11 (𝜑𝑁 ∈ {𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0})
77 infssuzle 12960 . . . . . . . . . . 11 (({𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0} ⊆ (ℤ‘1) ∧ 𝑁 ∈ {𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0}) → inf({𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0}, ℝ, < ) ≤ 𝑁)
7863, 76, 77sylancr 585 . . . . . . . . . 10 (𝜑 → inf({𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0}, ℝ, < ) ≤ 𝑁)
796, 78eqbrtrid 5180 . . . . . . . . 9 (𝜑𝐾𝑁)
80 nn0uz 12909 . . . . . . . . . . 11 0 = (ℤ‘0)
8127, 80eleqtrdi 2836 . . . . . . . . . 10 (𝜑𝐾 ∈ (ℤ‘0))
824nnzd 12630 . . . . . . . . . 10 (𝜑𝑁 ∈ ℤ)
83 elfz5 13540 . . . . . . . . . 10 ((𝐾 ∈ (ℤ‘0) ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (0...𝑁) ↔ 𝐾𝑁))
8481, 82, 83syl2anc 582 . . . . . . . . 9 (𝜑 → (𝐾 ∈ (0...𝑁) ↔ 𝐾𝑁))
8579, 84mpbird 256 . . . . . . . 8 (𝜑𝐾 ∈ (0...𝑁))
86 fzsplit 13574 . . . . . . . 8 (𝐾 ∈ (0...𝑁) → (0...𝑁) = ((0...𝐾) ∪ ((𝐾 + 1)...𝑁)))
8785, 86syl 17 . . . . . . 7 (𝜑 → (0...𝑁) = ((0...𝐾) ∪ ((𝐾 + 1)...𝑁)))
88 fzfid 13986 . . . . . . 7 (𝜑 → (0...𝑁) ∈ Fin)
89 elfznn0 13641 . . . . . . . . 9 (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0)
9033, 89, 39syl2an 594 . . . . . . . 8 ((𝜑𝑘 ∈ (0...𝑁)) → (𝐴𝑘) ∈ ℂ)
9116, 89, 50syl2an 594 . . . . . . . 8 ((𝜑𝑘 ∈ (0...𝑁)) → ((𝑇 · 𝑋)↑𝑘) ∈ ℂ)
9290, 91mulcld 11274 . . . . . . 7 ((𝜑𝑘 ∈ (0...𝑁)) → ((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) ∈ ℂ)
9360, 87, 88, 92fsumsplit 15739 . . . . . 6 (𝜑 → Σ𝑘 ∈ (0...𝑁)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) = (Σ𝑘 ∈ (0...𝐾)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) + Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘))))
9456, 93eqtrd 2766 . . . . 5 (𝜑 → (𝐹‘(𝑇 · 𝑋)) = (Σ𝑘 ∈ (0...𝐾)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) + Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘))))
9594fveq2d 6896 . . . 4 (𝜑 → (abs‘(𝐹‘(𝑇 · 𝑋))) = (abs‘(Σ𝑘 ∈ (0...𝐾)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) + Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)))))
961coefv0 26271 . . . . . . . . . . . . 13 (𝐹 ∈ (Poly‘𝑆) → (𝐹‘0) = (𝐴‘0))
973, 96syl 17 . . . . . . . . . . . 12 (𝜑 → (𝐹‘0) = (𝐴‘0))
9897eqcomd 2732 . . . . . . . . . . 11 (𝜑 → (𝐴‘0) = (𝐹‘0))
9916exp0d 14152 . . . . . . . . . . 11 (𝜑 → ((𝑇 · 𝑋)↑0) = 1)
10098, 99oveq12d 7433 . . . . . . . . . 10 (𝜑 → ((𝐴‘0) · ((𝑇 · 𝑋)↑0)) = ((𝐹‘0) · 1))
10123mulridd 11271 . . . . . . . . . 10 (𝜑 → ((𝐹‘0) · 1) = (𝐹‘0))
102100, 101eqtrd 2766 . . . . . . . . 9 (𝜑 → ((𝐴‘0) · ((𝑇 · 𝑋)↑0)) = (𝐹‘0))
103 1e0p1 12764 . . . . . . . . . . . . 13 1 = (0 + 1)
104103oveq1i 7425 . . . . . . . . . . . 12 (1...𝐾) = ((0 + 1)...𝐾)
105104sumeq1i 15696 . . . . . . . . . . 11 Σ𝑘 ∈ (1...𝐾)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) = Σ𝑘 ∈ ((0 + 1)...𝐾)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘))
10626, 62eleqtrdi 2836 . . . . . . . . . . . 12 (𝜑𝐾 ∈ (ℤ‘1))
107 elfznn 13577 . . . . . . . . . . . . . . 15 (𝑘 ∈ (1...𝐾) → 𝑘 ∈ ℕ)
108107nnnn0d 12577 . . . . . . . . . . . . . 14 (𝑘 ∈ (1...𝐾) → 𝑘 ∈ ℕ0)
10933, 108, 39syl2an 594 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (1...𝐾)) → (𝐴𝑘) ∈ ℂ)
11016, 108, 50syl2an 594 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (1...𝐾)) → ((𝑇 · 𝑋)↑𝑘) ∈ ℂ)
111109, 110mulcld 11274 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (1...𝐾)) → ((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) ∈ ℂ)
112 fveq2 6892 . . . . . . . . . . . . 13 (𝑘 = 𝐾 → (𝐴𝑘) = (𝐴𝐾))
113 oveq2 7423 . . . . . . . . . . . . 13 (𝑘 = 𝐾 → ((𝑇 · 𝑋)↑𝑘) = ((𝑇 · 𝑋)↑𝐾))
114112, 113oveq12d 7433 . . . . . . . . . . . 12 (𝑘 = 𝐾 → ((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) = ((𝐴𝐾) · ((𝑇 · 𝑋)↑𝐾)))
115106, 111, 114fsumm1 15749 . . . . . . . . . . 11 (𝜑 → Σ𝑘 ∈ (1...𝐾)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) = (Σ𝑘 ∈ (1...(𝐾 − 1))((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) + ((𝐴𝐾) · ((𝑇 · 𝑋)↑𝐾))))
116105, 115eqtr3id 2780 . . . . . . . . . 10 (𝜑 → Σ𝑘 ∈ ((0 + 1)...𝐾)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) = (Σ𝑘 ∈ (1...(𝐾 − 1))((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) + ((𝐴𝐾) · ((𝑇 · 𝑋)↑𝐾))))
117 elfznn 13577 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 ∈ (1...(𝐾 − 1)) → 𝑘 ∈ ℕ)
118117adantl 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ (1...(𝐾 − 1))) → 𝑘 ∈ ℕ)
119118nnred 12272 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ (1...(𝐾 − 1))) → 𝑘 ∈ ℝ)
12057adantr 479 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ (1...(𝐾 − 1))) → 𝐾 ∈ ℝ)
121 peano2rem 11567 . . . . . . . . . . . . . . . . . . . 20 (𝐾 ∈ ℝ → (𝐾 − 1) ∈ ℝ)
122120, 121syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ (1...(𝐾 − 1))) → (𝐾 − 1) ∈ ℝ)
123 elfzle2 13552 . . . . . . . . . . . . . . . . . . . 20 (𝑘 ∈ (1...(𝐾 − 1)) → 𝑘 ≤ (𝐾 − 1))
124123adantl 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ (1...(𝐾 − 1))) → 𝑘 ≤ (𝐾 − 1))
125120ltm1d 12191 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ (1...(𝐾 − 1))) → (𝐾 − 1) < 𝐾)
126119, 122, 120, 124, 125lelttrd 11412 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ (1...(𝐾 − 1))) → 𝑘 < 𝐾)
127119, 120ltnled 11401 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ (1...(𝐾 − 1))) → (𝑘 < 𝐾 ↔ ¬ 𝐾𝑘))
128126, 127mpbid 231 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ (1...(𝐾 − 1))) → ¬ 𝐾𝑘)
129 infssuzle 12960 . . . . . . . . . . . . . . . . . . 19 (({𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0} ⊆ (ℤ‘1) ∧ 𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0}) → inf({𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0}, ℝ, < ) ≤ 𝑘)
1306, 129eqbrtrid 5180 . . . . . . . . . . . . . . . . . 18 (({𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0} ⊆ (ℤ‘1) ∧ 𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0}) → 𝐾𝑘)
13163, 130mpan 688 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0} → 𝐾𝑘)
132128, 131nsyl 140 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (1...(𝐾 − 1))) → ¬ 𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0})
133 fveq2 6892 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 𝑘 → (𝐴𝑛) = (𝐴𝑘))
134133neeq1d 2990 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 𝑘 → ((𝐴𝑛) ≠ 0 ↔ (𝐴𝑘) ≠ 0))
135134elrab3 3683 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ℕ → (𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0} ↔ (𝐴𝑘) ≠ 0))
136118, 135syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ (1...(𝐾 − 1))) → (𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0} ↔ (𝐴𝑘) ≠ 0))
137136necon2bbid 2974 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (1...(𝐾 − 1))) → ((𝐴𝑘) = 0 ↔ ¬ 𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0}))
138132, 137mpbird 256 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (1...(𝐾 − 1))) → (𝐴𝑘) = 0)
139138oveq1d 7430 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (1...(𝐾 − 1))) → ((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) = (0 · ((𝑇 · 𝑋)↑𝑘)))
140117nnnn0d 12577 . . . . . . . . . . . . . . . 16 (𝑘 ∈ (1...(𝐾 − 1)) → 𝑘 ∈ ℕ0)
14116, 140, 50syl2an 594 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (1...(𝐾 − 1))) → ((𝑇 · 𝑋)↑𝑘) ∈ ℂ)
142141mul02d 11452 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (1...(𝐾 − 1))) → (0 · ((𝑇 · 𝑋)↑𝑘)) = 0)
143139, 142eqtrd 2766 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (1...(𝐾 − 1))) → ((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) = 0)
144143sumeq2dv 15701 . . . . . . . . . . . 12 (𝜑 → Σ𝑘 ∈ (1...(𝐾 − 1))((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) = Σ𝑘 ∈ (1...(𝐾 − 1))0)
145 fzfi 13985 . . . . . . . . . . . . . 14 (1...(𝐾 − 1)) ∈ Fin
146145olci 864 . . . . . . . . . . . . 13 ((1...(𝐾 − 1)) ⊆ (ℤ‘1) ∨ (1...(𝐾 − 1)) ∈ Fin)
147 sumz 15720 . . . . . . . . . . . . 13 (((1...(𝐾 − 1)) ⊆ (ℤ‘1) ∨ (1...(𝐾 − 1)) ∈ Fin) → Σ𝑘 ∈ (1...(𝐾 − 1))0 = 0)
148146, 147ax-mp 5 . . . . . . . . . . . 12 Σ𝑘 ∈ (1...(𝐾 − 1))0 = 0
149144, 148eqtrdi 2782 . . . . . . . . . . 11 (𝜑 → Σ𝑘 ∈ (1...(𝐾 − 1))((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) = 0)
15012, 15, 27mulexpd 14173 . . . . . . . . . . . . . 14 (𝜑 → ((𝑇 · 𝑋)↑𝐾) = ((𝑇𝐾) · (𝑋𝐾)))
151150oveq2d 7431 . . . . . . . . . . . . 13 (𝜑 → ((𝐴𝐾) · ((𝑇 · 𝑋)↑𝐾)) = ((𝐴𝐾) · ((𝑇𝐾) · (𝑋𝐾))))
15233, 27ffvelcdmd 7090 . . . . . . . . . . . . . 14 (𝜑 → (𝐴𝐾) ∈ ℂ)
15312, 27expcld 14158 . . . . . . . . . . . . . 14 (𝜑 → (𝑇𝐾) ∈ ℂ)
15428recnd 11282 . . . . . . . . . . . . . 14 (𝜑 → (𝑋𝐾) ∈ ℂ)
155152, 153, 154mulassd 11277 . . . . . . . . . . . . 13 (𝜑 → (((𝐴𝐾) · (𝑇𝐾)) · (𝑋𝐾)) = ((𝐴𝐾) · ((𝑇𝐾) · (𝑋𝐾))))
156151, 155eqtr4d 2769 . . . . . . . . . . . 12 (𝜑 → ((𝐴𝐾) · ((𝑇 · 𝑋)↑𝐾)) = (((𝐴𝐾) · (𝑇𝐾)) · (𝑋𝐾)))
1577oveq1i 7425 . . . . . . . . . . . . . . . 16 (𝑇𝐾) = ((-((𝐹‘0) / (𝐴𝐾))↑𝑐(1 / 𝐾))↑𝐾)
15857recnd 11282 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐾 ∈ ℂ)
15926nnne0d 12307 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐾 ≠ 0)
160158, 159recid2d 12030 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((1 / 𝐾) · 𝐾) = 1)
161160oveq2d 7431 . . . . . . . . . . . . . . . . 17 (𝜑 → (-((𝐹‘0) / (𝐴𝐾))↑𝑐((1 / 𝐾) · 𝐾)) = (-((𝐹‘0) / (𝐴𝐾))↑𝑐1))
16225simprd 494 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐴𝐾) ≠ 0)
16323, 152, 162divcld 12034 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝐹‘0) / (𝐴𝐾)) ∈ ℂ)
164163negcld 11598 . . . . . . . . . . . . . . . . . 18 (𝜑 → -((𝐹‘0) / (𝐴𝐾)) ∈ ℂ)
16526nnrecred 12308 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (1 / 𝐾) ∈ ℝ)
166165recnd 11282 . . . . . . . . . . . . . . . . . 18 (𝜑 → (1 / 𝐾) ∈ ℂ)
167164, 166, 27cxpmul2d 26732 . . . . . . . . . . . . . . . . 17 (𝜑 → (-((𝐹‘0) / (𝐴𝐾))↑𝑐((1 / 𝐾) · 𝐾)) = ((-((𝐹‘0) / (𝐴𝐾))↑𝑐(1 / 𝐾))↑𝐾))
168164cxp1d 26729 . . . . . . . . . . . . . . . . 17 (𝜑 → (-((𝐹‘0) / (𝐴𝐾))↑𝑐1) = -((𝐹‘0) / (𝐴𝐾)))
169161, 167, 1683eqtr3d 2774 . . . . . . . . . . . . . . . 16 (𝜑 → ((-((𝐹‘0) / (𝐴𝐾))↑𝑐(1 / 𝐾))↑𝐾) = -((𝐹‘0) / (𝐴𝐾)))
170157, 169eqtrid 2778 . . . . . . . . . . . . . . 15 (𝜑 → (𝑇𝐾) = -((𝐹‘0) / (𝐴𝐾)))
171170oveq2d 7431 . . . . . . . . . . . . . 14 (𝜑 → ((𝐴𝐾) · (𝑇𝐾)) = ((𝐴𝐾) · -((𝐹‘0) / (𝐴𝐾))))
172152, 163mulneg2d 11708 . . . . . . . . . . . . . 14 (𝜑 → ((𝐴𝐾) · -((𝐹‘0) / (𝐴𝐾))) = -((𝐴𝐾) · ((𝐹‘0) / (𝐴𝐾))))
17323, 152, 162divcan2d 12036 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐴𝐾) · ((𝐹‘0) / (𝐴𝐾))) = (𝐹‘0))
174173negeqd 11494 . . . . . . . . . . . . . 14 (𝜑 → -((𝐴𝐾) · ((𝐹‘0) / (𝐴𝐾))) = -(𝐹‘0))
175171, 172, 1743eqtrd 2770 . . . . . . . . . . . . 13 (𝜑 → ((𝐴𝐾) · (𝑇𝐾)) = -(𝐹‘0))
176175oveq1d 7430 . . . . . . . . . . . 12 (𝜑 → (((𝐴𝐾) · (𝑇𝐾)) · (𝑋𝐾)) = (-(𝐹‘0) · (𝑋𝐾)))
17723, 154mulneg1d 11707 . . . . . . . . . . . 12 (𝜑 → (-(𝐹‘0) · (𝑋𝐾)) = -((𝐹‘0) · (𝑋𝐾)))
178156, 176, 1773eqtrd 2770 . . . . . . . . . . 11 (𝜑 → ((𝐴𝐾) · ((𝑇 · 𝑋)↑𝐾)) = -((𝐹‘0) · (𝑋𝐾)))
179149, 178oveq12d 7433 . . . . . . . . . 10 (𝜑 → (Σ𝑘 ∈ (1...(𝐾 − 1))((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) + ((𝐴𝐾) · ((𝑇 · 𝑋)↑𝐾))) = (0 + -((𝐹‘0) · (𝑋𝐾))))
18023, 154mulcld 11274 . . . . . . . . . . . 12 (𝜑 → ((𝐹‘0) · (𝑋𝐾)) ∈ ℂ)
181180negcld 11598 . . . . . . . . . . 11 (𝜑 → -((𝐹‘0) · (𝑋𝐾)) ∈ ℂ)
182181addlidd 11455 . . . . . . . . . 10 (𝜑 → (0 + -((𝐹‘0) · (𝑋𝐾))) = -((𝐹‘0) · (𝑋𝐾)))
183116, 179, 1823eqtrd 2770 . . . . . . . . 9 (𝜑 → Σ𝑘 ∈ ((0 + 1)...𝐾)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) = -((𝐹‘0) · (𝑋𝐾)))
184102, 183oveq12d 7433 . . . . . . . 8 (𝜑 → (((𝐴‘0) · ((𝑇 · 𝑋)↑0)) + Σ𝑘 ∈ ((0 + 1)...𝐾)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘))) = ((𝐹‘0) + -((𝐹‘0) · (𝑋𝐾))))
185 fveq2 6892 . . . . . . . . . 10 (𝑘 = 0 → (𝐴𝑘) = (𝐴‘0))
186 oveq2 7423 . . . . . . . . . 10 (𝑘 = 0 → ((𝑇 · 𝑋)↑𝑘) = ((𝑇 · 𝑋)↑0))
187185, 186oveq12d 7433 . . . . . . . . 9 (𝑘 = 0 → ((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) = ((𝐴‘0) · ((𝑇 · 𝑋)↑0)))
18881, 52, 187fsum1p 15751 . . . . . . . 8 (𝜑 → Σ𝑘 ∈ (0...𝐾)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) = (((𝐴‘0) · ((𝑇 · 𝑋)↑0)) + Σ𝑘 ∈ ((0 + 1)...𝐾)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘))))
189101oveq1d 7430 . . . . . . . . 9 (𝜑 → (((𝐹‘0) · 1) − ((𝐹‘0) · (𝑋𝐾))) = ((𝐹‘0) − ((𝐹‘0) · (𝑋𝐾))))
190 1cnd 11249 . . . . . . . . . 10 (𝜑 → 1 ∈ ℂ)
19123, 190, 154subdid 11710 . . . . . . . . 9 (𝜑 → ((𝐹‘0) · (1 − (𝑋𝐾))) = (((𝐹‘0) · 1) − ((𝐹‘0) · (𝑋𝐾))))
19223, 180negsubd 11617 . . . . . . . . 9 (𝜑 → ((𝐹‘0) + -((𝐹‘0) · (𝑋𝐾))) = ((𝐹‘0) − ((𝐹‘0) · (𝑋𝐾))))
193189, 191, 1923eqtr4d 2776 . . . . . . . 8 (𝜑 → ((𝐹‘0) · (1 − (𝑋𝐾))) = ((𝐹‘0) + -((𝐹‘0) · (𝑋𝐾))))
194184, 188, 1933eqtr4d 2776 . . . . . . 7 (𝜑 → Σ𝑘 ∈ (0...𝐾)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) = ((𝐹‘0) · (1 − (𝑋𝐾))))
195194fveq2d 6896 . . . . . 6 (𝜑 → (abs‘Σ𝑘 ∈ (0...𝐾)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘))) = (abs‘((𝐹‘0) · (1 − (𝑋𝐾)))))
196 1re 11254 . . . . . . . . 9 1 ∈ ℝ
197 resubcl 11564 . . . . . . . . 9 ((1 ∈ ℝ ∧ (𝑋𝐾) ∈ ℝ) → (1 − (𝑋𝐾)) ∈ ℝ)
198196, 28, 197sylancr 585 . . . . . . . 8 (𝜑 → (1 − (𝑋𝐾)) ∈ ℝ)
199198recnd 11282 . . . . . . 7 (𝜑 → (1 − (𝑋𝐾)) ∈ ℂ)
20023, 199absmuld 15453 . . . . . 6 (𝜑 → (abs‘((𝐹‘0) · (1 − (𝑋𝐾)))) = ((abs‘(𝐹‘0)) · (abs‘(1 − (𝑋𝐾)))))
20113rpge0d 13067 . . . . . . . . . . 11 (𝜑 → 0 ≤ 𝑋)
20211simp2d 1140 . . . . . . . . . . . . . 14 (𝜑𝑈 ∈ ℝ+)
203202rpred 13063 . . . . . . . . . . . . 13 (𝜑𝑈 ∈ ℝ)
204 min1 13215 . . . . . . . . . . . . 13 ((1 ∈ ℝ ∧ 𝑈 ∈ ℝ) → if(1 ≤ 𝑈, 1, 𝑈) ≤ 1)
205196, 203, 204sylancr 585 . . . . . . . . . . . 12 (𝜑 → if(1 ≤ 𝑈, 1, 𝑈) ≤ 1)
2069, 205eqbrtrid 5180 . . . . . . . . . . 11 (𝜑𝑋 ≤ 1)
207 exple1 14188 . . . . . . . . . . 11 (((𝑋 ∈ ℝ ∧ 0 ≤ 𝑋𝑋 ≤ 1) ∧ 𝐾 ∈ ℕ0) → (𝑋𝐾) ≤ 1)
20814, 201, 206, 27, 207syl31anc 1370 . . . . . . . . . 10 (𝜑 → (𝑋𝐾) ≤ 1)
209 subge0 11767 . . . . . . . . . . 11 ((1 ∈ ℝ ∧ (𝑋𝐾) ∈ ℝ) → (0 ≤ (1 − (𝑋𝐾)) ↔ (𝑋𝐾) ≤ 1))
210196, 28, 209sylancr 585 . . . . . . . . . 10 (𝜑 → (0 ≤ (1 − (𝑋𝐾)) ↔ (𝑋𝐾) ≤ 1))
211208, 210mpbird 256 . . . . . . . . 9 (𝜑 → 0 ≤ (1 − (𝑋𝐾)))
212198, 211absidd 15421 . . . . . . . 8 (𝜑 → (abs‘(1 − (𝑋𝐾))) = (1 − (𝑋𝐾)))
213212oveq2d 7431 . . . . . . 7 (𝜑 → ((abs‘(𝐹‘0)) · (abs‘(1 − (𝑋𝐾)))) = ((abs‘(𝐹‘0)) · (1 − (𝑋𝐾))))
21424recnd 11282 . . . . . . . 8 (𝜑 → (abs‘(𝐹‘0)) ∈ ℂ)
215214, 190, 154subdid 11710 . . . . . . 7 (𝜑 → ((abs‘(𝐹‘0)) · (1 − (𝑋𝐾))) = (((abs‘(𝐹‘0)) · 1) − ((abs‘(𝐹‘0)) · (𝑋𝐾))))
216214mulridd 11271 . . . . . . . 8 (𝜑 → ((abs‘(𝐹‘0)) · 1) = (abs‘(𝐹‘0)))
217216oveq1d 7430 . . . . . . 7 (𝜑 → (((abs‘(𝐹‘0)) · 1) − ((abs‘(𝐹‘0)) · (𝑋𝐾))) = ((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋𝐾))))
218213, 215, 2173eqtrd 2770 . . . . . 6 (𝜑 → ((abs‘(𝐹‘0)) · (abs‘(1 − (𝑋𝐾)))) = ((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋𝐾))))
219195, 200, 2183eqtrrd 2771 . . . . 5 (𝜑 → ((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋𝐾))) = (abs‘Σ𝑘 ∈ (0...𝐾)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘))))
220219oveq1d 7430 . . . 4 (𝜑 → (((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋𝐾))) + (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)))) = ((abs‘Σ𝑘 ∈ (0...𝐾)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘))) + (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)))))
22154, 95, 2203brtr4d 5177 . . 3 (𝜑 → (abs‘(𝐹‘(𝑇 · 𝑋))) ≤ (((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋𝐾))) + (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)))))
22243abscld 15435 . . . . . . 7 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘))) ∈ ℝ)
22331, 222fsumrecl 15732 . . . . . 6 (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘))) ∈ ℝ)
22431, 43fsumabs 15799 . . . . . 6 (𝜑 → (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘))) ≤ Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘))))
225 expcl 14092 . . . . . . . . . . . 12 ((𝑇 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (𝑇𝑘) ∈ ℂ)
22612, 38, 225syl2an2r 683 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑇𝑘) ∈ ℂ)
22740, 226mulcld 11274 . . . . . . . . . 10 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((𝐴𝑘) · (𝑇𝑘)) ∈ ℂ)
228227abscld 15435 . . . . . . . . 9 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘((𝐴𝑘) · (𝑇𝑘))) ∈ ℝ)
22931, 228fsumrecl 15732 . . . . . . . 8 (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) ∈ ℝ)
23014, 35reexpcld 14175 . . . . . . . 8 (𝜑 → (𝑋↑(𝐾 + 1)) ∈ ℝ)
231229, 230remulcld 11284 . . . . . . 7 (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) · (𝑋↑(𝐾 + 1))) ∈ ℝ)
232230adantr 479 . . . . . . . . . 10 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑋↑(𝐾 + 1)) ∈ ℝ)
233228, 232remulcld 11284 . . . . . . . . 9 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((abs‘((𝐴𝑘) · (𝑇𝑘))) · (𝑋↑(𝐾 + 1))) ∈ ℝ)
23412adantr 479 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑇 ∈ ℂ)
23515adantr 479 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑋 ∈ ℂ)
236234, 235, 38mulexpd 14173 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((𝑇 · 𝑋)↑𝑘) = ((𝑇𝑘) · (𝑋𝑘)))
237236oveq2d 7431 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) = ((𝐴𝑘) · ((𝑇𝑘) · (𝑋𝑘))))
23814adantr 479 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑋 ∈ ℝ)
239238, 38reexpcld 14175 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑋𝑘) ∈ ℝ)
240239recnd 11282 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑋𝑘) ∈ ℂ)
24140, 226, 240mulassd 11277 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → (((𝐴𝑘) · (𝑇𝑘)) · (𝑋𝑘)) = ((𝐴𝑘) · ((𝑇𝑘) · (𝑋𝑘))))
242237, 241eqtr4d 2769 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) = (((𝐴𝑘) · (𝑇𝑘)) · (𝑋𝑘)))
243242fveq2d 6896 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘))) = (abs‘(((𝐴𝑘) · (𝑇𝑘)) · (𝑋𝑘))))
244227, 240absmuld 15453 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘(((𝐴𝑘) · (𝑇𝑘)) · (𝑋𝑘))) = ((abs‘((𝐴𝑘) · (𝑇𝑘))) · (abs‘(𝑋𝑘))))
245 elfzelz 13548 . . . . . . . . . . . . . . 15 (𝑘 ∈ ((𝐾 + 1)...𝑁) → 𝑘 ∈ ℤ)
246 rpexpcl 14093 . . . . . . . . . . . . . . 15 ((𝑋 ∈ ℝ+𝑘 ∈ ℤ) → (𝑋𝑘) ∈ ℝ+)
24713, 245, 246syl2an 594 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑋𝑘) ∈ ℝ+)
248247rpge0d 13067 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → 0 ≤ (𝑋𝑘))
249239, 248absidd 15421 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘(𝑋𝑘)) = (𝑋𝑘))
250249oveq2d 7431 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((abs‘((𝐴𝑘) · (𝑇𝑘))) · (abs‘(𝑋𝑘))) = ((abs‘((𝐴𝑘) · (𝑇𝑘))) · (𝑋𝑘)))
251243, 244, 2503eqtrd 2770 . . . . . . . . . 10 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘))) = ((abs‘((𝐴𝑘) · (𝑇𝑘))) · (𝑋𝑘)))
252227absge0d 15443 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → 0 ≤ (abs‘((𝐴𝑘) · (𝑇𝑘))))
25335adantr 479 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝐾 + 1) ∈ ℕ0)
25436adantl 480 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑘 ∈ (ℤ‘(𝐾 + 1)))
255201adantr 479 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → 0 ≤ 𝑋)
256206adantr 479 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑋 ≤ 1)
257238, 253, 254, 255, 256leexp2rd 14266 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑋𝑘) ≤ (𝑋↑(𝐾 + 1)))
258239, 232, 228, 252, 257lemul2ad 12199 . . . . . . . . . 10 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((abs‘((𝐴𝑘) · (𝑇𝑘))) · (𝑋𝑘)) ≤ ((abs‘((𝐴𝑘) · (𝑇𝑘))) · (𝑋↑(𝐾 + 1))))
259251, 258eqbrtrd 5167 . . . . . . . . 9 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘))) ≤ ((abs‘((𝐴𝑘) · (𝑇𝑘))) · (𝑋↑(𝐾 + 1))))
26031, 222, 233, 259fsumle 15797 . . . . . . . 8 (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘))) ≤ Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((abs‘((𝐴𝑘) · (𝑇𝑘))) · (𝑋↑(𝐾 + 1))))
261230recnd 11282 . . . . . . . . 9 (𝜑 → (𝑋↑(𝐾 + 1)) ∈ ℂ)
262228recnd 11282 . . . . . . . . 9 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘((𝐴𝑘) · (𝑇𝑘))) ∈ ℂ)
26331, 261, 262fsummulc1 15783 . . . . . . . 8 (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) · (𝑋↑(𝐾 + 1))) = Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((abs‘((𝐴𝑘) · (𝑇𝑘))) · (𝑋↑(𝐾 + 1))))
264260, 263breqtrrd 5173 . . . . . . 7 (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘))) ≤ (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) · (𝑋↑(𝐾 + 1))))
26515, 27expp1d 14159 . . . . . . . . . . 11 (𝜑 → (𝑋↑(𝐾 + 1)) = ((𝑋𝐾) · 𝑋))
266154, 15mulcomd 11275 . . . . . . . . . . 11 (𝜑 → ((𝑋𝐾) · 𝑋) = (𝑋 · (𝑋𝐾)))
267265, 266eqtrd 2766 . . . . . . . . . 10 (𝜑 → (𝑋↑(𝐾 + 1)) = (𝑋 · (𝑋𝐾)))
268267oveq2d 7431 . . . . . . . . 9 (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) · (𝑋↑(𝐾 + 1))) = (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) · (𝑋 · (𝑋𝐾))))
269229recnd 11282 . . . . . . . . . 10 (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) ∈ ℂ)
270269, 15, 154mulassd 11277 . . . . . . . . 9 (𝜑 → ((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) · 𝑋) · (𝑋𝐾)) = (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) · (𝑋 · (𝑋𝐾))))
271268, 270eqtr4d 2769 . . . . . . . 8 (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) · (𝑋↑(𝐾 + 1))) = ((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) · 𝑋) · (𝑋𝐾)))
272229, 14remulcld 11284 . . . . . . . . 9 (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) · 𝑋) ∈ ℝ)
273 nnssz 12625 . . . . . . . . . . . 12 ℕ ⊆ ℤ
27461, 273sstri 3990 . . . . . . . . . . 11 {𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0} ⊆ ℤ
27576ne0d 4337 . . . . . . . . . . . . 13 (𝜑 → {𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0} ≠ ∅)
276 infssuzcl 12961 . . . . . . . . . . . . 13 (({𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0} ⊆ (ℤ‘1) ∧ {𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0} ≠ ∅) → inf({𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0}, ℝ, < ) ∈ {𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0})
27763, 275, 276sylancr 585 . . . . . . . . . . . 12 (𝜑 → inf({𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0}, ℝ, < ) ∈ {𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0})
2786, 277eqeltrid 2830 . . . . . . . . . . 11 (𝜑𝐾 ∈ {𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0})
279274, 278sselid 3978 . . . . . . . . . 10 (𝜑𝐾 ∈ ℤ)
28013, 279rpexpcld 14258 . . . . . . . . 9 (𝜑 → (𝑋𝐾) ∈ ℝ+)
281 peano2re 11427 . . . . . . . . . . . 12 𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) ∈ ℝ → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) + 1) ∈ ℝ)
282229, 281syl 17 . . . . . . . . . . 11 (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) + 1) ∈ ℝ)
283282, 14remulcld 11284 . . . . . . . . . 10 (𝜑 → ((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) + 1) · 𝑋) ∈ ℝ)
284229ltp1d 12189 . . . . . . . . . . 11 (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) < (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) + 1))
285229, 282, 13, 284ltmul1dd 13118 . . . . . . . . . 10 (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) · 𝑋) < ((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) + 1) · 𝑋))
286 min2 13216 . . . . . . . . . . . . . 14 ((1 ∈ ℝ ∧ 𝑈 ∈ ℝ) → if(1 ≤ 𝑈, 1, 𝑈) ≤ 𝑈)
287196, 203, 286sylancr 585 . . . . . . . . . . . . 13 (𝜑 → if(1 ≤ 𝑈, 1, 𝑈) ≤ 𝑈)
2889, 287eqbrtrid 5180 . . . . . . . . . . . 12 (𝜑𝑋𝑈)
289288, 8breqtrdi 5186 . . . . . . . . . . 11 (𝜑𝑋 ≤ ((abs‘(𝐹‘0)) / (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) + 1)))
290 0red 11257 . . . . . . . . . . . . 13 (𝜑 → 0 ∈ ℝ)
29131, 228, 252fsumge0 15793 . . . . . . . . . . . . 13 (𝜑 → 0 ≤ Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))))
292290, 229, 282, 291, 284lelttrd 11412 . . . . . . . . . . . 12 (𝜑 → 0 < (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) + 1))
293 lemuldiv2 12140 . . . . . . . . . . . 12 ((𝑋 ∈ ℝ ∧ (abs‘(𝐹‘0)) ∈ ℝ ∧ ((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) + 1) ∈ ℝ ∧ 0 < (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) + 1))) → (((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) + 1) · 𝑋) ≤ (abs‘(𝐹‘0)) ↔ 𝑋 ≤ ((abs‘(𝐹‘0)) / (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) + 1))))
29414, 24, 282, 292, 293syl112anc 1371 . . . . . . . . . . 11 (𝜑 → (((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) + 1) · 𝑋) ≤ (abs‘(𝐹‘0)) ↔ 𝑋 ≤ ((abs‘(𝐹‘0)) / (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) + 1))))
295289, 294mpbird 256 . . . . . . . . . 10 (𝜑 → ((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) + 1) · 𝑋) ≤ (abs‘(𝐹‘0)))
296272, 283, 24, 285, 295ltletrd 11414 . . . . . . . . 9 (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) · 𝑋) < (abs‘(𝐹‘0)))
297272, 24, 280, 296ltmul1dd 13118 . . . . . . . 8 (𝜑 → ((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) · 𝑋) · (𝑋𝐾)) < ((abs‘(𝐹‘0)) · (𝑋𝐾)))
298271, 297eqbrtrd 5167 . . . . . . 7 (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) · (𝑋↑(𝐾 + 1))) < ((abs‘(𝐹‘0)) · (𝑋𝐾)))
299223, 231, 29, 264, 298lelttrd 11412 . . . . . 6 (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘))) < ((abs‘(𝐹‘0)) · (𝑋𝐾)))
30045, 223, 29, 224, 299lelttrd 11412 . . . . 5 (𝜑 → (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘))) < ((abs‘(𝐹‘0)) · (𝑋𝐾)))
30145, 29, 24, 300ltsub2dd 11867 . . . 4 (𝜑 → ((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋𝐾))) < ((abs‘(𝐹‘0)) − (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)))))
30230, 45, 24ltaddsubd 11854 . . . 4 (𝜑 → ((((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋𝐾))) + (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)))) < (abs‘(𝐹‘0)) ↔ ((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋𝐾))) < ((abs‘(𝐹‘0)) − (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘))))))
303301, 302mpbird 256 . . 3 (𝜑 → (((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋𝐾))) + (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)))) < (abs‘(𝐹‘0)))
30420, 46, 24, 221, 303lelttrd 11412 . 2 (𝜑 → (abs‘(𝐹‘(𝑇 · 𝑋))) < (abs‘(𝐹‘0)))
305 2fveq3 6897 . . . 4 (𝑥 = (𝑇 · 𝑋) → (abs‘(𝐹𝑥)) = (abs‘(𝐹‘(𝑇 · 𝑋))))
306305breq1d 5155 . . 3 (𝑥 = (𝑇 · 𝑋) → ((abs‘(𝐹𝑥)) < (abs‘(𝐹‘0)) ↔ (abs‘(𝐹‘(𝑇 · 𝑋))) < (abs‘(𝐹‘0))))
307306rspcev 3609 . 2 (((𝑇 · 𝑋) ∈ ℂ ∧ (abs‘(𝐹‘(𝑇 · 𝑋))) < (abs‘(𝐹‘0))) → ∃𝑥 ∈ ℂ (abs‘(𝐹𝑥)) < (abs‘(𝐹‘0)))
30816, 304, 307syl2anc 582 1 (𝜑 → ∃𝑥 ∈ ℂ (abs‘(𝐹𝑥)) < (abs‘(𝐹‘0)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 394  wo 845  w3a 1084   = wceq 1534  wcel 2099  wne 2930  wrex 3060  {crab 3420  cun 3946  cin 3947  wss 3948  c0 4324  ifcif 4525   class class class wbr 5145  wf 6541  cfv 6545  (class class class)co 7415  Fincfn 8965  infcinf 9476  cc 11146  cr 11147  0cc0 11148  1c1 11149   + caddc 11151   · cmul 11153   < clt 11288  cle 11289  cmin 11484  -cneg 11485   / cdiv 11911  cn 12257  0cn0 12517  cz 12603  cuz 12867  +crp 13021  ...cfz 13531  cexp 14074  abscabs 15233  Σcsu 15684  0𝑝c0p 25685  Polycply 26207  coeffccoe 26209  degcdgr 26210  𝑐ccxp 26578
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-rep 5282  ax-sep 5296  ax-nul 5303  ax-pow 5361  ax-pr 5425  ax-un 7737  ax-inf2 9676  ax-cnex 11204  ax-resscn 11205  ax-1cn 11206  ax-icn 11207  ax-addcl 11208  ax-addrcl 11209  ax-mulcl 11210  ax-mulrcl 11211  ax-mulcom 11212  ax-addass 11213  ax-mulass 11214  ax-distr 11215  ax-i2m1 11216  ax-1ne0 11217  ax-1rid 11218  ax-rnegex 11219  ax-rrecex 11220  ax-cnre 11221  ax-pre-lttri 11222  ax-pre-lttrn 11223  ax-pre-ltadd 11224  ax-pre-mulgt0 11225  ax-pre-sup 11226  ax-addf 11227
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3365  df-reu 3366  df-rab 3421  df-v 3466  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3968  df-nul 4325  df-if 4526  df-pw 4601  df-sn 4626  df-pr 4628  df-tp 4630  df-op 4632  df-uni 4908  df-int 4949  df-iun 4997  df-iin 4998  df-br 5146  df-opab 5208  df-mpt 5229  df-tr 5263  df-id 5572  df-eprel 5578  df-po 5586  df-so 5587  df-fr 5629  df-se 5630  df-we 5631  df-xp 5680  df-rel 5681  df-cnv 5682  df-co 5683  df-dm 5684  df-rn 5685  df-res 5686  df-ima 5687  df-pred 6304  df-ord 6370  df-on 6371  df-lim 6372  df-suc 6373  df-iota 6497  df-fun 6547  df-fn 6548  df-f 6549  df-f1 6550  df-fo 6551  df-f1o 6552  df-fv 6553  df-isom 6554  df-riota 7371  df-ov 7418  df-oprab 7419  df-mpo 7420  df-of 7681  df-om 7868  df-1st 7994  df-2nd 7995  df-supp 8166  df-frecs 8287  df-wrecs 8318  df-recs 8392  df-rdg 8431  df-1o 8487  df-2o 8488  df-er 8725  df-map 8848  df-pm 8849  df-ixp 8918  df-en 8966  df-dom 8967  df-sdom 8968  df-fin 8969  df-fsupp 9398  df-fi 9446  df-sup 9477  df-inf 9478  df-oi 9545  df-card 9974  df-pnf 11290  df-mnf 11291  df-xr 11292  df-ltxr 11293  df-le 11294  df-sub 11486  df-neg 11487  df-div 11912  df-nn 12258  df-2 12320  df-3 12321  df-4 12322  df-5 12323  df-6 12324  df-7 12325  df-8 12326  df-9 12327  df-n0 12518  df-z 12604  df-dec 12723  df-uz 12868  df-q 12978  df-rp 13022  df-xneg 13139  df-xadd 13140  df-xmul 13141  df-ioo 13375  df-ioc 13376  df-ico 13377  df-icc 13378  df-fz 13532  df-fzo 13675  df-fl 13805  df-mod 13883  df-seq 14015  df-exp 14075  df-fac 14285  df-bc 14314  df-hash 14342  df-shft 15066  df-cj 15098  df-re 15099  df-im 15100  df-sqrt 15234  df-abs 15235  df-limsup 15467  df-clim 15484  df-rlim 15485  df-sum 15685  df-ef 16063  df-sin 16065  df-cos 16066  df-pi 16068  df-struct 17143  df-sets 17160  df-slot 17178  df-ndx 17190  df-base 17208  df-ress 17237  df-plusg 17273  df-mulr 17274  df-starv 17275  df-sca 17276  df-vsca 17277  df-ip 17278  df-tset 17279  df-ple 17280  df-ds 17282  df-unif 17283  df-hom 17284  df-cco 17285  df-rest 17431  df-topn 17432  df-0g 17450  df-gsum 17451  df-topgen 17452  df-pt 17453  df-prds 17456  df-xrs 17511  df-qtop 17516  df-imas 17517  df-xps 17519  df-mre 17593  df-mrc 17594  df-acs 17596  df-mgm 18627  df-sgrp 18706  df-mnd 18722  df-submnd 18768  df-mulg 19057  df-cntz 19306  df-cmn 19775  df-psmet 21330  df-xmet 21331  df-met 21332  df-bl 21333  df-mopn 21334  df-fbas 21335  df-fg 21336  df-cnfld 21339  df-top 22883  df-topon 22900  df-topsp 22922  df-bases 22936  df-cld 23010  df-ntr 23011  df-cls 23012  df-nei 23089  df-lp 23127  df-perf 23128  df-cn 23218  df-cnp 23219  df-haus 23306  df-tx 23553  df-hmeo 23746  df-fil 23837  df-fm 23929  df-flim 23930  df-flf 23931  df-xms 24313  df-ms 24314  df-tms 24315  df-cncf 24885  df-0p 25686  df-limc 25882  df-dv 25883  df-ply 26211  df-coe 26213  df-dgr 26214  df-log 26579  df-cxp 26580
This theorem is referenced by:  ftalem6  27102
  Copyright terms: Public domain W3C validator