This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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) Usage of this theorem is discouraged because it depends on ax-mulf . Use mpomulcn instead. (New usage is discouraged.)

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 𝐽 )