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

Theorem ftalem5 25668
Description: Lemma for fta 25671: Main proof. We have already shifted the minimum found in ftalem3 25666 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 25667 . . . . 5 (𝜑 → ((𝐾 ∈ ℕ ∧ (𝐴𝐾) ≠ 0) ∧ (𝑇 ∈ ℂ ∧ 𝑈 ∈ ℝ+𝑋 ∈ ℝ+)))
1110simprd 499 . . . 4 (𝜑 → (𝑇 ∈ ℂ ∧ 𝑈 ∈ ℝ+𝑋 ∈ ℝ+))
1211simp1d 1139 . . 3 (𝜑𝑇 ∈ ℂ)
1311simp3d 1141 . . . . 5 (𝜑𝑋 ∈ ℝ+)
1413rpred 12428 . . . 4 (𝜑𝑋 ∈ ℝ)
1514recnd 10667 . . 3 (𝜑𝑋 ∈ ℂ)
1612, 15mulcld 10659 . 2 (𝜑 → (𝑇 · 𝑋) ∈ ℂ)
17 plyf 24801 . . . . . 6 (𝐹 ∈ (Poly‘𝑆) → 𝐹:ℂ⟶ℂ)
183, 17syl 17 . . . . 5 (𝜑𝐹:ℂ⟶ℂ)
1918, 16ffvelrnd 6843 . . . 4 (𝜑 → (𝐹‘(𝑇 · 𝑋)) ∈ ℂ)
2019abscld 14796 . . 3 (𝜑 → (abs‘(𝐹‘(𝑇 · 𝑋))) ∈ ℝ)
21 0cn 10631 . . . . . . 7 0 ∈ ℂ
22 ffvelrn 6840 . . . . . . 7 ((𝐹:ℂ⟶ℂ ∧ 0 ∈ ℂ) → (𝐹‘0) ∈ ℂ)
2318, 21, 22sylancl 589 . . . . . 6 (𝜑 → (𝐹‘0) ∈ ℂ)
2423abscld 14796 . . . . 5 (𝜑 → (abs‘(𝐹‘0)) ∈ ℝ)
2510simpld 498 . . . . . . . . 9 (𝜑 → (𝐾 ∈ ℕ ∧ (𝐴𝐾) ≠ 0))
2625simpld 498 . . . . . . . 8 (𝜑𝐾 ∈ ℕ)
2726nnnn0d 11952 . . . . . . 7 (𝜑𝐾 ∈ ℕ0)
2814, 27reexpcld 13532 . . . . . 6 (𝜑 → (𝑋𝐾) ∈ ℝ)
2924, 28remulcld 10669 . . . . 5 (𝜑 → ((abs‘(𝐹‘0)) · (𝑋𝐾)) ∈ ℝ)
3024, 29resubcld 11066 . . . 4 (𝜑 → ((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋𝐾))) ∈ ℝ)
31 fzfid 13345 . . . . . 6 (𝜑 → ((𝐾 + 1)...𝑁) ∈ Fin)
321coef3 24835 . . . . . . . . 9 (𝐹 ∈ (Poly‘𝑆) → 𝐴:ℕ0⟶ℂ)
333, 32syl 17 . . . . . . . 8 (𝜑𝐴:ℕ0⟶ℂ)
34 peano2nn0 11934 . . . . . . . . . 10 (𝐾 ∈ ℕ0 → (𝐾 + 1) ∈ ℕ0)
3527, 34syl 17 . . . . . . . . 9 (𝜑 → (𝐾 + 1) ∈ ℕ0)
36 elfzuz 12907 . . . . . . . . 9 (𝑘 ∈ ((𝐾 + 1)...𝑁) → 𝑘 ∈ (ℤ‘(𝐾 + 1)))
37 eluznn0 12314 . . . . . . . . 9 (((𝐾 + 1) ∈ ℕ0𝑘 ∈ (ℤ‘(𝐾 + 1))) → 𝑘 ∈ ℕ0)
3835, 36, 37syl2an 598 . . . . . . . 8 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑘 ∈ ℕ0)
39 ffvelrn 6840 . . . . . . . 8 ((𝐴:ℕ0⟶ℂ ∧ 𝑘 ∈ ℕ0) → (𝐴𝑘) ∈ ℂ)
4033, 38, 39syl2an2r 684 . . . . . . 7 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝐴𝑘) ∈ ℂ)
4116adantr 484 . . . . . . . 8 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑇 · 𝑋) ∈ ℂ)
4241, 38expcld 13515 . . . . . . 7 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((𝑇 · 𝑋)↑𝑘) ∈ ℂ)
4340, 42mulcld 10659 . . . . . 6 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) ∈ ℂ)
4431, 43fsumcl 15090 . . . . 5 (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) ∈ ℂ)
4544abscld 14796 . . . 4 (𝜑 → (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘))) ∈ ℝ)
4630, 45readdcld 10668 . . 3 (𝜑 → (((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋𝐾))) + (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)))) ∈ ℝ)
47 fzfid 13345 . . . . . 6 (𝜑 → (0...𝐾) ∈ Fin)
48 elfznn0 13004 . . . . . . . 8 (𝑘 ∈ (0...𝐾) → 𝑘 ∈ ℕ0)
4933, 48, 39syl2an 598 . . . . . . 7 ((𝜑𝑘 ∈ (0...𝐾)) → (𝐴𝑘) ∈ ℂ)
50 expcl 13452 . . . . . . . 8 (((𝑇 · 𝑋) ∈ ℂ ∧ 𝑘 ∈ ℕ0) → ((𝑇 · 𝑋)↑𝑘) ∈ ℂ)
5116, 48, 50syl2an 598 . . . . . . 7 ((𝜑𝑘 ∈ (0...𝐾)) → ((𝑇 · 𝑋)↑𝑘) ∈ ℂ)
5249, 51mulcld 10659 . . . . . 6 ((𝜑𝑘 ∈ (0...𝐾)) → ((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) ∈ ℂ)
5347, 52fsumcl 15090 . . . . 5 (𝜑 → Σ𝑘 ∈ (0...𝐾)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) ∈ ℂ)
5453, 44abstrid 14816 . . . 4 (𝜑 → (abs‘(Σ𝑘 ∈ (0...𝐾)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) + Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)))) ≤ ((abs‘Σ𝑘 ∈ (0...𝐾)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘))) + (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)))))
551, 2coeid2 24842 . . . . . . 7 ((𝐹 ∈ (Poly‘𝑆) ∧ (𝑇 · 𝑋) ∈ ℂ) → (𝐹‘(𝑇 · 𝑋)) = Σ𝑘 ∈ (0...𝑁)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)))
563, 16, 55syl2anc 587 . . . . . 6 (𝜑 → (𝐹‘(𝑇 · 𝑋)) = Σ𝑘 ∈ (0...𝑁)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)))
5726nnred 11649 . . . . . . . . 9 (𝜑𝐾 ∈ ℝ)
5857ltp1d 11568 . . . . . . . 8 (𝜑𝐾 < (𝐾 + 1))
59 fzdisj 12938 . . . . . . . 8 (𝐾 < (𝐾 + 1) → ((0...𝐾) ∩ ((𝐾 + 1)...𝑁)) = ∅)
6058, 59syl 17 . . . . . . 7 (𝜑 → ((0...𝐾) ∩ ((𝐾 + 1)...𝑁)) = ∅)
61 ssrab2 4042 . . . . . . . . . . . 12 {𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0} ⊆ ℕ
62 nnuz 12278 . . . . . . . . . . . 12 ℕ = (ℤ‘1)
6361, 62sseqtri 3989 . . . . . . . . . . 11 {𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0} ⊆ (ℤ‘1)
64 fveq2 6661 . . . . . . . . . . . . 13 (𝑛 = 𝑁 → (𝐴𝑛) = (𝐴𝑁))
6564neeq1d 3073 . . . . . . . . . . . 12 (𝑛 = 𝑁 → ((𝐴𝑛) ≠ 0 ↔ (𝐴𝑁) ≠ 0))
664nnne0d 11684 . . . . . . . . . . . . 13 (𝜑𝑁 ≠ 0)
672, 1dgreq0 24868 . . . . . . . . . . . . . . . 16 (𝐹 ∈ (Poly‘𝑆) → (𝐹 = 0𝑝 ↔ (𝐴𝑁) = 0))
683, 67syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (𝐹 = 0𝑝 ↔ (𝐴𝑁) = 0))
69 fveq2 6661 . . . . . . . . . . . . . . . . 17 (𝐹 = 0𝑝 → (deg‘𝐹) = (deg‘0𝑝))
70 dgr0 24865 . . . . . . . . . . . . . . . . 17 (deg‘0𝑝) = 0
7169, 70syl6eq 2875 . . . . . . . . . . . . . . . 16 (𝐹 = 0𝑝 → (deg‘𝐹) = 0)
722, 71syl5eq 2871 . . . . . . . . . . . . . . 15 (𝐹 = 0𝑝𝑁 = 0)
7368, 72syl6bir 257 . . . . . . . . . . . . . 14 (𝜑 → ((𝐴𝑁) = 0 → 𝑁 = 0))
7473necon3d 3035 . . . . . . . . . . . . 13 (𝜑 → (𝑁 ≠ 0 → (𝐴𝑁) ≠ 0))
7566, 74mpd 15 . . . . . . . . . . . 12 (𝜑 → (𝐴𝑁) ≠ 0)
7665, 4, 75elrabd 3668 . . . . . . . . . . 11 (𝜑𝑁 ∈ {𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0})
77 infssuzle 12328 . . . . . . . . . . 11 (({𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0} ⊆ (ℤ‘1) ∧ 𝑁 ∈ {𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0}) → inf({𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0}, ℝ, < ) ≤ 𝑁)
7863, 76, 77sylancr 590 . . . . . . . . . 10 (𝜑 → inf({𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0}, ℝ, < ) ≤ 𝑁)
796, 78eqbrtrid 5087 . . . . . . . . 9 (𝜑𝐾𝑁)
80 nn0uz 12277 . . . . . . . . . . 11 0 = (ℤ‘0)
8127, 80eleqtrdi 2926 . . . . . . . . . 10 (𝜑𝐾 ∈ (ℤ‘0))
824nnzd 12083 . . . . . . . . . 10 (𝜑𝑁 ∈ ℤ)
83 elfz5 12903 . . . . . . . . . 10 ((𝐾 ∈ (ℤ‘0) ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (0...𝑁) ↔ 𝐾𝑁))
8481, 82, 83syl2anc 587 . . . . . . . . 9 (𝜑 → (𝐾 ∈ (0...𝑁) ↔ 𝐾𝑁))
8579, 84mpbird 260 . . . . . . . 8 (𝜑𝐾 ∈ (0...𝑁))
86 fzsplit 12937 . . . . . . . 8 (𝐾 ∈ (0...𝑁) → (0...𝑁) = ((0...𝐾) ∪ ((𝐾 + 1)...𝑁)))
8785, 86syl 17 . . . . . . 7 (𝜑 → (0...𝑁) = ((0...𝐾) ∪ ((𝐾 + 1)...𝑁)))
88 fzfid 13345 . . . . . . 7 (𝜑 → (0...𝑁) ∈ Fin)
89 elfznn0 13004 . . . . . . . . 9 (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0)
9033, 89, 39syl2an 598 . . . . . . . 8 ((𝜑𝑘 ∈ (0...𝑁)) → (𝐴𝑘) ∈ ℂ)
9116, 89, 50syl2an 598 . . . . . . . 8 ((𝜑𝑘 ∈ (0...𝑁)) → ((𝑇 · 𝑋)↑𝑘) ∈ ℂ)
9290, 91mulcld 10659 . . . . . . 7 ((𝜑𝑘 ∈ (0...𝑁)) → ((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) ∈ ℂ)
9360, 87, 88, 92fsumsplit 15097 . . . . . 6 (𝜑 → Σ𝑘 ∈ (0...𝑁)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) = (Σ𝑘 ∈ (0...𝐾)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) + Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘))))
9456, 93eqtrd 2859 . . . . 5 (𝜑 → (𝐹‘(𝑇 · 𝑋)) = (Σ𝑘 ∈ (0...𝐾)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) + Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘))))
9594fveq2d 6665 . . . 4 (𝜑 → (abs‘(𝐹‘(𝑇 · 𝑋))) = (abs‘(Σ𝑘 ∈ (0...𝐾)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) + Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)))))
961coefv0 24851 . . . . . . . . . . . . 13 (𝐹 ∈ (Poly‘𝑆) → (𝐹‘0) = (𝐴‘0))
973, 96syl 17 . . . . . . . . . . . 12 (𝜑 → (𝐹‘0) = (𝐴‘0))
9897eqcomd 2830 . . . . . . . . . . 11 (𝜑 → (𝐴‘0) = (𝐹‘0))
9916exp0d 13509 . . . . . . . . . . 11 (𝜑 → ((𝑇 · 𝑋)↑0) = 1)
10098, 99oveq12d 7167 . . . . . . . . . 10 (𝜑 → ((𝐴‘0) · ((𝑇 · 𝑋)↑0)) = ((𝐹‘0) · 1))
10123mulid1d 10656 . . . . . . . . . 10 (𝜑 → ((𝐹‘0) · 1) = (𝐹‘0))
102100, 101eqtrd 2859 . . . . . . . . 9 (𝜑 → ((𝐴‘0) · ((𝑇 · 𝑋)↑0)) = (𝐹‘0))
103 1e0p1 12137 . . . . . . . . . . . . 13 1 = (0 + 1)
104103oveq1i 7159 . . . . . . . . . . . 12 (1...𝐾) = ((0 + 1)...𝐾)
105104sumeq1i 15055 . . . . . . . . . . 11 Σ𝑘 ∈ (1...𝐾)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) = Σ𝑘 ∈ ((0 + 1)...𝐾)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘))
10626, 62eleqtrdi 2926 . . . . . . . . . . . 12 (𝜑𝐾 ∈ (ℤ‘1))
107 elfznn 12940 . . . . . . . . . . . . . . 15 (𝑘 ∈ (1...𝐾) → 𝑘 ∈ ℕ)
108107nnnn0d 11952 . . . . . . . . . . . . . 14 (𝑘 ∈ (1...𝐾) → 𝑘 ∈ ℕ0)
10933, 108, 39syl2an 598 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (1...𝐾)) → (𝐴𝑘) ∈ ℂ)
11016, 108, 50syl2an 598 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (1...𝐾)) → ((𝑇 · 𝑋)↑𝑘) ∈ ℂ)
111109, 110mulcld 10659 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (1...𝐾)) → ((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) ∈ ℂ)
112 fveq2 6661 . . . . . . . . . . . . 13 (𝑘 = 𝐾 → (𝐴𝑘) = (𝐴𝐾))
113 oveq2 7157 . . . . . . . . . . . . 13 (𝑘 = 𝐾 → ((𝑇 · 𝑋)↑𝑘) = ((𝑇 · 𝑋)↑𝐾))
114112, 113oveq12d 7167 . . . . . . . . . . . 12 (𝑘 = 𝐾 → ((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) = ((𝐴𝐾) · ((𝑇 · 𝑋)↑𝐾)))
115106, 111, 114fsumm1 15106 . . . . . . . . . . 11 (𝜑 → Σ𝑘 ∈ (1...𝐾)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) = (Σ𝑘 ∈ (1...(𝐾 − 1))((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) + ((𝐴𝐾) · ((𝑇 · 𝑋)↑𝐾))))
116105, 115syl5eqr 2873 . . . . . . . . . 10 (𝜑 → Σ𝑘 ∈ ((0 + 1)...𝐾)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) = (Σ𝑘 ∈ (1...(𝐾 − 1))((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) + ((𝐴𝐾) · ((𝑇 · 𝑋)↑𝐾))))
117 elfznn 12940 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 ∈ (1...(𝐾 − 1)) → 𝑘 ∈ ℕ)
118117adantl 485 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ (1...(𝐾 − 1))) → 𝑘 ∈ ℕ)
119118nnred 11649 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ (1...(𝐾 − 1))) → 𝑘 ∈ ℝ)
12057adantr 484 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ (1...(𝐾 − 1))) → 𝐾 ∈ ℝ)
121 peano2rem 10951 . . . . . . . . . . . . . . . . . . . 20 (𝐾 ∈ ℝ → (𝐾 − 1) ∈ ℝ)
122120, 121syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ (1...(𝐾 − 1))) → (𝐾 − 1) ∈ ℝ)
123 elfzle2 12915 . . . . . . . . . . . . . . . . . . . 20 (𝑘 ∈ (1...(𝐾 − 1)) → 𝑘 ≤ (𝐾 − 1))
124123adantl 485 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ (1...(𝐾 − 1))) → 𝑘 ≤ (𝐾 − 1))
125120ltm1d 11570 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ (1...(𝐾 − 1))) → (𝐾 − 1) < 𝐾)
126119, 122, 120, 124, 125lelttrd 10796 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ (1...(𝐾 − 1))) → 𝑘 < 𝐾)
127119, 120ltnled 10785 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ (1...(𝐾 − 1))) → (𝑘 < 𝐾 ↔ ¬ 𝐾𝑘))
128126, 127mpbid 235 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ (1...(𝐾 − 1))) → ¬ 𝐾𝑘)
129 infssuzle 12328 . . . . . . . . . . . . . . . . . . 19 (({𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0} ⊆ (ℤ‘1) ∧ 𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0}) → inf({𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0}, ℝ, < ) ≤ 𝑘)
1306, 129eqbrtrid 5087 . . . . . . . . . . . . . . . . . 18 (({𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0} ⊆ (ℤ‘1) ∧ 𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0}) → 𝐾𝑘)
13163, 130mpan 689 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0} → 𝐾𝑘)
132128, 131nsyl 142 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (1...(𝐾 − 1))) → ¬ 𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0})
133 fveq2 6661 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 𝑘 → (𝐴𝑛) = (𝐴𝑘))
134133neeq1d 3073 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 𝑘 → ((𝐴𝑛) ≠ 0 ↔ (𝐴𝑘) ≠ 0))
135134elrab3 3667 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ℕ → (𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0} ↔ (𝐴𝑘) ≠ 0))
136118, 135syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ (1...(𝐾 − 1))) → (𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0} ↔ (𝐴𝑘) ≠ 0))
137136necon2bbid 3057 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (1...(𝐾 − 1))) → ((𝐴𝑘) = 0 ↔ ¬ 𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0}))
138132, 137mpbird 260 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (1...(𝐾 − 1))) → (𝐴𝑘) = 0)
139138oveq1d 7164 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (1...(𝐾 − 1))) → ((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) = (0 · ((𝑇 · 𝑋)↑𝑘)))
140117nnnn0d 11952 . . . . . . . . . . . . . . . 16 (𝑘 ∈ (1...(𝐾 − 1)) → 𝑘 ∈ ℕ0)
14116, 140, 50syl2an 598 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (1...(𝐾 − 1))) → ((𝑇 · 𝑋)↑𝑘) ∈ ℂ)
142141mul02d 10836 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (1...(𝐾 − 1))) → (0 · ((𝑇 · 𝑋)↑𝑘)) = 0)
143139, 142eqtrd 2859 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (1...(𝐾 − 1))) → ((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) = 0)
144143sumeq2dv 15060 . . . . . . . . . . . 12 (𝜑 → Σ𝑘 ∈ (1...(𝐾 − 1))((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) = Σ𝑘 ∈ (1...(𝐾 − 1))0)
145 fzfi 13344 . . . . . . . . . . . . . 14 (1...(𝐾 − 1)) ∈ Fin
146145olci 863 . . . . . . . . . . . . 13 ((1...(𝐾 − 1)) ⊆ (ℤ‘1) ∨ (1...(𝐾 − 1)) ∈ Fin)
147 sumz 15079 . . . . . . . . . . . . 13 (((1...(𝐾 − 1)) ⊆ (ℤ‘1) ∨ (1...(𝐾 − 1)) ∈ Fin) → Σ𝑘 ∈ (1...(𝐾 − 1))0 = 0)
148146, 147ax-mp 5 . . . . . . . . . . . 12 Σ𝑘 ∈ (1...(𝐾 − 1))0 = 0
149144, 148syl6eq 2875 . . . . . . . . . . 11 (𝜑 → Σ𝑘 ∈ (1...(𝐾 − 1))((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) = 0)
15012, 15, 27mulexpd 13530 . . . . . . . . . . . . . 14 (𝜑 → ((𝑇 · 𝑋)↑𝐾) = ((𝑇𝐾) · (𝑋𝐾)))
151150oveq2d 7165 . . . . . . . . . . . . 13 (𝜑 → ((𝐴𝐾) · ((𝑇 · 𝑋)↑𝐾)) = ((𝐴𝐾) · ((𝑇𝐾) · (𝑋𝐾))))
15233, 27ffvelrnd 6843 . . . . . . . . . . . . . 14 (𝜑 → (𝐴𝐾) ∈ ℂ)
15312, 27expcld 13515 . . . . . . . . . . . . . 14 (𝜑 → (𝑇𝐾) ∈ ℂ)
15428recnd 10667 . . . . . . . . . . . . . 14 (𝜑 → (𝑋𝐾) ∈ ℂ)
155152, 153, 154mulassd 10662 . . . . . . . . . . . . 13 (𝜑 → (((𝐴𝐾) · (𝑇𝐾)) · (𝑋𝐾)) = ((𝐴𝐾) · ((𝑇𝐾) · (𝑋𝐾))))
156151, 155eqtr4d 2862 . . . . . . . . . . . 12 (𝜑 → ((𝐴𝐾) · ((𝑇 · 𝑋)↑𝐾)) = (((𝐴𝐾) · (𝑇𝐾)) · (𝑋𝐾)))
1577oveq1i 7159 . . . . . . . . . . . . . . . 16 (𝑇𝐾) = ((-((𝐹‘0) / (𝐴𝐾))↑𝑐(1 / 𝐾))↑𝐾)
15857recnd 10667 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐾 ∈ ℂ)
15926nnne0d 11684 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐾 ≠ 0)
160158, 159recid2d 11410 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((1 / 𝐾) · 𝐾) = 1)
161160oveq2d 7165 . . . . . . . . . . . . . . . . 17 (𝜑 → (-((𝐹‘0) / (𝐴𝐾))↑𝑐((1 / 𝐾) · 𝐾)) = (-((𝐹‘0) / (𝐴𝐾))↑𝑐1))
16225simprd 499 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐴𝐾) ≠ 0)
16323, 152, 162divcld 11414 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝐹‘0) / (𝐴𝐾)) ∈ ℂ)
164163negcld 10982 . . . . . . . . . . . . . . . . . 18 (𝜑 → -((𝐹‘0) / (𝐴𝐾)) ∈ ℂ)
16526nnrecred 11685 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (1 / 𝐾) ∈ ℝ)
166165recnd 10667 . . . . . . . . . . . . . . . . . 18 (𝜑 → (1 / 𝐾) ∈ ℂ)
167164, 166, 27cxpmul2d 25306 . . . . . . . . . . . . . . . . 17 (𝜑 → (-((𝐹‘0) / (𝐴𝐾))↑𝑐((1 / 𝐾) · 𝐾)) = ((-((𝐹‘0) / (𝐴𝐾))↑𝑐(1 / 𝐾))↑𝐾))
168164cxp1d 25303 . . . . . . . . . . . . . . . . 17 (𝜑 → (-((𝐹‘0) / (𝐴𝐾))↑𝑐1) = -((𝐹‘0) / (𝐴𝐾)))
169161, 167, 1683eqtr3d 2867 . . . . . . . . . . . . . . . 16 (𝜑 → ((-((𝐹‘0) / (𝐴𝐾))↑𝑐(1 / 𝐾))↑𝐾) = -((𝐹‘0) / (𝐴𝐾)))
170157, 169syl5eq 2871 . . . . . . . . . . . . . . 15 (𝜑 → (𝑇𝐾) = -((𝐹‘0) / (𝐴𝐾)))
171170oveq2d 7165 . . . . . . . . . . . . . 14 (𝜑 → ((𝐴𝐾) · (𝑇𝐾)) = ((𝐴𝐾) · -((𝐹‘0) / (𝐴𝐾))))
172152, 163mulneg2d 11092 . . . . . . . . . . . . . 14 (𝜑 → ((𝐴𝐾) · -((𝐹‘0) / (𝐴𝐾))) = -((𝐴𝐾) · ((𝐹‘0) / (𝐴𝐾))))
17323, 152, 162divcan2d 11416 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐴𝐾) · ((𝐹‘0) / (𝐴𝐾))) = (𝐹‘0))
174173negeqd 10878 . . . . . . . . . . . . . 14 (𝜑 → -((𝐴𝐾) · ((𝐹‘0) / (𝐴𝐾))) = -(𝐹‘0))
175171, 172, 1743eqtrd 2863 . . . . . . . . . . . . 13 (𝜑 → ((𝐴𝐾) · (𝑇𝐾)) = -(𝐹‘0))
176175oveq1d 7164 . . . . . . . . . . . 12 (𝜑 → (((𝐴𝐾) · (𝑇𝐾)) · (𝑋𝐾)) = (-(𝐹‘0) · (𝑋𝐾)))
17723, 154mulneg1d 11091 . . . . . . . . . . . 12 (𝜑 → (-(𝐹‘0) · (𝑋𝐾)) = -((𝐹‘0) · (𝑋𝐾)))
178156, 176, 1773eqtrd 2863 . . . . . . . . . . 11 (𝜑 → ((𝐴𝐾) · ((𝑇 · 𝑋)↑𝐾)) = -((𝐹‘0) · (𝑋𝐾)))
179149, 178oveq12d 7167 . . . . . . . . . 10 (𝜑 → (Σ𝑘 ∈ (1...(𝐾 − 1))((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) + ((𝐴𝐾) · ((𝑇 · 𝑋)↑𝐾))) = (0 + -((𝐹‘0) · (𝑋𝐾))))
18023, 154mulcld 10659 . . . . . . . . . . . 12 (𝜑 → ((𝐹‘0) · (𝑋𝐾)) ∈ ℂ)
181180negcld 10982 . . . . . . . . . . 11 (𝜑 → -((𝐹‘0) · (𝑋𝐾)) ∈ ℂ)
182181addid2d 10839 . . . . . . . . . 10 (𝜑 → (0 + -((𝐹‘0) · (𝑋𝐾))) = -((𝐹‘0) · (𝑋𝐾)))
183116, 179, 1823eqtrd 2863 . . . . . . . . 9 (𝜑 → Σ𝑘 ∈ ((0 + 1)...𝐾)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) = -((𝐹‘0) · (𝑋𝐾)))
184102, 183oveq12d 7167 . . . . . . . 8 (𝜑 → (((𝐴‘0) · ((𝑇 · 𝑋)↑0)) + Σ𝑘 ∈ ((0 + 1)...𝐾)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘))) = ((𝐹‘0) + -((𝐹‘0) · (𝑋𝐾))))
185 fveq2 6661 . . . . . . . . . 10 (𝑘 = 0 → (𝐴𝑘) = (𝐴‘0))
186 oveq2 7157 . . . . . . . . . 10 (𝑘 = 0 → ((𝑇 · 𝑋)↑𝑘) = ((𝑇 · 𝑋)↑0))
187185, 186oveq12d 7167 . . . . . . . . 9 (𝑘 = 0 → ((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) = ((𝐴‘0) · ((𝑇 · 𝑋)↑0)))
18881, 52, 187fsum1p 15108 . . . . . . . 8 (𝜑 → Σ𝑘 ∈ (0...𝐾)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) = (((𝐴‘0) · ((𝑇 · 𝑋)↑0)) + Σ𝑘 ∈ ((0 + 1)...𝐾)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘))))
189101oveq1d 7164 . . . . . . . . 9 (𝜑 → (((𝐹‘0) · 1) − ((𝐹‘0) · (𝑋𝐾))) = ((𝐹‘0) − ((𝐹‘0) · (𝑋𝐾))))
190 1cnd 10634 . . . . . . . . . 10 (𝜑 → 1 ∈ ℂ)
19123, 190, 154subdid 11094 . . . . . . . . 9 (𝜑 → ((𝐹‘0) · (1 − (𝑋𝐾))) = (((𝐹‘0) · 1) − ((𝐹‘0) · (𝑋𝐾))))
19223, 180negsubd 11001 . . . . . . . . 9 (𝜑 → ((𝐹‘0) + -((𝐹‘0) · (𝑋𝐾))) = ((𝐹‘0) − ((𝐹‘0) · (𝑋𝐾))))
193189, 191, 1923eqtr4d 2869 . . . . . . . 8 (𝜑 → ((𝐹‘0) · (1 − (𝑋𝐾))) = ((𝐹‘0) + -((𝐹‘0) · (𝑋𝐾))))
194184, 188, 1933eqtr4d 2869 . . . . . . 7 (𝜑 → Σ𝑘 ∈ (0...𝐾)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) = ((𝐹‘0) · (1 − (𝑋𝐾))))
195194fveq2d 6665 . . . . . 6 (𝜑 → (abs‘Σ𝑘 ∈ (0...𝐾)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘))) = (abs‘((𝐹‘0) · (1 − (𝑋𝐾)))))
196 1re 10639 . . . . . . . . 9 1 ∈ ℝ
197 resubcl 10948 . . . . . . . . 9 ((1 ∈ ℝ ∧ (𝑋𝐾) ∈ ℝ) → (1 − (𝑋𝐾)) ∈ ℝ)
198196, 28, 197sylancr 590 . . . . . . . 8 (𝜑 → (1 − (𝑋𝐾)) ∈ ℝ)
199198recnd 10667 . . . . . . 7 (𝜑 → (1 − (𝑋𝐾)) ∈ ℂ)
20023, 199absmuld 14814 . . . . . 6 (𝜑 → (abs‘((𝐹‘0) · (1 − (𝑋𝐾)))) = ((abs‘(𝐹‘0)) · (abs‘(1 − (𝑋𝐾)))))
20113rpge0d 12432 . . . . . . . . . . 11 (𝜑 → 0 ≤ 𝑋)
20211simp2d 1140 . . . . . . . . . . . . . 14 (𝜑𝑈 ∈ ℝ+)
203202rpred 12428 . . . . . . . . . . . . 13 (𝜑𝑈 ∈ ℝ)
204 min1 12579 . . . . . . . . . . . . 13 ((1 ∈ ℝ ∧ 𝑈 ∈ ℝ) → if(1 ≤ 𝑈, 1, 𝑈) ≤ 1)
205196, 203, 204sylancr 590 . . . . . . . . . . . 12 (𝜑 → if(1 ≤ 𝑈, 1, 𝑈) ≤ 1)
2069, 205eqbrtrid 5087 . . . . . . . . . . 11 (𝜑𝑋 ≤ 1)
207 exple1 13545 . . . . . . . . . . 11 (((𝑋 ∈ ℝ ∧ 0 ≤ 𝑋𝑋 ≤ 1) ∧ 𝐾 ∈ ℕ0) → (𝑋𝐾) ≤ 1)
20814, 201, 206, 27, 207syl31anc 1370 . . . . . . . . . 10 (𝜑 → (𝑋𝐾) ≤ 1)
209 subge0 11151 . . . . . . . . . . 11 ((1 ∈ ℝ ∧ (𝑋𝐾) ∈ ℝ) → (0 ≤ (1 − (𝑋𝐾)) ↔ (𝑋𝐾) ≤ 1))
210196, 28, 209sylancr 590 . . . . . . . . . 10 (𝜑 → (0 ≤ (1 − (𝑋𝐾)) ↔ (𝑋𝐾) ≤ 1))
211208, 210mpbird 260 . . . . . . . . 9 (𝜑 → 0 ≤ (1 − (𝑋𝐾)))
212198, 211absidd 14782 . . . . . . . 8 (𝜑 → (abs‘(1 − (𝑋𝐾))) = (1 − (𝑋𝐾)))
213212oveq2d 7165 . . . . . . 7 (𝜑 → ((abs‘(𝐹‘0)) · (abs‘(1 − (𝑋𝐾)))) = ((abs‘(𝐹‘0)) · (1 − (𝑋𝐾))))
21424recnd 10667 . . . . . . . 8 (𝜑 → (abs‘(𝐹‘0)) ∈ ℂ)
215214, 190, 154subdid 11094 . . . . . . 7 (𝜑 → ((abs‘(𝐹‘0)) · (1 − (𝑋𝐾))) = (((abs‘(𝐹‘0)) · 1) − ((abs‘(𝐹‘0)) · (𝑋𝐾))))
216214mulid1d 10656 . . . . . . . 8 (𝜑 → ((abs‘(𝐹‘0)) · 1) = (abs‘(𝐹‘0)))
217216oveq1d 7164 . . . . . . 7 (𝜑 → (((abs‘(𝐹‘0)) · 1) − ((abs‘(𝐹‘0)) · (𝑋𝐾))) = ((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋𝐾))))
218213, 215, 2173eqtrd 2863 . . . . . 6 (𝜑 → ((abs‘(𝐹‘0)) · (abs‘(1 − (𝑋𝐾)))) = ((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋𝐾))))
219195, 200, 2183eqtrrd 2864 . . . . 5 (𝜑 → ((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋𝐾))) = (abs‘Σ𝑘 ∈ (0...𝐾)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘))))
220219oveq1d 7164 . . . 4 (𝜑 → (((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋𝐾))) + (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)))) = ((abs‘Σ𝑘 ∈ (0...𝐾)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘))) + (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)))))
22154, 95, 2203brtr4d 5084 . . 3 (𝜑 → (abs‘(𝐹‘(𝑇 · 𝑋))) ≤ (((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋𝐾))) + (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)))))
22243abscld 14796 . . . . . . 7 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘))) ∈ ℝ)
22331, 222fsumrecl 15091 . . . . . 6 (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘))) ∈ ℝ)
22431, 43fsumabs 15156 . . . . . 6 (𝜑 → (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘))) ≤ Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘))))
225 expcl 13452 . . . . . . . . . . . 12 ((𝑇 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (𝑇𝑘) ∈ ℂ)
22612, 38, 225syl2an2r 684 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑇𝑘) ∈ ℂ)
22740, 226mulcld 10659 . . . . . . . . . 10 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((𝐴𝑘) · (𝑇𝑘)) ∈ ℂ)
228227abscld 14796 . . . . . . . . 9 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘((𝐴𝑘) · (𝑇𝑘))) ∈ ℝ)
22931, 228fsumrecl 15091 . . . . . . . 8 (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) ∈ ℝ)
23014, 35reexpcld 13532 . . . . . . . 8 (𝜑 → (𝑋↑(𝐾 + 1)) ∈ ℝ)
231229, 230remulcld 10669 . . . . . . 7 (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) · (𝑋↑(𝐾 + 1))) ∈ ℝ)
232230adantr 484 . . . . . . . . . 10 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑋↑(𝐾 + 1)) ∈ ℝ)
233228, 232remulcld 10669 . . . . . . . . 9 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((abs‘((𝐴𝑘) · (𝑇𝑘))) · (𝑋↑(𝐾 + 1))) ∈ ℝ)
23412adantr 484 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑇 ∈ ℂ)
23515adantr 484 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑋 ∈ ℂ)
236234, 235, 38mulexpd 13530 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((𝑇 · 𝑋)↑𝑘) = ((𝑇𝑘) · (𝑋𝑘)))
237236oveq2d 7165 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) = ((𝐴𝑘) · ((𝑇𝑘) · (𝑋𝑘))))
23814adantr 484 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑋 ∈ ℝ)
239238, 38reexpcld 13532 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑋𝑘) ∈ ℝ)
240239recnd 10667 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑋𝑘) ∈ ℂ)
24140, 226, 240mulassd 10662 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → (((𝐴𝑘) · (𝑇𝑘)) · (𝑋𝑘)) = ((𝐴𝑘) · ((𝑇𝑘) · (𝑋𝑘))))
242237, 241eqtr4d 2862 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) = (((𝐴𝑘) · (𝑇𝑘)) · (𝑋𝑘)))
243242fveq2d 6665 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘))) = (abs‘(((𝐴𝑘) · (𝑇𝑘)) · (𝑋𝑘))))
244227, 240absmuld 14814 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘(((𝐴𝑘) · (𝑇𝑘)) · (𝑋𝑘))) = ((abs‘((𝐴𝑘) · (𝑇𝑘))) · (abs‘(𝑋𝑘))))
245 elfzelz 12911 . . . . . . . . . . . . . . 15 (𝑘 ∈ ((𝐾 + 1)...𝑁) → 𝑘 ∈ ℤ)
246 rpexpcl 13453 . . . . . . . . . . . . . . 15 ((𝑋 ∈ ℝ+𝑘 ∈ ℤ) → (𝑋𝑘) ∈ ℝ+)
24713, 245, 246syl2an 598 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑋𝑘) ∈ ℝ+)
248247rpge0d 12432 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → 0 ≤ (𝑋𝑘))
249239, 248absidd 14782 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘(𝑋𝑘)) = (𝑋𝑘))
250249oveq2d 7165 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((abs‘((𝐴𝑘) · (𝑇𝑘))) · (abs‘(𝑋𝑘))) = ((abs‘((𝐴𝑘) · (𝑇𝑘))) · (𝑋𝑘)))
251243, 244, 2503eqtrd 2863 . . . . . . . . . 10 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘))) = ((abs‘((𝐴𝑘) · (𝑇𝑘))) · (𝑋𝑘)))
252227absge0d 14804 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → 0 ≤ (abs‘((𝐴𝑘) · (𝑇𝑘))))
25335adantr 484 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝐾 + 1) ∈ ℕ0)
25436adantl 485 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑘 ∈ (ℤ‘(𝐾 + 1)))
255201adantr 484 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → 0 ≤ 𝑋)
256206adantr 484 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑋 ≤ 1)
257238, 253, 254, 255, 256leexp2rd 13623 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑋𝑘) ≤ (𝑋↑(𝐾 + 1)))
258239, 232, 228, 252, 257lemul2ad 11578 . . . . . . . . . 10 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((abs‘((𝐴𝑘) · (𝑇𝑘))) · (𝑋𝑘)) ≤ ((abs‘((𝐴𝑘) · (𝑇𝑘))) · (𝑋↑(𝐾 + 1))))
259251, 258eqbrtrd 5074 . . . . . . . . 9 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘))) ≤ ((abs‘((𝐴𝑘) · (𝑇𝑘))) · (𝑋↑(𝐾 + 1))))
26031, 222, 233, 259fsumle 15154 . . . . . . . 8 (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘))) ≤ Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((abs‘((𝐴𝑘) · (𝑇𝑘))) · (𝑋↑(𝐾 + 1))))
261230recnd 10667 . . . . . . . . 9 (𝜑 → (𝑋↑(𝐾 + 1)) ∈ ℂ)
262228recnd 10667 . . . . . . . . 9 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘((𝐴𝑘) · (𝑇𝑘))) ∈ ℂ)
26331, 261, 262fsummulc1 15140 . . . . . . . 8 (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) · (𝑋↑(𝐾 + 1))) = Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((abs‘((𝐴𝑘) · (𝑇𝑘))) · (𝑋↑(𝐾 + 1))))
264260, 263breqtrrd 5080 . . . . . . 7 (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘))) ≤ (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) · (𝑋↑(𝐾 + 1))))
26515, 27expp1d 13516 . . . . . . . . . . 11 (𝜑 → (𝑋↑(𝐾 + 1)) = ((𝑋𝐾) · 𝑋))
266154, 15mulcomd 10660 . . . . . . . . . . 11 (𝜑 → ((𝑋𝐾) · 𝑋) = (𝑋 · (𝑋𝐾)))
267265, 266eqtrd 2859 . . . . . . . . . 10 (𝜑 → (𝑋↑(𝐾 + 1)) = (𝑋 · (𝑋𝐾)))
268267oveq2d 7165 . . . . . . . . 9 (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) · (𝑋↑(𝐾 + 1))) = (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) · (𝑋 · (𝑋𝐾))))
269229recnd 10667 . . . . . . . . . 10 (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) ∈ ℂ)
270269, 15, 154mulassd 10662 . . . . . . . . 9 (𝜑 → ((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) · 𝑋) · (𝑋𝐾)) = (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) · (𝑋 · (𝑋𝐾))))
271268, 270eqtr4d 2862 . . . . . . . 8 (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) · (𝑋↑(𝐾 + 1))) = ((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) · 𝑋) · (𝑋𝐾)))
272229, 14remulcld 10669 . . . . . . . . 9 (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) · 𝑋) ∈ ℝ)
273 nnssz 11999 . . . . . . . . . . . 12 ℕ ⊆ ℤ
27461, 273sstri 3962 . . . . . . . . . . 11 {𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0} ⊆ ℤ
27576ne0d 4284 . . . . . . . . . . . . 13 (𝜑 → {𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0} ≠ ∅)
276 infssuzcl 12329 . . . . . . . . . . . . 13 (({𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0} ⊆ (ℤ‘1) ∧ {𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0} ≠ ∅) → inf({𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0}, ℝ, < ) ∈ {𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0})
27763, 275, 276sylancr 590 . . . . . . . . . . . 12 (𝜑 → inf({𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0}, ℝ, < ) ∈ {𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0})
2786, 277eqeltrid 2920 . . . . . . . . . . 11 (𝜑𝐾 ∈ {𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0})
279274, 278sseldi 3951 . . . . . . . . . 10 (𝜑𝐾 ∈ ℤ)
28013, 279rpexpcld 13613 . . . . . . . . 9 (𝜑 → (𝑋𝐾) ∈ ℝ+)
281 peano2re 10811 . . . . . . . . . . . 12 𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) ∈ ℝ → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) + 1) ∈ ℝ)
282229, 281syl 17 . . . . . . . . . . 11 (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) + 1) ∈ ℝ)
283282, 14remulcld 10669 . . . . . . . . . 10 (𝜑 → ((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) + 1) · 𝑋) ∈ ℝ)
284229ltp1d 11568 . . . . . . . . . . 11 (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) < (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) + 1))
285229, 282, 13, 284ltmul1dd 12483 . . . . . . . . . 10 (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) · 𝑋) < ((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) + 1) · 𝑋))
286 min2 12580 . . . . . . . . . . . . . 14 ((1 ∈ ℝ ∧ 𝑈 ∈ ℝ) → if(1 ≤ 𝑈, 1, 𝑈) ≤ 𝑈)
287196, 203, 286sylancr 590 . . . . . . . . . . . . 13 (𝜑 → if(1 ≤ 𝑈, 1, 𝑈) ≤ 𝑈)
2889, 287eqbrtrid 5087 . . . . . . . . . . . 12 (𝜑𝑋𝑈)
289288, 8breqtrdi 5093 . . . . . . . . . . 11 (𝜑𝑋 ≤ ((abs‘(𝐹‘0)) / (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) + 1)))
290 0red 10642 . . . . . . . . . . . . 13 (𝜑 → 0 ∈ ℝ)
29131, 228, 252fsumge0 15150 . . . . . . . . . . . . 13 (𝜑 → 0 ≤ Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))))
292290, 229, 282, 291, 284lelttrd 10796 . . . . . . . . . . . 12 (𝜑 → 0 < (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) + 1))
293 lemuldiv2 11519 . . . . . . . . . . . 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 260 . . . . . . . . . 10 (𝜑 → ((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) + 1) · 𝑋) ≤ (abs‘(𝐹‘0)))
296272, 283, 24, 285, 295ltletrd 10798 . . . . . . . . 9 (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) · 𝑋) < (abs‘(𝐹‘0)))
297272, 24, 280, 296ltmul1dd 12483 . . . . . . . 8 (𝜑 → ((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) · 𝑋) · (𝑋𝐾)) < ((abs‘(𝐹‘0)) · (𝑋𝐾)))
298271, 297eqbrtrd 5074 . . . . . . 7 (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) · (𝑋↑(𝐾 + 1))) < ((abs‘(𝐹‘0)) · (𝑋𝐾)))
299223, 231, 29, 264, 298lelttrd 10796 . . . . . 6 (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘))) < ((abs‘(𝐹‘0)) · (𝑋𝐾)))
30045, 223, 29, 224, 299lelttrd 10796 . . . . 5 (𝜑 → (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘))) < ((abs‘(𝐹‘0)) · (𝑋𝐾)))
30145, 29, 24, 300ltsub2dd 11251 . . . 4 (𝜑 → ((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋𝐾))) < ((abs‘(𝐹‘0)) − (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)))))
30230, 45, 24ltaddsubd 11238 . . . 4 (𝜑 → ((((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋𝐾))) + (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)))) < (abs‘(𝐹‘0)) ↔ ((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋𝐾))) < ((abs‘(𝐹‘0)) − (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘))))))
303301, 302mpbird 260 . . 3 (𝜑 → (((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋𝐾))) + (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)))) < (abs‘(𝐹‘0)))
30420, 46, 24, 221, 303lelttrd 10796 . 2 (𝜑 → (abs‘(𝐹‘(𝑇 · 𝑋))) < (abs‘(𝐹‘0)))
305 2fveq3 6666 . . . 4 (𝑥 = (𝑇 · 𝑋) → (abs‘(𝐹𝑥)) = (abs‘(𝐹‘(𝑇 · 𝑋))))
306305breq1d 5062 . . 3 (𝑥 = (𝑇 · 𝑋) → ((abs‘(𝐹𝑥)) < (abs‘(𝐹‘0)) ↔ (abs‘(𝐹‘(𝑇 · 𝑋))) < (abs‘(𝐹‘0))))
307306rspcev 3609 . 2 (((𝑇 · 𝑋) ∈ ℂ ∧ (abs‘(𝐹‘(𝑇 · 𝑋))) < (abs‘(𝐹‘0))) → ∃𝑥 ∈ ℂ (abs‘(𝐹𝑥)) < (abs‘(𝐹‘0)))
30816, 304, 307syl2anc 587 1 (𝜑 → ∃𝑥 ∈ ℂ (abs‘(𝐹𝑥)) < (abs‘(𝐹‘0)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  wo 844  w3a 1084   = wceq 1538  wcel 2115  wne 3014  wrex 3134  {crab 3137  cun 3917  cin 3918  wss 3919  c0 4276  ifcif 4450   class class class wbr 5052  wf 6339  cfv 6343  (class class class)co 7149  Fincfn 8505  infcinf 8902  cc 10533  cr 10534  0cc0 10535  1c1 10536   + caddc 10538   · cmul 10540   < clt 10673  cle 10674  cmin 10868  -cneg 10869   / cdiv 11295  cn 11634  0cn0 11894  cz 11978  cuz 12240  +crp 12386  ...cfz 12894  cexp 13434  abscabs 14593  Σcsu 15042  0𝑝c0p 24279  Polycply 24787  coeffccoe 24789  degcdgr 24790  𝑐ccxp 25153
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-rep 5176  ax-sep 5189  ax-nul 5196  ax-pow 5253  ax-pr 5317  ax-un 7455  ax-inf2 9101  ax-cnex 10591  ax-resscn 10592  ax-1cn 10593  ax-icn 10594  ax-addcl 10595  ax-addrcl 10596  ax-mulcl 10597  ax-mulrcl 10598  ax-mulcom 10599  ax-addass 10600  ax-mulass 10601  ax-distr 10602  ax-i2m1 10603  ax-1ne0 10604  ax-1rid 10605  ax-rnegex 10606  ax-rrecex 10607  ax-cnre 10608  ax-pre-lttri 10609  ax-pre-lttrn 10610  ax-pre-ltadd 10611  ax-pre-mulgt0 10612  ax-pre-sup 10613  ax-addf 10614  ax-mulf 10615
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-nel 3119  df-ral 3138  df-rex 3139  df-reu 3140  df-rmo 3141  df-rab 3142  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-pss 3938  df-nul 4277  df-if 4451  df-pw 4524  df-sn 4551  df-pr 4553  df-tp 4555  df-op 4557  df-uni 4825  df-int 4863  df-iun 4907  df-iin 4908  df-br 5053  df-opab 5115  df-mpt 5133  df-tr 5159  df-id 5447  df-eprel 5452  df-po 5461  df-so 5462  df-fr 5501  df-se 5502  df-we 5503  df-xp 5548  df-rel 5549  df-cnv 5550  df-co 5551  df-dm 5552  df-rn 5553  df-res 5554  df-ima 5555  df-pred 6135  df-ord 6181  df-on 6182  df-lim 6183  df-suc 6184  df-iota 6302  df-fun 6345  df-fn 6346  df-f 6347  df-f1 6348  df-fo 6349  df-f1o 6350  df-fv 6351  df-isom 6352  df-riota 7107  df-ov 7152  df-oprab 7153  df-mpo 7154  df-of 7403  df-om 7575  df-1st 7684  df-2nd 7685  df-supp 7827  df-wrecs 7943  df-recs 8004  df-rdg 8042  df-1o 8098  df-2o 8099  df-oadd 8102  df-er 8285  df-map 8404  df-pm 8405  df-ixp 8458  df-en 8506  df-dom 8507  df-sdom 8508  df-fin 8509  df-fsupp 8831  df-fi 8872  df-sup 8903  df-inf 8904  df-oi 8971  df-card 9365  df-pnf 10675  df-mnf 10676  df-xr 10677  df-ltxr 10678  df-le 10679  df-sub 10870  df-neg 10871  df-div 11296  df-nn 11635  df-2 11697  df-3 11698  df-4 11699  df-5 11700  df-6 11701  df-7 11702  df-8 11703  df-9 11704  df-n0 11895  df-z 11979  df-dec 12096  df-uz 12241  df-q 12346  df-rp 12387  df-xneg 12504  df-xadd 12505  df-xmul 12506  df-ioo 12739  df-ioc 12740  df-ico 12741  df-icc 12742  df-fz 12895  df-fzo 13038  df-fl 13166  df-mod 13242  df-seq 13374  df-exp 13435  df-fac 13639  df-bc 13668  df-hash 13696  df-shft 14426  df-cj 14458  df-re 14459  df-im 14460  df-sqrt 14594  df-abs 14595  df-limsup 14828  df-clim 14845  df-rlim 14846  df-sum 15043  df-ef 15421  df-sin 15423  df-cos 15424  df-pi 15426  df-struct 16485  df-ndx 16486  df-slot 16487  df-base 16489  df-sets 16490  df-ress 16491  df-plusg 16578  df-mulr 16579  df-starv 16580  df-sca 16581  df-vsca 16582  df-ip 16583  df-tset 16584  df-ple 16585  df-ds 16587  df-unif 16588  df-hom 16589  df-cco 16590  df-rest 16696  df-topn 16697  df-0g 16715  df-gsum 16716  df-topgen 16717  df-pt 16718  df-prds 16721  df-xrs 16775  df-qtop 16780  df-imas 16781  df-xps 16783  df-mre 16857  df-mrc 16858  df-acs 16860  df-mgm 17852  df-sgrp 17901  df-mnd 17912  df-submnd 17957  df-mulg 18225  df-cntz 18447  df-cmn 18908  df-psmet 20090  df-xmet 20091  df-met 20092  df-bl 20093  df-mopn 20094  df-fbas 20095  df-fg 20096  df-cnfld 20099  df-top 21505  df-topon 21522  df-topsp 21544  df-bases 21557  df-cld 21630  df-ntr 21631  df-cls 21632  df-nei 21709  df-lp 21747  df-perf 21748  df-cn 21838  df-cnp 21839  df-haus 21926  df-tx 22173  df-hmeo 22366  df-fil 22457  df-fm 22549  df-flim 22550  df-flf 22551  df-xms 22933  df-ms 22934  df-tms 22935  df-cncf 23489  df-0p 24280  df-limc 24475  df-dv 24476  df-ply 24791  df-coe 24793  df-dgr 24794  df-log 25154  df-cxp 25155
This theorem is referenced by:  ftalem6  25669
  Copyright terms: Public domain W3C validator