Step |
Hyp |
Ref |
Expression |
1 |
|
ply1term.1 |
⊢ 𝐹 = ( 𝑧 ∈ ℂ ↦ ( 𝐴 · ( 𝑧 ↑ 𝑁 ) ) ) |
2 |
|
ssel2 |
⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐴 ∈ 𝑆 ) → 𝐴 ∈ ℂ ) |
3 |
1
|
ply1termlem |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( if ( 𝑘 = 𝑁 , 𝐴 , 0 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) |
4 |
2 3
|
stoic3 |
⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐴 ∈ 𝑆 ∧ 𝑁 ∈ ℕ0 ) → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( if ( 𝑘 = 𝑁 , 𝐴 , 0 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) |
5 |
|
simp1 |
⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐴 ∈ 𝑆 ∧ 𝑁 ∈ ℕ0 ) → 𝑆 ⊆ ℂ ) |
6 |
|
0cnd |
⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐴 ∈ 𝑆 ∧ 𝑁 ∈ ℕ0 ) → 0 ∈ ℂ ) |
7 |
6
|
snssd |
⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐴 ∈ 𝑆 ∧ 𝑁 ∈ ℕ0 ) → { 0 } ⊆ ℂ ) |
8 |
5 7
|
unssd |
⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐴 ∈ 𝑆 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑆 ∪ { 0 } ) ⊆ ℂ ) |
9 |
|
simp3 |
⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐴 ∈ 𝑆 ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℕ0 ) |
10 |
|
simpl2 |
⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐴 ∈ 𝑆 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝐴 ∈ 𝑆 ) |
11 |
|
elun1 |
⊢ ( 𝐴 ∈ 𝑆 → 𝐴 ∈ ( 𝑆 ∪ { 0 } ) ) |
12 |
10 11
|
syl |
⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐴 ∈ 𝑆 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝐴 ∈ ( 𝑆 ∪ { 0 } ) ) |
13 |
|
ssun2 |
⊢ { 0 } ⊆ ( 𝑆 ∪ { 0 } ) |
14 |
|
c0ex |
⊢ 0 ∈ V |
15 |
14
|
snss |
⊢ ( 0 ∈ ( 𝑆 ∪ { 0 } ) ↔ { 0 } ⊆ ( 𝑆 ∪ { 0 } ) ) |
16 |
13 15
|
mpbir |
⊢ 0 ∈ ( 𝑆 ∪ { 0 } ) |
17 |
|
ifcl |
⊢ ( ( 𝐴 ∈ ( 𝑆 ∪ { 0 } ) ∧ 0 ∈ ( 𝑆 ∪ { 0 } ) ) → if ( 𝑘 = 𝑁 , 𝐴 , 0 ) ∈ ( 𝑆 ∪ { 0 } ) ) |
18 |
12 16 17
|
sylancl |
⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐴 ∈ 𝑆 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → if ( 𝑘 = 𝑁 , 𝐴 , 0 ) ∈ ( 𝑆 ∪ { 0 } ) ) |
19 |
8 9 18
|
elplyd |
⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐴 ∈ 𝑆 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( if ( 𝑘 = 𝑁 , 𝐴 , 0 ) · ( 𝑧 ↑ 𝑘 ) ) ) ∈ ( Poly ‘ ( 𝑆 ∪ { 0 } ) ) ) |
20 |
4 19
|
eqeltrd |
⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐴 ∈ 𝑆 ∧ 𝑁 ∈ ℕ0 ) → 𝐹 ∈ ( Poly ‘ ( 𝑆 ∪ { 0 } ) ) ) |
21 |
|
plyun0 |
⊢ ( Poly ‘ ( 𝑆 ∪ { 0 } ) ) = ( Poly ‘ 𝑆 ) |
22 |
20 21
|
eleqtrdi |
⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐴 ∈ 𝑆 ∧ 𝑁 ∈ ℕ0 ) → 𝐹 ∈ ( Poly ‘ 𝑆 ) ) |