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	$$⊢J=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
Assertion	mulcn	$$⊢\times \in \left(\left(J{\times }_{t}J\right)\mathrm{Cn}J\right)$$

Proof

Step	Hyp	Ref	Expression
1		addcn.j	$$⊢J=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
2		ax-mulf	$$⊢\times :ℂ\times ℂ⟶ℂ$$
3		mulcn2	$$⊢\left(a\in {ℝ}^{+}\wedge b\in ℂ\wedge c\in ℂ\right)\to \exists y\in {ℝ}^{+}\exists z\in {ℝ}^{+}\forall u\in ℂ\forall v\in ℂ\left(\left(\left|u-b\right|<y\wedge \left|v-c\right|<z\right)\to \left|uv-bc\right|<a\right)$$
4	1 2 3	addcnlem	$$⊢\times \in \left(\left(J{\times }_{t}J\right)\mathrm{Cn}J\right)$$