Step |
Hyp |
Ref |
Expression |
1 |
|
coeval |
⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( coeff ‘ 𝐹 ) = ( ℩ 𝑎 ∈ ( ℂ ↑m ℕ0 ) ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) ) |
2 |
|
coeeu |
⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ∃! 𝑎 ∈ ( ℂ ↑m ℕ0 ) ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) |
3 |
|
riotacl2 |
⊢ ( ∃! 𝑎 ∈ ( ℂ ↑m ℕ0 ) ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) → ( ℩ 𝑎 ∈ ( ℂ ↑m ℕ0 ) ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) ∈ { 𝑎 ∈ ( ℂ ↑m ℕ0 ) ∣ ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) } ) |
4 |
2 3
|
syl |
⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( ℩ 𝑎 ∈ ( ℂ ↑m ℕ0 ) ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) ∈ { 𝑎 ∈ ( ℂ ↑m ℕ0 ) ∣ ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) } ) |
5 |
1 4
|
eqeltrd |
⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( coeff ‘ 𝐹 ) ∈ { 𝑎 ∈ ( ℂ ↑m ℕ0 ) ∣ ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) } ) |
6 |
|
imaeq1 |
⊢ ( 𝑎 = ( coeff ‘ 𝐹 ) → ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = ( ( coeff ‘ 𝐹 ) “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) ) |
7 |
6
|
eqeq1d |
⊢ ( 𝑎 = ( coeff ‘ 𝐹 ) → ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ↔ ( ( coeff ‘ 𝐹 ) “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ) ) |
8 |
|
fveq1 |
⊢ ( 𝑎 = ( coeff ‘ 𝐹 ) → ( 𝑎 ‘ 𝑘 ) = ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) ) |
9 |
8
|
oveq1d |
⊢ ( 𝑎 = ( coeff ‘ 𝐹 ) → ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = ( ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) |
10 |
9
|
sumeq2sdv |
⊢ ( 𝑎 = ( coeff ‘ 𝐹 ) → Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) |
11 |
10
|
mpteq2dv |
⊢ ( 𝑎 = ( coeff ‘ 𝐹 ) → ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) |
12 |
11
|
eqeq2d |
⊢ ( 𝑎 = ( coeff ‘ 𝐹 ) → ( 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ↔ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) |
13 |
7 12
|
anbi12d |
⊢ ( 𝑎 = ( coeff ‘ 𝐹 ) → ( ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ↔ ( ( ( coeff ‘ 𝐹 ) “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) ) |
14 |
13
|
rexbidv |
⊢ ( 𝑎 = ( coeff ‘ 𝐹 ) → ( ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ↔ ∃ 𝑛 ∈ ℕ0 ( ( ( coeff ‘ 𝐹 ) “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) ) |
15 |
14
|
elrab |
⊢ ( ( coeff ‘ 𝐹 ) ∈ { 𝑎 ∈ ( ℂ ↑m ℕ0 ) ∣ ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) } ↔ ( ( coeff ‘ 𝐹 ) ∈ ( ℂ ↑m ℕ0 ) ∧ ∃ 𝑛 ∈ ℕ0 ( ( ( coeff ‘ 𝐹 ) “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) ) |
16 |
5 15
|
sylib |
⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( ( coeff ‘ 𝐹 ) ∈ ( ℂ ↑m ℕ0 ) ∧ ∃ 𝑛 ∈ ℕ0 ( ( ( coeff ‘ 𝐹 ) “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) ) |