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

Theorem ftalem5 24848
 Description: Lemma for fta 24851: Main proof. We have already shifted the minimum found in ftalem3 24846 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 24847 . . . . 5 (𝜑 → ((𝐾 ∈ ℕ ∧ (𝐴𝐾) ≠ 0) ∧ (𝑇 ∈ ℂ ∧ 𝑈 ∈ ℝ+𝑋 ∈ ℝ+)))
1110simprd 478 . . . 4 (𝜑 → (𝑇 ∈ ℂ ∧ 𝑈 ∈ ℝ+𝑋 ∈ ℝ+))
1211simp1d 1093 . . 3 (𝜑𝑇 ∈ ℂ)
1311simp3d 1095 . . . . 5 (𝜑𝑋 ∈ ℝ+)
1413rpred 11910 . . . 4 (𝜑𝑋 ∈ ℝ)
1514recnd 10106 . . 3 (𝜑𝑋 ∈ ℂ)
1612, 15mulcld 10098 . 2 (𝜑 → (𝑇 · 𝑋) ∈ ℂ)
17 plyf 23999 . . . . . 6 (𝐹 ∈ (Poly‘𝑆) → 𝐹:ℂ⟶ℂ)
183, 17syl 17 . . . . 5 (𝜑𝐹:ℂ⟶ℂ)
1918, 16ffvelrnd 6400 . . . 4 (𝜑 → (𝐹‘(𝑇 · 𝑋)) ∈ ℂ)
2019abscld 14219 . . 3 (𝜑 → (abs‘(𝐹‘(𝑇 · 𝑋))) ∈ ℝ)
21 0cn 10070 . . . . . . 7 0 ∈ ℂ
22 ffvelrn 6397 . . . . . . 7 ((𝐹:ℂ⟶ℂ ∧ 0 ∈ ℂ) → (𝐹‘0) ∈ ℂ)
2318, 21, 22sylancl 695 . . . . . 6 (𝜑 → (𝐹‘0) ∈ ℂ)
2423abscld 14219 . . . . 5 (𝜑 → (abs‘(𝐹‘0)) ∈ ℝ)
2510simpld 474 . . . . . . . . 9 (𝜑 → (𝐾 ∈ ℕ ∧ (𝐴𝐾) ≠ 0))
2625simpld 474 . . . . . . . 8 (𝜑𝐾 ∈ ℕ)
2726nnnn0d 11389 . . . . . . 7 (𝜑𝐾 ∈ ℕ0)
2814, 27reexpcld 13065 . . . . . 6 (𝜑 → (𝑋𝐾) ∈ ℝ)
2924, 28remulcld 10108 . . . . 5 (𝜑 → ((abs‘(𝐹‘0)) · (𝑋𝐾)) ∈ ℝ)
3024, 29resubcld 10496 . . . 4 (𝜑 → ((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋𝐾))) ∈ ℝ)
31 fzfid 12812 . . . . . 6 (𝜑 → ((𝐾 + 1)...𝑁) ∈ Fin)
32 peano2nn0 11371 . . . . . . . . . 10 (𝐾 ∈ ℕ0 → (𝐾 + 1) ∈ ℕ0)
3327, 32syl 17 . . . . . . . . 9 (𝜑 → (𝐾 + 1) ∈ ℕ0)
34 elfzuz 12376 . . . . . . . . 9 (𝑘 ∈ ((𝐾 + 1)...𝑁) → 𝑘 ∈ (ℤ‘(𝐾 + 1)))
35 eluznn0 11795 . . . . . . . . 9 (((𝐾 + 1) ∈ ℕ0𝑘 ∈ (ℤ‘(𝐾 + 1))) → 𝑘 ∈ ℕ0)
3633, 34, 35syl2an 493 . . . . . . . 8 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑘 ∈ ℕ0)
371coef3 24033 . . . . . . . . . 10 (𝐹 ∈ (Poly‘𝑆) → 𝐴:ℕ0⟶ℂ)
383, 37syl 17 . . . . . . . . 9 (𝜑𝐴:ℕ0⟶ℂ)
39 ffvelrn 6397 . . . . . . . . 9 ((𝐴:ℕ0⟶ℂ ∧ 𝑘 ∈ ℕ0) → (𝐴𝑘) ∈ ℂ)
4038, 39sylan 487 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ0) → (𝐴𝑘) ∈ ℂ)
4136, 40syldan 486 . . . . . . 7 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝐴𝑘) ∈ ℂ)
4216adantr 480 . . . . . . . 8 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑇 · 𝑋) ∈ ℂ)
4342, 36expcld 13048 . . . . . . 7 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((𝑇 · 𝑋)↑𝑘) ∈ ℂ)
4441, 43mulcld 10098 . . . . . 6 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) ∈ ℂ)
4531, 44fsumcl 14508 . . . . 5 (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) ∈ ℂ)
4645abscld 14219 . . . 4 (𝜑 → (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘))) ∈ ℝ)
4730, 46readdcld 10107 . . 3 (𝜑 → (((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋𝐾))) + (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)))) ∈ ℝ)
48 fzfid 12812 . . . . . 6 (𝜑 → (0...𝐾) ∈ Fin)
49 elfznn0 12471 . . . . . . . 8 (𝑘 ∈ (0...𝐾) → 𝑘 ∈ ℕ0)
5038, 49, 39syl2an 493 . . . . . . 7 ((𝜑𝑘 ∈ (0...𝐾)) → (𝐴𝑘) ∈ ℂ)
51 expcl 12918 . . . . . . . 8 (((𝑇 · 𝑋) ∈ ℂ ∧ 𝑘 ∈ ℕ0) → ((𝑇 · 𝑋)↑𝑘) ∈ ℂ)
5216, 49, 51syl2an 493 . . . . . . 7 ((𝜑𝑘 ∈ (0...𝐾)) → ((𝑇 · 𝑋)↑𝑘) ∈ ℂ)
5350, 52mulcld 10098 . . . . . 6 ((𝜑𝑘 ∈ (0...𝐾)) → ((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) ∈ ℂ)
5448, 53fsumcl 14508 . . . . 5 (𝜑 → Σ𝑘 ∈ (0...𝐾)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) ∈ ℂ)
5554, 45abstrid 14239 . . . 4 (𝜑 → (abs‘(Σ𝑘 ∈ (0...𝐾)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) + Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)))) ≤ ((abs‘Σ𝑘 ∈ (0...𝐾)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘))) + (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)))))
561, 2coeid2 24040 . . . . . . 7 ((𝐹 ∈ (Poly‘𝑆) ∧ (𝑇 · 𝑋) ∈ ℂ) → (𝐹‘(𝑇 · 𝑋)) = Σ𝑘 ∈ (0...𝑁)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)))
573, 16, 56syl2anc 694 . . . . . 6 (𝜑 → (𝐹‘(𝑇 · 𝑋)) = Σ𝑘 ∈ (0...𝑁)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)))
5826nnred 11073 . . . . . . . . 9 (𝜑𝐾 ∈ ℝ)
5958ltp1d 10992 . . . . . . . 8 (𝜑𝐾 < (𝐾 + 1))
60 fzdisj 12406 . . . . . . . 8 (𝐾 < (𝐾 + 1) → ((0...𝐾) ∩ ((𝐾 + 1)...𝑁)) = ∅)
6159, 60syl 17 . . . . . . 7 (𝜑 → ((0...𝐾) ∩ ((𝐾 + 1)...𝑁)) = ∅)
62 ssrab2 3720 . . . . . . . . . . . 12 {𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0} ⊆ ℕ
63 nnuz 11761 . . . . . . . . . . . 12 ℕ = (ℤ‘1)
6462, 63sseqtri 3670 . . . . . . . . . . 11 {𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0} ⊆ (ℤ‘1)
654nnne0d 11103 . . . . . . . . . . . . 13 (𝜑𝑁 ≠ 0)
662, 1dgreq0 24066 . . . . . . . . . . . . . . . 16 (𝐹 ∈ (Poly‘𝑆) → (𝐹 = 0𝑝 ↔ (𝐴𝑁) = 0))
673, 66syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (𝐹 = 0𝑝 ↔ (𝐴𝑁) = 0))
68 fveq2 6229 . . . . . . . . . . . . . . . . 17 (𝐹 = 0𝑝 → (deg‘𝐹) = (deg‘0𝑝))
69 dgr0 24063 . . . . . . . . . . . . . . . . 17 (deg‘0𝑝) = 0
7068, 69syl6eq 2701 . . . . . . . . . . . . . . . 16 (𝐹 = 0𝑝 → (deg‘𝐹) = 0)
712, 70syl5eq 2697 . . . . . . . . . . . . . . 15 (𝐹 = 0𝑝𝑁 = 0)
7267, 71syl6bir 244 . . . . . . . . . . . . . 14 (𝜑 → ((𝐴𝑁) = 0 → 𝑁 = 0))
7372necon3d 2844 . . . . . . . . . . . . 13 (𝜑 → (𝑁 ≠ 0 → (𝐴𝑁) ≠ 0))
7465, 73mpd 15 . . . . . . . . . . . 12 (𝜑 → (𝐴𝑁) ≠ 0)
75 fveq2 6229 . . . . . . . . . . . . . 14 (𝑛 = 𝑁 → (𝐴𝑛) = (𝐴𝑁))
7675neeq1d 2882 . . . . . . . . . . . . 13 (𝑛 = 𝑁 → ((𝐴𝑛) ≠ 0 ↔ (𝐴𝑁) ≠ 0))
7776elrab 3396 . . . . . . . . . . . 12 (𝑁 ∈ {𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0} ↔ (𝑁 ∈ ℕ ∧ (𝐴𝑁) ≠ 0))
784, 74, 77sylanbrc 699 . . . . . . . . . . 11 (𝜑𝑁 ∈ {𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0})
79 infssuzle 11809 . . . . . . . . . . 11 (({𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0} ⊆ (ℤ‘1) ∧ 𝑁 ∈ {𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0}) → inf({𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0}, ℝ, < ) ≤ 𝑁)
8064, 78, 79sylancr 696 . . . . . . . . . 10 (𝜑 → inf({𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0}, ℝ, < ) ≤ 𝑁)
816, 80syl5eqbr 4720 . . . . . . . . 9 (𝜑𝐾𝑁)
82 nn0uz 11760 . . . . . . . . . . 11 0 = (ℤ‘0)
8327, 82syl6eleq 2740 . . . . . . . . . 10 (𝜑𝐾 ∈ (ℤ‘0))
844nnzd 11519 . . . . . . . . . 10 (𝜑𝑁 ∈ ℤ)
85 elfz5 12372 . . . . . . . . . 10 ((𝐾 ∈ (ℤ‘0) ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (0...𝑁) ↔ 𝐾𝑁))
8683, 84, 85syl2anc 694 . . . . . . . . 9 (𝜑 → (𝐾 ∈ (0...𝑁) ↔ 𝐾𝑁))
8781, 86mpbird 247 . . . . . . . 8 (𝜑𝐾 ∈ (0...𝑁))
88 fzsplit 12405 . . . . . . . 8 (𝐾 ∈ (0...𝑁) → (0...𝑁) = ((0...𝐾) ∪ ((𝐾 + 1)...𝑁)))
8987, 88syl 17 . . . . . . 7 (𝜑 → (0...𝑁) = ((0...𝐾) ∪ ((𝐾 + 1)...𝑁)))
90 fzfid 12812 . . . . . . 7 (𝜑 → (0...𝑁) ∈ Fin)
91 elfznn0 12471 . . . . . . . . 9 (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0)
9238, 91, 39syl2an 493 . . . . . . . 8 ((𝜑𝑘 ∈ (0...𝑁)) → (𝐴𝑘) ∈ ℂ)
9316, 91, 51syl2an 493 . . . . . . . 8 ((𝜑𝑘 ∈ (0...𝑁)) → ((𝑇 · 𝑋)↑𝑘) ∈ ℂ)
9492, 93mulcld 10098 . . . . . . 7 ((𝜑𝑘 ∈ (0...𝑁)) → ((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) ∈ ℂ)
9561, 89, 90, 94fsumsplit 14515 . . . . . 6 (𝜑 → Σ𝑘 ∈ (0...𝑁)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) = (Σ𝑘 ∈ (0...𝐾)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) + Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘))))
9657, 95eqtrd 2685 . . . . 5 (𝜑 → (𝐹‘(𝑇 · 𝑋)) = (Σ𝑘 ∈ (0...𝐾)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) + Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘))))
9796fveq2d 6233 . . . 4 (𝜑 → (abs‘(𝐹‘(𝑇 · 𝑋))) = (abs‘(Σ𝑘 ∈ (0...𝐾)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) + Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)))))
981coefv0 24049 . . . . . . . . . . . . 13 (𝐹 ∈ (Poly‘𝑆) → (𝐹‘0) = (𝐴‘0))
993, 98syl 17 . . . . . . . . . . . 12 (𝜑 → (𝐹‘0) = (𝐴‘0))
10099eqcomd 2657 . . . . . . . . . . 11 (𝜑 → (𝐴‘0) = (𝐹‘0))
10116exp0d 13042 . . . . . . . . . . 11 (𝜑 → ((𝑇 · 𝑋)↑0) = 1)
102100, 101oveq12d 6708 . . . . . . . . . 10 (𝜑 → ((𝐴‘0) · ((𝑇 · 𝑋)↑0)) = ((𝐹‘0) · 1))
10323mulid1d 10095 . . . . . . . . . 10 (𝜑 → ((𝐹‘0) · 1) = (𝐹‘0))
104102, 103eqtrd 2685 . . . . . . . . 9 (𝜑 → ((𝐴‘0) · ((𝑇 · 𝑋)↑0)) = (𝐹‘0))
105 1e0p1 11590 . . . . . . . . . . . . 13 1 = (0 + 1)
106105oveq1i 6700 . . . . . . . . . . . 12 (1...𝐾) = ((0 + 1)...𝐾)
107106sumeq1i 14472 . . . . . . . . . . 11 Σ𝑘 ∈ (1...𝐾)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) = Σ𝑘 ∈ ((0 + 1)...𝐾)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘))
10826, 63syl6eleq 2740 . . . . . . . . . . . 12 (𝜑𝐾 ∈ (ℤ‘1))
109 elfznn 12408 . . . . . . . . . . . . . . 15 (𝑘 ∈ (1...𝐾) → 𝑘 ∈ ℕ)
110109nnnn0d 11389 . . . . . . . . . . . . . 14 (𝑘 ∈ (1...𝐾) → 𝑘 ∈ ℕ0)
11138, 110, 39syl2an 493 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (1...𝐾)) → (𝐴𝑘) ∈ ℂ)
11216, 110, 51syl2an 493 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (1...𝐾)) → ((𝑇 · 𝑋)↑𝑘) ∈ ℂ)
113111, 112mulcld 10098 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (1...𝐾)) → ((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) ∈ ℂ)
114 fveq2 6229 . . . . . . . . . . . . 13 (𝑘 = 𝐾 → (𝐴𝑘) = (𝐴𝐾))
115 oveq2 6698 . . . . . . . . . . . . 13 (𝑘 = 𝐾 → ((𝑇 · 𝑋)↑𝑘) = ((𝑇 · 𝑋)↑𝐾))
116114, 115oveq12d 6708 . . . . . . . . . . . 12 (𝑘 = 𝐾 → ((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) = ((𝐴𝐾) · ((𝑇 · 𝑋)↑𝐾)))
117108, 113, 116fsumm1 14524 . . . . . . . . . . 11 (𝜑 → Σ𝑘 ∈ (1...𝐾)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) = (Σ𝑘 ∈ (1...(𝐾 − 1))((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) + ((𝐴𝐾) · ((𝑇 · 𝑋)↑𝐾))))
118107, 117syl5eqr 2699 . . . . . . . . . 10 (𝜑 → Σ𝑘 ∈ ((0 + 1)...𝐾)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) = (Σ𝑘 ∈ (1...(𝐾 − 1))((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) + ((𝐴𝐾) · ((𝑇 · 𝑋)↑𝐾))))
119 elfznn 12408 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 ∈ (1...(𝐾 − 1)) → 𝑘 ∈ ℕ)
120119adantl 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ (1...(𝐾 − 1))) → 𝑘 ∈ ℕ)
121120nnred 11073 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ (1...(𝐾 − 1))) → 𝑘 ∈ ℝ)
12258adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ (1...(𝐾 − 1))) → 𝐾 ∈ ℝ)
123 peano2rem 10386 . . . . . . . . . . . . . . . . . . . 20 (𝐾 ∈ ℝ → (𝐾 − 1) ∈ ℝ)
124122, 123syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ (1...(𝐾 − 1))) → (𝐾 − 1) ∈ ℝ)
125 elfzle2 12383 . . . . . . . . . . . . . . . . . . . 20 (𝑘 ∈ (1...(𝐾 − 1)) → 𝑘 ≤ (𝐾 − 1))
126125adantl 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ (1...(𝐾 − 1))) → 𝑘 ≤ (𝐾 − 1))
127122ltm1d 10994 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ (1...(𝐾 − 1))) → (𝐾 − 1) < 𝐾)
128121, 124, 122, 126, 127lelttrd 10233 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ (1...(𝐾 − 1))) → 𝑘 < 𝐾)
129121, 122ltnled 10222 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ (1...(𝐾 − 1))) → (𝑘 < 𝐾 ↔ ¬ 𝐾𝑘))
130128, 129mpbid 222 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ (1...(𝐾 − 1))) → ¬ 𝐾𝑘)
131 infssuzle 11809 . . . . . . . . . . . . . . . . . . 19 (({𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0} ⊆ (ℤ‘1) ∧ 𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0}) → inf({𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0}, ℝ, < ) ≤ 𝑘)
1326, 131syl5eqbr 4720 . . . . . . . . . . . . . . . . . 18 (({𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0} ⊆ (ℤ‘1) ∧ 𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0}) → 𝐾𝑘)
13364, 132mpan 706 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0} → 𝐾𝑘)
134130, 133nsyl 135 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (1...(𝐾 − 1))) → ¬ 𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0})
135 fveq2 6229 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 𝑘 → (𝐴𝑛) = (𝐴𝑘))
136135neeq1d 2882 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 𝑘 → ((𝐴𝑛) ≠ 0 ↔ (𝐴𝑘) ≠ 0))
137136elrab3 3397 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ℕ → (𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0} ↔ (𝐴𝑘) ≠ 0))
138120, 137syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ (1...(𝐾 − 1))) → (𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0} ↔ (𝐴𝑘) ≠ 0))
139138necon2bbid 2866 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (1...(𝐾 − 1))) → ((𝐴𝑘) = 0 ↔ ¬ 𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0}))
140134, 139mpbird 247 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (1...(𝐾 − 1))) → (𝐴𝑘) = 0)
141140oveq1d 6705 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (1...(𝐾 − 1))) → ((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) = (0 · ((𝑇 · 𝑋)↑𝑘)))
142119nnnn0d 11389 . . . . . . . . . . . . . . . 16 (𝑘 ∈ (1...(𝐾 − 1)) → 𝑘 ∈ ℕ0)
14316, 142, 51syl2an 493 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (1...(𝐾 − 1))) → ((𝑇 · 𝑋)↑𝑘) ∈ ℂ)
144143mul02d 10272 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (1...(𝐾 − 1))) → (0 · ((𝑇 · 𝑋)↑𝑘)) = 0)
145141, 144eqtrd 2685 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (1...(𝐾 − 1))) → ((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) = 0)
146145sumeq2dv 14477 . . . . . . . . . . . 12 (𝜑 → Σ𝑘 ∈ (1...(𝐾 − 1))((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) = Σ𝑘 ∈ (1...(𝐾 − 1))0)
147 fzfi 12811 . . . . . . . . . . . . . 14 (1...(𝐾 − 1)) ∈ Fin
148147olci 405 . . . . . . . . . . . . 13 ((1...(𝐾 − 1)) ⊆ (ℤ‘1) ∨ (1...(𝐾 − 1)) ∈ Fin)
149 sumz 14497 . . . . . . . . . . . . 13 (((1...(𝐾 − 1)) ⊆ (ℤ‘1) ∨ (1...(𝐾 − 1)) ∈ Fin) → Σ𝑘 ∈ (1...(𝐾 − 1))0 = 0)
150148, 149ax-mp 5 . . . . . . . . . . . 12 Σ𝑘 ∈ (1...(𝐾 − 1))0 = 0
151146, 150syl6eq 2701 . . . . . . . . . . 11 (𝜑 → Σ𝑘 ∈ (1...(𝐾 − 1))((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) = 0)
15212, 15, 27mulexpd 13063 . . . . . . . . . . . . . 14 (𝜑 → ((𝑇 · 𝑋)↑𝐾) = ((𝑇𝐾) · (𝑋𝐾)))
153152oveq2d 6706 . . . . . . . . . . . . 13 (𝜑 → ((𝐴𝐾) · ((𝑇 · 𝑋)↑𝐾)) = ((𝐴𝐾) · ((𝑇𝐾) · (𝑋𝐾))))
15438, 27ffvelrnd 6400 . . . . . . . . . . . . . 14 (𝜑 → (𝐴𝐾) ∈ ℂ)
15512, 27expcld 13048 . . . . . . . . . . . . . 14 (𝜑 → (𝑇𝐾) ∈ ℂ)
15628recnd 10106 . . . . . . . . . . . . . 14 (𝜑 → (𝑋𝐾) ∈ ℂ)
157154, 155, 156mulassd 10101 . . . . . . . . . . . . 13 (𝜑 → (((𝐴𝐾) · (𝑇𝐾)) · (𝑋𝐾)) = ((𝐴𝐾) · ((𝑇𝐾) · (𝑋𝐾))))
158153, 157eqtr4d 2688 . . . . . . . . . . . 12 (𝜑 → ((𝐴𝐾) · ((𝑇 · 𝑋)↑𝐾)) = (((𝐴𝐾) · (𝑇𝐾)) · (𝑋𝐾)))
1597oveq1i 6700 . . . . . . . . . . . . . . . 16 (𝑇𝐾) = ((-((𝐹‘0) / (𝐴𝐾))↑𝑐(1 / 𝐾))↑𝐾)
16058recnd 10106 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐾 ∈ ℂ)
16126nnne0d 11103 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐾 ≠ 0)
162160, 161recid2d 10835 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((1 / 𝐾) · 𝐾) = 1)
163162oveq2d 6706 . . . . . . . . . . . . . . . . 17 (𝜑 → (-((𝐹‘0) / (𝐴𝐾))↑𝑐((1 / 𝐾) · 𝐾)) = (-((𝐹‘0) / (𝐴𝐾))↑𝑐1))
16425simprd 478 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐴𝐾) ≠ 0)
16523, 154, 164divcld 10839 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝐹‘0) / (𝐴𝐾)) ∈ ℂ)
166165negcld 10417 . . . . . . . . . . . . . . . . . 18 (𝜑 → -((𝐹‘0) / (𝐴𝐾)) ∈ ℂ)
16726nnrecred 11104 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (1 / 𝐾) ∈ ℝ)
168167recnd 10106 . . . . . . . . . . . . . . . . . 18 (𝜑 → (1 / 𝐾) ∈ ℂ)
169166, 168, 27cxpmul2d 24500 . . . . . . . . . . . . . . . . 17 (𝜑 → (-((𝐹‘0) / (𝐴𝐾))↑𝑐((1 / 𝐾) · 𝐾)) = ((-((𝐹‘0) / (𝐴𝐾))↑𝑐(1 / 𝐾))↑𝐾))
170166cxp1d 24497 . . . . . . . . . . . . . . . . 17 (𝜑 → (-((𝐹‘0) / (𝐴𝐾))↑𝑐1) = -((𝐹‘0) / (𝐴𝐾)))
171163, 169, 1703eqtr3d 2693 . . . . . . . . . . . . . . . 16 (𝜑 → ((-((𝐹‘0) / (𝐴𝐾))↑𝑐(1 / 𝐾))↑𝐾) = -((𝐹‘0) / (𝐴𝐾)))
172159, 171syl5eq 2697 . . . . . . . . . . . . . . 15 (𝜑 → (𝑇𝐾) = -((𝐹‘0) / (𝐴𝐾)))
173172oveq2d 6706 . . . . . . . . . . . . . 14 (𝜑 → ((𝐴𝐾) · (𝑇𝐾)) = ((𝐴𝐾) · -((𝐹‘0) / (𝐴𝐾))))
174154, 165mulneg2d 10522 . . . . . . . . . . . . . 14 (𝜑 → ((𝐴𝐾) · -((𝐹‘0) / (𝐴𝐾))) = -((𝐴𝐾) · ((𝐹‘0) / (𝐴𝐾))))
17523, 154, 164divcan2d 10841 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐴𝐾) · ((𝐹‘0) / (𝐴𝐾))) = (𝐹‘0))
176175negeqd 10313 . . . . . . . . . . . . . 14 (𝜑 → -((𝐴𝐾) · ((𝐹‘0) / (𝐴𝐾))) = -(𝐹‘0))
177173, 174, 1763eqtrd 2689 . . . . . . . . . . . . 13 (𝜑 → ((𝐴𝐾) · (𝑇𝐾)) = -(𝐹‘0))
178177oveq1d 6705 . . . . . . . . . . . 12 (𝜑 → (((𝐴𝐾) · (𝑇𝐾)) · (𝑋𝐾)) = (-(𝐹‘0) · (𝑋𝐾)))
17923, 156mulneg1d 10521 . . . . . . . . . . . 12 (𝜑 → (-(𝐹‘0) · (𝑋𝐾)) = -((𝐹‘0) · (𝑋𝐾)))
180158, 178, 1793eqtrd 2689 . . . . . . . . . . 11 (𝜑 → ((𝐴𝐾) · ((𝑇 · 𝑋)↑𝐾)) = -((𝐹‘0) · (𝑋𝐾)))
181151, 180oveq12d 6708 . . . . . . . . . 10 (𝜑 → (Σ𝑘 ∈ (1...(𝐾 − 1))((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) + ((𝐴𝐾) · ((𝑇 · 𝑋)↑𝐾))) = (0 + -((𝐹‘0) · (𝑋𝐾))))
18223, 156mulcld 10098 . . . . . . . . . . . 12 (𝜑 → ((𝐹‘0) · (𝑋𝐾)) ∈ ℂ)
183182negcld 10417 . . . . . . . . . . 11 (𝜑 → -((𝐹‘0) · (𝑋𝐾)) ∈ ℂ)
184183addid2d 10275 . . . . . . . . . 10 (𝜑 → (0 + -((𝐹‘0) · (𝑋𝐾))) = -((𝐹‘0) · (𝑋𝐾)))
185118, 181, 1843eqtrd 2689 . . . . . . . . 9 (𝜑 → Σ𝑘 ∈ ((0 + 1)...𝐾)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) = -((𝐹‘0) · (𝑋𝐾)))
186104, 185oveq12d 6708 . . . . . . . 8 (𝜑 → (((𝐴‘0) · ((𝑇 · 𝑋)↑0)) + Σ𝑘 ∈ ((0 + 1)...𝐾)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘))) = ((𝐹‘0) + -((𝐹‘0) · (𝑋𝐾))))
187 fveq2 6229 . . . . . . . . . 10 (𝑘 = 0 → (𝐴𝑘) = (𝐴‘0))
188 oveq2 6698 . . . . . . . . . 10 (𝑘 = 0 → ((𝑇 · 𝑋)↑𝑘) = ((𝑇 · 𝑋)↑0))
189187, 188oveq12d 6708 . . . . . . . . 9 (𝑘 = 0 → ((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) = ((𝐴‘0) · ((𝑇 · 𝑋)↑0)))
19083, 53, 189fsum1p 14526 . . . . . . . 8 (𝜑 → Σ𝑘 ∈ (0...𝐾)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) = (((𝐴‘0) · ((𝑇 · 𝑋)↑0)) + Σ𝑘 ∈ ((0 + 1)...𝐾)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘))))
191103oveq1d 6705 . . . . . . . . 9 (𝜑 → (((𝐹‘0) · 1) − ((𝐹‘0) · (𝑋𝐾))) = ((𝐹‘0) − ((𝐹‘0) · (𝑋𝐾))))
192 1cnd 10094 . . . . . . . . . 10 (𝜑 → 1 ∈ ℂ)
19323, 192, 156subdid 10524 . . . . . . . . 9 (𝜑 → ((𝐹‘0) · (1 − (𝑋𝐾))) = (((𝐹‘0) · 1) − ((𝐹‘0) · (𝑋𝐾))))
19423, 182negsubd 10436 . . . . . . . . 9 (𝜑 → ((𝐹‘0) + -((𝐹‘0) · (𝑋𝐾))) = ((𝐹‘0) − ((𝐹‘0) · (𝑋𝐾))))
195191, 193, 1943eqtr4d 2695 . . . . . . . 8 (𝜑 → ((𝐹‘0) · (1 − (𝑋𝐾))) = ((𝐹‘0) + -((𝐹‘0) · (𝑋𝐾))))
196186, 190, 1953eqtr4d 2695 . . . . . . 7 (𝜑 → Σ𝑘 ∈ (0...𝐾)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) = ((𝐹‘0) · (1 − (𝑋𝐾))))
197196fveq2d 6233 . . . . . 6 (𝜑 → (abs‘Σ𝑘 ∈ (0...𝐾)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘))) = (abs‘((𝐹‘0) · (1 − (𝑋𝐾)))))
198 1re 10077 . . . . . . . . 9 1 ∈ ℝ
199 resubcl 10383 . . . . . . . . 9 ((1 ∈ ℝ ∧ (𝑋𝐾) ∈ ℝ) → (1 − (𝑋𝐾)) ∈ ℝ)
200198, 28, 199sylancr 696 . . . . . . . 8 (𝜑 → (1 − (𝑋𝐾)) ∈ ℝ)
201200recnd 10106 . . . . . . 7 (𝜑 → (1 − (𝑋𝐾)) ∈ ℂ)
20223, 201absmuld 14237 . . . . . 6 (𝜑 → (abs‘((𝐹‘0) · (1 − (𝑋𝐾)))) = ((abs‘(𝐹‘0)) · (abs‘(1 − (𝑋𝐾)))))
20313rpge0d 11914 . . . . . . . . . . 11 (𝜑 → 0 ≤ 𝑋)
20411simp2d 1094 . . . . . . . . . . . . . 14 (𝜑𝑈 ∈ ℝ+)
205204rpred 11910 . . . . . . . . . . . . 13 (𝜑𝑈 ∈ ℝ)
206 min1 12058 . . . . . . . . . . . . 13 ((1 ∈ ℝ ∧ 𝑈 ∈ ℝ) → if(1 ≤ 𝑈, 1, 𝑈) ≤ 1)
207198, 205, 206sylancr 696 . . . . . . . . . . . 12 (𝜑 → if(1 ≤ 𝑈, 1, 𝑈) ≤ 1)
2089, 207syl5eqbr 4720 . . . . . . . . . . 11 (𝜑𝑋 ≤ 1)
209 exple1 12960 . . . . . . . . . . 11 (((𝑋 ∈ ℝ ∧ 0 ≤ 𝑋𝑋 ≤ 1) ∧ 𝐾 ∈ ℕ0) → (𝑋𝐾) ≤ 1)
21014, 203, 208, 27, 209syl31anc 1369 . . . . . . . . . 10 (𝜑 → (𝑋𝐾) ≤ 1)
211 subge0 10579 . . . . . . . . . . 11 ((1 ∈ ℝ ∧ (𝑋𝐾) ∈ ℝ) → (0 ≤ (1 − (𝑋𝐾)) ↔ (𝑋𝐾) ≤ 1))
212198, 28, 211sylancr 696 . . . . . . . . . 10 (𝜑 → (0 ≤ (1 − (𝑋𝐾)) ↔ (𝑋𝐾) ≤ 1))
213210, 212mpbird 247 . . . . . . . . 9 (𝜑 → 0 ≤ (1 − (𝑋𝐾)))
214200, 213absidd 14205 . . . . . . . 8 (𝜑 → (abs‘(1 − (𝑋𝐾))) = (1 − (𝑋𝐾)))
215214oveq2d 6706 . . . . . . 7 (𝜑 → ((abs‘(𝐹‘0)) · (abs‘(1 − (𝑋𝐾)))) = ((abs‘(𝐹‘0)) · (1 − (𝑋𝐾))))
21624recnd 10106 . . . . . . . 8 (𝜑 → (abs‘(𝐹‘0)) ∈ ℂ)
217216, 192, 156subdid 10524 . . . . . . 7 (𝜑 → ((abs‘(𝐹‘0)) · (1 − (𝑋𝐾))) = (((abs‘(𝐹‘0)) · 1) − ((abs‘(𝐹‘0)) · (𝑋𝐾))))
218216mulid1d 10095 . . . . . . . 8 (𝜑 → ((abs‘(𝐹‘0)) · 1) = (abs‘(𝐹‘0)))
219218oveq1d 6705 . . . . . . 7 (𝜑 → (((abs‘(𝐹‘0)) · 1) − ((abs‘(𝐹‘0)) · (𝑋𝐾))) = ((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋𝐾))))
220215, 217, 2193eqtrd 2689 . . . . . 6 (𝜑 → ((abs‘(𝐹‘0)) · (abs‘(1 − (𝑋𝐾)))) = ((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋𝐾))))
221197, 202, 2203eqtrrd 2690 . . . . 5 (𝜑 → ((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋𝐾))) = (abs‘Σ𝑘 ∈ (0...𝐾)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘))))
222221oveq1d 6705 . . . 4 (𝜑 → (((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋𝐾))) + (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)))) = ((abs‘Σ𝑘 ∈ (0...𝐾)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘))) + (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)))))
22355, 97, 2223brtr4d 4717 . . 3 (𝜑 → (abs‘(𝐹‘(𝑇 · 𝑋))) ≤ (((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋𝐾))) + (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)))))
22444abscld 14219 . . . . . . 7 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘))) ∈ ℝ)
22531, 224fsumrecl 14509 . . . . . 6 (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘))) ∈ ℝ)
22631, 44fsumabs 14577 . . . . . 6 (𝜑 → (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘))) ≤ Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘))))
227 expcl 12918 . . . . . . . . . . . . 13 ((𝑇 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (𝑇𝑘) ∈ ℂ)
22812, 227sylan 487 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ0) → (𝑇𝑘) ∈ ℂ)
22936, 228syldan 486 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑇𝑘) ∈ ℂ)
23041, 229mulcld 10098 . . . . . . . . . 10 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((𝐴𝑘) · (𝑇𝑘)) ∈ ℂ)
231230abscld 14219 . . . . . . . . 9 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘((𝐴𝑘) · (𝑇𝑘))) ∈ ℝ)
23231, 231fsumrecl 14509 . . . . . . . 8 (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) ∈ ℝ)
23314, 33reexpcld 13065 . . . . . . . 8 (𝜑 → (𝑋↑(𝐾 + 1)) ∈ ℝ)
234232, 233remulcld 10108 . . . . . . 7 (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) · (𝑋↑(𝐾 + 1))) ∈ ℝ)
235233adantr 480 . . . . . . . . . 10 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑋↑(𝐾 + 1)) ∈ ℝ)
236231, 235remulcld 10108 . . . . . . . . 9 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((abs‘((𝐴𝑘) · (𝑇𝑘))) · (𝑋↑(𝐾 + 1))) ∈ ℝ)
23712adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑇 ∈ ℂ)
23815adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑋 ∈ ℂ)
239237, 238, 36mulexpd 13063 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((𝑇 · 𝑋)↑𝑘) = ((𝑇𝑘) · (𝑋𝑘)))
240239oveq2d 6706 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) = ((𝐴𝑘) · ((𝑇𝑘) · (𝑋𝑘))))
24114adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑋 ∈ ℝ)
242241, 36reexpcld 13065 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑋𝑘) ∈ ℝ)
243242recnd 10106 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑋𝑘) ∈ ℂ)
24441, 229, 243mulassd 10101 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → (((𝐴𝑘) · (𝑇𝑘)) · (𝑋𝑘)) = ((𝐴𝑘) · ((𝑇𝑘) · (𝑋𝑘))))
245240, 244eqtr4d 2688 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)) = (((𝐴𝑘) · (𝑇𝑘)) · (𝑋𝑘)))
246245fveq2d 6233 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘))) = (abs‘(((𝐴𝑘) · (𝑇𝑘)) · (𝑋𝑘))))
247230, 243absmuld 14237 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘(((𝐴𝑘) · (𝑇𝑘)) · (𝑋𝑘))) = ((abs‘((𝐴𝑘) · (𝑇𝑘))) · (abs‘(𝑋𝑘))))
248 elfzelz 12380 . . . . . . . . . . . . . . 15 (𝑘 ∈ ((𝐾 + 1)...𝑁) → 𝑘 ∈ ℤ)
249 rpexpcl 12919 . . . . . . . . . . . . . . 15 ((𝑋 ∈ ℝ+𝑘 ∈ ℤ) → (𝑋𝑘) ∈ ℝ+)
25013, 248, 249syl2an 493 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑋𝑘) ∈ ℝ+)
251250rpge0d 11914 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → 0 ≤ (𝑋𝑘))
252242, 251absidd 14205 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘(𝑋𝑘)) = (𝑋𝑘))
253252oveq2d 6706 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((abs‘((𝐴𝑘) · (𝑇𝑘))) · (abs‘(𝑋𝑘))) = ((abs‘((𝐴𝑘) · (𝑇𝑘))) · (𝑋𝑘)))
254246, 247, 2533eqtrd 2689 . . . . . . . . . 10 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘))) = ((abs‘((𝐴𝑘) · (𝑇𝑘))) · (𝑋𝑘)))
255230absge0d 14227 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → 0 ≤ (abs‘((𝐴𝑘) · (𝑇𝑘))))
25633adantr 480 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝐾 + 1) ∈ ℕ0)
25734adantl 481 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑘 ∈ (ℤ‘(𝐾 + 1)))
258203adantr 480 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → 0 ≤ 𝑋)
259208adantr 480 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑋 ≤ 1)
260241, 256, 257, 258, 259leexp2rd 13082 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑋𝑘) ≤ (𝑋↑(𝐾 + 1)))
261242, 235, 231, 255, 260lemul2ad 11002 . . . . . . . . . 10 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((abs‘((𝐴𝑘) · (𝑇𝑘))) · (𝑋𝑘)) ≤ ((abs‘((𝐴𝑘) · (𝑇𝑘))) · (𝑋↑(𝐾 + 1))))
262254, 261eqbrtrd 4707 . . . . . . . . 9 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘))) ≤ ((abs‘((𝐴𝑘) · (𝑇𝑘))) · (𝑋↑(𝐾 + 1))))
26331, 224, 236, 262fsumle 14575 . . . . . . . 8 (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘))) ≤ Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((abs‘((𝐴𝑘) · (𝑇𝑘))) · (𝑋↑(𝐾 + 1))))
264233recnd 10106 . . . . . . . . 9 (𝜑 → (𝑋↑(𝐾 + 1)) ∈ ℂ)
265231recnd 10106 . . . . . . . . 9 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘((𝐴𝑘) · (𝑇𝑘))) ∈ ℂ)
26631, 264, 265fsummulc1 14561 . . . . . . . 8 (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) · (𝑋↑(𝐾 + 1))) = Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((abs‘((𝐴𝑘) · (𝑇𝑘))) · (𝑋↑(𝐾 + 1))))
267263, 266breqtrrd 4713 . . . . . . 7 (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘))) ≤ (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) · (𝑋↑(𝐾 + 1))))
26815, 27expp1d 13049 . . . . . . . . . . 11 (𝜑 → (𝑋↑(𝐾 + 1)) = ((𝑋𝐾) · 𝑋))
269156, 15mulcomd 10099 . . . . . . . . . . 11 (𝜑 → ((𝑋𝐾) · 𝑋) = (𝑋 · (𝑋𝐾)))
270268, 269eqtrd 2685 . . . . . . . . . 10 (𝜑 → (𝑋↑(𝐾 + 1)) = (𝑋 · (𝑋𝐾)))
271270oveq2d 6706 . . . . . . . . 9 (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) · (𝑋↑(𝐾 + 1))) = (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) · (𝑋 · (𝑋𝐾))))
272232recnd 10106 . . . . . . . . . 10 (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) ∈ ℂ)
273272, 15, 156mulassd 10101 . . . . . . . . 9 (𝜑 → ((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) · 𝑋) · (𝑋𝐾)) = (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) · (𝑋 · (𝑋𝐾))))
274271, 273eqtr4d 2688 . . . . . . . 8 (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) · (𝑋↑(𝐾 + 1))) = ((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) · 𝑋) · (𝑋𝐾)))
275232, 14remulcld 10108 . . . . . . . . 9 (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) · 𝑋) ∈ ℝ)
276 nnssz 11435 . . . . . . . . . . . 12 ℕ ⊆ ℤ
27762, 276sstri 3645 . . . . . . . . . . 11 {𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0} ⊆ ℤ
278 ne0i 3954 . . . . . . . . . . . . . 14 (𝑁 ∈ {𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0} → {𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0} ≠ ∅)
27978, 278syl 17 . . . . . . . . . . . . 13 (𝜑 → {𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0} ≠ ∅)
280 infssuzcl 11810 . . . . . . . . . . . . 13 (({𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0} ⊆ (ℤ‘1) ∧ {𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0} ≠ ∅) → inf({𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0}, ℝ, < ) ∈ {𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0})
28164, 279, 280sylancr 696 . . . . . . . . . . . 12 (𝜑 → inf({𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0}, ℝ, < ) ∈ {𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0})
2826, 281syl5eqel 2734 . . . . . . . . . . 11 (𝜑𝐾 ∈ {𝑛 ∈ ℕ ∣ (𝐴𝑛) ≠ 0})
283277, 282sseldi 3634 . . . . . . . . . 10 (𝜑𝐾 ∈ ℤ)
28413, 283rpexpcld 13072 . . . . . . . . 9 (𝜑 → (𝑋𝐾) ∈ ℝ+)
285 peano2re 10247 . . . . . . . . . . . 12 𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) ∈ ℝ → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) + 1) ∈ ℝ)
286232, 285syl 17 . . . . . . . . . . 11 (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) + 1) ∈ ℝ)
287286, 14remulcld 10108 . . . . . . . . . 10 (𝜑 → ((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) + 1) · 𝑋) ∈ ℝ)
288232ltp1d 10992 . . . . . . . . . . 11 (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) < (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) + 1))
289232, 286, 13, 288ltmul1dd 11965 . . . . . . . . . 10 (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) · 𝑋) < ((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) + 1) · 𝑋))
290 min2 12059 . . . . . . . . . . . . . 14 ((1 ∈ ℝ ∧ 𝑈 ∈ ℝ) → if(1 ≤ 𝑈, 1, 𝑈) ≤ 𝑈)
291198, 205, 290sylancr 696 . . . . . . . . . . . . 13 (𝜑 → if(1 ≤ 𝑈, 1, 𝑈) ≤ 𝑈)
2929, 291syl5eqbr 4720 . . . . . . . . . . . 12 (𝜑𝑋𝑈)
293292, 8syl6breq 4726 . . . . . . . . . . 11 (𝜑𝑋 ≤ ((abs‘(𝐹‘0)) / (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) + 1)))
294 0red 10079 . . . . . . . . . . . . 13 (𝜑 → 0 ∈ ℝ)
29531, 231, 255fsumge0 14571 . . . . . . . . . . . . 13 (𝜑 → 0 ≤ Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))))
296294, 232, 286, 295, 288lelttrd 10233 . . . . . . . . . . . 12 (𝜑 → 0 < (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) + 1))
297 lemuldiv2 10942 . . . . . . . . . . . 12 ((𝑋 ∈ ℝ ∧ (abs‘(𝐹‘0)) ∈ ℝ ∧ ((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) + 1) ∈ ℝ ∧ 0 < (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) + 1))) → (((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) + 1) · 𝑋) ≤ (abs‘(𝐹‘0)) ↔ 𝑋 ≤ ((abs‘(𝐹‘0)) / (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) + 1))))
29814, 24, 286, 296, 297syl112anc 1370 . . . . . . . . . . 11 (𝜑 → (((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) + 1) · 𝑋) ≤ (abs‘(𝐹‘0)) ↔ 𝑋 ≤ ((abs‘(𝐹‘0)) / (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) + 1))))
299293, 298mpbird 247 . . . . . . . . . 10 (𝜑 → ((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) + 1) · 𝑋) ≤ (abs‘(𝐹‘0)))
300275, 287, 24, 289, 299ltletrd 10235 . . . . . . . . 9 (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) · 𝑋) < (abs‘(𝐹‘0)))
301275, 24, 284, 300ltmul1dd 11965 . . . . . . . 8 (𝜑 → ((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) · 𝑋) · (𝑋𝐾)) < ((abs‘(𝐹‘0)) · (𝑋𝐾)))
302274, 301eqbrtrd 4707 . . . . . . 7 (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · (𝑇𝑘))) · (𝑋↑(𝐾 + 1))) < ((abs‘(𝐹‘0)) · (𝑋𝐾)))
303225, 234, 29, 267, 302lelttrd 10233 . . . . . 6 (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘))) < ((abs‘(𝐹‘0)) · (𝑋𝐾)))
30446, 225, 29, 226, 303lelttrd 10233 . . . . 5 (𝜑 → (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘))) < ((abs‘(𝐹‘0)) · (𝑋𝐾)))
30546, 29, 24, 304ltsub2dd 10678 . . . 4 (𝜑 → ((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋𝐾))) < ((abs‘(𝐹‘0)) − (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)))))
30630, 46, 24ltaddsubd 10665 . . . 4 (𝜑 → ((((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋𝐾))) + (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)))) < (abs‘(𝐹‘0)) ↔ ((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋𝐾))) < ((abs‘(𝐹‘0)) − (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘))))))
307305, 306mpbird 247 . . 3 (𝜑 → (((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋𝐾))) + (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴𝑘) · ((𝑇 · 𝑋)↑𝑘)))) < (abs‘(𝐹‘0)))
30820, 47, 24, 223, 307lelttrd 10233 . 2 (𝜑 → (abs‘(𝐹‘(𝑇 · 𝑋))) < (abs‘(𝐹‘0)))
309 fveq2 6229 . . . . 5 (𝑥 = (𝑇 · 𝑋) → (𝐹𝑥) = (𝐹‘(𝑇 · 𝑋)))
310309fveq2d 6233 . . . 4 (𝑥 = (𝑇 · 𝑋) → (abs‘(𝐹𝑥)) = (abs‘(𝐹‘(𝑇 · 𝑋))))
311310breq1d 4695 . . 3 (𝑥 = (𝑇 · 𝑋) → ((abs‘(𝐹𝑥)) < (abs‘(𝐹‘0)) ↔ (abs‘(𝐹‘(𝑇 · 𝑋))) < (abs‘(𝐹‘0))))
312311rspcev 3340 . 2 (((𝑇 · 𝑋) ∈ ℂ ∧ (abs‘(𝐹‘(𝑇 · 𝑋))) < (abs‘(𝐹‘0))) → ∃𝑥 ∈ ℂ (abs‘(𝐹𝑥)) < (abs‘(𝐹‘0)))
31316, 308, 312syl2anc 694 1 (𝜑 → ∃𝑥 ∈ ℂ (abs‘(𝐹𝑥)) < (abs‘(𝐹‘0)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∨ wo 382   ∧ wa 383   ∧ w3a 1054   = wceq 1523   ∈ wcel 2030   ≠ wne 2823  ∃wrex 2942  {crab 2945   ∪ cun 3605   ∩ cin 3606   ⊆ wss 3607  ∅c0 3948  ifcif 4119   class class class wbr 4685  ⟶wf 5922  ‘cfv 5926  (class class class)co 6690  Fincfn 7997  infcinf 8388  ℂcc 9972  ℝcr 9973  0cc0 9974  1c1 9975   + caddc 9977   · cmul 9979   < clt 10112   ≤ cle 10113   − cmin 10304  -cneg 10305   / cdiv 10722  ℕcn 11058  ℕ0cn0 11330  ℤcz 11415  ℤ≥cuz 11725  ℝ+crp 11870  ...cfz 12364  ↑cexp 12900  abscabs 14018  Σcsu 14460  0𝑝c0p 23481  Polycply 23985  coeffccoe 23987  degcdgr 23988  ↑𝑐ccxp 24347 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-inf2 8576  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052  ax-addf 10053  ax-mulf 10054 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-iin 4555  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-of 6939  df-om 7108  df-1st 7210  df-2nd 7211  df-supp 7341  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-2o 7606  df-oadd 7609  df-er 7787  df-map 7901  df-pm 7902  df-ixp 7951  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-fsupp 8317  df-fi 8358  df-sup 8389  df-inf 8390  df-oi 8456  df-card 8803  df-cda 9028  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-4 11119  df-5 11120  df-6 11121  df-7 11122  df-8 11123  df-9 11124  df-n0 11331  df-z 11416  df-dec 11532  df-uz 11726  df-q 11827  df-rp 11871  df-xneg 11984  df-xadd 11985  df-xmul 11986  df-ioo 12217  df-ioc 12218  df-ico 12219  df-icc 12220  df-fz 12365  df-fzo 12505  df-fl 12633  df-mod 12709  df-seq 12842  df-exp 12901  df-fac 13101  df-bc 13130  df-hash 13158  df-shft 13851  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-limsup 14246  df-clim 14263  df-rlim 14264  df-sum 14461  df-ef 14842  df-sin 14844  df-cos 14845  df-pi 14847  df-struct 15906  df-ndx 15907  df-slot 15908  df-base 15910  df-sets 15911  df-ress 15912  df-plusg 16001  df-mulr 16002  df-starv 16003  df-sca 16004  df-vsca 16005  df-ip 16006  df-tset 16007  df-ple 16008  df-ds 16011  df-unif 16012  df-hom 16013  df-cco 16014  df-rest 16130  df-topn 16131  df-0g 16149  df-gsum 16150  df-topgen 16151  df-pt 16152  df-prds 16155  df-xrs 16209  df-qtop 16214  df-imas 16215  df-xps 16217  df-mre 16293  df-mrc 16294  df-acs 16296  df-mgm 17289  df-sgrp 17331  df-mnd 17342  df-submnd 17383  df-mulg 17588  df-cntz 17796  df-cmn 18241  df-psmet 19786  df-xmet 19787  df-met 19788  df-bl 19789  df-mopn 19790  df-fbas 19791  df-fg 19792  df-cnfld 19795  df-top 20747  df-topon 20764  df-topsp 20785  df-bases 20798  df-cld 20871  df-ntr 20872  df-cls 20873  df-nei 20950  df-lp 20988  df-perf 20989  df-cn 21079  df-cnp 21080  df-haus 21167  df-tx 21413  df-hmeo 21606  df-fil 21697  df-fm 21789  df-flim 21790  df-flf 21791  df-xms 22172  df-ms 22173  df-tms 22174  df-cncf 22728  df-0p 23482  df-limc 23675  df-dv 23676  df-ply 23989  df-coe 23991  df-dgr 23992  df-log 24348  df-cxp 24349 This theorem is referenced by:  ftalem6  24849
 Copyright terms: Public domain W3C validator