Step | Hyp | Ref
| Expression |
1 | | coeeq.1 |
. . 3
⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆)) |
2 | | coeval 24972 |
. . 3
⊢ (𝐹 ∈ (Poly‘𝑆) → (coeff‘𝐹) = (℩𝑎 ∈ (ℂ
↑m ℕ0)∃𝑛 ∈ ℕ0 ((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))))) |
3 | 1, 2 | syl 17 |
. 2
⊢ (𝜑 → (coeff‘𝐹) = (℩𝑎 ∈ (ℂ
↑m ℕ0)∃𝑛 ∈ ℕ0 ((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))))) |
4 | | coeeq.2 |
. . . 4
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
5 | | coeeq.4 |
. . . 4
⊢ (𝜑 → (𝐴 “
(ℤ≥‘(𝑁 + 1))) = {0}) |
6 | | coeeq.5 |
. . . 4
⊢ (𝜑 → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘)))) |
7 | | fvoveq1 7193 |
. . . . . . . 8
⊢ (𝑛 = 𝑁 → (ℤ≥‘(𝑛 + 1)) =
(ℤ≥‘(𝑁 + 1))) |
8 | 7 | imaeq2d 5903 |
. . . . . . 7
⊢ (𝑛 = 𝑁 → (𝐴 “
(ℤ≥‘(𝑛 + 1))) = (𝐴 “
(ℤ≥‘(𝑁 + 1)))) |
9 | 8 | eqeq1d 2740 |
. . . . . 6
⊢ (𝑛 = 𝑁 → ((𝐴 “
(ℤ≥‘(𝑛 + 1))) = {0} ↔ (𝐴 “
(ℤ≥‘(𝑁 + 1))) = {0})) |
10 | | oveq2 7178 |
. . . . . . . . 9
⊢ (𝑛 = 𝑁 → (0...𝑛) = (0...𝑁)) |
11 | 10 | sumeq1d 15151 |
. . . . . . . 8
⊢ (𝑛 = 𝑁 → Σ𝑘 ∈ (0...𝑛)((𝐴‘𝑘) · (𝑧↑𝑘)) = Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘))) |
12 | 11 | mpteq2dv 5126 |
. . . . . . 7
⊢ (𝑛 = 𝑁 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝐴‘𝑘) · (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘)))) |
13 | 12 | eqeq2d 2749 |
. . . . . 6
⊢ (𝑛 = 𝑁 → (𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝐴‘𝑘) · (𝑧↑𝑘))) ↔ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘))))) |
14 | 9, 13 | anbi12d 634 |
. . . . 5
⊢ (𝑛 = 𝑁 → (((𝐴 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝐴‘𝑘) · (𝑧↑𝑘)))) ↔ ((𝐴 “
(ℤ≥‘(𝑁 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘)))))) |
15 | 14 | rspcev 3526 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ ((𝐴 “
(ℤ≥‘(𝑁 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘))))) → ∃𝑛 ∈ ℕ0 ((𝐴 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝐴‘𝑘) · (𝑧↑𝑘))))) |
16 | 4, 5, 6, 15 | syl12anc 836 |
. . 3
⊢ (𝜑 → ∃𝑛 ∈ ℕ0 ((𝐴 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝐴‘𝑘) · (𝑧↑𝑘))))) |
17 | | coeeq.3 |
. . . . 5
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) |
18 | | cnex 10696 |
. . . . . 6
⊢ ℂ
∈ V |
19 | | nn0ex 11982 |
. . . . . 6
⊢
ℕ0 ∈ V |
20 | 18, 19 | elmap 8481 |
. . . . 5
⊢ (𝐴 ∈ (ℂ
↑m ℕ0) ↔ 𝐴:ℕ0⟶ℂ) |
21 | 17, 20 | sylibr 237 |
. . . 4
⊢ (𝜑 → 𝐴 ∈ (ℂ ↑m
ℕ0)) |
22 | | coeeu 24974 |
. . . . 5
⊢ (𝐹 ∈ (Poly‘𝑆) → ∃!𝑎 ∈ (ℂ
↑m ℕ0)∃𝑛 ∈ ℕ0 ((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) |
23 | 1, 22 | syl 17 |
. . . 4
⊢ (𝜑 → ∃!𝑎 ∈ (ℂ ↑m
ℕ0)∃𝑛 ∈ ℕ0 ((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) |
24 | | imaeq1 5898 |
. . . . . . . 8
⊢ (𝑎 = 𝐴 → (𝑎 “ (ℤ≥‘(𝑛 + 1))) = (𝐴 “
(ℤ≥‘(𝑛 + 1)))) |
25 | 24 | eqeq1d 2740 |
. . . . . . 7
⊢ (𝑎 = 𝐴 → ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ↔ (𝐴 “
(ℤ≥‘(𝑛 + 1))) = {0})) |
26 | | fveq1 6673 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝐴 → (𝑎‘𝑘) = (𝐴‘𝑘)) |
27 | 26 | oveq1d 7185 |
. . . . . . . . . 10
⊢ (𝑎 = 𝐴 → ((𝑎‘𝑘) · (𝑧↑𝑘)) = ((𝐴‘𝑘) · (𝑧↑𝑘))) |
28 | 27 | sumeq2sdv 15154 |
. . . . . . . . 9
⊢ (𝑎 = 𝐴 → Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)) = Σ𝑘 ∈ (0...𝑛)((𝐴‘𝑘) · (𝑧↑𝑘))) |
29 | 28 | mpteq2dv 5126 |
. . . . . . . 8
⊢ (𝑎 = 𝐴 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝐴‘𝑘) · (𝑧↑𝑘)))) |
30 | 29 | eqeq2d 2749 |
. . . . . . 7
⊢ (𝑎 = 𝐴 → (𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))) ↔ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝐴‘𝑘) · (𝑧↑𝑘))))) |
31 | 25, 30 | anbi12d 634 |
. . . . . 6
⊢ (𝑎 = 𝐴 → (((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) ↔ ((𝐴 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝐴‘𝑘) · (𝑧↑𝑘)))))) |
32 | 31 | rexbidv 3207 |
. . . . 5
⊢ (𝑎 = 𝐴 → (∃𝑛 ∈ ℕ0 ((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) ↔ ∃𝑛 ∈ ℕ0 ((𝐴 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝐴‘𝑘) · (𝑧↑𝑘)))))) |
33 | 32 | riota2 7153 |
. . . 4
⊢ ((𝐴 ∈ (ℂ
↑m ℕ0) ∧ ∃!𝑎 ∈ (ℂ ↑m
ℕ0)∃𝑛 ∈ ℕ0 ((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) → (∃𝑛 ∈ ℕ0 ((𝐴 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝐴‘𝑘) · (𝑧↑𝑘)))) ↔ (℩𝑎 ∈ (ℂ ↑m
ℕ0)∃𝑛 ∈ ℕ0 ((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) = 𝐴)) |
34 | 21, 23, 33 | syl2anc 587 |
. . 3
⊢ (𝜑 → (∃𝑛 ∈ ℕ0 ((𝐴 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝐴‘𝑘) · (𝑧↑𝑘)))) ↔ (℩𝑎 ∈ (ℂ ↑m
ℕ0)∃𝑛 ∈ ℕ0 ((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) = 𝐴)) |
35 | 16, 34 | mpbid 235 |
. 2
⊢ (𝜑 → (℩𝑎 ∈ (ℂ
↑m ℕ0)∃𝑛 ∈ ℕ0 ((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) = 𝐴) |
36 | 3, 35 | eqtrd 2773 |
1
⊢ (𝜑 → (coeff‘𝐹) = 𝐴) |