Metamath Proof Explorer

Theorem plycn

Description: A polynomial is a continuous function. (Contributed by Mario Carneiro, 23-Jul-2014)

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 ffvelrn ⊢ 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 mulcn ⊢ × ∈ TopOpen ⁡ ℂ fld × t TopOpen ⁡ ℂ fld Cn TopOpen ⁡ ℂ fld
18 17 a1i ⊢ F ∈ Poly ⁡ S ∧ k ∈ 0 … deg ⁡ F → × ∈ TopOpen ⁡ ℂ fld × t TopOpen ⁡ ℂ fld Cn TopOpen ⁡ ℂ fld
19 8 13 16 18 cnmpt12f ⊢ F ∈ Poly ⁡ S ∧ k ∈ 0 … deg ⁡ F → z ∈ ℂ ⟼ coeff ⁡ F ⁡ k ⁢ z k ∈ TopOpen ⁡ ℂ fld Cn TopOpen ⁡ ℂ fld
20 4 6 7 19 fsumcn ⊢ F ∈ Poly ⁡ S → z ∈ ℂ ⟼ ∑ k = 0 deg ⁡ F coeff ⁡ F ⁡ k ⁢ z k ∈ TopOpen ⁡ ℂ fld Cn TopOpen ⁡ ℂ fld
21 3 20 eqeltrd ⊢ F ∈ Poly ⁡ S → F ∈ TopOpen ⁡ ℂ fld Cn TopOpen ⁡ ℂ fld
22 4 cncfcn1 ⊢ ℂ ⟶cn ℂ = TopOpen ⁡ ℂ fld Cn TopOpen ⁡ ℂ fld
23 21 22 eleqtrrdi ⊢ F ∈ Poly ⁡ S → F : ℂ ⟶cn ℂ