| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | elply 26235 | . . 3
⊢ (𝐹 ∈ (Poly‘𝑆) ↔ (𝑆 ⊆ ℂ ∧ ∃𝑛 ∈ ℕ0
∃𝑓 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0)𝐹 =
(𝑧 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑛)((𝑓‘𝑘) · (𝑧↑𝑘))))) | 
| 2 |  | simpr 484 | . . . . . . . . . . . . 13
⊢ (((𝑆 ⊆ ℂ ∧ 𝑛 ∈ ℕ0)
∧ 𝑓 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0)) → 𝑓 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0)) | 
| 3 |  | simpll 766 | . . . . . . . . . . . . . . . 16
⊢ (((𝑆 ⊆ ℂ ∧ 𝑛 ∈ ℕ0)
∧ 𝑓 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0)) → 𝑆 ⊆ ℂ) | 
| 4 |  | cnex 11237 | . . . . . . . . . . . . . . . 16
⊢ ℂ
∈ V | 
| 5 |  | ssexg 5322 | . . . . . . . . . . . . . . . 16
⊢ ((𝑆 ⊆ ℂ ∧ ℂ
∈ V) → 𝑆 ∈
V) | 
| 6 | 3, 4, 5 | sylancl 586 | . . . . . . . . . . . . . . 15
⊢ (((𝑆 ⊆ ℂ ∧ 𝑛 ∈ ℕ0)
∧ 𝑓 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0)) → 𝑆 ∈ V) | 
| 7 |  | snex 5435 | . . . . . . . . . . . . . . 15
⊢ {0}
∈ V | 
| 8 |  | unexg 7764 | . . . . . . . . . . . . . . 15
⊢ ((𝑆 ∈ V ∧ {0} ∈ V)
→ (𝑆 ∪ {0}) ∈
V) | 
| 9 | 6, 7, 8 | sylancl 586 | . . . . . . . . . . . . . 14
⊢ (((𝑆 ⊆ ℂ ∧ 𝑛 ∈ ℕ0)
∧ 𝑓 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0)) → (𝑆 ∪ {0}) ∈ V) | 
| 10 |  | nn0ex 12534 | . . . . . . . . . . . . . 14
⊢
ℕ0 ∈ V | 
| 11 |  | elmapg 8880 | . . . . . . . . . . . . . 14
⊢ (((𝑆 ∪ {0}) ∈ V ∧
ℕ0 ∈ V) → (𝑓 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0) ↔ 𝑓:ℕ0⟶(𝑆 ∪ {0}))) | 
| 12 | 9, 10, 11 | sylancl 586 | . . . . . . . . . . . . 13
⊢ (((𝑆 ⊆ ℂ ∧ 𝑛 ∈ ℕ0)
∧ 𝑓 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0)) → (𝑓 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0) ↔ 𝑓:ℕ0⟶(𝑆 ∪ {0}))) | 
| 13 | 2, 12 | mpbid 232 | . . . . . . . . . . . 12
⊢ (((𝑆 ⊆ ℂ ∧ 𝑛 ∈ ℕ0)
∧ 𝑓 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0)) → 𝑓:ℕ0⟶(𝑆 ∪ {0})) | 
| 14 | 13 | ffvelcdmda 7103 | . . . . . . . . . . 11
⊢ ((((𝑆 ⊆ ℂ ∧ 𝑛 ∈ ℕ0)
∧ 𝑓 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0)) ∧ 𝑥 ∈ ℕ0) → (𝑓‘𝑥) ∈ (𝑆 ∪ {0})) | 
| 15 |  | ssun2 4178 | . . . . . . . . . . . 12
⊢ {0}
⊆ (𝑆 ∪
{0}) | 
| 16 |  | c0ex 11256 | . . . . . . . . . . . . 13
⊢ 0 ∈
V | 
| 17 | 16 | snss 4784 | . . . . . . . . . . . 12
⊢ (0 ∈
(𝑆 ∪ {0}) ↔ {0}
⊆ (𝑆 ∪
{0})) | 
| 18 | 15, 17 | mpbir 231 | . . . . . . . . . . 11
⊢ 0 ∈
(𝑆 ∪
{0}) | 
| 19 |  | ifcl 4570 | . . . . . . . . . . 11
⊢ (((𝑓‘𝑥) ∈ (𝑆 ∪ {0}) ∧ 0 ∈ (𝑆 ∪ {0})) → if(𝑥 ∈ (0...𝑛), (𝑓‘𝑥), 0) ∈ (𝑆 ∪ {0})) | 
| 20 | 14, 18, 19 | sylancl 586 | . . . . . . . . . 10
⊢ ((((𝑆 ⊆ ℂ ∧ 𝑛 ∈ ℕ0)
∧ 𝑓 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0)) ∧ 𝑥 ∈ ℕ0) → if(𝑥 ∈ (0...𝑛), (𝑓‘𝑥), 0) ∈ (𝑆 ∪ {0})) | 
| 21 | 20 | fmpttd 7134 | . . . . . . . . 9
⊢ (((𝑆 ⊆ ℂ ∧ 𝑛 ∈ ℕ0)
∧ 𝑓 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0)) → (𝑥 ∈ ℕ0 ↦ if(𝑥 ∈ (0...𝑛), (𝑓‘𝑥), 0)):ℕ0⟶(𝑆 ∪ {0})) | 
| 22 |  | elmapg 8880 | . . . . . . . . . 10
⊢ (((𝑆 ∪ {0}) ∈ V ∧
ℕ0 ∈ V) → ((𝑥 ∈ ℕ0 ↦ if(𝑥 ∈ (0...𝑛), (𝑓‘𝑥), 0)) ∈ ((𝑆 ∪ {0}) ↑m
ℕ0) ↔ (𝑥 ∈ ℕ0 ↦ if(𝑥 ∈ (0...𝑛), (𝑓‘𝑥), 0)):ℕ0⟶(𝑆 ∪ {0}))) | 
| 23 | 9, 10, 22 | sylancl 586 | . . . . . . . . 9
⊢ (((𝑆 ⊆ ℂ ∧ 𝑛 ∈ ℕ0)
∧ 𝑓 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0)) → ((𝑥 ∈ ℕ0 ↦ if(𝑥 ∈ (0...𝑛), (𝑓‘𝑥), 0)) ∈ ((𝑆 ∪ {0}) ↑m
ℕ0) ↔ (𝑥 ∈ ℕ0 ↦ if(𝑥 ∈ (0...𝑛), (𝑓‘𝑥), 0)):ℕ0⟶(𝑆 ∪ {0}))) | 
| 24 | 21, 23 | mpbird 257 | . . . . . . . 8
⊢ (((𝑆 ⊆ ℂ ∧ 𝑛 ∈ ℕ0)
∧ 𝑓 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0)) → (𝑥 ∈ ℕ0 ↦ if(𝑥 ∈ (0...𝑛), (𝑓‘𝑥), 0)) ∈ ((𝑆 ∪ {0}) ↑m
ℕ0)) | 
| 25 |  | eleq1w 2823 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑘 → (𝑥 ∈ (0...𝑛) ↔ 𝑘 ∈ (0...𝑛))) | 
| 26 |  | fveq2 6905 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑘 → (𝑓‘𝑥) = (𝑓‘𝑘)) | 
| 27 | 25, 26 | ifbieq1d 4549 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑘 → if(𝑥 ∈ (0...𝑛), (𝑓‘𝑥), 0) = if(𝑘 ∈ (0...𝑛), (𝑓‘𝑘), 0)) | 
| 28 |  | eqid 2736 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℕ0
↦ if(𝑥 ∈
(0...𝑛), (𝑓‘𝑥), 0)) = (𝑥 ∈ ℕ0 ↦ if(𝑥 ∈ (0...𝑛), (𝑓‘𝑥), 0)) | 
| 29 |  | fvex 6918 | . . . . . . . . . . . . . . . . 17
⊢ (𝑓‘𝑘) ∈ V | 
| 30 | 29, 16 | ifex 4575 | . . . . . . . . . . . . . . . 16
⊢ if(𝑘 ∈ (0...𝑛), (𝑓‘𝑘), 0) ∈ V | 
| 31 | 27, 28, 30 | fvmpt 7015 | . . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℕ0
→ ((𝑥 ∈
ℕ0 ↦ if(𝑥 ∈ (0...𝑛), (𝑓‘𝑥), 0))‘𝑘) = if(𝑘 ∈ (0...𝑛), (𝑓‘𝑘), 0)) | 
| 32 | 31 | ad2antll 729 | . . . . . . . . . . . . . 14
⊢ (((𝑆 ⊆ ℂ ∧ 𝑛 ∈ ℕ0)
∧ (𝑓 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0) ∧ 𝑘 ∈ ℕ0)) → ((𝑥 ∈ ℕ0
↦ if(𝑥 ∈
(0...𝑛), (𝑓‘𝑥), 0))‘𝑘) = if(𝑘 ∈ (0...𝑛), (𝑓‘𝑘), 0)) | 
| 33 |  | iffalse 4533 | . . . . . . . . . . . . . . 15
⊢ (¬
𝑘 ∈ (0...𝑛) → if(𝑘 ∈ (0...𝑛), (𝑓‘𝑘), 0) = 0) | 
| 34 | 33 | eqeq2d 2747 | . . . . . . . . . . . . . 14
⊢ (¬
𝑘 ∈ (0...𝑛) → (((𝑥 ∈ ℕ0 ↦ if(𝑥 ∈ (0...𝑛), (𝑓‘𝑥), 0))‘𝑘) = if(𝑘 ∈ (0...𝑛), (𝑓‘𝑘), 0) ↔ ((𝑥 ∈ ℕ0 ↦ if(𝑥 ∈ (0...𝑛), (𝑓‘𝑥), 0))‘𝑘) = 0)) | 
| 35 | 32, 34 | syl5ibcom 245 | . . . . . . . . . . . . 13
⊢ (((𝑆 ⊆ ℂ ∧ 𝑛 ∈ ℕ0)
∧ (𝑓 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0) ∧ 𝑘 ∈ ℕ0)) → (¬
𝑘 ∈ (0...𝑛) → ((𝑥 ∈ ℕ0 ↦ if(𝑥 ∈ (0...𝑛), (𝑓‘𝑥), 0))‘𝑘) = 0)) | 
| 36 | 35 | necon1ad 2956 | . . . . . . . . . . . 12
⊢ (((𝑆 ⊆ ℂ ∧ 𝑛 ∈ ℕ0)
∧ (𝑓 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0) ∧ 𝑘 ∈ ℕ0)) → (((𝑥 ∈ ℕ0
↦ if(𝑥 ∈
(0...𝑛), (𝑓‘𝑥), 0))‘𝑘) ≠ 0 → 𝑘 ∈ (0...𝑛))) | 
| 37 |  | elfzle2 13569 | . . . . . . . . . . . 12
⊢ (𝑘 ∈ (0...𝑛) → 𝑘 ≤ 𝑛) | 
| 38 | 36, 37 | syl6 35 | . . . . . . . . . . 11
⊢ (((𝑆 ⊆ ℂ ∧ 𝑛 ∈ ℕ0)
∧ (𝑓 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0) ∧ 𝑘 ∈ ℕ0)) → (((𝑥 ∈ ℕ0
↦ if(𝑥 ∈
(0...𝑛), (𝑓‘𝑥), 0))‘𝑘) ≠ 0 → 𝑘 ≤ 𝑛)) | 
| 39 | 38 | anassrs 467 | . . . . . . . . . 10
⊢ ((((𝑆 ⊆ ℂ ∧ 𝑛 ∈ ℕ0)
∧ 𝑓 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0)) ∧ 𝑘 ∈ ℕ0) → (((𝑥 ∈ ℕ0
↦ if(𝑥 ∈
(0...𝑛), (𝑓‘𝑥), 0))‘𝑘) ≠ 0 → 𝑘 ≤ 𝑛)) | 
| 40 | 39 | ralrimiva 3145 | . . . . . . . . 9
⊢ (((𝑆 ⊆ ℂ ∧ 𝑛 ∈ ℕ0)
∧ 𝑓 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0)) → ∀𝑘 ∈ ℕ0 (((𝑥 ∈ ℕ0
↦ if(𝑥 ∈
(0...𝑛), (𝑓‘𝑥), 0))‘𝑘) ≠ 0 → 𝑘 ≤ 𝑛)) | 
| 41 |  | simplr 768 | . . . . . . . . . 10
⊢ (((𝑆 ⊆ ℂ ∧ 𝑛 ∈ ℕ0)
∧ 𝑓 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0)) → 𝑛 ∈ ℕ0) | 
| 42 |  | 0cnd 11255 | . . . . . . . . . . . . 13
⊢ (((𝑆 ⊆ ℂ ∧ 𝑛 ∈ ℕ0)
∧ 𝑓 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0)) → 0 ∈ ℂ) | 
| 43 | 42 | snssd 4808 | . . . . . . . . . . . 12
⊢ (((𝑆 ⊆ ℂ ∧ 𝑛 ∈ ℕ0)
∧ 𝑓 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0)) → {0} ⊆ ℂ) | 
| 44 | 3, 43 | unssd 4191 | . . . . . . . . . . 11
⊢ (((𝑆 ⊆ ℂ ∧ 𝑛 ∈ ℕ0)
∧ 𝑓 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0)) → (𝑆 ∪ {0}) ⊆
ℂ) | 
| 45 | 21, 44 | fssd 6752 | . . . . . . . . . 10
⊢ (((𝑆 ⊆ ℂ ∧ 𝑛 ∈ ℕ0)
∧ 𝑓 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0)) → (𝑥 ∈ ℕ0 ↦ if(𝑥 ∈ (0...𝑛), (𝑓‘𝑥),
0)):ℕ0⟶ℂ) | 
| 46 |  | plyco0 26232 | . . . . . . . . . 10
⊢ ((𝑛 ∈ ℕ0
∧ (𝑥 ∈
ℕ0 ↦ if(𝑥 ∈ (0...𝑛), (𝑓‘𝑥), 0)):ℕ0⟶ℂ)
→ (((𝑥 ∈
ℕ0 ↦ if(𝑥 ∈ (0...𝑛), (𝑓‘𝑥), 0)) “
(ℤ≥‘(𝑛 + 1))) = {0} ↔ ∀𝑘 ∈ ℕ0
(((𝑥 ∈
ℕ0 ↦ if(𝑥 ∈ (0...𝑛), (𝑓‘𝑥), 0))‘𝑘) ≠ 0 → 𝑘 ≤ 𝑛))) | 
| 47 | 41, 45, 46 | syl2anc 584 | . . . . . . . . 9
⊢ (((𝑆 ⊆ ℂ ∧ 𝑛 ∈ ℕ0)
∧ 𝑓 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0)) → (((𝑥 ∈ ℕ0 ↦ if(𝑥 ∈ (0...𝑛), (𝑓‘𝑥), 0)) “
(ℤ≥‘(𝑛 + 1))) = {0} ↔ ∀𝑘 ∈ ℕ0
(((𝑥 ∈
ℕ0 ↦ if(𝑥 ∈ (0...𝑛), (𝑓‘𝑥), 0))‘𝑘) ≠ 0 → 𝑘 ≤ 𝑛))) | 
| 48 | 40, 47 | mpbird 257 | . . . . . . . 8
⊢ (((𝑆 ⊆ ℂ ∧ 𝑛 ∈ ℕ0)
∧ 𝑓 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0)) → ((𝑥 ∈ ℕ0 ↦ if(𝑥 ∈ (0...𝑛), (𝑓‘𝑥), 0)) “
(ℤ≥‘(𝑛 + 1))) = {0}) | 
| 49 |  | eqidd 2737 | . . . . . . . 8
⊢ (((𝑆 ⊆ ℂ ∧ 𝑛 ∈ ℕ0)
∧ 𝑓 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0)) → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑓‘𝑘) · (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑓‘𝑘) · (𝑧↑𝑘)))) | 
| 50 |  | imaeq1 6072 | . . . . . . . . . . 11
⊢ (𝑎 = (𝑥 ∈ ℕ0 ↦ if(𝑥 ∈ (0...𝑛), (𝑓‘𝑥), 0)) → (𝑎 “ (ℤ≥‘(𝑛 + 1))) = ((𝑥 ∈ ℕ0 ↦ if(𝑥 ∈ (0...𝑛), (𝑓‘𝑥), 0)) “
(ℤ≥‘(𝑛 + 1)))) | 
| 51 | 50 | eqeq1d 2738 | . . . . . . . . . 10
⊢ (𝑎 = (𝑥 ∈ ℕ0 ↦ if(𝑥 ∈ (0...𝑛), (𝑓‘𝑥), 0)) → ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ↔ ((𝑥 ∈ ℕ0
↦ if(𝑥 ∈
(0...𝑛), (𝑓‘𝑥), 0)) “
(ℤ≥‘(𝑛 + 1))) = {0})) | 
| 52 |  | fveq1 6904 | . . . . . . . . . . . . . . 15
⊢ (𝑎 = (𝑥 ∈ ℕ0 ↦ if(𝑥 ∈ (0...𝑛), (𝑓‘𝑥), 0)) → (𝑎‘𝑘) = ((𝑥 ∈ ℕ0 ↦ if(𝑥 ∈ (0...𝑛), (𝑓‘𝑥), 0))‘𝑘)) | 
| 53 |  | elfznn0 13661 | . . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ (0...𝑛) → 𝑘 ∈ ℕ0) | 
| 54 | 53, 31 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ (0...𝑛) → ((𝑥 ∈ ℕ0 ↦ if(𝑥 ∈ (0...𝑛), (𝑓‘𝑥), 0))‘𝑘) = if(𝑘 ∈ (0...𝑛), (𝑓‘𝑘), 0)) | 
| 55 |  | iftrue 4530 | . . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ (0...𝑛) → if(𝑘 ∈ (0...𝑛), (𝑓‘𝑘), 0) = (𝑓‘𝑘)) | 
| 56 | 54, 55 | eqtrd 2776 | . . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ (0...𝑛) → ((𝑥 ∈ ℕ0 ↦ if(𝑥 ∈ (0...𝑛), (𝑓‘𝑥), 0))‘𝑘) = (𝑓‘𝑘)) | 
| 57 | 52, 56 | sylan9eq 2796 | . . . . . . . . . . . . . 14
⊢ ((𝑎 = (𝑥 ∈ ℕ0 ↦ if(𝑥 ∈ (0...𝑛), (𝑓‘𝑥), 0)) ∧ 𝑘 ∈ (0...𝑛)) → (𝑎‘𝑘) = (𝑓‘𝑘)) | 
| 58 | 57 | oveq1d 7447 | . . . . . . . . . . . . 13
⊢ ((𝑎 = (𝑥 ∈ ℕ0 ↦ if(𝑥 ∈ (0...𝑛), (𝑓‘𝑥), 0)) ∧ 𝑘 ∈ (0...𝑛)) → ((𝑎‘𝑘) · (𝑧↑𝑘)) = ((𝑓‘𝑘) · (𝑧↑𝑘))) | 
| 59 | 58 | sumeq2dv 15739 | . . . . . . . . . . . 12
⊢ (𝑎 = (𝑥 ∈ ℕ0 ↦ if(𝑥 ∈ (0...𝑛), (𝑓‘𝑥), 0)) → Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)) = Σ𝑘 ∈ (0...𝑛)((𝑓‘𝑘) · (𝑧↑𝑘))) | 
| 60 | 59 | mpteq2dv 5243 | . . . . . . . . . . 11
⊢ (𝑎 = (𝑥 ∈ ℕ0 ↦ if(𝑥 ∈ (0...𝑛), (𝑓‘𝑥), 0)) → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑓‘𝑘) · (𝑧↑𝑘)))) | 
| 61 | 60 | eqeq2d 2747 | . . . . . . . . . 10
⊢ (𝑎 = (𝑥 ∈ ℕ0 ↦ if(𝑥 ∈ (0...𝑛), (𝑓‘𝑥), 0)) → ((𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑓‘𝑘) · (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))) ↔ (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑓‘𝑘) · (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑓‘𝑘) · (𝑧↑𝑘))))) | 
| 62 | 51, 61 | anbi12d 632 | . . . . . . . . 9
⊢ (𝑎 = (𝑥 ∈ ℕ0 ↦ if(𝑥 ∈ (0...𝑛), (𝑓‘𝑥), 0)) → (((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ (𝑧 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑛)((𝑓‘𝑘) · (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) ↔ (((𝑥 ∈ ℕ0 ↦ if(𝑥 ∈ (0...𝑛), (𝑓‘𝑥), 0)) “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑓‘𝑘) · (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑓‘𝑘) · (𝑧↑𝑘)))))) | 
| 63 | 62 | rspcev 3621 | . . . . . . . 8
⊢ (((𝑥 ∈ ℕ0
↦ if(𝑥 ∈
(0...𝑛), (𝑓‘𝑥), 0)) ∈ ((𝑆 ∪ {0}) ↑m
ℕ0) ∧ (((𝑥 ∈ ℕ0 ↦ if(𝑥 ∈ (0...𝑛), (𝑓‘𝑥), 0)) “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑓‘𝑘) · (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑓‘𝑘) · (𝑧↑𝑘))))) → ∃𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0)((𝑎
“ (ℤ≥‘(𝑛 + 1))) = {0} ∧ (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑓‘𝑘) · (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) | 
| 64 | 24, 48, 49, 63 | syl12anc 836 | . . . . . . 7
⊢ (((𝑆 ⊆ ℂ ∧ 𝑛 ∈ ℕ0)
∧ 𝑓 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0)) → ∃𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0)((𝑎
“ (ℤ≥‘(𝑛 + 1))) = {0} ∧ (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑓‘𝑘) · (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) | 
| 65 |  | eqeq1 2740 | . . . . . . . . 9
⊢ (𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑓‘𝑘) · (𝑧↑𝑘))) → (𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))) ↔ (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑓‘𝑘) · (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) | 
| 66 | 65 | anbi2d 630 | . . . . . . . 8
⊢ (𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑓‘𝑘) · (𝑧↑𝑘))) → (((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) ↔ ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ (𝑧 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑛)((𝑓‘𝑘) · (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))))) | 
| 67 | 66 | rexbidv 3178 | . . . . . . 7
⊢ (𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑓‘𝑘) · (𝑧↑𝑘))) → (∃𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0)((𝑎
“ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) ↔ ∃𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0)((𝑎
“ (ℤ≥‘(𝑛 + 1))) = {0} ∧ (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑓‘𝑘) · (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))))) | 
| 68 | 64, 67 | syl5ibrcom 247 | . . . . . 6
⊢ (((𝑆 ⊆ ℂ ∧ 𝑛 ∈ ℕ0)
∧ 𝑓 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0)) → (𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑓‘𝑘) · (𝑧↑𝑘))) → ∃𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0)((𝑎
“ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))))) | 
| 69 | 68 | rexlimdva 3154 | . . . . 5
⊢ ((𝑆 ⊆ ℂ ∧ 𝑛 ∈ ℕ0)
→ (∃𝑓 ∈
((𝑆 ∪ {0})
↑m ℕ0)𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑓‘𝑘) · (𝑧↑𝑘))) → ∃𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0)((𝑎
“ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))))) | 
| 70 | 69 | reximdva 3167 | . . . 4
⊢ (𝑆 ⊆ ℂ →
(∃𝑛 ∈
ℕ0 ∃𝑓 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0)𝐹 =
(𝑧 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑛)((𝑓‘𝑘) · (𝑧↑𝑘))) → ∃𝑛 ∈ ℕ0 ∃𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0)((𝑎
“ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))))) | 
| 71 | 70 | imdistani 568 | . . 3
⊢ ((𝑆 ⊆ ℂ ∧
∃𝑛 ∈
ℕ0 ∃𝑓 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0)𝐹 =
(𝑧 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑛)((𝑓‘𝑘) · (𝑧↑𝑘)))) → (𝑆 ⊆ ℂ ∧ ∃𝑛 ∈ ℕ0
∃𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0)((𝑎
“ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))))) | 
| 72 | 1, 71 | sylbi 217 | . 2
⊢ (𝐹 ∈ (Poly‘𝑆) → (𝑆 ⊆ ℂ ∧ ∃𝑛 ∈ ℕ0
∃𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0)((𝑎
“ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))))) | 
| 73 |  | simpr 484 | . . . . . 6
⊢ (((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) | 
| 74 | 73 | reximi 3083 | . . . . 5
⊢
(∃𝑎 ∈
((𝑆 ∪ {0})
↑m ℕ0)((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) → ∃𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0)𝐹 =
(𝑧 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) | 
| 75 | 74 | reximi 3083 | . . . 4
⊢
(∃𝑛 ∈
ℕ0 ∃𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0)((𝑎
“ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) → ∃𝑛 ∈ ℕ0 ∃𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0)𝐹 =
(𝑧 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) | 
| 76 | 75 | anim2i 617 | . . 3
⊢ ((𝑆 ⊆ ℂ ∧
∃𝑛 ∈
ℕ0 ∃𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0)((𝑎
“ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) → (𝑆 ⊆ ℂ ∧ ∃𝑛 ∈ ℕ0
∃𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0)𝐹 =
(𝑧 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) | 
| 77 |  | elply 26235 | . . 3
⊢ (𝐹 ∈ (Poly‘𝑆) ↔ (𝑆 ⊆ ℂ ∧ ∃𝑛 ∈ ℕ0
∃𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0)𝐹 =
(𝑧 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) | 
| 78 | 76, 77 | sylibr 234 | . 2
⊢ ((𝑆 ⊆ ℂ ∧
∃𝑛 ∈
ℕ0 ∃𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0)((𝑎
“ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) → 𝐹 ∈ (Poly‘𝑆)) | 
| 79 | 72, 78 | impbii 209 | 1
⊢ (𝐹 ∈ (Poly‘𝑆) ↔ (𝑆 ⊆ ℂ ∧ ∃𝑛 ∈ ℕ0
∃𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0)((𝑎
“ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))))) |