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

Metamath Proof Explorer

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 = TopOpen (ℂ_{fld})$
	Assertion	sqcn	$⊢ (x \in ℂ ⟼ x^{2}) \in (J Cn J)$

Proof

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