Theorem mulcn

Description: Complex number multiplication is a continuous function. Part of Proposition 14-4.16 of Gleason p. 243. (Contributed by NM, 30-Jul-2007) (Proof shortened by Mario Carneiro, 5-May-2014)

	Ref	Expression
Hypothesis	addcn.j	⊢ 𝐽 = ( TopOpen ‘ ℂfld )
Assertion	mulcn	⊢ · ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 )

Proof

Step	Hyp	Ref	Expression
1		addcn.j	⊢ 𝐽 = ( TopOpen ‘ ℂfld )
2		ax-mulf	⊢ · : ( ℂ × ℂ ) ⟶ ℂ
3		mulcn2	⊢ ( ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ) → ∃ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑢 ∈ ℂ ∀ 𝑣 ∈ ℂ ( ( ( abs ‘ ( 𝑢 − 𝑏 ) ) < 𝑦 ∧ ( abs ‘ ( 𝑣 − 𝑐 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝑢 · 𝑣 ) − ( 𝑏 · 𝑐 ) ) ) < 𝑎 ) )
4	1 2 3	addcnlem	⊢ · ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 )