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	⊢ 𝐽 = ( TopOpen ‘ ℂfld )
Assertion	sqcn	⊢ ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 2 ) ) ∈ ( 𝐽 Cn 𝐽 )

Proof

Step	Hyp	Ref	Expression
1		sqcn.j	⊢ 𝐽 = ( TopOpen ‘ ℂfld )
2		2nn0	⊢ 2 ∈ ℕ0
3	1	expcn	⊢ ( 2 ∈ ℕ0 → ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 2 ) ) ∈ ( 𝐽 Cn 𝐽 ) )
4	2 3	ax-mp	⊢ ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 2 ) ) ∈ ( 𝐽 Cn 𝐽 )