Step | Hyp | Ref
| Expression |
1 | | dgrle.1 |
. 2
⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆)) |
2 | | dgrle.2 |
. 2
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
3 | | simpll 786 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑘 ≤ 𝑁) → 𝜑) |
4 | | simpr 476 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑘 ≤ 𝑁) → 𝑘 ≤ 𝑁) |
5 | | simplr 788 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑘 ≤ 𝑁) → 𝑘 ∈ ℕ0) |
6 | | nn0uz 11598 |
. . . . . . . 8
⊢
ℕ0 = (ℤ≥‘0) |
7 | 5, 6 | syl6eleq 2698 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑘 ≤ 𝑁) → 𝑘 ∈
(ℤ≥‘0)) |
8 | 2 | nn0zd 11356 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ ℤ) |
9 | 8 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑘 ≤ 𝑁) → 𝑁 ∈ ℤ) |
10 | | elfz5 12205 |
. . . . . . 7
⊢ ((𝑘 ∈
(ℤ≥‘0) ∧ 𝑁 ∈ ℤ) → (𝑘 ∈ (0...𝑁) ↔ 𝑘 ≤ 𝑁)) |
11 | 7, 9, 10 | syl2anc 691 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑘 ≤ 𝑁) → (𝑘 ∈ (0...𝑁) ↔ 𝑘 ≤ 𝑁)) |
12 | 4, 11 | mpbird 246 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑘 ≤ 𝑁) → 𝑘 ∈ (0...𝑁)) |
13 | | dgrle.3 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝐴 ∈ ℂ) |
14 | 3, 12, 13 | syl2anc 691 |
. . . 4
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑘 ≤ 𝑁) → 𝐴 ∈ ℂ) |
15 | | 0cnd 9912 |
. . . 4
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
𝑘 ≤ 𝑁) → 0 ∈ ℂ) |
16 | 14, 15 | ifclda 4070 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → if(𝑘 ≤ 𝑁, 𝐴, 0) ∈ ℂ) |
17 | | eqid 2610 |
. . 3
⊢ (𝑘 ∈ ℕ0
↦ if(𝑘 ≤ 𝑁, 𝐴, 0)) = (𝑘 ∈ ℕ0 ↦ if(𝑘 ≤ 𝑁, 𝐴, 0)) |
18 | 16, 17 | fmptd 6292 |
. 2
⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦ if(𝑘 ≤ 𝑁, 𝐴,
0)):ℕ0⟶ℂ) |
19 | | simpr 476 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
ℕ0) |
20 | 17 | fvmpt2 6200 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℕ0
∧ if(𝑘 ≤ 𝑁, 𝐴, 0) ∈ ℂ) → ((𝑘 ∈ ℕ0
↦ if(𝑘 ≤ 𝑁, 𝐴, 0))‘𝑘) = if(𝑘 ≤ 𝑁, 𝐴, 0)) |
21 | 19, 16, 20 | syl2anc 691 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑘 ∈ ℕ0
↦ if(𝑘 ≤ 𝑁, 𝐴, 0))‘𝑘) = if(𝑘 ≤ 𝑁, 𝐴, 0)) |
22 | 21 | neeq1d 2841 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝑘 ∈ ℕ0
↦ if(𝑘 ≤ 𝑁, 𝐴, 0))‘𝑘) ≠ 0 ↔ if(𝑘 ≤ 𝑁, 𝐴, 0) ≠ 0)) |
23 | | iffalse 4045 |
. . . . . . 7
⊢ (¬
𝑘 ≤ 𝑁 → if(𝑘 ≤ 𝑁, 𝐴, 0) = 0) |
24 | 23 | necon1ai 2809 |
. . . . . 6
⊢ (if(𝑘 ≤ 𝑁, 𝐴, 0) ≠ 0 → 𝑘 ≤ 𝑁) |
25 | 22, 24 | syl6bi 242 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝑘 ∈ ℕ0
↦ if(𝑘 ≤ 𝑁, 𝐴, 0))‘𝑘) ≠ 0 → 𝑘 ≤ 𝑁)) |
26 | 25 | ralrimiva 2949 |
. . . 4
⊢ (𝜑 → ∀𝑘 ∈ ℕ0 (((𝑘 ∈ ℕ0
↦ if(𝑘 ≤ 𝑁, 𝐴, 0))‘𝑘) ≠ 0 → 𝑘 ≤ 𝑁)) |
27 | | nfv 1830 |
. . . . 5
⊢
Ⅎ𝑚(((𝑘 ∈ ℕ0
↦ if(𝑘 ≤ 𝑁, 𝐴, 0))‘𝑘) ≠ 0 → 𝑘 ≤ 𝑁) |
28 | | nffvmpt1 6111 |
. . . . . . 7
⊢
Ⅎ𝑘((𝑘 ∈ ℕ0 ↦ if(𝑘 ≤ 𝑁, 𝐴, 0))‘𝑚) |
29 | | nfcv 2751 |
. . . . . . 7
⊢
Ⅎ𝑘0 |
30 | 28, 29 | nfne 2882 |
. . . . . 6
⊢
Ⅎ𝑘((𝑘 ∈ ℕ0
↦ if(𝑘 ≤ 𝑁, 𝐴, 0))‘𝑚) ≠ 0 |
31 | | nfv 1830 |
. . . . . 6
⊢
Ⅎ𝑘 𝑚 ≤ 𝑁 |
32 | 30, 31 | nfim 1813 |
. . . . 5
⊢
Ⅎ𝑘(((𝑘 ∈ ℕ0
↦ if(𝑘 ≤ 𝑁, 𝐴, 0))‘𝑚) ≠ 0 → 𝑚 ≤ 𝑁) |
33 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑘 = 𝑚 → ((𝑘 ∈ ℕ0 ↦ if(𝑘 ≤ 𝑁, 𝐴, 0))‘𝑘) = ((𝑘 ∈ ℕ0 ↦ if(𝑘 ≤ 𝑁, 𝐴, 0))‘𝑚)) |
34 | 33 | neeq1d 2841 |
. . . . . 6
⊢ (𝑘 = 𝑚 → (((𝑘 ∈ ℕ0 ↦ if(𝑘 ≤ 𝑁, 𝐴, 0))‘𝑘) ≠ 0 ↔ ((𝑘 ∈ ℕ0 ↦ if(𝑘 ≤ 𝑁, 𝐴, 0))‘𝑚) ≠ 0)) |
35 | | breq1 4586 |
. . . . . 6
⊢ (𝑘 = 𝑚 → (𝑘 ≤ 𝑁 ↔ 𝑚 ≤ 𝑁)) |
36 | 34, 35 | imbi12d 333 |
. . . . 5
⊢ (𝑘 = 𝑚 → ((((𝑘 ∈ ℕ0 ↦ if(𝑘 ≤ 𝑁, 𝐴, 0))‘𝑘) ≠ 0 → 𝑘 ≤ 𝑁) ↔ (((𝑘 ∈ ℕ0 ↦ if(𝑘 ≤ 𝑁, 𝐴, 0))‘𝑚) ≠ 0 → 𝑚 ≤ 𝑁))) |
37 | 27, 32, 36 | cbvral 3143 |
. . . 4
⊢
(∀𝑘 ∈
ℕ0 (((𝑘
∈ ℕ0 ↦ if(𝑘 ≤ 𝑁, 𝐴, 0))‘𝑘) ≠ 0 → 𝑘 ≤ 𝑁) ↔ ∀𝑚 ∈ ℕ0 (((𝑘 ∈ ℕ0
↦ if(𝑘 ≤ 𝑁, 𝐴, 0))‘𝑚) ≠ 0 → 𝑚 ≤ 𝑁)) |
38 | 26, 37 | sylib 207 |
. . 3
⊢ (𝜑 → ∀𝑚 ∈ ℕ0 (((𝑘 ∈ ℕ0
↦ if(𝑘 ≤ 𝑁, 𝐴, 0))‘𝑚) ≠ 0 → 𝑚 ≤ 𝑁)) |
39 | | plyco0 23752 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ (𝑘 ∈
ℕ0 ↦ if(𝑘 ≤ 𝑁, 𝐴, 0)):ℕ0⟶ℂ)
→ (((𝑘 ∈
ℕ0 ↦ if(𝑘 ≤ 𝑁, 𝐴, 0)) “
(ℤ≥‘(𝑁 + 1))) = {0} ↔ ∀𝑚 ∈ ℕ0
(((𝑘 ∈
ℕ0 ↦ if(𝑘 ≤ 𝑁, 𝐴, 0))‘𝑚) ≠ 0 → 𝑚 ≤ 𝑁))) |
40 | 2, 18, 39 | syl2anc 691 |
. . 3
⊢ (𝜑 → (((𝑘 ∈ ℕ0 ↦ if(𝑘 ≤ 𝑁, 𝐴, 0)) “
(ℤ≥‘(𝑁 + 1))) = {0} ↔ ∀𝑚 ∈ ℕ0
(((𝑘 ∈
ℕ0 ↦ if(𝑘 ≤ 𝑁, 𝐴, 0))‘𝑚) ≠ 0 → 𝑚 ≤ 𝑁))) |
41 | 38, 40 | mpbird 246 |
. 2
⊢ (𝜑 → ((𝑘 ∈ ℕ0 ↦ if(𝑘 ≤ 𝑁, 𝐴, 0)) “
(ℤ≥‘(𝑁 + 1))) = {0}) |
42 | | dgrle.4 |
. . 3
⊢ (𝜑 → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(𝐴 · (𝑧↑𝑘)))) |
43 | | nfcv 2751 |
. . . . . 6
⊢
Ⅎ𝑚(((𝑘 ∈ ℕ0 ↦ if(𝑘 ≤ 𝑁, 𝐴, 0))‘𝑘) · (𝑧↑𝑘)) |
44 | | nfcv 2751 |
. . . . . . 7
⊢
Ⅎ𝑘
· |
45 | | nfcv 2751 |
. . . . . . 7
⊢
Ⅎ𝑘(𝑧↑𝑚) |
46 | 28, 44, 45 | nfov 6575 |
. . . . . 6
⊢
Ⅎ𝑘(((𝑘 ∈ ℕ0 ↦ if(𝑘 ≤ 𝑁, 𝐴, 0))‘𝑚) · (𝑧↑𝑚)) |
47 | | oveq2 6557 |
. . . . . . 7
⊢ (𝑘 = 𝑚 → (𝑧↑𝑘) = (𝑧↑𝑚)) |
48 | 33, 47 | oveq12d 6567 |
. . . . . 6
⊢ (𝑘 = 𝑚 → (((𝑘 ∈ ℕ0 ↦ if(𝑘 ≤ 𝑁, 𝐴, 0))‘𝑘) · (𝑧↑𝑘)) = (((𝑘 ∈ ℕ0 ↦ if(𝑘 ≤ 𝑁, 𝐴, 0))‘𝑚) · (𝑧↑𝑚))) |
49 | 43, 46, 48 | cbvsumi 14275 |
. . . . 5
⊢
Σ𝑘 ∈
(0...𝑁)(((𝑘 ∈ ℕ0
↦ if(𝑘 ≤ 𝑁, 𝐴, 0))‘𝑘) · (𝑧↑𝑘)) = Σ𝑚 ∈ (0...𝑁)(((𝑘 ∈ ℕ0 ↦ if(𝑘 ≤ 𝑁, 𝐴, 0))‘𝑚) · (𝑧↑𝑚)) |
50 | | elfznn0 12302 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0) |
51 | 50 | adantl 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0) |
52 | | elfzle2 12216 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ≤ 𝑁) |
53 | 52 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ≤ 𝑁) |
54 | 53 | iftrued 4044 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑁)) → if(𝑘 ≤ 𝑁, 𝐴, 0) = 𝐴) |
55 | 13 | adantlr 747 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑁)) → 𝐴 ∈ ℂ) |
56 | 54, 55 | eqeltrd 2688 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑁)) → if(𝑘 ≤ 𝑁, 𝐴, 0) ∈ ℂ) |
57 | 51, 56, 20 | syl2anc 691 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑘 ∈ ℕ0 ↦ if(𝑘 ≤ 𝑁, 𝐴, 0))‘𝑘) = if(𝑘 ≤ 𝑁, 𝐴, 0)) |
58 | 57, 54 | eqtrd 2644 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑘 ∈ ℕ0 ↦ if(𝑘 ≤ 𝑁, 𝐴, 0))‘𝑘) = 𝐴) |
59 | 58 | oveq1d 6564 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑁)) → (((𝑘 ∈ ℕ0 ↦ if(𝑘 ≤ 𝑁, 𝐴, 0))‘𝑘) · (𝑧↑𝑘)) = (𝐴 · (𝑧↑𝑘))) |
60 | 59 | sumeq2dv 14281 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑘 ∈ (0...𝑁)(((𝑘 ∈ ℕ0 ↦ if(𝑘 ≤ 𝑁, 𝐴, 0))‘𝑘) · (𝑧↑𝑘)) = Σ𝑘 ∈ (0...𝑁)(𝐴 · (𝑧↑𝑘))) |
61 | 49, 60 | syl5eqr 2658 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑚 ∈ (0...𝑁)(((𝑘 ∈ ℕ0 ↦ if(𝑘 ≤ 𝑁, 𝐴, 0))‘𝑚) · (𝑧↑𝑚)) = Σ𝑘 ∈ (0...𝑁)(𝐴 · (𝑧↑𝑘))) |
62 | 61 | mpteq2dva 4672 |
. . 3
⊢ (𝜑 → (𝑧 ∈ ℂ ↦ Σ𝑚 ∈ (0...𝑁)(((𝑘 ∈ ℕ0 ↦ if(𝑘 ≤ 𝑁, 𝐴, 0))‘𝑚) · (𝑧↑𝑚))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(𝐴 · (𝑧↑𝑘)))) |
63 | 42, 62 | eqtr4d 2647 |
. 2
⊢ (𝜑 → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑚 ∈ (0...𝑁)(((𝑘 ∈ ℕ0 ↦ if(𝑘 ≤ 𝑁, 𝐴, 0))‘𝑚) · (𝑧↑𝑚)))) |
64 | 1, 2, 18, 41, 63 | coeeq 23787 |
1
⊢ (𝜑 → (coeff‘𝐹) = (𝑘 ∈ ℕ0 ↦ if(𝑘 ≤ 𝑁, 𝐴, 0))) |