Step |
Hyp |
Ref |
Expression |
1 |
|
plyssc |
⊢ ( Poly ‘ 𝑆 ) ⊆ ( Poly ‘ ℂ ) |
2 |
1
|
sseli |
⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐹 ∈ ( Poly ‘ ℂ ) ) |
3 |
|
cnring |
⊢ ℂfld ∈ Ring |
4 |
|
cnfldbas |
⊢ ℂ = ( Base ‘ ℂfld ) |
5 |
4
|
subrgid |
⊢ ( ℂfld ∈ Ring → ℂ ∈ ( SubRing ‘ ℂfld ) ) |
6 |
3 5
|
ax-mp |
⊢ ℂ ∈ ( SubRing ‘ ℂfld ) |
7 |
|
dvnply2 |
⊢ ( ( ℂ ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ ℂ ) ∧ 𝑁 ∈ ℕ0 ) → ( ( ℂ D𝑛 𝐹 ) ‘ 𝑁 ) ∈ ( Poly ‘ ℂ ) ) |
8 |
6 7
|
mp3an1 |
⊢ ( ( 𝐹 ∈ ( Poly ‘ ℂ ) ∧ 𝑁 ∈ ℕ0 ) → ( ( ℂ D𝑛 𝐹 ) ‘ 𝑁 ) ∈ ( Poly ‘ ℂ ) ) |
9 |
2 8
|
sylan |
⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( ℂ D𝑛 𝐹 ) ‘ 𝑁 ) ∈ ( Poly ‘ ℂ ) ) |