Theorem fprodadd2cncf

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

	Ref	Expression
Hypotheses	fprodadd2cncf.k	⊢ Ⅎ 𝑘 𝜑
	fprodadd2cncf.a	⊢ ( 𝜑 → 𝐴 ∈ Fin )
	fprodadd2cncf.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
	fprodadd2cncf.f	⊢ 𝐹 = ( 𝑥 ∈ ℂ ↦ ∏ 𝑘 ∈ 𝐴 ( 𝐵 + 𝑥 ) )
Assertion	fprodadd2cncf	⊢ ( 𝜑 → 𝐹 ∈ ( ℂ –cn→ ℂ ) )

Proof

Step	Hyp	Ref	Expression
1		fprodadd2cncf.k	⊢ Ⅎ 𝑘 𝜑
2		fprodadd2cncf.a	⊢ ( 𝜑 → 𝐴 ∈ Fin )
3		fprodadd2cncf.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
4		fprodadd2cncf.f	⊢ 𝐹 = ( 𝑥 ∈ ℂ ↦ ∏ 𝑘 ∈ 𝐴 ( 𝐵 + 𝑥 ) )
5	4	a1i	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ ℂ ↦ ∏ 𝑘 ∈ 𝐴 ( 𝐵 + 𝑥 ) ) )
6		eqid	⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
7	6	cnfldtopon	⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
8	7	a1i	⊢ ( 𝜑 → ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) )
9		eqid	⊢ ( 𝑥 ∈ ℂ ↦ ( 𝐵 + 𝑥 ) ) = ( 𝑥 ∈ ℂ ↦ ( 𝐵 + 𝑥 ) )
10	3 9	add2cncf	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝑥 ∈ ℂ ↦ ( 𝐵 + 𝑥 ) ) ∈ ( ℂ –cn→ ℂ ) )
11	6	cncfcn1	⊢ ( ℂ –cn→ ℂ ) = ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) )
12	11	a1i	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( ℂ –cn→ ℂ ) = ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) )
13	10 12	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝑥 ∈ ℂ ↦ ( 𝐵 + 𝑥 ) ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) )
14	1 6 8 2 13	fprodcn	⊢ ( 𝜑 → ( 𝑥 ∈ ℂ ↦ ∏ 𝑘 ∈ 𝐴 ( 𝐵 + 𝑥 ) ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) )
15	5 14	eqeltrd	⊢ ( 𝜑 → 𝐹 ∈ ( ( 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	⊢ ( 𝜑 → 𝐹 ∈ ( ℂ –cn→ ℂ ) )