Theorem sqrtcl

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

	Ref	Expression
Assertion	sqrtcl	$$⊢A\in ℂ\to \sqrt{A}\in ℂ$$

Proof

Step	Hyp	Ref	Expression
1		sqrtval	$$⊢A\in ℂ\to \sqrt{A}=\left(\iota x\in ℂ|\left(x^2=A\wedge 0\le \Re \left(x\right)\wedge \mathrm{i}x\notin {ℝ}^{+}\right)\right)$$
2		sqreu	$$⊢A\in ℂ\to \exists !x\in ℂ\left(x^2=A\wedge 0\le \Re \left(x\right)\wedge \mathrm{i}x\notin {ℝ}^{+}\right)$$
3		riotacl	$$⊢\exists !x\in ℂ\left(x^2=A\wedge 0\le \Re \left(x\right)\wedge \mathrm{i}x\notin {ℝ}^{+}\right)\to \left(\iota x\in ℂ|\left(x^2=A\wedge 0\le \Re \left(x\right)\wedge \mathrm{i}x\notin {ℝ}^{+}\right)\right)\in ℂ$$
4	2 3	syl	$$⊢A\in ℂ\to \left(\iota x\in ℂ|\left(x^2=A\wedge 0\le \Re \left(x\right)\wedge \mathrm{i}x\notin {ℝ}^{+}\right)\right)\in ℂ$$
5	1 4	eqeltrd	$$⊢A\in ℂ\to \sqrt{A}\in ℂ$$