Theorem sqrtval

Description: Value of square root function. (Contributed by Mario Carneiro, 8-Jul-2013)

	Ref	Expression
Assertion	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)$$

Proof

Step	Hyp	Ref	Expression
1		eqeq2	$$⊢y=A\to \left(x^2=y\leftrightarrow x^2=A\right)$$
2	1	3anbi1d	$$⊢y=A\to \left(\left(x^2=y\wedge 0\le \Re \left(x\right)\wedge \mathrm{i}x\notin {ℝ}^{+}\right)\leftrightarrow \left(x^2=A\wedge 0\le \Re \left(x\right)\wedge \mathrm{i}x\notin {ℝ}^{+}\right)\right)$$
3	2	riotabidv	$$⊢y=A\to \left(\iota x\in ℂ|\left(x^2=y\wedge 0\le \Re \left(x\right)\wedge \mathrm{i}x\notin {ℝ}^{+}\right)\right)=\left(\iota x\in ℂ|\left(x^2=A\wedge 0\le \Re \left(x\right)\wedge \mathrm{i}x\notin {ℝ}^{+}\right)\right)$$
4		df-sqrt	$$⊢\surd =\left(y\in ℂ⟼\left(\iota x\in ℂ|\left(x^2=y\wedge 0\le \Re \left(x\right)\wedge \mathrm{i}x\notin {ℝ}^{+}\right)\right)\right)$$
5		riotaex	$$⊢\left(\iota x\in ℂ|\left(x^2=A\wedge 0\le \Re \left(x\right)\wedge \mathrm{i}x\notin {ℝ}^{+}\right)\right)\in \mathrm{V}$$
6	3 4 5	fvmpt	$$⊢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)$$