Proof of Theorem ftalem5
| Step | Hyp | Ref
| 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, 𝑈) |
| 10 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | ftalem4 27119 |
. . . . 5
⊢ (𝜑 → ((𝐾 ∈ ℕ ∧ (𝐴‘𝐾) ≠ 0) ∧ (𝑇 ∈ ℂ ∧ 𝑈 ∈ ℝ+ ∧ 𝑋 ∈
ℝ+))) |
| 11 | 10 | simprd 495 |
. . . 4
⊢ (𝜑 → (𝑇 ∈ ℂ ∧ 𝑈 ∈ ℝ+ ∧ 𝑋 ∈
ℝ+)) |
| 12 | 11 | simp1d 1143 |
. . 3
⊢ (𝜑 → 𝑇 ∈ ℂ) |
| 13 | 11 | simp3d 1145 |
. . . . 5
⊢ (𝜑 → 𝑋 ∈
ℝ+) |
| 14 | 13 | rpred 13077 |
. . . 4
⊢ (𝜑 → 𝑋 ∈ ℝ) |
| 15 | 14 | recnd 11289 |
. . 3
⊢ (𝜑 → 𝑋 ∈ ℂ) |
| 16 | 12, 15 | mulcld 11281 |
. 2
⊢ (𝜑 → (𝑇 · 𝑋) ∈ ℂ) |
| 17 | | plyf 26237 |
. . . . . 6
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐹:ℂ⟶ℂ) |
| 18 | 3, 17 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐹:ℂ⟶ℂ) |
| 19 | 18, 16 | ffvelcdmd 7105 |
. . . 4
⊢ (𝜑 → (𝐹‘(𝑇 · 𝑋)) ∈ ℂ) |
| 20 | 19 | abscld 15475 |
. . 3
⊢ (𝜑 → (abs‘(𝐹‘(𝑇 · 𝑋))) ∈ ℝ) |
| 21 | | 0cn 11253 |
. . . . . . 7
⊢ 0 ∈
ℂ |
| 22 | | ffvelcdm 7101 |
. . . . . . 7
⊢ ((𝐹:ℂ⟶ℂ ∧ 0
∈ ℂ) → (𝐹‘0) ∈ ℂ) |
| 23 | 18, 21, 22 | sylancl 586 |
. . . . . 6
⊢ (𝜑 → (𝐹‘0) ∈ ℂ) |
| 24 | 23 | abscld 15475 |
. . . . 5
⊢ (𝜑 → (abs‘(𝐹‘0)) ∈
ℝ) |
| 25 | 10 | simpld 494 |
. . . . . . . . 9
⊢ (𝜑 → (𝐾 ∈ ℕ ∧ (𝐴‘𝐾) ≠ 0)) |
| 26 | 25 | simpld 494 |
. . . . . . . 8
⊢ (𝜑 → 𝐾 ∈ ℕ) |
| 27 | 26 | nnnn0d 12587 |
. . . . . . 7
⊢ (𝜑 → 𝐾 ∈
ℕ0) |
| 28 | 14, 27 | reexpcld 14203 |
. . . . . 6
⊢ (𝜑 → (𝑋↑𝐾) ∈ ℝ) |
| 29 | 24, 28 | remulcld 11291 |
. . . . 5
⊢ (𝜑 → ((abs‘(𝐹‘0)) · (𝑋↑𝐾)) ∈ ℝ) |
| 30 | 24, 29 | resubcld 11691 |
. . . 4
⊢ (𝜑 → ((abs‘(𝐹‘0)) −
((abs‘(𝐹‘0))
· (𝑋↑𝐾))) ∈
ℝ) |
| 31 | | fzfid 14014 |
. . . . . 6
⊢ (𝜑 → ((𝐾 + 1)...𝑁) ∈ Fin) |
| 32 | 1 | coef3 26271 |
. . . . . . . . 9
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐴:ℕ0⟶ℂ) |
| 33 | 3, 32 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) |
| 34 | | peano2nn0 12566 |
. . . . . . . . . 10
⊢ (𝐾 ∈ ℕ0
→ (𝐾 + 1) ∈
ℕ0) |
| 35 | 27, 34 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝐾 + 1) ∈
ℕ0) |
| 36 | | elfzuz 13560 |
. . . . . . . . 9
⊢ (𝑘 ∈ ((𝐾 + 1)...𝑁) → 𝑘 ∈ (ℤ≥‘(𝐾 + 1))) |
| 37 | | eluznn0 12959 |
. . . . . . . . 9
⊢ (((𝐾 + 1) ∈ ℕ0
∧ 𝑘 ∈
(ℤ≥‘(𝐾 + 1))) → 𝑘 ∈ ℕ0) |
| 38 | 35, 36, 37 | syl2an 596 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑘 ∈ ℕ0) |
| 39 | | ffvelcdm 7101 |
. . . . . . . 8
⊢ ((𝐴:ℕ0⟶ℂ ∧
𝑘 ∈
ℕ0) → (𝐴‘𝑘) ∈ ℂ) |
| 40 | 33, 38, 39 | syl2an2r 685 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝐴‘𝑘) ∈ ℂ) |
| 41 | 16 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑇 · 𝑋) ∈ ℂ) |
| 42 | 41, 38 | expcld 14186 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((𝑇 · 𝑋)↑𝑘) ∈ ℂ) |
| 43 | 40, 42 | mulcld 11281 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) ∈ ℂ) |
| 44 | 31, 43 | fsumcl 15769 |
. . . . 5
⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) ∈ ℂ) |
| 45 | 44 | abscld 15475 |
. . . 4
⊢ (𝜑 → (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) ∈ ℝ) |
| 46 | 30, 45 | readdcld 11290 |
. . 3
⊢ (𝜑 → (((abs‘(𝐹‘0)) −
((abs‘(𝐹‘0))
· (𝑋↑𝐾))) + (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))) ∈ ℝ) |
| 47 | | fzfid 14014 |
. . . . . 6
⊢ (𝜑 → (0...𝐾) ∈ Fin) |
| 48 | | elfznn0 13660 |
. . . . . . . 8
⊢ (𝑘 ∈ (0...𝐾) → 𝑘 ∈ ℕ0) |
| 49 | 33, 48, 39 | syl2an 596 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐾)) → (𝐴‘𝑘) ∈ ℂ) |
| 50 | | expcl 14120 |
. . . . . . . 8
⊢ (((𝑇 · 𝑋) ∈ ℂ ∧ 𝑘 ∈ ℕ0) → ((𝑇 · 𝑋)↑𝑘) ∈ ℂ) |
| 51 | 16, 48, 50 | syl2an 596 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐾)) → ((𝑇 · 𝑋)↑𝑘) ∈ ℂ) |
| 52 | 49, 51 | mulcld 11281 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐾)) → ((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) ∈ ℂ) |
| 53 | 47, 52 | fsumcl 15769 |
. . . . 5
⊢ (𝜑 → Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) ∈ ℂ) |
| 54 | 53, 44 | abstrid 15495 |
. . . 4
⊢ (𝜑 → (abs‘(Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) + Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))) ≤ ((abs‘Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) + (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))))) |
| 55 | 1, 2 | coeid2 26278 |
. . . . . . 7
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (𝑇 · 𝑋) ∈ ℂ) → (𝐹‘(𝑇 · 𝑋)) = Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) |
| 56 | 3, 16, 55 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → (𝐹‘(𝑇 · 𝑋)) = Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) |
| 57 | 26 | nnred 12281 |
. . . . . . . . 9
⊢ (𝜑 → 𝐾 ∈ ℝ) |
| 58 | 57 | ltp1d 12198 |
. . . . . . . 8
⊢ (𝜑 → 𝐾 < (𝐾 + 1)) |
| 59 | | fzdisj 13591 |
. . . . . . . 8
⊢ (𝐾 < (𝐾 + 1) → ((0...𝐾) ∩ ((𝐾 + 1)...𝑁)) = ∅) |
| 60 | 58, 59 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((0...𝐾) ∩ ((𝐾 + 1)...𝑁)) = ∅) |
| 61 | | ssrab2 4080 |
. . . . . . . . . . . 12
⊢ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ⊆ ℕ |
| 62 | | nnuz 12921 |
. . . . . . . . . . . 12
⊢ ℕ =
(ℤ≥‘1) |
| 63 | 61, 62 | sseqtri 4032 |
. . . . . . . . . . 11
⊢ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ⊆
(ℤ≥‘1) |
| 64 | | fveq2 6906 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑁 → (𝐴‘𝑛) = (𝐴‘𝑁)) |
| 65 | 64 | neeq1d 3000 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑁 → ((𝐴‘𝑛) ≠ 0 ↔ (𝐴‘𝑁) ≠ 0)) |
| 66 | 4 | nnne0d 12316 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ≠ 0) |
| 67 | 2, 1 | dgreq0 26305 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 ∈ (Poly‘𝑆) → (𝐹 = 0𝑝 ↔ (𝐴‘𝑁) = 0)) |
| 68 | 3, 67 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐹 = 0𝑝 ↔ (𝐴‘𝑁) = 0)) |
| 69 | | fveq2 6906 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹 = 0𝑝 →
(deg‘𝐹) =
(deg‘0𝑝)) |
| 70 | | dgr0 26302 |
. . . . . . . . . . . . . . . . 17
⊢
(deg‘0𝑝) = 0 |
| 71 | 69, 70 | eqtrdi 2793 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 = 0𝑝 →
(deg‘𝐹) =
0) |
| 72 | 2, 71 | eqtrid 2789 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 = 0𝑝 →
𝑁 = 0) |
| 73 | 68, 72 | biimtrrdi 254 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐴‘𝑁) = 0 → 𝑁 = 0)) |
| 74 | 73 | necon3d 2961 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑁 ≠ 0 → (𝐴‘𝑁) ≠ 0)) |
| 75 | 66, 74 | mpd 15 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴‘𝑁) ≠ 0) |
| 76 | 65, 4, 75 | elrabd 3694 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0}) |
| 77 | | infssuzle 12973 |
. . . . . . . . . . 11
⊢ (({𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ⊆
(ℤ≥‘1) ∧ 𝑁 ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0}) → inf({𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0}, ℝ, < ) ≤ 𝑁) |
| 78 | 63, 76, 77 | sylancr 587 |
. . . . . . . . . 10
⊢ (𝜑 → inf({𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0}, ℝ, < ) ≤ 𝑁) |
| 79 | 6, 78 | eqbrtrid 5178 |
. . . . . . . . 9
⊢ (𝜑 → 𝐾 ≤ 𝑁) |
| 80 | | nn0uz 12920 |
. . . . . . . . . . 11
⊢
ℕ0 = (ℤ≥‘0) |
| 81 | 27, 80 | eleqtrdi 2851 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐾 ∈
(ℤ≥‘0)) |
| 82 | 4 | nnzd 12640 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ ℤ) |
| 83 | | elfz5 13556 |
. . . . . . . . . 10
⊢ ((𝐾 ∈
(ℤ≥‘0) ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (0...𝑁) ↔ 𝐾 ≤ 𝑁)) |
| 84 | 81, 82, 83 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → (𝐾 ∈ (0...𝑁) ↔ 𝐾 ≤ 𝑁)) |
| 85 | 79, 84 | mpbird 257 |
. . . . . . . 8
⊢ (𝜑 → 𝐾 ∈ (0...𝑁)) |
| 86 | | fzsplit 13590 |
. . . . . . . 8
⊢ (𝐾 ∈ (0...𝑁) → (0...𝑁) = ((0...𝐾) ∪ ((𝐾 + 1)...𝑁))) |
| 87 | 85, 86 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (0...𝑁) = ((0...𝐾) ∪ ((𝐾 + 1)...𝑁))) |
| 88 | | fzfid 14014 |
. . . . . . 7
⊢ (𝜑 → (0...𝑁) ∈ Fin) |
| 89 | | elfznn0 13660 |
. . . . . . . . 9
⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0) |
| 90 | 33, 89, 39 | syl2an 596 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝐴‘𝑘) ∈ ℂ) |
| 91 | 16, 89, 50 | syl2an 596 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝑇 · 𝑋)↑𝑘) ∈ ℂ) |
| 92 | 90, 91 | mulcld 11281 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) ∈ ℂ) |
| 93 | 60, 87, 88, 92 | fsumsplit 15777 |
. . . . . 6
⊢ (𝜑 → Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = (Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) + Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))) |
| 94 | 56, 93 | eqtrd 2777 |
. . . . 5
⊢ (𝜑 → (𝐹‘(𝑇 · 𝑋)) = (Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) + Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))) |
| 95 | 94 | fveq2d 6910 |
. . . 4
⊢ (𝜑 → (abs‘(𝐹‘(𝑇 · 𝑋))) = (abs‘(Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) + Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))))) |
| 96 | 1 | coefv0 26287 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∈ (Poly‘𝑆) → (𝐹‘0) = (𝐴‘0)) |
| 97 | 3, 96 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐹‘0) = (𝐴‘0)) |
| 98 | 97 | eqcomd 2743 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴‘0) = (𝐹‘0)) |
| 99 | 16 | exp0d 14180 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑇 · 𝑋)↑0) = 1) |
| 100 | 98, 99 | oveq12d 7449 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐴‘0) · ((𝑇 · 𝑋)↑0)) = ((𝐹‘0) · 1)) |
| 101 | 23 | mulridd 11278 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐹‘0) · 1) = (𝐹‘0)) |
| 102 | 100, 101 | eqtrd 2777 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐴‘0) · ((𝑇 · 𝑋)↑0)) = (𝐹‘0)) |
| 103 | | 1e0p1 12775 |
. . . . . . . . . . . . 13
⊢ 1 = (0 +
1) |
| 104 | 103 | oveq1i 7441 |
. . . . . . . . . . . 12
⊢
(1...𝐾) = ((0 +
1)...𝐾) |
| 105 | 104 | sumeq1i 15733 |
. . . . . . . . . . 11
⊢
Σ𝑘 ∈
(1...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = Σ𝑘 ∈ ((0 + 1)...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) |
| 106 | 26, 62 | eleqtrdi 2851 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐾 ∈
(ℤ≥‘1)) |
| 107 | | elfznn 13593 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ (1...𝐾) → 𝑘 ∈ ℕ) |
| 108 | 107 | nnnn0d 12587 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ (1...𝐾) → 𝑘 ∈ ℕ0) |
| 109 | 33, 108, 39 | syl2an 596 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐾)) → (𝐴‘𝑘) ∈ ℂ) |
| 110 | 16, 108, 50 | syl2an 596 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐾)) → ((𝑇 · 𝑋)↑𝑘) ∈ ℂ) |
| 111 | 109, 110 | mulcld 11281 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐾)) → ((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) ∈ ℂ) |
| 112 | | fveq2 6906 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝐾 → (𝐴‘𝑘) = (𝐴‘𝐾)) |
| 113 | | oveq2 7439 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝐾 → ((𝑇 · 𝑋)↑𝑘) = ((𝑇 · 𝑋)↑𝐾)) |
| 114 | 112, 113 | oveq12d 7449 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝐾 → ((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = ((𝐴‘𝐾) · ((𝑇 · 𝑋)↑𝐾))) |
| 115 | 106, 111,
114 | fsumm1 15787 |
. . . . . . . . . . 11
⊢ (𝜑 → Σ𝑘 ∈ (1...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = (Σ𝑘 ∈ (1...(𝐾 − 1))((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) + ((𝐴‘𝐾) · ((𝑇 · 𝑋)↑𝐾)))) |
| 116 | 105, 115 | eqtr3id 2791 |
. . . . . . . . . 10
⊢ (𝜑 → Σ𝑘 ∈ ((0 + 1)...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = (Σ𝑘 ∈ (1...(𝐾 − 1))((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) + ((𝐴‘𝐾) · ((𝑇 · 𝑋)↑𝐾)))) |
| 117 | | elfznn 13593 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 ∈ (1...(𝐾 − 1)) → 𝑘 ∈ ℕ) |
| 118 | 117 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → 𝑘 ∈ ℕ) |
| 119 | 118 | nnred 12281 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → 𝑘 ∈ ℝ) |
| 120 | 57 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → 𝐾 ∈ ℝ) |
| 121 | | peano2rem 11576 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐾 ∈ ℝ → (𝐾 − 1) ∈
ℝ) |
| 122 | 120, 121 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → (𝐾 − 1) ∈ ℝ) |
| 123 | | elfzle2 13568 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈ (1...(𝐾 − 1)) → 𝑘 ≤ (𝐾 − 1)) |
| 124 | 123 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → 𝑘 ≤ (𝐾 − 1)) |
| 125 | 120 | ltm1d 12200 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → (𝐾 − 1) < 𝐾) |
| 126 | 119, 122,
120, 124, 125 | lelttrd 11419 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → 𝑘 < 𝐾) |
| 127 | 119, 120 | ltnled 11408 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → (𝑘 < 𝐾 ↔ ¬ 𝐾 ≤ 𝑘)) |
| 128 | 126, 127 | mpbid 232 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → ¬ 𝐾 ≤ 𝑘) |
| 129 | | infssuzle 12973 |
. . . . . . . . . . . . . . . . . . 19
⊢ (({𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ⊆
(ℤ≥‘1) ∧ 𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0}) → inf({𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0}, ℝ, < ) ≤ 𝑘) |
| 130 | 6, 129 | eqbrtrid 5178 |
. . . . . . . . . . . . . . . . . 18
⊢ (({𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ⊆
(ℤ≥‘1) ∧ 𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0}) → 𝐾 ≤ 𝑘) |
| 131 | 63, 130 | mpan 690 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} → 𝐾 ≤ 𝑘) |
| 132 | 128, 131 | nsyl 140 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → ¬ 𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0}) |
| 133 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = 𝑘 → (𝐴‘𝑛) = (𝐴‘𝑘)) |
| 134 | 133 | neeq1d 3000 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 𝑘 → ((𝐴‘𝑛) ≠ 0 ↔ (𝐴‘𝑘) ≠ 0)) |
| 135 | 134 | elrab3 3693 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ ℕ → (𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ↔ (𝐴‘𝑘) ≠ 0)) |
| 136 | 118, 135 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → (𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ↔ (𝐴‘𝑘) ≠ 0)) |
| 137 | 136 | necon2bbid 2984 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → ((𝐴‘𝑘) = 0 ↔ ¬ 𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0})) |
| 138 | 132, 137 | mpbird 257 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → (𝐴‘𝑘) = 0) |
| 139 | 138 | oveq1d 7446 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → ((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = (0 · ((𝑇 · 𝑋)↑𝑘))) |
| 140 | 117 | nnnn0d 12587 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ (1...(𝐾 − 1)) → 𝑘 ∈ ℕ0) |
| 141 | 16, 140, 50 | syl2an 596 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → ((𝑇 · 𝑋)↑𝑘) ∈ ℂ) |
| 142 | 141 | mul02d 11459 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → (0 · ((𝑇 · 𝑋)↑𝑘)) = 0) |
| 143 | 139, 142 | eqtrd 2777 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → ((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = 0) |
| 144 | 143 | sumeq2dv 15738 |
. . . . . . . . . . . 12
⊢ (𝜑 → Σ𝑘 ∈ (1...(𝐾 − 1))((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = Σ𝑘 ∈ (1...(𝐾 − 1))0) |
| 145 | | fzfi 14013 |
. . . . . . . . . . . . . 14
⊢
(1...(𝐾 − 1))
∈ Fin |
| 146 | 145 | olci 867 |
. . . . . . . . . . . . 13
⊢
((1...(𝐾 − 1))
⊆ (ℤ≥‘1) ∨ (1...(𝐾 − 1)) ∈ Fin) |
| 147 | | sumz 15758 |
. . . . . . . . . . . . 13
⊢
(((1...(𝐾 −
1)) ⊆ (ℤ≥‘1) ∨ (1...(𝐾 − 1)) ∈ Fin) → Σ𝑘 ∈ (1...(𝐾 − 1))0 = 0) |
| 148 | 146, 147 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
Σ𝑘 ∈
(1...(𝐾 − 1))0 =
0 |
| 149 | 144, 148 | eqtrdi 2793 |
. . . . . . . . . . 11
⊢ (𝜑 → Σ𝑘 ∈ (1...(𝐾 − 1))((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = 0) |
| 150 | 12, 15, 27 | mulexpd 14201 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑇 · 𝑋)↑𝐾) = ((𝑇↑𝐾) · (𝑋↑𝐾))) |
| 151 | 150 | oveq2d 7447 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐴‘𝐾) · ((𝑇 · 𝑋)↑𝐾)) = ((𝐴‘𝐾) · ((𝑇↑𝐾) · (𝑋↑𝐾)))) |
| 152 | 33, 27 | ffvelcdmd 7105 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐴‘𝐾) ∈ ℂ) |
| 153 | 12, 27 | expcld 14186 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑇↑𝐾) ∈ ℂ) |
| 154 | 28 | recnd 11289 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑋↑𝐾) ∈ ℂ) |
| 155 | 152, 153,
154 | mulassd 11284 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((𝐴‘𝐾) · (𝑇↑𝐾)) · (𝑋↑𝐾)) = ((𝐴‘𝐾) · ((𝑇↑𝐾) · (𝑋↑𝐾)))) |
| 156 | 151, 155 | eqtr4d 2780 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐴‘𝐾) · ((𝑇 · 𝑋)↑𝐾)) = (((𝐴‘𝐾) · (𝑇↑𝐾)) · (𝑋↑𝐾))) |
| 157 | 7 | oveq1i 7441 |
. . . . . . . . . . . . . . . 16
⊢ (𝑇↑𝐾) = ((-((𝐹‘0) / (𝐴‘𝐾))↑𝑐(1 / 𝐾))↑𝐾) |
| 158 | 57 | recnd 11289 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐾 ∈ ℂ) |
| 159 | 26 | nnne0d 12316 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐾 ≠ 0) |
| 160 | 158, 159 | recid2d 12039 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((1 / 𝐾) · 𝐾) = 1) |
| 161 | 160 | oveq2d 7447 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (-((𝐹‘0) / (𝐴‘𝐾))↑𝑐((1 / 𝐾) · 𝐾)) = (-((𝐹‘0) / (𝐴‘𝐾))↑𝑐1)) |
| 162 | 25 | simprd 495 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐴‘𝐾) ≠ 0) |
| 163 | 23, 152, 162 | divcld 12043 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝐹‘0) / (𝐴‘𝐾)) ∈ ℂ) |
| 164 | 163 | negcld 11607 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → -((𝐹‘0) / (𝐴‘𝐾)) ∈ ℂ) |
| 165 | 26 | nnrecred 12317 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (1 / 𝐾) ∈ ℝ) |
| 166 | 165 | recnd 11289 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (1 / 𝐾) ∈ ℂ) |
| 167 | 164, 166,
27 | cxpmul2d 26751 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (-((𝐹‘0) / (𝐴‘𝐾))↑𝑐((1 / 𝐾) · 𝐾)) = ((-((𝐹‘0) / (𝐴‘𝐾))↑𝑐(1 / 𝐾))↑𝐾)) |
| 168 | 164 | cxp1d 26748 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (-((𝐹‘0) / (𝐴‘𝐾))↑𝑐1) = -((𝐹‘0) / (𝐴‘𝐾))) |
| 169 | 161, 167,
168 | 3eqtr3d 2785 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((-((𝐹‘0) / (𝐴‘𝐾))↑𝑐(1 / 𝐾))↑𝐾) = -((𝐹‘0) / (𝐴‘𝐾))) |
| 170 | 157, 169 | eqtrid 2789 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑇↑𝐾) = -((𝐹‘0) / (𝐴‘𝐾))) |
| 171 | 170 | oveq2d 7447 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐴‘𝐾) · (𝑇↑𝐾)) = ((𝐴‘𝐾) · -((𝐹‘0) / (𝐴‘𝐾)))) |
| 172 | 152, 163 | mulneg2d 11717 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐴‘𝐾) · -((𝐹‘0) / (𝐴‘𝐾))) = -((𝐴‘𝐾) · ((𝐹‘0) / (𝐴‘𝐾)))) |
| 173 | 23, 152, 162 | divcan2d 12045 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝐴‘𝐾) · ((𝐹‘0) / (𝐴‘𝐾))) = (𝐹‘0)) |
| 174 | 173 | negeqd 11502 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → -((𝐴‘𝐾) · ((𝐹‘0) / (𝐴‘𝐾))) = -(𝐹‘0)) |
| 175 | 171, 172,
174 | 3eqtrd 2781 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐴‘𝐾) · (𝑇↑𝐾)) = -(𝐹‘0)) |
| 176 | 175 | oveq1d 7446 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝐴‘𝐾) · (𝑇↑𝐾)) · (𝑋↑𝐾)) = (-(𝐹‘0) · (𝑋↑𝐾))) |
| 177 | 23, 154 | mulneg1d 11716 |
. . . . . . . . . . . 12
⊢ (𝜑 → (-(𝐹‘0) · (𝑋↑𝐾)) = -((𝐹‘0) · (𝑋↑𝐾))) |
| 178 | 156, 176,
177 | 3eqtrd 2781 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐴‘𝐾) · ((𝑇 · 𝑋)↑𝐾)) = -((𝐹‘0) · (𝑋↑𝐾))) |
| 179 | 149, 178 | oveq12d 7449 |
. . . . . . . . . 10
⊢ (𝜑 → (Σ𝑘 ∈ (1...(𝐾 − 1))((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) + ((𝐴‘𝐾) · ((𝑇 · 𝑋)↑𝐾))) = (0 + -((𝐹‘0) · (𝑋↑𝐾)))) |
| 180 | 23, 154 | mulcld 11281 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐹‘0) · (𝑋↑𝐾)) ∈ ℂ) |
| 181 | 180 | negcld 11607 |
. . . . . . . . . . 11
⊢ (𝜑 → -((𝐹‘0) · (𝑋↑𝐾)) ∈ ℂ) |
| 182 | 181 | addlidd 11462 |
. . . . . . . . . 10
⊢ (𝜑 → (0 + -((𝐹‘0) · (𝑋↑𝐾))) = -((𝐹‘0) · (𝑋↑𝐾))) |
| 183 | 116, 179,
182 | 3eqtrd 2781 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑘 ∈ ((0 + 1)...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = -((𝐹‘0) · (𝑋↑𝐾))) |
| 184 | 102, 183 | oveq12d 7449 |
. . . . . . . 8
⊢ (𝜑 → (((𝐴‘0) · ((𝑇 · 𝑋)↑0)) + Σ𝑘 ∈ ((0 + 1)...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) = ((𝐹‘0) + -((𝐹‘0) · (𝑋↑𝐾)))) |
| 185 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑘 = 0 → (𝐴‘𝑘) = (𝐴‘0)) |
| 186 | | oveq2 7439 |
. . . . . . . . . 10
⊢ (𝑘 = 0 → ((𝑇 · 𝑋)↑𝑘) = ((𝑇 · 𝑋)↑0)) |
| 187 | 185, 186 | oveq12d 7449 |
. . . . . . . . 9
⊢ (𝑘 = 0 → ((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = ((𝐴‘0) · ((𝑇 · 𝑋)↑0))) |
| 188 | 81, 52, 187 | fsum1p 15789 |
. . . . . . . 8
⊢ (𝜑 → Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = (((𝐴‘0) · ((𝑇 · 𝑋)↑0)) + Σ𝑘 ∈ ((0 + 1)...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))) |
| 189 | 101 | oveq1d 7446 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐹‘0) · 1) − ((𝐹‘0) · (𝑋↑𝐾))) = ((𝐹‘0) − ((𝐹‘0) · (𝑋↑𝐾)))) |
| 190 | | 1cnd 11256 |
. . . . . . . . . 10
⊢ (𝜑 → 1 ∈
ℂ) |
| 191 | 23, 190, 154 | subdid 11719 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐹‘0) · (1 − (𝑋↑𝐾))) = (((𝐹‘0) · 1) − ((𝐹‘0) · (𝑋↑𝐾)))) |
| 192 | 23, 180 | negsubd 11626 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐹‘0) + -((𝐹‘0) · (𝑋↑𝐾))) = ((𝐹‘0) − ((𝐹‘0) · (𝑋↑𝐾)))) |
| 193 | 189, 191,
192 | 3eqtr4d 2787 |
. . . . . . . 8
⊢ (𝜑 → ((𝐹‘0) · (1 − (𝑋↑𝐾))) = ((𝐹‘0) + -((𝐹‘0) · (𝑋↑𝐾)))) |
| 194 | 184, 188,
193 | 3eqtr4d 2787 |
. . . . . . 7
⊢ (𝜑 → Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = ((𝐹‘0) · (1 − (𝑋↑𝐾)))) |
| 195 | 194 | fveq2d 6910 |
. . . . . 6
⊢ (𝜑 → (abs‘Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) = (abs‘((𝐹‘0) · (1 − (𝑋↑𝐾))))) |
| 196 | | 1re 11261 |
. . . . . . . . 9
⊢ 1 ∈
ℝ |
| 197 | | resubcl 11573 |
. . . . . . . . 9
⊢ ((1
∈ ℝ ∧ (𝑋↑𝐾) ∈ ℝ) → (1 − (𝑋↑𝐾)) ∈ ℝ) |
| 198 | 196, 28, 197 | sylancr 587 |
. . . . . . . 8
⊢ (𝜑 → (1 − (𝑋↑𝐾)) ∈ ℝ) |
| 199 | 198 | recnd 11289 |
. . . . . . 7
⊢ (𝜑 → (1 − (𝑋↑𝐾)) ∈ ℂ) |
| 200 | 23, 199 | absmuld 15493 |
. . . . . 6
⊢ (𝜑 → (abs‘((𝐹‘0) · (1 −
(𝑋↑𝐾)))) = ((abs‘(𝐹‘0)) · (abs‘(1 −
(𝑋↑𝐾))))) |
| 201 | 13 | rpge0d 13081 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ≤ 𝑋) |
| 202 | 11 | simp2d 1144 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑈 ∈
ℝ+) |
| 203 | 202 | rpred 13077 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑈 ∈ ℝ) |
| 204 | | min1 13231 |
. . . . . . . . . . . . 13
⊢ ((1
∈ ℝ ∧ 𝑈
∈ ℝ) → if(1 ≤ 𝑈, 1, 𝑈) ≤ 1) |
| 205 | 196, 203,
204 | sylancr 587 |
. . . . . . . . . . . 12
⊢ (𝜑 → if(1 ≤ 𝑈, 1, 𝑈) ≤ 1) |
| 206 | 9, 205 | eqbrtrid 5178 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ≤ 1) |
| 207 | | exple1 14216 |
. . . . . . . . . . 11
⊢ (((𝑋 ∈ ℝ ∧ 0 ≤
𝑋 ∧ 𝑋 ≤ 1) ∧ 𝐾 ∈ ℕ0) → (𝑋↑𝐾) ≤ 1) |
| 208 | 14, 201, 206, 27, 207 | syl31anc 1375 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑋↑𝐾) ≤ 1) |
| 209 | | subge0 11776 |
. . . . . . . . . . 11
⊢ ((1
∈ ℝ ∧ (𝑋↑𝐾) ∈ ℝ) → (0 ≤ (1 −
(𝑋↑𝐾)) ↔ (𝑋↑𝐾) ≤ 1)) |
| 210 | 196, 28, 209 | sylancr 587 |
. . . . . . . . . 10
⊢ (𝜑 → (0 ≤ (1 − (𝑋↑𝐾)) ↔ (𝑋↑𝐾) ≤ 1)) |
| 211 | 208, 210 | mpbird 257 |
. . . . . . . . 9
⊢ (𝜑 → 0 ≤ (1 − (𝑋↑𝐾))) |
| 212 | 198, 211 | absidd 15461 |
. . . . . . . 8
⊢ (𝜑 → (abs‘(1 −
(𝑋↑𝐾))) = (1 − (𝑋↑𝐾))) |
| 213 | 212 | oveq2d 7447 |
. . . . . . 7
⊢ (𝜑 → ((abs‘(𝐹‘0)) ·
(abs‘(1 − (𝑋↑𝐾)))) = ((abs‘(𝐹‘0)) · (1 − (𝑋↑𝐾)))) |
| 214 | 24 | recnd 11289 |
. . . . . . . 8
⊢ (𝜑 → (abs‘(𝐹‘0)) ∈
ℂ) |
| 215 | 214, 190,
154 | subdid 11719 |
. . . . . . 7
⊢ (𝜑 → ((abs‘(𝐹‘0)) · (1 −
(𝑋↑𝐾))) = (((abs‘(𝐹‘0)) · 1) −
((abs‘(𝐹‘0))
· (𝑋↑𝐾)))) |
| 216 | 214 | mulridd 11278 |
. . . . . . . 8
⊢ (𝜑 → ((abs‘(𝐹‘0)) · 1) =
(abs‘(𝐹‘0))) |
| 217 | 216 | oveq1d 7446 |
. . . . . . 7
⊢ (𝜑 → (((abs‘(𝐹‘0)) · 1) −
((abs‘(𝐹‘0))
· (𝑋↑𝐾))) = ((abs‘(𝐹‘0)) −
((abs‘(𝐹‘0))
· (𝑋↑𝐾)))) |
| 218 | 213, 215,
217 | 3eqtrd 2781 |
. . . . . 6
⊢ (𝜑 → ((abs‘(𝐹‘0)) ·
(abs‘(1 − (𝑋↑𝐾)))) = ((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋↑𝐾)))) |
| 219 | 195, 200,
218 | 3eqtrrd 2782 |
. . . . 5
⊢ (𝜑 → ((abs‘(𝐹‘0)) −
((abs‘(𝐹‘0))
· (𝑋↑𝐾))) = (abs‘Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))) |
| 220 | 219 | oveq1d 7446 |
. . . 4
⊢ (𝜑 → (((abs‘(𝐹‘0)) −
((abs‘(𝐹‘0))
· (𝑋↑𝐾))) + (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))) = ((abs‘Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) + (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))))) |
| 221 | 54, 95, 220 | 3brtr4d 5175 |
. . 3
⊢ (𝜑 → (abs‘(𝐹‘(𝑇 · 𝑋))) ≤ (((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋↑𝐾))) + (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))))) |
| 222 | 43 | abscld 15475 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) ∈ ℝ) |
| 223 | 31, 222 | fsumrecl 15770 |
. . . . . 6
⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) ∈ ℝ) |
| 224 | 31, 43 | fsumabs 15837 |
. . . . . 6
⊢ (𝜑 → (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) ≤ Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))) |
| 225 | | expcl 14120 |
. . . . . . . . . . . 12
⊢ ((𝑇 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (𝑇↑𝑘) ∈
ℂ) |
| 226 | 12, 38, 225 | syl2an2r 685 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑇↑𝑘) ∈ ℂ) |
| 227 | 40, 226 | mulcld 11281 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((𝐴‘𝑘) · (𝑇↑𝑘)) ∈ ℂ) |
| 228 | 227 | abscld 15475 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) ∈ ℝ) |
| 229 | 31, 228 | fsumrecl 15770 |
. . . . . . . 8
⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) ∈ ℝ) |
| 230 | 14, 35 | reexpcld 14203 |
. . . . . . . 8
⊢ (𝜑 → (𝑋↑(𝐾 + 1)) ∈ ℝ) |
| 231 | 229, 230 | remulcld 11291 |
. . . . . . 7
⊢ (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1))) ∈ ℝ) |
| 232 | 230 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑋↑(𝐾 + 1)) ∈ ℝ) |
| 233 | 228, 232 | remulcld 11291 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1))) ∈ ℝ) |
| 234 | 12 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑇 ∈ ℂ) |
| 235 | 15 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑋 ∈ ℂ) |
| 236 | 234, 235,
38 | mulexpd 14201 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((𝑇 · 𝑋)↑𝑘) = ((𝑇↑𝑘) · (𝑋↑𝑘))) |
| 237 | 236 | oveq2d 7447 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = ((𝐴‘𝑘) · ((𝑇↑𝑘) · (𝑋↑𝑘)))) |
| 238 | 14 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑋 ∈ ℝ) |
| 239 | 238, 38 | reexpcld 14203 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑋↑𝑘) ∈ ℝ) |
| 240 | 239 | recnd 11289 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑋↑𝑘) ∈ ℂ) |
| 241 | 40, 226, 240 | mulassd 11284 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (((𝐴‘𝑘) · (𝑇↑𝑘)) · (𝑋↑𝑘)) = ((𝐴‘𝑘) · ((𝑇↑𝑘) · (𝑋↑𝑘)))) |
| 242 | 237, 241 | eqtr4d 2780 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = (((𝐴‘𝑘) · (𝑇↑𝑘)) · (𝑋↑𝑘))) |
| 243 | 242 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) = (abs‘(((𝐴‘𝑘) · (𝑇↑𝑘)) · (𝑋↑𝑘)))) |
| 244 | 227, 240 | absmuld 15493 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘(((𝐴‘𝑘) · (𝑇↑𝑘)) · (𝑋↑𝑘))) = ((abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (abs‘(𝑋↑𝑘)))) |
| 245 | | elfzelz 13564 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ((𝐾 + 1)...𝑁) → 𝑘 ∈ ℤ) |
| 246 | | rpexpcl 14121 |
. . . . . . . . . . . . . . 15
⊢ ((𝑋 ∈ ℝ+
∧ 𝑘 ∈ ℤ)
→ (𝑋↑𝑘) ∈
ℝ+) |
| 247 | 13, 245, 246 | syl2an 596 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑋↑𝑘) ∈
ℝ+) |
| 248 | 247 | rpge0d 13081 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 0 ≤ (𝑋↑𝑘)) |
| 249 | 239, 248 | absidd 15461 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘(𝑋↑𝑘)) = (𝑋↑𝑘)) |
| 250 | 249 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (abs‘(𝑋↑𝑘))) = ((abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑𝑘))) |
| 251 | 243, 244,
250 | 3eqtrd 2781 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) = ((abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑𝑘))) |
| 252 | 227 | absge0d 15483 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 0 ≤ (abs‘((𝐴‘𝑘) · (𝑇↑𝑘)))) |
| 253 | 35 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝐾 + 1) ∈
ℕ0) |
| 254 | 36 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑘 ∈ (ℤ≥‘(𝐾 + 1))) |
| 255 | 201 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 0 ≤ 𝑋) |
| 256 | 206 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑋 ≤ 1) |
| 257 | 238, 253,
254, 255, 256 | leexp2rd 14294 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑋↑𝑘) ≤ (𝑋↑(𝐾 + 1))) |
| 258 | 239, 232,
228, 252, 257 | lemul2ad 12208 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑𝑘)) ≤ ((abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1)))) |
| 259 | 251, 258 | eqbrtrd 5165 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) ≤ ((abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1)))) |
| 260 | 31, 222, 233, 259 | fsumle 15835 |
. . . . . . . 8
⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) ≤ Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1)))) |
| 261 | 230 | recnd 11289 |
. . . . . . . . 9
⊢ (𝜑 → (𝑋↑(𝐾 + 1)) ∈ ℂ) |
| 262 | 228 | recnd 11289 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) ∈ ℂ) |
| 263 | 31, 261, 262 | fsummulc1 15821 |
. . . . . . . 8
⊢ (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1))) = Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1)))) |
| 264 | 260, 263 | breqtrrd 5171 |
. . . . . . 7
⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) ≤ (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1)))) |
| 265 | 15, 27 | expp1d 14187 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑋↑(𝐾 + 1)) = ((𝑋↑𝐾) · 𝑋)) |
| 266 | 154, 15 | mulcomd 11282 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑋↑𝐾) · 𝑋) = (𝑋 · (𝑋↑𝐾))) |
| 267 | 265, 266 | eqtrd 2777 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑋↑(𝐾 + 1)) = (𝑋 · (𝑋↑𝐾))) |
| 268 | 267 | oveq2d 7447 |
. . . . . . . . 9
⊢ (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1))) = (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋 · (𝑋↑𝐾)))) |
| 269 | 229 | recnd 11289 |
. . . . . . . . . 10
⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) ∈ ℂ) |
| 270 | 269, 15, 154 | mulassd 11284 |
. . . . . . . . 9
⊢ (𝜑 → ((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · 𝑋) · (𝑋↑𝐾)) = (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋 · (𝑋↑𝐾)))) |
| 271 | 268, 270 | eqtr4d 2780 |
. . . . . . . 8
⊢ (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1))) = ((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · 𝑋) · (𝑋↑𝐾))) |
| 272 | 229, 14 | remulcld 11291 |
. . . . . . . . 9
⊢ (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · 𝑋) ∈ ℝ) |
| 273 | | nnssz 12635 |
. . . . . . . . . . . 12
⊢ ℕ
⊆ ℤ |
| 274 | 61, 273 | sstri 3993 |
. . . . . . . . . . 11
⊢ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ⊆ ℤ |
| 275 | 76 | ne0d 4342 |
. . . . . . . . . . . . 13
⊢ (𝜑 → {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ≠ ∅) |
| 276 | | infssuzcl 12974 |
. . . . . . . . . . . . 13
⊢ (({𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ⊆
(ℤ≥‘1) ∧ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ≠ ∅) → inf({𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0}, ℝ, < ) ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0}) |
| 277 | 63, 275, 276 | sylancr 587 |
. . . . . . . . . . . 12
⊢ (𝜑 → inf({𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0}, ℝ, < ) ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0}) |
| 278 | 6, 277 | eqeltrid 2845 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐾 ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0}) |
| 279 | 274, 278 | sselid 3981 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐾 ∈ ℤ) |
| 280 | 13, 279 | rpexpcld 14286 |
. . . . . . . . 9
⊢ (𝜑 → (𝑋↑𝐾) ∈
ℝ+) |
| 281 | | peano2re 11434 |
. . . . . . . . . . . 12
⊢
(Σ𝑘 ∈
((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) ∈ ℝ → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1) ∈ ℝ) |
| 282 | 229, 281 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1) ∈ ℝ) |
| 283 | 282, 14 | remulcld 11291 |
. . . . . . . . . 10
⊢ (𝜑 → ((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1) · 𝑋) ∈ ℝ) |
| 284 | 229 | ltp1d 12198 |
. . . . . . . . . . 11
⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) < (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1)) |
| 285 | 229, 282,
13, 284 | ltmul1dd 13132 |
. . . . . . . . . 10
⊢ (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · 𝑋) < ((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1) · 𝑋)) |
| 286 | | min2 13232 |
. . . . . . . . . . . . . 14
⊢ ((1
∈ ℝ ∧ 𝑈
∈ ℝ) → if(1 ≤ 𝑈, 1, 𝑈) ≤ 𝑈) |
| 287 | 196, 203,
286 | sylancr 587 |
. . . . . . . . . . . . 13
⊢ (𝜑 → if(1 ≤ 𝑈, 1, 𝑈) ≤ 𝑈) |
| 288 | 9, 287 | eqbrtrid 5178 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑋 ≤ 𝑈) |
| 289 | 288, 8 | breqtrdi 5184 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ≤ ((abs‘(𝐹‘0)) / (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1))) |
| 290 | | 0red 11264 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 ∈
ℝ) |
| 291 | 31, 228, 252 | fsumge0 15831 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 ≤ Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘)))) |
| 292 | 290, 229,
282, 291, 284 | lelttrd 11419 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 < (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1)) |
| 293 | | lemuldiv2 12149 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∈ ℝ ∧
(abs‘(𝐹‘0))
∈ ℝ ∧ ((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1) ∈ ℝ ∧ 0 <
(Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1))) → (((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1) · 𝑋) ≤ (abs‘(𝐹‘0)) ↔ 𝑋 ≤ ((abs‘(𝐹‘0)) / (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1)))) |
| 294 | 14, 24, 282, 292, 293 | syl112anc 1376 |
. . . . . . . . . . 11
⊢ (𝜑 → (((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1) · 𝑋) ≤ (abs‘(𝐹‘0)) ↔ 𝑋 ≤ ((abs‘(𝐹‘0)) / (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1)))) |
| 295 | 289, 294 | mpbird 257 |
. . . . . . . . . 10
⊢ (𝜑 → ((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1) · 𝑋) ≤ (abs‘(𝐹‘0))) |
| 296 | 272, 283,
24, 285, 295 | ltletrd 11421 |
. . . . . . . . 9
⊢ (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · 𝑋) < (abs‘(𝐹‘0))) |
| 297 | 272, 24, 280, 296 | ltmul1dd 13132 |
. . . . . . . 8
⊢ (𝜑 → ((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · 𝑋) · (𝑋↑𝐾)) < ((abs‘(𝐹‘0)) · (𝑋↑𝐾))) |
| 298 | 271, 297 | eqbrtrd 5165 |
. . . . . . 7
⊢ (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1))) < ((abs‘(𝐹‘0)) · (𝑋↑𝐾))) |
| 299 | 223, 231,
29, 264, 298 | lelttrd 11419 |
. . . . . 6
⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) < ((abs‘(𝐹‘0)) · (𝑋↑𝐾))) |
| 300 | 45, 223, 29, 224, 299 | lelttrd 11419 |
. . . . 5
⊢ (𝜑 → (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) < ((abs‘(𝐹‘0)) · (𝑋↑𝐾))) |
| 301 | 45, 29, 24, 300 | ltsub2dd 11876 |
. . . 4
⊢ (𝜑 → ((abs‘(𝐹‘0)) −
((abs‘(𝐹‘0))
· (𝑋↑𝐾))) < ((abs‘(𝐹‘0)) −
(abs‘Σ𝑘 ∈
((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))))) |
| 302 | 30, 45, 24 | ltaddsubd 11863 |
. . . 4
⊢ (𝜑 → ((((abs‘(𝐹‘0)) −
((abs‘(𝐹‘0))
· (𝑋↑𝐾))) + (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))) < (abs‘(𝐹‘0)) ↔ ((abs‘(𝐹‘0)) −
((abs‘(𝐹‘0))
· (𝑋↑𝐾))) < ((abs‘(𝐹‘0)) −
(abs‘Σ𝑘 ∈
((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))))) |
| 303 | 301, 302 | mpbird 257 |
. . 3
⊢ (𝜑 → (((abs‘(𝐹‘0)) −
((abs‘(𝐹‘0))
· (𝑋↑𝐾))) + (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))) < (abs‘(𝐹‘0))) |
| 304 | 20, 46, 24, 221, 303 | lelttrd 11419 |
. 2
⊢ (𝜑 → (abs‘(𝐹‘(𝑇 · 𝑋))) < (abs‘(𝐹‘0))) |
| 305 | | 2fveq3 6911 |
. . . 4
⊢ (𝑥 = (𝑇 · 𝑋) → (abs‘(𝐹‘𝑥)) = (abs‘(𝐹‘(𝑇 · 𝑋)))) |
| 306 | 305 | breq1d 5153 |
. . 3
⊢ (𝑥 = (𝑇 · 𝑋) → ((abs‘(𝐹‘𝑥)) < (abs‘(𝐹‘0)) ↔ (abs‘(𝐹‘(𝑇 · 𝑋))) < (abs‘(𝐹‘0)))) |
| 307 | 306 | rspcev 3622 |
. 2
⊢ (((𝑇 · 𝑋) ∈ ℂ ∧ (abs‘(𝐹‘(𝑇 · 𝑋))) < (abs‘(𝐹‘0))) → ∃𝑥 ∈ ℂ (abs‘(𝐹‘𝑥)) < (abs‘(𝐹‘0))) |
| 308 | 16, 304, 307 | syl2anc 584 |
1
⊢ (𝜑 → ∃𝑥 ∈ ℂ (abs‘(𝐹‘𝑥)) < (abs‘(𝐹‘0))) |