| Step | Hyp | Ref
| Expression |
| 1 | | simp1 1137 |
. 2
⊢ ((𝑆 ⊆ ℂ ∧ 𝑁 ∈ ℕ0
∧ 𝐴:ℕ0⟶𝑆) → 𝑆 ⊆ ℂ) |
| 2 | | simp2 1138 |
. . 3
⊢ ((𝑆 ⊆ ℂ ∧ 𝑁 ∈ ℕ0
∧ 𝐴:ℕ0⟶𝑆) → 𝑁 ∈
ℕ0) |
| 3 | | simp3 1139 |
. . . . 5
⊢ ((𝑆 ⊆ ℂ ∧ 𝑁 ∈ ℕ0
∧ 𝐴:ℕ0⟶𝑆) → 𝐴:ℕ0⟶𝑆) |
| 4 | | ssun1 4178 |
. . . . 5
⊢ 𝑆 ⊆ (𝑆 ∪ {0}) |
| 5 | | fss 6752 |
. . . . 5
⊢ ((𝐴:ℕ0⟶𝑆 ∧ 𝑆 ⊆ (𝑆 ∪ {0})) → 𝐴:ℕ0⟶(𝑆 ∪ {0})) |
| 6 | 3, 4, 5 | sylancl 586 |
. . . 4
⊢ ((𝑆 ⊆ ℂ ∧ 𝑁 ∈ ℕ0
∧ 𝐴:ℕ0⟶𝑆) → 𝐴:ℕ0⟶(𝑆 ∪ {0})) |
| 7 | | 0cnd 11254 |
. . . . . . . 8
⊢ ((𝑆 ⊆ ℂ ∧ 𝑁 ∈ ℕ0
∧ 𝐴:ℕ0⟶𝑆) → 0 ∈
ℂ) |
| 8 | 7 | snssd 4809 |
. . . . . . 7
⊢ ((𝑆 ⊆ ℂ ∧ 𝑁 ∈ ℕ0
∧ 𝐴:ℕ0⟶𝑆) → {0} ⊆
ℂ) |
| 9 | 1, 8 | unssd 4192 |
. . . . . 6
⊢ ((𝑆 ⊆ ℂ ∧ 𝑁 ∈ ℕ0
∧ 𝐴:ℕ0⟶𝑆) → (𝑆 ∪ {0}) ⊆
ℂ) |
| 10 | | cnex 11236 |
. . . . . 6
⊢ ℂ
∈ V |
| 11 | | ssexg 5323 |
. . . . . 6
⊢ (((𝑆 ∪ {0}) ⊆ ℂ
∧ ℂ ∈ V) → (𝑆 ∪ {0}) ∈ V) |
| 12 | 9, 10, 11 | sylancl 586 |
. . . . 5
⊢ ((𝑆 ⊆ ℂ ∧ 𝑁 ∈ ℕ0
∧ 𝐴:ℕ0⟶𝑆) → (𝑆 ∪ {0}) ∈ V) |
| 13 | | nn0ex 12532 |
. . . . 5
⊢
ℕ0 ∈ V |
| 14 | | elmapg 8879 |
. . . . 5
⊢ (((𝑆 ∪ {0}) ∈ V ∧
ℕ0 ∈ V) → (𝐴 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0) ↔ 𝐴:ℕ0⟶(𝑆 ∪ {0}))) |
| 15 | 12, 13, 14 | sylancl 586 |
. . . 4
⊢ ((𝑆 ⊆ ℂ ∧ 𝑁 ∈ ℕ0
∧ 𝐴:ℕ0⟶𝑆) → (𝐴 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0) ↔ 𝐴:ℕ0⟶(𝑆 ∪ {0}))) |
| 16 | 6, 15 | mpbird 257 |
. . 3
⊢ ((𝑆 ⊆ ℂ ∧ 𝑁 ∈ ℕ0
∧ 𝐴:ℕ0⟶𝑆) → 𝐴 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0)) |
| 17 | | eqidd 2738 |
. . 3
⊢ ((𝑆 ⊆ ℂ ∧ 𝑁 ∈ ℕ0
∧ 𝐴:ℕ0⟶𝑆) → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘)))) |
| 18 | | oveq2 7439 |
. . . . . . 7
⊢ (𝑛 = 𝑁 → (0...𝑛) = (0...𝑁)) |
| 19 | 18 | sumeq1d 15736 |
. . . . . 6
⊢ (𝑛 = 𝑁 → Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)) = Σ𝑘 ∈ (0...𝑁)((𝑎‘𝑘) · (𝑧↑𝑘))) |
| 20 | 19 | mpteq2dv 5244 |
. . . . 5
⊢ (𝑛 = 𝑁 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑎‘𝑘) · (𝑧↑𝑘)))) |
| 21 | 20 | eqeq2d 2748 |
. . . 4
⊢ (𝑛 = 𝑁 → ((𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))) ↔ (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑎‘𝑘) · (𝑧↑𝑘))))) |
| 22 | | fveq1 6905 |
. . . . . . . 8
⊢ (𝑎 = 𝐴 → (𝑎‘𝑘) = (𝐴‘𝑘)) |
| 23 | 22 | oveq1d 7446 |
. . . . . . 7
⊢ (𝑎 = 𝐴 → ((𝑎‘𝑘) · (𝑧↑𝑘)) = ((𝐴‘𝑘) · (𝑧↑𝑘))) |
| 24 | 23 | sumeq2sdv 15739 |
. . . . . 6
⊢ (𝑎 = 𝐴 → Σ𝑘 ∈ (0...𝑁)((𝑎‘𝑘) · (𝑧↑𝑘)) = Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘))) |
| 25 | 24 | mpteq2dv 5244 |
. . . . 5
⊢ (𝑎 = 𝐴 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑎‘𝑘) · (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘)))) |
| 26 | 25 | eqeq2d 2748 |
. . . 4
⊢ (𝑎 = 𝐴 → ((𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑎‘𝑘) · (𝑧↑𝑘))) ↔ (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘))))) |
| 27 | 21, 26 | rspc2ev 3635 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0) ∧ (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘)))) → ∃𝑛 ∈ ℕ0 ∃𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0)(𝑧
∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) |
| 28 | 2, 16, 17, 27 | syl3anc 1373 |
. 2
⊢ ((𝑆 ⊆ ℂ ∧ 𝑁 ∈ ℕ0
∧ 𝐴:ℕ0⟶𝑆) → ∃𝑛 ∈ ℕ0
∃𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0)(𝑧
∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) |
| 29 | | elply 26234 |
. 2
⊢ ((𝑧 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘))) ∈ (Poly‘𝑆) ↔ (𝑆 ⊆ ℂ ∧ ∃𝑛 ∈ ℕ0
∃𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0)(𝑧
∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) |
| 30 | 1, 28, 29 | sylanbrc 583 |
1
⊢ ((𝑆 ⊆ ℂ ∧ 𝑁 ∈ ℕ0
∧ 𝐴:ℕ0⟶𝑆) → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘))) ∈ (Poly‘𝑆)) |