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=0deg⁡Fcoeff⁡F⁡k⁢zk
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⁡ℂfldCnTopOpen⁡ℂfld
14 10 adantl ⊢F∈Poly⁡S∧k∈0…deg⁡F→k∈ℕ0
15 4 expcn ⊢k∈ℕ0→z∈ℂ⟼zk∈TopOpen⁡ℂfldCnTopOpen⁡ℂfld
16 14 15 syl ⊢F∈Poly⁡S∧k∈0…deg⁡F→z∈ℂ⟼zk∈TopOpen⁡ℂfldCnTopOpen⁡ℂfld
17 4 mulcn ⊢×∈TopOpen⁡ℂfld×tTopOpen⁡ℂfldCnTopOpen⁡ℂfld
18 17 a1i ⊢F∈Poly⁡S∧k∈0…deg⁡F→×∈TopOpen⁡ℂfld×tTopOpen⁡ℂfldCnTopOpen⁡ℂfld
19 8 13 16 18 cnmpt12f ⊢F∈Poly⁡S∧k∈0…deg⁡F→z∈ℂ⟼coeff⁡F⁡k⁢zk∈TopOpen⁡ℂfldCnTopOpen⁡ℂfld
20 4 6 7 19 fsumcn ⊢F∈Poly⁡S→z∈ℂ⟼∑k=0deg⁡Fcoeff⁡F⁡k⁢zk∈TopOpen⁡ℂfldCnTopOpen⁡ℂfld
21 3 20 eqeltrd ⊢F∈Poly⁡S→F∈TopOpen⁡ℂfldCnTopOpen⁡ℂfld
22 4 cncfcn1 ⊢ℂ⟶cnℂ=TopOpen⁡ℂfldCnTopOpen⁡ℂfld
23 21 22 eleqtrrdi ⊢F∈Poly⁡S→F:ℂ⟶cnℂ