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 ⊢ 𝐽 = ( 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 𝐽 )