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 ⊢ J = TopOpen ⁡ ℂ fld
Assertion mulcn ⊢ × ∈ J × t J Cn J

Proof

Step Hyp Ref Expression
1 addcn.j ⊢ J = TopOpen ⁡ ℂ fld
2 ax-mulf ⊢ × : ℂ × ℂ ⟶ ℂ
3 mulcn2 ⊢ a ∈ ℝ + ∧ b ∈ ℂ ∧ c ∈ ℂ → ∃ y ∈ ℝ + ∃ z ∈ ℝ + ∀ u ∈ ℂ ∀ v ∈ ℂ u − b < y ∧ v − c < z → u ⁢ v − b ⁢ c < a
4 1 2 3 addcnlem ⊢ × ∈ J × t J Cn J