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 ` CCfld )
Assertion	sqcn	|- ( x e. CC |-> ( x ^ 2 ) ) e. ( J Cn J )

Proof

Step	Hyp	Ref	Expression
1		sqcn.j	|- J = ( TopOpen ` CCfld )
2		2nn0	|- 2 e. NN0
3	1	expcn	|- ( 2 e. NN0 -> ( x e. CC |-> ( x ^ 2 ) ) e. ( J Cn J ) )
4	2 3	ax-mp	|- ( x e. CC |-> ( x ^ 2 ) ) e. ( J Cn J )