Step | Hyp | Ref
| Expression |
1 | | coeeq.1 |
. . 3
⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆)) |
2 | | coeval 23783 |
. . 3
⊢ (𝐹 ∈ (Poly‘𝑆) → (coeff‘𝐹) = (℩𝑎 ∈ (ℂ
↑𝑚 ℕ0)∃𝑛 ∈ ℕ0 ((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))))) |
3 | 1, 2 | syl 17 |
. 2
⊢ (𝜑 → (coeff‘𝐹) = (℩𝑎 ∈ (ℂ
↑𝑚 ℕ0)∃𝑛 ∈ ℕ0 ((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))))) |
4 | | coeeq.2 |
. . . 4
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
5 | | coeeq.4 |
. . . 4
⊢ (𝜑 → (𝐴 “
(ℤ≥‘(𝑁 + 1))) = {0}) |
6 | | coeeq.5 |
. . . 4
⊢ (𝜑 → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘)))) |
7 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑛 = 𝑁 → (𝑛 + 1) = (𝑁 + 1)) |
8 | 7 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑛 = 𝑁 → (ℤ≥‘(𝑛 + 1)) =
(ℤ≥‘(𝑁 + 1))) |
9 | 8 | imaeq2d 5385 |
. . . . . . 7
⊢ (𝑛 = 𝑁 → (𝐴 “
(ℤ≥‘(𝑛 + 1))) = (𝐴 “
(ℤ≥‘(𝑁 + 1)))) |
10 | 9 | eqeq1d 2612 |
. . . . . 6
⊢ (𝑛 = 𝑁 → ((𝐴 “
(ℤ≥‘(𝑛 + 1))) = {0} ↔ (𝐴 “
(ℤ≥‘(𝑁 + 1))) = {0})) |
11 | | oveq2 6557 |
. . . . . . . . 9
⊢ (𝑛 = 𝑁 → (0...𝑛) = (0...𝑁)) |
12 | 11 | sumeq1d 14279 |
. . . . . . . 8
⊢ (𝑛 = 𝑁 → Σ𝑘 ∈ (0...𝑛)((𝐴‘𝑘) · (𝑧↑𝑘)) = Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘))) |
13 | 12 | mpteq2dv 4673 |
. . . . . . 7
⊢ (𝑛 = 𝑁 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝐴‘𝑘) · (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘)))) |
14 | 13 | eqeq2d 2620 |
. . . . . 6
⊢ (𝑛 = 𝑁 → (𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝐴‘𝑘) · (𝑧↑𝑘))) ↔ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘))))) |
15 | 10, 14 | anbi12d 743 |
. . . . 5
⊢ (𝑛 = 𝑁 → (((𝐴 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝐴‘𝑘) · (𝑧↑𝑘)))) ↔ ((𝐴 “
(ℤ≥‘(𝑁 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘)))))) |
16 | 15 | rspcev 3282 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ ((𝐴 “
(ℤ≥‘(𝑁 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘))))) → ∃𝑛 ∈ ℕ0 ((𝐴 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝐴‘𝑘) · (𝑧↑𝑘))))) |
17 | 4, 5, 6, 16 | syl12anc 1316 |
. . 3
⊢ (𝜑 → ∃𝑛 ∈ ℕ0 ((𝐴 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝐴‘𝑘) · (𝑧↑𝑘))))) |
18 | | coeeq.3 |
. . . . 5
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) |
19 | | cnex 9896 |
. . . . . 6
⊢ ℂ
∈ V |
20 | | nn0ex 11175 |
. . . . . 6
⊢
ℕ0 ∈ V |
21 | 19, 20 | elmap 7772 |
. . . . 5
⊢ (𝐴 ∈ (ℂ
↑𝑚 ℕ0) ↔ 𝐴:ℕ0⟶ℂ) |
22 | 18, 21 | sylibr 223 |
. . . 4
⊢ (𝜑 → 𝐴 ∈ (ℂ ↑𝑚
ℕ0)) |
23 | | coeeu 23785 |
. . . . 5
⊢ (𝐹 ∈ (Poly‘𝑆) → ∃!𝑎 ∈ (ℂ
↑𝑚 ℕ0)∃𝑛 ∈ ℕ0 ((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) |
24 | 1, 23 | syl 17 |
. . . 4
⊢ (𝜑 → ∃!𝑎 ∈ (ℂ ↑𝑚
ℕ0)∃𝑛 ∈ ℕ0 ((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) |
25 | | imaeq1 5380 |
. . . . . . . 8
⊢ (𝑎 = 𝐴 → (𝑎 “ (ℤ≥‘(𝑛 + 1))) = (𝐴 “
(ℤ≥‘(𝑛 + 1)))) |
26 | 25 | eqeq1d 2612 |
. . . . . . 7
⊢ (𝑎 = 𝐴 → ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ↔ (𝐴 “
(ℤ≥‘(𝑛 + 1))) = {0})) |
27 | | fveq1 6102 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝐴 → (𝑎‘𝑘) = (𝐴‘𝑘)) |
28 | 27 | oveq1d 6564 |
. . . . . . . . . 10
⊢ (𝑎 = 𝐴 → ((𝑎‘𝑘) · (𝑧↑𝑘)) = ((𝐴‘𝑘) · (𝑧↑𝑘))) |
29 | 28 | sumeq2sdv 14282 |
. . . . . . . . 9
⊢ (𝑎 = 𝐴 → Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)) = Σ𝑘 ∈ (0...𝑛)((𝐴‘𝑘) · (𝑧↑𝑘))) |
30 | 29 | mpteq2dv 4673 |
. . . . . . . 8
⊢ (𝑎 = 𝐴 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝐴‘𝑘) · (𝑧↑𝑘)))) |
31 | 30 | eqeq2d 2620 |
. . . . . . 7
⊢ (𝑎 = 𝐴 → (𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))) ↔ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝐴‘𝑘) · (𝑧↑𝑘))))) |
32 | 26, 31 | anbi12d 743 |
. . . . . 6
⊢ (𝑎 = 𝐴 → (((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) ↔ ((𝐴 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝐴‘𝑘) · (𝑧↑𝑘)))))) |
33 | 32 | rexbidv 3034 |
. . . . 5
⊢ (𝑎 = 𝐴 → (∃𝑛 ∈ ℕ0 ((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) ↔ ∃𝑛 ∈ ℕ0 ((𝐴 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝐴‘𝑘) · (𝑧↑𝑘)))))) |
34 | 33 | riota2 6533 |
. . . 4
⊢ ((𝐴 ∈ (ℂ
↑𝑚 ℕ0) ∧ ∃!𝑎 ∈ (ℂ
↑𝑚 ℕ0)∃𝑛 ∈ ℕ0 ((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) → (∃𝑛 ∈ ℕ0 ((𝐴 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝐴‘𝑘) · (𝑧↑𝑘)))) ↔ (℩𝑎 ∈ (ℂ ↑𝑚
ℕ0)∃𝑛 ∈ ℕ0 ((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) = 𝐴)) |
35 | 22, 24, 34 | syl2anc 691 |
. . 3
⊢ (𝜑 → (∃𝑛 ∈ ℕ0 ((𝐴 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝐴‘𝑘) · (𝑧↑𝑘)))) ↔ (℩𝑎 ∈ (ℂ ↑𝑚
ℕ0)∃𝑛 ∈ ℕ0 ((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) = 𝐴)) |
36 | 17, 35 | mpbid 221 |
. 2
⊢ (𝜑 → (℩𝑎 ∈ (ℂ
↑𝑚 ℕ0)∃𝑛 ∈ ℕ0 ((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) = 𝐴) |
37 | 3, 36 | eqtrd 2644 |
1
⊢ (𝜑 → (coeff‘𝐹) = 𝐴) |