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 24802 |
. . . . 5
⊢ (𝜑 → ((𝐾 ∈ ℕ ∧ (𝐴‘𝐾) ≠ 0) ∧ (𝑇 ∈ ℂ ∧ 𝑈 ∈ ℝ+ ∧ 𝑋 ∈
ℝ+))) |
11 | 10 | simprd 479 |
. . . 4
⊢ (𝜑 → (𝑇 ∈ ℂ ∧ 𝑈 ∈ ℝ+ ∧ 𝑋 ∈
ℝ+)) |
12 | 11 | simp1d 1073 |
. . 3
⊢ (𝜑 → 𝑇 ∈ ℂ) |
13 | 11 | simp3d 1075 |
. . . . 5
⊢ (𝜑 → 𝑋 ∈
ℝ+) |
14 | 13 | rpred 11872 |
. . . 4
⊢ (𝜑 → 𝑋 ∈ ℝ) |
15 | 14 | recnd 10068 |
. . 3
⊢ (𝜑 → 𝑋 ∈ ℂ) |
16 | 12, 15 | mulcld 10060 |
. 2
⊢ (𝜑 → (𝑇 · 𝑋) ∈ ℂ) |
17 | | plyf 23954 |
. . . . . 6
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐹:ℂ⟶ℂ) |
18 | 3, 17 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐹:ℂ⟶ℂ) |
19 | 18, 16 | ffvelrnd 6360 |
. . . 4
⊢ (𝜑 → (𝐹‘(𝑇 · 𝑋)) ∈ ℂ) |
20 | 19 | abscld 14175 |
. . 3
⊢ (𝜑 → (abs‘(𝐹‘(𝑇 · 𝑋))) ∈ ℝ) |
21 | | 0cn 10032 |
. . . . . . 7
⊢ 0 ∈
ℂ |
22 | | ffvelrn 6357 |
. . . . . . 7
⊢ ((𝐹:ℂ⟶ℂ ∧ 0
∈ ℂ) → (𝐹‘0) ∈ ℂ) |
23 | 18, 21, 22 | sylancl 694 |
. . . . . 6
⊢ (𝜑 → (𝐹‘0) ∈ ℂ) |
24 | 23 | abscld 14175 |
. . . . 5
⊢ (𝜑 → (abs‘(𝐹‘0)) ∈
ℝ) |
25 | 10 | simpld 475 |
. . . . . . . . 9
⊢ (𝜑 → (𝐾 ∈ ℕ ∧ (𝐴‘𝐾) ≠ 0)) |
26 | 25 | simpld 475 |
. . . . . . . 8
⊢ (𝜑 → 𝐾 ∈ ℕ) |
27 | 26 | nnnn0d 11351 |
. . . . . . 7
⊢ (𝜑 → 𝐾 ∈
ℕ0) |
28 | 14, 27 | reexpcld 13025 |
. . . . . 6
⊢ (𝜑 → (𝑋↑𝐾) ∈ ℝ) |
29 | 24, 28 | remulcld 10070 |
. . . . 5
⊢ (𝜑 → ((abs‘(𝐹‘0)) · (𝑋↑𝐾)) ∈ ℝ) |
30 | 24, 29 | resubcld 10458 |
. . . 4
⊢ (𝜑 → ((abs‘(𝐹‘0)) −
((abs‘(𝐹‘0))
· (𝑋↑𝐾))) ∈
ℝ) |
31 | | fzfid 12772 |
. . . . . 6
⊢ (𝜑 → ((𝐾 + 1)...𝑁) ∈ Fin) |
32 | | peano2nn0 11333 |
. . . . . . . . . 10
⊢ (𝐾 ∈ ℕ0
→ (𝐾 + 1) ∈
ℕ0) |
33 | 27, 32 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝐾 + 1) ∈
ℕ0) |
34 | | elfzuz 12338 |
. . . . . . . . 9
⊢ (𝑘 ∈ ((𝐾 + 1)...𝑁) → 𝑘 ∈ (ℤ≥‘(𝐾 + 1))) |
35 | | eluznn0 11757 |
. . . . . . . . 9
⊢ (((𝐾 + 1) ∈ ℕ0
∧ 𝑘 ∈
(ℤ≥‘(𝐾 + 1))) → 𝑘 ∈ ℕ0) |
36 | 33, 34, 35 | syl2an 494 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑘 ∈ ℕ0) |
37 | 1 | coef3 23988 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐴:ℕ0⟶ℂ) |
38 | 3, 37 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) |
39 | | ffvelrn 6357 |
. . . . . . . . 9
⊢ ((𝐴:ℕ0⟶ℂ ∧
𝑘 ∈
ℕ0) → (𝐴‘𝑘) ∈ ℂ) |
40 | 38, 39 | sylan 488 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐴‘𝑘) ∈ ℂ) |
41 | 36, 40 | syldan 487 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝐴‘𝑘) ∈ ℂ) |
42 | 16 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑇 · 𝑋) ∈ ℂ) |
43 | 42, 36 | expcld 13008 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((𝑇 · 𝑋)↑𝑘) ∈ ℂ) |
44 | 41, 43 | mulcld 10060 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) ∈ ℂ) |
45 | 31, 44 | fsumcl 14464 |
. . . . 5
⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) ∈ ℂ) |
46 | 45 | abscld 14175 |
. . . 4
⊢ (𝜑 → (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) ∈ ℝ) |
47 | 30, 46 | readdcld 10069 |
. . 3
⊢ (𝜑 → (((abs‘(𝐹‘0)) −
((abs‘(𝐹‘0))
· (𝑋↑𝐾))) + (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))) ∈ ℝ) |
48 | | fzfid 12772 |
. . . . . 6
⊢ (𝜑 → (0...𝐾) ∈ Fin) |
49 | | elfznn0 12433 |
. . . . . . . 8
⊢ (𝑘 ∈ (0...𝐾) → 𝑘 ∈ ℕ0) |
50 | 38, 49, 39 | syl2an 494 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐾)) → (𝐴‘𝑘) ∈ ℂ) |
51 | | expcl 12878 |
. . . . . . . 8
⊢ (((𝑇 · 𝑋) ∈ ℂ ∧ 𝑘 ∈ ℕ0) → ((𝑇 · 𝑋)↑𝑘) ∈ ℂ) |
52 | 16, 49, 51 | syl2an 494 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐾)) → ((𝑇 · 𝑋)↑𝑘) ∈ ℂ) |
53 | 50, 52 | mulcld 10060 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐾)) → ((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) ∈ ℂ) |
54 | 48, 53 | fsumcl 14464 |
. . . . 5
⊢ (𝜑 → Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) ∈ ℂ) |
55 | 54, 45 | abstrid 14195 |
. . . 4
⊢ (𝜑 → (abs‘(Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) + Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))) ≤ ((abs‘Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) + (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))))) |
56 | 1, 2 | coeid2 23995 |
. . . . . . 7
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (𝑇 · 𝑋) ∈ ℂ) → (𝐹‘(𝑇 · 𝑋)) = Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) |
57 | 3, 16, 56 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → (𝐹‘(𝑇 · 𝑋)) = Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) |
58 | 26 | nnred 11035 |
. . . . . . . . 9
⊢ (𝜑 → 𝐾 ∈ ℝ) |
59 | 58 | ltp1d 10954 |
. . . . . . . 8
⊢ (𝜑 → 𝐾 < (𝐾 + 1)) |
60 | | fzdisj 12368 |
. . . . . . . 8
⊢ (𝐾 < (𝐾 + 1) → ((0...𝐾) ∩ ((𝐾 + 1)...𝑁)) = ∅) |
61 | 59, 60 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((0...𝐾) ∩ ((𝐾 + 1)...𝑁)) = ∅) |
62 | | ssrab2 3687 |
. . . . . . . . . . . 12
⊢ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ⊆ ℕ |
63 | | nnuz 11723 |
. . . . . . . . . . . 12
⊢ ℕ =
(ℤ≥‘1) |
64 | 62, 63 | sseqtri 3637 |
. . . . . . . . . . 11
⊢ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ⊆
(ℤ≥‘1) |
65 | 4 | nnne0d 11065 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ≠ 0) |
66 | 2, 1 | dgreq0 24021 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 ∈ (Poly‘𝑆) → (𝐹 = 0𝑝 ↔ (𝐴‘𝑁) = 0)) |
67 | 3, 66 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐹 = 0𝑝 ↔ (𝐴‘𝑁) = 0)) |
68 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹 = 0𝑝 →
(deg‘𝐹) =
(deg‘0𝑝)) |
69 | | dgr0 24018 |
. . . . . . . . . . . . . . . . 17
⊢
(deg‘0𝑝) = 0 |
70 | 68, 69 | syl6eq 2672 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 = 0𝑝 →
(deg‘𝐹) =
0) |
71 | 2, 70 | syl5eq 2668 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 = 0𝑝 →
𝑁 = 0) |
72 | 67, 71 | syl6bir 244 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐴‘𝑁) = 0 → 𝑁 = 0)) |
73 | 72 | necon3d 2815 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑁 ≠ 0 → (𝐴‘𝑁) ≠ 0)) |
74 | 65, 73 | mpd 15 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴‘𝑁) ≠ 0) |
75 | | fveq2 6191 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑁 → (𝐴‘𝑛) = (𝐴‘𝑁)) |
76 | 75 | neeq1d 2853 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑁 → ((𝐴‘𝑛) ≠ 0 ↔ (𝐴‘𝑁) ≠ 0)) |
77 | 76 | elrab 3363 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ↔ (𝑁 ∈ ℕ ∧ (𝐴‘𝑁) ≠ 0)) |
78 | 4, 74, 77 | sylanbrc 698 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0}) |
79 | | infssuzle 11771 |
. . . . . . . . . . 11
⊢ (({𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ⊆
(ℤ≥‘1) ∧ 𝑁 ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0}) → inf({𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0}, ℝ, < ) ≤ 𝑁) |
80 | 64, 78, 79 | sylancr 695 |
. . . . . . . . . 10
⊢ (𝜑 → inf({𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0}, ℝ, < ) ≤ 𝑁) |
81 | 6, 80 | syl5eqbr 4688 |
. . . . . . . . 9
⊢ (𝜑 → 𝐾 ≤ 𝑁) |
82 | | nn0uz 11722 |
. . . . . . . . . . 11
⊢
ℕ0 = (ℤ≥‘0) |
83 | 27, 82 | syl6eleq 2711 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐾 ∈
(ℤ≥‘0)) |
84 | 4 | nnzd 11481 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ ℤ) |
85 | | elfz5 12334 |
. . . . . . . . . 10
⊢ ((𝐾 ∈
(ℤ≥‘0) ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (0...𝑁) ↔ 𝐾 ≤ 𝑁)) |
86 | 83, 84, 85 | syl2anc 693 |
. . . . . . . . 9
⊢ (𝜑 → (𝐾 ∈ (0...𝑁) ↔ 𝐾 ≤ 𝑁)) |
87 | 81, 86 | mpbird 247 |
. . . . . . . 8
⊢ (𝜑 → 𝐾 ∈ (0...𝑁)) |
88 | | fzsplit 12367 |
. . . . . . . 8
⊢ (𝐾 ∈ (0...𝑁) → (0...𝑁) = ((0...𝐾) ∪ ((𝐾 + 1)...𝑁))) |
89 | 87, 88 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (0...𝑁) = ((0...𝐾) ∪ ((𝐾 + 1)...𝑁))) |
90 | | fzfid 12772 |
. . . . . . 7
⊢ (𝜑 → (0...𝑁) ∈ Fin) |
91 | | elfznn0 12433 |
. . . . . . . . 9
⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0) |
92 | 38, 91, 39 | syl2an 494 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝐴‘𝑘) ∈ ℂ) |
93 | 16, 91, 51 | syl2an 494 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝑇 · 𝑋)↑𝑘) ∈ ℂ) |
94 | 92, 93 | mulcld 10060 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) ∈ ℂ) |
95 | 61, 89, 90, 94 | fsumsplit 14471 |
. . . . . 6
⊢ (𝜑 → Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = (Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) + Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))) |
96 | 57, 95 | eqtrd 2656 |
. . . . 5
⊢ (𝜑 → (𝐹‘(𝑇 · 𝑋)) = (Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) + Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))) |
97 | 96 | fveq2d 6195 |
. . . 4
⊢ (𝜑 → (abs‘(𝐹‘(𝑇 · 𝑋))) = (abs‘(Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) + Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))))) |
98 | 1 | coefv0 24004 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∈ (Poly‘𝑆) → (𝐹‘0) = (𝐴‘0)) |
99 | 3, 98 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐹‘0) = (𝐴‘0)) |
100 | 99 | eqcomd 2628 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴‘0) = (𝐹‘0)) |
101 | 16 | exp0d 13002 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑇 · 𝑋)↑0) = 1) |
102 | 100, 101 | oveq12d 6668 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐴‘0) · ((𝑇 · 𝑋)↑0)) = ((𝐹‘0) · 1)) |
103 | 23 | mulid1d 10057 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐹‘0) · 1) = (𝐹‘0)) |
104 | 102, 103 | eqtrd 2656 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐴‘0) · ((𝑇 · 𝑋)↑0)) = (𝐹‘0)) |
105 | | 1e0p1 11552 |
. . . . . . . . . . . . 13
⊢ 1 = (0 +
1) |
106 | 105 | oveq1i 6660 |
. . . . . . . . . . . 12
⊢
(1...𝐾) = ((0 +
1)...𝐾) |
107 | 106 | sumeq1i 14428 |
. . . . . . . . . . 11
⊢
Σ𝑘 ∈
(1...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = Σ𝑘 ∈ ((0 + 1)...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) |
108 | 26, 63 | syl6eleq 2711 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐾 ∈
(ℤ≥‘1)) |
109 | | elfznn 12370 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ (1...𝐾) → 𝑘 ∈ ℕ) |
110 | 109 | nnnn0d 11351 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ (1...𝐾) → 𝑘 ∈ ℕ0) |
111 | 38, 110, 39 | syl2an 494 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐾)) → (𝐴‘𝑘) ∈ ℂ) |
112 | 16, 110, 51 | syl2an 494 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐾)) → ((𝑇 · 𝑋)↑𝑘) ∈ ℂ) |
113 | 111, 112 | mulcld 10060 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐾)) → ((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) ∈ ℂ) |
114 | | fveq2 6191 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝐾 → (𝐴‘𝑘) = (𝐴‘𝐾)) |
115 | | oveq2 6658 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝐾 → ((𝑇 · 𝑋)↑𝑘) = ((𝑇 · 𝑋)↑𝐾)) |
116 | 114, 115 | oveq12d 6668 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝐾 → ((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = ((𝐴‘𝐾) · ((𝑇 · 𝑋)↑𝐾))) |
117 | 108, 113,
116 | fsumm1 14480 |
. . . . . . . . . . 11
⊢ (𝜑 → Σ𝑘 ∈ (1...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = (Σ𝑘 ∈ (1...(𝐾 − 1))((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) + ((𝐴‘𝐾) · ((𝑇 · 𝑋)↑𝐾)))) |
118 | 107, 117 | syl5eqr 2670 |
. . . . . . . . . 10
⊢ (𝜑 → Σ𝑘 ∈ ((0 + 1)...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = (Σ𝑘 ∈ (1...(𝐾 − 1))((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) + ((𝐴‘𝐾) · ((𝑇 · 𝑋)↑𝐾)))) |
119 | | elfznn 12370 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 ∈ (1...(𝐾 − 1)) → 𝑘 ∈ ℕ) |
120 | 119 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → 𝑘 ∈ ℕ) |
121 | 120 | nnred 11035 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → 𝑘 ∈ ℝ) |
122 | 58 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → 𝐾 ∈ ℝ) |
123 | | peano2rem 10348 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐾 ∈ ℝ → (𝐾 − 1) ∈
ℝ) |
124 | 122, 123 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → (𝐾 − 1) ∈ ℝ) |
125 | | elfzle2 12345 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈ (1...(𝐾 − 1)) → 𝑘 ≤ (𝐾 − 1)) |
126 | 125 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → 𝑘 ≤ (𝐾 − 1)) |
127 | 122 | ltm1d 10956 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → (𝐾 − 1) < 𝐾) |
128 | 121, 124,
122, 126, 127 | lelttrd 10195 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → 𝑘 < 𝐾) |
129 | 121, 122 | ltnled 10184 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → (𝑘 < 𝐾 ↔ ¬ 𝐾 ≤ 𝑘)) |
130 | 128, 129 | mpbid 222 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → ¬ 𝐾 ≤ 𝑘) |
131 | | infssuzle 11771 |
. . . . . . . . . . . . . . . . . . 19
⊢ (({𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ⊆
(ℤ≥‘1) ∧ 𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0}) → inf({𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0}, ℝ, < ) ≤ 𝑘) |
132 | 6, 131 | syl5eqbr 4688 |
. . . . . . . . . . . . . . . . . 18
⊢ (({𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ⊆
(ℤ≥‘1) ∧ 𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0}) → 𝐾 ≤ 𝑘) |
133 | 64, 132 | mpan 706 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} → 𝐾 ≤ 𝑘) |
134 | 130, 133 | nsyl 135 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → ¬ 𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0}) |
135 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = 𝑘 → (𝐴‘𝑛) = (𝐴‘𝑘)) |
136 | 135 | neeq1d 2853 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 𝑘 → ((𝐴‘𝑛) ≠ 0 ↔ (𝐴‘𝑘) ≠ 0)) |
137 | 136 | elrab3 3364 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ ℕ → (𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ↔ (𝐴‘𝑘) ≠ 0)) |
138 | 120, 137 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → (𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ↔ (𝐴‘𝑘) ≠ 0)) |
139 | 138 | necon2bbid 2837 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → ((𝐴‘𝑘) = 0 ↔ ¬ 𝑘 ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0})) |
140 | 134, 139 | mpbird 247 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → (𝐴‘𝑘) = 0) |
141 | 140 | oveq1d 6665 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → ((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = (0 · ((𝑇 · 𝑋)↑𝑘))) |
142 | 119 | nnnn0d 11351 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ (1...(𝐾 − 1)) → 𝑘 ∈ ℕ0) |
143 | 16, 142, 51 | syl2an 494 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → ((𝑇 · 𝑋)↑𝑘) ∈ ℂ) |
144 | 143 | mul02d 10234 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → (0 · ((𝑇 · 𝑋)↑𝑘)) = 0) |
145 | 141, 144 | eqtrd 2656 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 − 1))) → ((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = 0) |
146 | 145 | sumeq2dv 14433 |
. . . . . . . . . . . 12
⊢ (𝜑 → Σ𝑘 ∈ (1...(𝐾 − 1))((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = Σ𝑘 ∈ (1...(𝐾 − 1))0) |
147 | | fzfi 12771 |
. . . . . . . . . . . . . 14
⊢
(1...(𝐾 − 1))
∈ Fin |
148 | 147 | olci 406 |
. . . . . . . . . . . . 13
⊢
((1...(𝐾 − 1))
⊆ (ℤ≥‘1) ∨ (1...(𝐾 − 1)) ∈ Fin) |
149 | | sumz 14453 |
. . . . . . . . . . . . 13
⊢
(((1...(𝐾 −
1)) ⊆ (ℤ≥‘1) ∨ (1...(𝐾 − 1)) ∈ Fin) → Σ𝑘 ∈ (1...(𝐾 − 1))0 = 0) |
150 | 148, 149 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
Σ𝑘 ∈
(1...(𝐾 − 1))0 =
0 |
151 | 146, 150 | syl6eq 2672 |
. . . . . . . . . . 11
⊢ (𝜑 → Σ𝑘 ∈ (1...(𝐾 − 1))((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = 0) |
152 | 12, 15, 27 | mulexpd 13023 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑇 · 𝑋)↑𝐾) = ((𝑇↑𝐾) · (𝑋↑𝐾))) |
153 | 152 | oveq2d 6666 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐴‘𝐾) · ((𝑇 · 𝑋)↑𝐾)) = ((𝐴‘𝐾) · ((𝑇↑𝐾) · (𝑋↑𝐾)))) |
154 | 38, 27 | ffvelrnd 6360 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐴‘𝐾) ∈ ℂ) |
155 | 12, 27 | expcld 13008 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑇↑𝐾) ∈ ℂ) |
156 | 28 | recnd 10068 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑋↑𝐾) ∈ ℂ) |
157 | 154, 155,
156 | mulassd 10063 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((𝐴‘𝐾) · (𝑇↑𝐾)) · (𝑋↑𝐾)) = ((𝐴‘𝐾) · ((𝑇↑𝐾) · (𝑋↑𝐾)))) |
158 | 153, 157 | eqtr4d 2659 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐴‘𝐾) · ((𝑇 · 𝑋)↑𝐾)) = (((𝐴‘𝐾) · (𝑇↑𝐾)) · (𝑋↑𝐾))) |
159 | 7 | oveq1i 6660 |
. . . . . . . . . . . . . . . 16
⊢ (𝑇↑𝐾) = ((-((𝐹‘0) / (𝐴‘𝐾))↑𝑐(1 / 𝐾))↑𝐾) |
160 | 58 | recnd 10068 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐾 ∈ ℂ) |
161 | 26 | nnne0d 11065 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐾 ≠ 0) |
162 | 160, 161 | recid2d 10797 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((1 / 𝐾) · 𝐾) = 1) |
163 | 162 | oveq2d 6666 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (-((𝐹‘0) / (𝐴‘𝐾))↑𝑐((1 / 𝐾) · 𝐾)) = (-((𝐹‘0) / (𝐴‘𝐾))↑𝑐1)) |
164 | 25 | simprd 479 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐴‘𝐾) ≠ 0) |
165 | 23, 154, 164 | divcld 10801 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝐹‘0) / (𝐴‘𝐾)) ∈ ℂ) |
166 | 165 | negcld 10379 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → -((𝐹‘0) / (𝐴‘𝐾)) ∈ ℂ) |
167 | 26 | nnrecred 11066 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (1 / 𝐾) ∈ ℝ) |
168 | 167 | recnd 10068 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (1 / 𝐾) ∈ ℂ) |
169 | 166, 168,
27 | cxpmul2d 24455 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (-((𝐹‘0) / (𝐴‘𝐾))↑𝑐((1 / 𝐾) · 𝐾)) = ((-((𝐹‘0) / (𝐴‘𝐾))↑𝑐(1 / 𝐾))↑𝐾)) |
170 | 166 | cxp1d 24452 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (-((𝐹‘0) / (𝐴‘𝐾))↑𝑐1) = -((𝐹‘0) / (𝐴‘𝐾))) |
171 | 163, 169,
170 | 3eqtr3d 2664 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((-((𝐹‘0) / (𝐴‘𝐾))↑𝑐(1 / 𝐾))↑𝐾) = -((𝐹‘0) / (𝐴‘𝐾))) |
172 | 159, 171 | syl5eq 2668 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑇↑𝐾) = -((𝐹‘0) / (𝐴‘𝐾))) |
173 | 172 | oveq2d 6666 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐴‘𝐾) · (𝑇↑𝐾)) = ((𝐴‘𝐾) · -((𝐹‘0) / (𝐴‘𝐾)))) |
174 | 154, 165 | mulneg2d 10484 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐴‘𝐾) · -((𝐹‘0) / (𝐴‘𝐾))) = -((𝐴‘𝐾) · ((𝐹‘0) / (𝐴‘𝐾)))) |
175 | 23, 154, 164 | divcan2d 10803 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝐴‘𝐾) · ((𝐹‘0) / (𝐴‘𝐾))) = (𝐹‘0)) |
176 | 175 | negeqd 10275 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → -((𝐴‘𝐾) · ((𝐹‘0) / (𝐴‘𝐾))) = -(𝐹‘0)) |
177 | 173, 174,
176 | 3eqtrd 2660 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐴‘𝐾) · (𝑇↑𝐾)) = -(𝐹‘0)) |
178 | 177 | oveq1d 6665 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝐴‘𝐾) · (𝑇↑𝐾)) · (𝑋↑𝐾)) = (-(𝐹‘0) · (𝑋↑𝐾))) |
179 | 23, 156 | mulneg1d 10483 |
. . . . . . . . . . . 12
⊢ (𝜑 → (-(𝐹‘0) · (𝑋↑𝐾)) = -((𝐹‘0) · (𝑋↑𝐾))) |
180 | 158, 178,
179 | 3eqtrd 2660 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐴‘𝐾) · ((𝑇 · 𝑋)↑𝐾)) = -((𝐹‘0) · (𝑋↑𝐾))) |
181 | 151, 180 | oveq12d 6668 |
. . . . . . . . . 10
⊢ (𝜑 → (Σ𝑘 ∈ (1...(𝐾 − 1))((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) + ((𝐴‘𝐾) · ((𝑇 · 𝑋)↑𝐾))) = (0 + -((𝐹‘0) · (𝑋↑𝐾)))) |
182 | 23, 156 | mulcld 10060 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐹‘0) · (𝑋↑𝐾)) ∈ ℂ) |
183 | 182 | negcld 10379 |
. . . . . . . . . . 11
⊢ (𝜑 → -((𝐹‘0) · (𝑋↑𝐾)) ∈ ℂ) |
184 | 183 | addid2d 10237 |
. . . . . . . . . 10
⊢ (𝜑 → (0 + -((𝐹‘0) · (𝑋↑𝐾))) = -((𝐹‘0) · (𝑋↑𝐾))) |
185 | 118, 181,
184 | 3eqtrd 2660 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑘 ∈ ((0 + 1)...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = -((𝐹‘0) · (𝑋↑𝐾))) |
186 | 104, 185 | oveq12d 6668 |
. . . . . . . 8
⊢ (𝜑 → (((𝐴‘0) · ((𝑇 · 𝑋)↑0)) + Σ𝑘 ∈ ((0 + 1)...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) = ((𝐹‘0) + -((𝐹‘0) · (𝑋↑𝐾)))) |
187 | | fveq2 6191 |
. . . . . . . . . 10
⊢ (𝑘 = 0 → (𝐴‘𝑘) = (𝐴‘0)) |
188 | | oveq2 6658 |
. . . . . . . . . 10
⊢ (𝑘 = 0 → ((𝑇 · 𝑋)↑𝑘) = ((𝑇 · 𝑋)↑0)) |
189 | 187, 188 | oveq12d 6668 |
. . . . . . . . 9
⊢ (𝑘 = 0 → ((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = ((𝐴‘0) · ((𝑇 · 𝑋)↑0))) |
190 | 83, 53, 189 | fsum1p 14482 |
. . . . . . . 8
⊢ (𝜑 → Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = (((𝐴‘0) · ((𝑇 · 𝑋)↑0)) + Σ𝑘 ∈ ((0 + 1)...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))) |
191 | 103 | oveq1d 6665 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐹‘0) · 1) − ((𝐹‘0) · (𝑋↑𝐾))) = ((𝐹‘0) − ((𝐹‘0) · (𝑋↑𝐾)))) |
192 | | 1cnd 10056 |
. . . . . . . . . 10
⊢ (𝜑 → 1 ∈
ℂ) |
193 | 23, 192, 156 | subdid 10486 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐹‘0) · (1 − (𝑋↑𝐾))) = (((𝐹‘0) · 1) − ((𝐹‘0) · (𝑋↑𝐾)))) |
194 | 23, 182 | negsubd 10398 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐹‘0) + -((𝐹‘0) · (𝑋↑𝐾))) = ((𝐹‘0) − ((𝐹‘0) · (𝑋↑𝐾)))) |
195 | 191, 193,
194 | 3eqtr4d 2666 |
. . . . . . . 8
⊢ (𝜑 → ((𝐹‘0) · (1 − (𝑋↑𝐾))) = ((𝐹‘0) + -((𝐹‘0) · (𝑋↑𝐾)))) |
196 | 186, 190,
195 | 3eqtr4d 2666 |
. . . . . . 7
⊢ (𝜑 → Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = ((𝐹‘0) · (1 − (𝑋↑𝐾)))) |
197 | 196 | fveq2d 6195 |
. . . . . 6
⊢ (𝜑 → (abs‘Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) = (abs‘((𝐹‘0) · (1 − (𝑋↑𝐾))))) |
198 | | 1re 10039 |
. . . . . . . . 9
⊢ 1 ∈
ℝ |
199 | | resubcl 10345 |
. . . . . . . . 9
⊢ ((1
∈ ℝ ∧ (𝑋↑𝐾) ∈ ℝ) → (1 − (𝑋↑𝐾)) ∈ ℝ) |
200 | 198, 28, 199 | sylancr 695 |
. . . . . . . 8
⊢ (𝜑 → (1 − (𝑋↑𝐾)) ∈ ℝ) |
201 | 200 | recnd 10068 |
. . . . . . 7
⊢ (𝜑 → (1 − (𝑋↑𝐾)) ∈ ℂ) |
202 | 23, 201 | absmuld 14193 |
. . . . . 6
⊢ (𝜑 → (abs‘((𝐹‘0) · (1 −
(𝑋↑𝐾)))) = ((abs‘(𝐹‘0)) · (abs‘(1 −
(𝑋↑𝐾))))) |
203 | 13 | rpge0d 11876 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ≤ 𝑋) |
204 | 11 | simp2d 1074 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑈 ∈
ℝ+) |
205 | 204 | rpred 11872 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑈 ∈ ℝ) |
206 | | min1 12020 |
. . . . . . . . . . . . 13
⊢ ((1
∈ ℝ ∧ 𝑈
∈ ℝ) → if(1 ≤ 𝑈, 1, 𝑈) ≤ 1) |
207 | 198, 205,
206 | sylancr 695 |
. . . . . . . . . . . 12
⊢ (𝜑 → if(1 ≤ 𝑈, 1, 𝑈) ≤ 1) |
208 | 9, 207 | syl5eqbr 4688 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ≤ 1) |
209 | | exple1 12920 |
. . . . . . . . . . 11
⊢ (((𝑋 ∈ ℝ ∧ 0 ≤
𝑋 ∧ 𝑋 ≤ 1) ∧ 𝐾 ∈ ℕ0) → (𝑋↑𝐾) ≤ 1) |
210 | 14, 203, 208, 27, 209 | syl31anc 1329 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑋↑𝐾) ≤ 1) |
211 | | subge0 10541 |
. . . . . . . . . . 11
⊢ ((1
∈ ℝ ∧ (𝑋↑𝐾) ∈ ℝ) → (0 ≤ (1 −
(𝑋↑𝐾)) ↔ (𝑋↑𝐾) ≤ 1)) |
212 | 198, 28, 211 | sylancr 695 |
. . . . . . . . . 10
⊢ (𝜑 → (0 ≤ (1 − (𝑋↑𝐾)) ↔ (𝑋↑𝐾) ≤ 1)) |
213 | 210, 212 | mpbird 247 |
. . . . . . . . 9
⊢ (𝜑 → 0 ≤ (1 − (𝑋↑𝐾))) |
214 | 200, 213 | absidd 14161 |
. . . . . . . 8
⊢ (𝜑 → (abs‘(1 −
(𝑋↑𝐾))) = (1 − (𝑋↑𝐾))) |
215 | 214 | oveq2d 6666 |
. . . . . . 7
⊢ (𝜑 → ((abs‘(𝐹‘0)) ·
(abs‘(1 − (𝑋↑𝐾)))) = ((abs‘(𝐹‘0)) · (1 − (𝑋↑𝐾)))) |
216 | 24 | recnd 10068 |
. . . . . . . 8
⊢ (𝜑 → (abs‘(𝐹‘0)) ∈
ℂ) |
217 | 216, 192,
156 | subdid 10486 |
. . . . . . 7
⊢ (𝜑 → ((abs‘(𝐹‘0)) · (1 −
(𝑋↑𝐾))) = (((abs‘(𝐹‘0)) · 1) −
((abs‘(𝐹‘0))
· (𝑋↑𝐾)))) |
218 | 216 | mulid1d 10057 |
. . . . . . . 8
⊢ (𝜑 → ((abs‘(𝐹‘0)) · 1) =
(abs‘(𝐹‘0))) |
219 | 218 | oveq1d 6665 |
. . . . . . 7
⊢ (𝜑 → (((abs‘(𝐹‘0)) · 1) −
((abs‘(𝐹‘0))
· (𝑋↑𝐾))) = ((abs‘(𝐹‘0)) −
((abs‘(𝐹‘0))
· (𝑋↑𝐾)))) |
220 | 215, 217,
219 | 3eqtrd 2660 |
. . . . . 6
⊢ (𝜑 → ((abs‘(𝐹‘0)) ·
(abs‘(1 − (𝑋↑𝐾)))) = ((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋↑𝐾)))) |
221 | 197, 202,
220 | 3eqtrrd 2661 |
. . . . 5
⊢ (𝜑 → ((abs‘(𝐹‘0)) −
((abs‘(𝐹‘0))
· (𝑋↑𝐾))) = (abs‘Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))) |
222 | 221 | oveq1d 6665 |
. . . 4
⊢ (𝜑 → (((abs‘(𝐹‘0)) −
((abs‘(𝐹‘0))
· (𝑋↑𝐾))) + (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))) = ((abs‘Σ𝑘 ∈ (0...𝐾)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) + (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))))) |
223 | 55, 97, 222 | 3brtr4d 4685 |
. . 3
⊢ (𝜑 → (abs‘(𝐹‘(𝑇 · 𝑋))) ≤ (((abs‘(𝐹‘0)) − ((abs‘(𝐹‘0)) · (𝑋↑𝐾))) + (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))))) |
224 | 44 | abscld 14175 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) ∈ ℝ) |
225 | 31, 224 | fsumrecl 14465 |
. . . . . 6
⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) ∈ ℝ) |
226 | 31, 44 | fsumabs 14533 |
. . . . . 6
⊢ (𝜑 → (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) ≤ Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))) |
227 | | expcl 12878 |
. . . . . . . . . . . . 13
⊢ ((𝑇 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (𝑇↑𝑘) ∈
ℂ) |
228 | 12, 227 | sylan 488 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑇↑𝑘) ∈ ℂ) |
229 | 36, 228 | syldan 487 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑇↑𝑘) ∈ ℂ) |
230 | 41, 229 | mulcld 10060 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((𝐴‘𝑘) · (𝑇↑𝑘)) ∈ ℂ) |
231 | 230 | abscld 14175 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) ∈ ℝ) |
232 | 31, 231 | fsumrecl 14465 |
. . . . . . . 8
⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) ∈ ℝ) |
233 | 14, 33 | reexpcld 13025 |
. . . . . . . 8
⊢ (𝜑 → (𝑋↑(𝐾 + 1)) ∈ ℝ) |
234 | 232, 233 | remulcld 10070 |
. . . . . . 7
⊢ (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1))) ∈ ℝ) |
235 | 233 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑋↑(𝐾 + 1)) ∈ ℝ) |
236 | 231, 235 | remulcld 10070 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1))) ∈ ℝ) |
237 | 12 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑇 ∈ ℂ) |
238 | 15 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑋 ∈ ℂ) |
239 | 237, 238,
36 | mulexpd 13023 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((𝑇 · 𝑋)↑𝑘) = ((𝑇↑𝑘) · (𝑋↑𝑘))) |
240 | 239 | oveq2d 6666 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = ((𝐴‘𝑘) · ((𝑇↑𝑘) · (𝑋↑𝑘)))) |
241 | 14 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑋 ∈ ℝ) |
242 | 241, 36 | reexpcld 13025 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑋↑𝑘) ∈ ℝ) |
243 | 242 | recnd 10068 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑋↑𝑘) ∈ ℂ) |
244 | 41, 229, 243 | mulassd 10063 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (((𝐴‘𝑘) · (𝑇↑𝑘)) · (𝑋↑𝑘)) = ((𝐴‘𝑘) · ((𝑇↑𝑘) · (𝑋↑𝑘)))) |
245 | 240, 244 | eqtr4d 2659 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)) = (((𝐴‘𝑘) · (𝑇↑𝑘)) · (𝑋↑𝑘))) |
246 | 245 | fveq2d 6195 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) = (abs‘(((𝐴‘𝑘) · (𝑇↑𝑘)) · (𝑋↑𝑘)))) |
247 | 230, 243 | absmuld 14193 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘(((𝐴‘𝑘) · (𝑇↑𝑘)) · (𝑋↑𝑘))) = ((abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (abs‘(𝑋↑𝑘)))) |
248 | | elfzelz 12342 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ((𝐾 + 1)...𝑁) → 𝑘 ∈ ℤ) |
249 | | rpexpcl 12879 |
. . . . . . . . . . . . . . 15
⊢ ((𝑋 ∈ ℝ+
∧ 𝑘 ∈ ℤ)
→ (𝑋↑𝑘) ∈
ℝ+) |
250 | 13, 248, 249 | syl2an 494 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑋↑𝑘) ∈
ℝ+) |
251 | 250 | rpge0d 11876 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 0 ≤ (𝑋↑𝑘)) |
252 | 242, 251 | absidd 14161 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘(𝑋↑𝑘)) = (𝑋↑𝑘)) |
253 | 252 | oveq2d 6666 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (abs‘(𝑋↑𝑘))) = ((abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑𝑘))) |
254 | 246, 247,
253 | 3eqtrd 2660 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) = ((abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑𝑘))) |
255 | 230 | absge0d 14183 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 0 ≤ (abs‘((𝐴‘𝑘) · (𝑇↑𝑘)))) |
256 | 33 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝐾 + 1) ∈
ℕ0) |
257 | 34 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑘 ∈ (ℤ≥‘(𝐾 + 1))) |
258 | 203 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 0 ≤ 𝑋) |
259 | 208 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑋 ≤ 1) |
260 | 241, 256,
257, 258, 259 | leexp2rd 13042 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑋↑𝑘) ≤ (𝑋↑(𝐾 + 1))) |
261 | 242, 235,
231, 255, 260 | lemul2ad 10964 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ((abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑𝑘)) ≤ ((abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1)))) |
262 | 254, 261 | eqbrtrd 4675 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) ≤ ((abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1)))) |
263 | 31, 224, 236, 262 | fsumle 14531 |
. . . . . . . 8
⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) ≤ Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1)))) |
264 | 233 | recnd 10068 |
. . . . . . . . 9
⊢ (𝜑 → (𝑋↑(𝐾 + 1)) ∈ ℂ) |
265 | 231 | recnd 10068 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) ∈ ℂ) |
266 | 31, 264, 265 | fsummulc1 14517 |
. . . . . . . 8
⊢ (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1))) = Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1)))) |
267 | 263, 266 | breqtrrd 4681 |
. . . . . . 7
⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) ≤ (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1)))) |
268 | 15, 27 | expp1d 13009 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑋↑(𝐾 + 1)) = ((𝑋↑𝐾) · 𝑋)) |
269 | 156, 15 | mulcomd 10061 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑋↑𝐾) · 𝑋) = (𝑋 · (𝑋↑𝐾))) |
270 | 268, 269 | eqtrd 2656 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑋↑(𝐾 + 1)) = (𝑋 · (𝑋↑𝐾))) |
271 | 270 | oveq2d 6666 |
. . . . . . . . 9
⊢ (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1))) = (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋 · (𝑋↑𝐾)))) |
272 | 232 | recnd 10068 |
. . . . . . . . . 10
⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) ∈ ℂ) |
273 | 272, 15, 156 | mulassd 10063 |
. . . . . . . . 9
⊢ (𝜑 → ((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · 𝑋) · (𝑋↑𝐾)) = (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋 · (𝑋↑𝐾)))) |
274 | 271, 273 | eqtr4d 2659 |
. . . . . . . 8
⊢ (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1))) = ((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · 𝑋) · (𝑋↑𝐾))) |
275 | 232, 14 | remulcld 10070 |
. . . . . . . . 9
⊢ (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · 𝑋) ∈ ℝ) |
276 | | nnssz 11397 |
. . . . . . . . . . . 12
⊢ ℕ
⊆ ℤ |
277 | 62, 276 | sstri 3612 |
. . . . . . . . . . 11
⊢ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ⊆ ℤ |
278 | | ne0i 3921 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} → {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ≠ ∅) |
279 | 78, 278 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ≠ ∅) |
280 | | infssuzcl 11772 |
. . . . . . . . . . . . 13
⊢ (({𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ⊆
(ℤ≥‘1) ∧ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0} ≠ ∅) → inf({𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0}, ℝ, < ) ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0}) |
281 | 64, 279, 280 | sylancr 695 |
. . . . . . . . . . . 12
⊢ (𝜑 → inf({𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0}, ℝ, < ) ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0}) |
282 | 6, 281 | syl5eqel 2705 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐾 ∈ {𝑛 ∈ ℕ ∣ (𝐴‘𝑛) ≠ 0}) |
283 | 277, 282 | sseldi 3601 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐾 ∈ ℤ) |
284 | 13, 283 | rpexpcld 13032 |
. . . . . . . . 9
⊢ (𝜑 → (𝑋↑𝐾) ∈
ℝ+) |
285 | | peano2re 10209 |
. . . . . . . . . . . 12
⊢
(Σ𝑘 ∈
((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) ∈ ℝ → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1) ∈ ℝ) |
286 | 232, 285 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1) ∈ ℝ) |
287 | 286, 14 | remulcld 10070 |
. . . . . . . . . 10
⊢ (𝜑 → ((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1) · 𝑋) ∈ ℝ) |
288 | 232 | ltp1d 10954 |
. . . . . . . . . . 11
⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) < (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1)) |
289 | 232, 286,
13, 288 | ltmul1dd 11927 |
. . . . . . . . . 10
⊢ (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · 𝑋) < ((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1) · 𝑋)) |
290 | | min2 12021 |
. . . . . . . . . . . . . 14
⊢ ((1
∈ ℝ ∧ 𝑈
∈ ℝ) → if(1 ≤ 𝑈, 1, 𝑈) ≤ 𝑈) |
291 | 198, 205,
290 | sylancr 695 |
. . . . . . . . . . . . 13
⊢ (𝜑 → if(1 ≤ 𝑈, 1, 𝑈) ≤ 𝑈) |
292 | 9, 291 | syl5eqbr 4688 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑋 ≤ 𝑈) |
293 | 292, 8 | syl6breq 4694 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ≤ ((abs‘(𝐹‘0)) / (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1))) |
294 | | 0red 10041 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 ∈
ℝ) |
295 | 31, 231, 255 | fsumge0 14527 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 ≤ Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘)))) |
296 | 294, 232,
286, 295, 288 | lelttrd 10195 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 < (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1)) |
297 | | lemuldiv2 10904 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∈ ℝ ∧
(abs‘(𝐹‘0))
∈ ℝ ∧ ((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1) ∈ ℝ ∧ 0 <
(Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1))) → (((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1) · 𝑋) ≤ (abs‘(𝐹‘0)) ↔ 𝑋 ≤ ((abs‘(𝐹‘0)) / (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1)))) |
298 | 14, 24, 286, 296, 297 | syl112anc 1330 |
. . . . . . . . . . 11
⊢ (𝜑 → (((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1) · 𝑋) ≤ (abs‘(𝐹‘0)) ↔ 𝑋 ≤ ((abs‘(𝐹‘0)) / (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1)))) |
299 | 293, 298 | mpbird 247 |
. . . . . . . . . 10
⊢ (𝜑 → ((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) + 1) · 𝑋) ≤ (abs‘(𝐹‘0))) |
300 | 275, 287,
24, 289, 299 | ltletrd 10197 |
. . . . . . . . 9
⊢ (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · 𝑋) < (abs‘(𝐹‘0))) |
301 | 275, 24, 284, 300 | ltmul1dd 11927 |
. . . . . . . 8
⊢ (𝜑 → ((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · 𝑋) · (𝑋↑𝐾)) < ((abs‘(𝐹‘0)) · (𝑋↑𝐾))) |
302 | 274, 301 | eqbrtrd 4675 |
. . . . . . 7
⊢ (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · (𝑇↑𝑘))) · (𝑋↑(𝐾 + 1))) < ((abs‘(𝐹‘0)) · (𝑋↑𝐾))) |
303 | 225, 234,
29, 267, 302 | lelttrd 10195 |
. . . . . 6
⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)(abs‘((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) < ((abs‘(𝐹‘0)) · (𝑋↑𝐾))) |
304 | 46, 225, 29, 226, 303 | lelttrd 10195 |
. . . . 5
⊢ (𝜑 → (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))) < ((abs‘(𝐹‘0)) · (𝑋↑𝐾))) |
305 | 46, 29, 24, 304 | ltsub2dd 10640 |
. . . 4
⊢ (𝜑 → ((abs‘(𝐹‘0)) −
((abs‘(𝐹‘0))
· (𝑋↑𝐾))) < ((abs‘(𝐹‘0)) −
(abs‘Σ𝑘 ∈
((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘))))) |
306 | 30, 46, 24 | ltaddsubd 10627 |
. . . 4
⊢ (𝜑 → ((((abs‘(𝐹‘0)) −
((abs‘(𝐹‘0))
· (𝑋↑𝐾))) + (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))) < (abs‘(𝐹‘0)) ↔ ((abs‘(𝐹‘0)) −
((abs‘(𝐹‘0))
· (𝑋↑𝐾))) < ((abs‘(𝐹‘0)) −
(abs‘Σ𝑘 ∈
((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))))) |
307 | 305, 306 | mpbird 247 |
. . 3
⊢ (𝜑 → (((abs‘(𝐹‘0)) −
((abs‘(𝐹‘0))
· (𝑋↑𝐾))) + (abs‘Σ𝑘 ∈ ((𝐾 + 1)...𝑁)((𝐴‘𝑘) · ((𝑇 · 𝑋)↑𝑘)))) < (abs‘(𝐹‘0))) |
308 | 20, 47, 24, 223, 307 | lelttrd 10195 |
. 2
⊢ (𝜑 → (abs‘(𝐹‘(𝑇 · 𝑋))) < (abs‘(𝐹‘0))) |
309 | | fveq2 6191 |
. . . . 5
⊢ (𝑥 = (𝑇 · 𝑋) → (𝐹‘𝑥) = (𝐹‘(𝑇 · 𝑋))) |
310 | 309 | fveq2d 6195 |
. . . 4
⊢ (𝑥 = (𝑇 · 𝑋) → (abs‘(𝐹‘𝑥)) = (abs‘(𝐹‘(𝑇 · 𝑋)))) |
311 | 310 | breq1d 4663 |
. . 3
⊢ (𝑥 = (𝑇 · 𝑋) → ((abs‘(𝐹‘𝑥)) < (abs‘(𝐹‘0)) ↔ (abs‘(𝐹‘(𝑇 · 𝑋))) < (abs‘(𝐹‘0)))) |
312 | 311 | rspcev 3309 |
. 2
⊢ (((𝑇 · 𝑋) ∈ ℂ ∧ (abs‘(𝐹‘(𝑇 · 𝑋))) < (abs‘(𝐹‘0))) → ∃𝑥 ∈ ℂ (abs‘(𝐹‘𝑥)) < (abs‘(𝐹‘0))) |
313 | 16, 308, 312 | syl2anc 693 |
1
⊢ (𝜑 → ∃𝑥 ∈ ℂ (abs‘(𝐹‘𝑥)) < (abs‘(𝐹‘0))) |