Metamath Proof Explorer

Theorem plycn

Description: A polynomial is a continuous function. (Contributed by Mario Carneiro, 23-Jul-2014) Avoid ax-mulf . (Revised by GG, 16-Mar-2025)

Ref Expression
Assertion plycn ⊢ F ∈ Poly ⁡ S → F : ℂ ⟶cn ℂ

Proof

Step Hyp Ref Expression
1 eqid ⊢ coeff ⁡ F = coeff ⁡ F
2 eqid ⊢ deg ⁡ F = deg ⁡ F
3 1 2 coeid ⊢ F ∈ Poly ⁡ S → F = z ∈ ℂ ⟼ ∑ k = 0 deg ⁡ F coeff ⁡ F ⁡ k ⁢ z k
4 eqid ⊢ TopOpen ⁡ ℂ fld = TopOpen ⁡ ℂ fld
5 4 cnfldtopon ⊢ TopOpen ⁡ ℂ fld ∈ TopOn ⁡ ℂ
6 5 a1i ⊢ F ∈ Poly ⁡ S → TopOpen ⁡ ℂ fld ∈ TopOn ⁡ ℂ
7 fzfid ⊢ F ∈ Poly ⁡ S → 0 … deg ⁡ F ∈ Fin
8 5 a1i ⊢ F ∈ Poly ⁡ S ∧ k ∈ 0 … deg ⁡ F → TopOpen ⁡ ℂ fld ∈ TopOn ⁡ ℂ
9 1 coef3 ⊢ F ∈ Poly ⁡ S → coeff ⁡ F : ℕ 0 ⟶ ℂ
10 elfznn0 ⊢ k ∈ 0 … deg ⁡ F → k ∈ ℕ 0
11 ffvelcdm ⊢ coeff ⁡ F : ℕ 0 ⟶ ℂ ∧ k ∈ ℕ 0 → coeff ⁡ F ⁡ k ∈ ℂ
12 9 10 11 syl2an ⊢ F ∈ Poly ⁡ S ∧ k ∈ 0 … deg ⁡ F → coeff ⁡ F ⁡ k ∈ ℂ
13 8 8 12 cnmptc ⊢ F ∈ Poly ⁡ S ∧ k ∈ 0 … deg ⁡ F → z ∈ ℂ ⟼ coeff ⁡ F ⁡ k ∈ TopOpen ⁡ ℂ fld Cn TopOpen ⁡ ℂ fld
14 10 adantl ⊢ F ∈ Poly ⁡ S ∧ k ∈ 0 … deg ⁡ F → k ∈ ℕ 0
15 4 expcn ⊢ k ∈ ℕ 0 → z ∈ ℂ ⟼ z k ∈ TopOpen ⁡ ℂ fld Cn TopOpen ⁡ ℂ fld
16 14 15 syl ⊢ F ∈ Poly ⁡ S ∧ k ∈ 0 … deg ⁡ F → z ∈ ℂ ⟼ z k ∈ TopOpen ⁡ ℂ fld Cn TopOpen ⁡ ℂ fld
17 4 mpomulcn ⊢ u ∈ ℂ , v ∈ ℂ ⟼ u ⁢ v ∈ TopOpen ⁡ ℂ fld × t TopOpen ⁡ ℂ fld Cn TopOpen ⁡ ℂ fld
18 17 a1i ⊢ F ∈ Poly ⁡ S ∧ k ∈ 0 … deg ⁡ F → u ∈ ℂ , v ∈ ℂ ⟼ u ⁢ v ∈ TopOpen ⁡ ℂ fld × t TopOpen ⁡ ℂ fld Cn TopOpen ⁡ ℂ fld
19 oveq12 ⊢ u = coeff ⁡ F ⁡ k ∧ v = z k → u ⁢ v = coeff ⁡ F ⁡ k ⁢ z k
20 8 13 16 8 8 18 19 cnmpt12 ⊢ F ∈ Poly ⁡ S ∧ k ∈ 0 … deg ⁡ F → z ∈ ℂ ⟼ coeff ⁡ F ⁡ k ⁢ z k ∈ TopOpen ⁡ ℂ fld Cn TopOpen ⁡ ℂ fld
21 4 6 7 20 fsumcn ⊢ F ∈ Poly ⁡ S → z ∈ ℂ ⟼ ∑ k = 0 deg ⁡ F coeff ⁡ F ⁡ k ⁢ z k ∈ TopOpen ⁡ ℂ fld Cn TopOpen ⁡ ℂ fld
22 3 21 eqeltrd ⊢ F ∈ Poly ⁡ S → F ∈ TopOpen ⁡ ℂ fld Cn TopOpen ⁡ ℂ fld
23 4 cncfcn1 ⊢ ℂ ⟶cn ℂ = TopOpen ⁡ ℂ fld Cn TopOpen ⁡ ℂ fld
24 22 23 eleqtrrdi ⊢ F ∈ Poly ⁡ S → F : ℂ ⟶cn ℂ