Theorem sqrtcl

Description: Closure of the square root function over the complex numbers. (Contributed by Mario Carneiro, 10-Jul-2013)

	Ref	Expression
Assertion	sqrtcl	⊢ ( 𝐴 ∈ ℂ → ( √ ‘ 𝐴 ) ∈ ℂ )

Proof

Step	Hyp	Ref	Expression
1		sqrtval	⊢ ( 𝐴 ∈ ℂ → ( √ ‘ 𝐴 ) = ( ℩ 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ) )
2		sqreu	⊢ ( 𝐴 ∈ ℂ → ∃! 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) )
3		riotacl	⊢ ( ∃! 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) → ( ℩ 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ) ∈ ℂ )
4	2 3	syl	⊢ ( 𝐴 ∈ ℂ → ( ℩ 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ) ∈ ℂ )
5	1 4	eqeltrd	⊢ ( 𝐴 ∈ ℂ → ( √ ‘ 𝐴 ) ∈ ℂ )