Metamath Proof Explorer

Theorem fprodadd2cncf

Description: F is continuous. (Contributed by Glauco Siliprandi, 8-Apr-2021)

Ref Expression
Hypotheses fprodadd2cncf.k ⊢ Ⅎ k φ
fprodadd2cncf.a ⊢ φ → A ∈ Fin
fprodadd2cncf.b ⊢ φ ∧ k ∈ A → B ∈ ℂ
fprodadd2cncf.f ⊢ F = x ∈ ℂ ⟼ ∏ k ∈ A B + x
Assertion fprodadd2cncf ⊢ φ → F : ℂ ⟶cn ℂ

Proof

Step Hyp Ref Expression
1 fprodadd2cncf.k ⊢ Ⅎ k φ
2 fprodadd2cncf.a ⊢ φ → A ∈ Fin
3 fprodadd2cncf.b ⊢ φ ∧ k ∈ A → B ∈ ℂ
4 fprodadd2cncf.f ⊢ F = x ∈ ℂ ⟼ ∏ k ∈ A B + x
5 4 a1i ⊢ φ → F = x ∈ ℂ ⟼ ∏ k ∈ A B + x
6 eqid ⊢ TopOpen ⁡ ℂ fld = TopOpen ⁡ ℂ fld
7 6 cnfldtopon ⊢ TopOpen ⁡ ℂ fld ∈ TopOn ⁡ ℂ
8 7 a1i ⊢ φ → TopOpen ⁡ ℂ fld ∈ TopOn ⁡ ℂ
9 eqid ⊢ x ∈ ℂ ⟼ B + x = x ∈ ℂ ⟼ B + x
10 3 9 add2cncf ⊢ φ ∧ k ∈ A → x ∈ ℂ ⟼ B + x : ℂ ⟶cn ℂ
11 6 cncfcn1 ⊢ ℂ ⟶cn ℂ = TopOpen ⁡ ℂ fld Cn TopOpen ⁡ ℂ fld
12 11 a1i ⊢ φ ∧ k ∈ A → ℂ ⟶cn ℂ = TopOpen ⁡ ℂ fld Cn TopOpen ⁡ ℂ fld
13 10 12 eleqtrd ⊢ φ ∧ k ∈ A → x ∈ ℂ ⟼ B + x ∈ TopOpen ⁡ ℂ fld Cn TopOpen ⁡ ℂ fld
14 1 6 8 2 13 fprodcn ⊢ φ → x ∈ ℂ ⟼ ∏ k ∈ A B + x ∈ TopOpen ⁡ ℂ fld Cn TopOpen ⁡ ℂ fld
15 5 14 eqeltrd ⊢ φ → F ∈ TopOpen ⁡ ℂ fld Cn TopOpen ⁡ ℂ fld
16 11 a1i ⊢ φ → ℂ ⟶cn ℂ = TopOpen ⁡ ℂ fld Cn TopOpen ⁡ ℂ fld
17 16 eqcomd ⊢ φ → TopOpen ⁡ ℂ fld Cn TopOpen ⁡ ℂ fld = ℂ ⟶cn ℂ
18 15 17 eleqtrd ⊢ φ → F : ℂ ⟶cn ℂ