Step | Hyp | Ref
| Expression |
1 | | simp1 1138 |
. 2
⊢ ((𝑆 ⊆ ℂ ∧ 𝑁 ∈ ℕ0
∧ 𝐴:ℕ0⟶𝑆) → 𝑆 ⊆ ℂ) |
2 | | simp2 1139 |
. . 3
⊢ ((𝑆 ⊆ ℂ ∧ 𝑁 ∈ ℕ0
∧ 𝐴:ℕ0⟶𝑆) → 𝑁 ∈
ℕ0) |
3 | | simp3 1140 |
. . . . 5
⊢ ((𝑆 ⊆ ℂ ∧ 𝑁 ∈ ℕ0
∧ 𝐴:ℕ0⟶𝑆) → 𝐴:ℕ0⟶𝑆) |
4 | | ssun1 4091 |
. . . . 5
⊢ 𝑆 ⊆ (𝑆 ∪ {0}) |
5 | | fss 6567 |
. . . . 5
⊢ ((𝐴:ℕ0⟶𝑆 ∧ 𝑆 ⊆ (𝑆 ∪ {0})) → 𝐴:ℕ0⟶(𝑆 ∪ {0})) |
6 | 3, 4, 5 | sylancl 589 |
. . . 4
⊢ ((𝑆 ⊆ ℂ ∧ 𝑁 ∈ ℕ0
∧ 𝐴:ℕ0⟶𝑆) → 𝐴:ℕ0⟶(𝑆 ∪ {0})) |
7 | | 0cnd 10831 |
. . . . . . . 8
⊢ ((𝑆 ⊆ ℂ ∧ 𝑁 ∈ ℕ0
∧ 𝐴:ℕ0⟶𝑆) → 0 ∈
ℂ) |
8 | 7 | snssd 4727 |
. . . . . . 7
⊢ ((𝑆 ⊆ ℂ ∧ 𝑁 ∈ ℕ0
∧ 𝐴:ℕ0⟶𝑆) → {0} ⊆
ℂ) |
9 | 1, 8 | unssd 4105 |
. . . . . 6
⊢ ((𝑆 ⊆ ℂ ∧ 𝑁 ∈ ℕ0
∧ 𝐴:ℕ0⟶𝑆) → (𝑆 ∪ {0}) ⊆
ℂ) |
10 | | cnex 10815 |
. . . . . 6
⊢ ℂ
∈ V |
11 | | ssexg 5221 |
. . . . . 6
⊢ (((𝑆 ∪ {0}) ⊆ ℂ
∧ ℂ ∈ V) → (𝑆 ∪ {0}) ∈ V) |
12 | 9, 10, 11 | sylancl 589 |
. . . . 5
⊢ ((𝑆 ⊆ ℂ ∧ 𝑁 ∈ ℕ0
∧ 𝐴:ℕ0⟶𝑆) → (𝑆 ∪ {0}) ∈ V) |
13 | | nn0ex 12101 |
. . . . 5
⊢
ℕ0 ∈ V |
14 | | elmapg 8526 |
. . . . 5
⊢ (((𝑆 ∪ {0}) ∈ V ∧
ℕ0 ∈ V) → (𝐴 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0) ↔ 𝐴:ℕ0⟶(𝑆 ∪ {0}))) |
15 | 12, 13, 14 | sylancl 589 |
. . . 4
⊢ ((𝑆 ⊆ ℂ ∧ 𝑁 ∈ ℕ0
∧ 𝐴:ℕ0⟶𝑆) → (𝐴 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0) ↔ 𝐴:ℕ0⟶(𝑆 ∪ {0}))) |
16 | 6, 15 | mpbird 260 |
. . 3
⊢ ((𝑆 ⊆ ℂ ∧ 𝑁 ∈ ℕ0
∧ 𝐴:ℕ0⟶𝑆) → 𝐴 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0)) |
17 | | eqidd 2738 |
. . 3
⊢ ((𝑆 ⊆ ℂ ∧ 𝑁 ∈ ℕ0
∧ 𝐴:ℕ0⟶𝑆) → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘)))) |
18 | | oveq2 7226 |
. . . . . . 7
⊢ (𝑛 = 𝑁 → (0...𝑛) = (0...𝑁)) |
19 | 18 | sumeq1d 15270 |
. . . . . 6
⊢ (𝑛 = 𝑁 → Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)) = Σ𝑘 ∈ (0...𝑁)((𝑎‘𝑘) · (𝑧↑𝑘))) |
20 | 19 | mpteq2dv 5156 |
. . . . 5
⊢ (𝑛 = 𝑁 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑎‘𝑘) · (𝑧↑𝑘)))) |
21 | 20 | eqeq2d 2748 |
. . . 4
⊢ (𝑛 = 𝑁 → ((𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))) ↔ (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑎‘𝑘) · (𝑧↑𝑘))))) |
22 | | fveq1 6721 |
. . . . . . . 8
⊢ (𝑎 = 𝐴 → (𝑎‘𝑘) = (𝐴‘𝑘)) |
23 | 22 | oveq1d 7233 |
. . . . . . 7
⊢ (𝑎 = 𝐴 → ((𝑎‘𝑘) · (𝑧↑𝑘)) = ((𝐴‘𝑘) · (𝑧↑𝑘))) |
24 | 23 | sumeq2sdv 15273 |
. . . . . 6
⊢ (𝑎 = 𝐴 → Σ𝑘 ∈ (0...𝑁)((𝑎‘𝑘) · (𝑧↑𝑘)) = Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘))) |
25 | 24 | mpteq2dv 5156 |
. . . . 5
⊢ (𝑎 = 𝐴 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑎‘𝑘) · (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘)))) |
26 | 25 | eqeq2d 2748 |
. . . 4
⊢ (𝑎 = 𝐴 → ((𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑎‘𝑘) · (𝑧↑𝑘))) ↔ (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘))))) |
27 | 21, 26 | rspc2ev 3554 |
. . 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 25094 |
. 2
⊢ ((𝑧 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘))) ∈ (Poly‘𝑆) ↔ (𝑆 ⊆ ℂ ∧ ∃𝑛 ∈ ℕ0
∃𝑎 ∈ ((𝑆 ∪ {0}) ↑m
ℕ0)(𝑧
∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) |
30 | 1, 28, 29 | sylanbrc 586 |
1
⊢ ((𝑆 ⊆ ℂ ∧ 𝑁 ∈ ℕ0
∧ 𝐴:ℕ0⟶𝑆) → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘))) ∈ (Poly‘𝑆)) |