Theorem sqcn

Description: The square function on complex numbers is continuous. (Contributed by NM, 13-Jun-2007) (Proof shortened by Mario Carneiro, 5-May-2014)

	Ref	Expression
Hypothesis	sqcn.j	$$⊢J=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
Assertion	sqcn	$$⊢\left(x\in ℂ⟼x^2\right)\in \left(J\mathrm{Cn}J\right)$$

Proof

Step	Hyp	Ref	Expression
1		sqcn.j	$$⊢J=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
2		2nn0	$$⊢2\in {\mathbb{N}}_0$$
3	1	expcn	$$⊢2\in {\mathbb{N}}_0\to \left(x\in ℂ⟼x^2\right)\in \left(J\mathrm{Cn}J\right)$$
4	2 3	ax-mp	$$⊢\left(x\in ℂ⟼x^2\right)\in \left(J\mathrm{Cn}J\right)$$