sqrtval

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

		Ref	Expression
	Assertion	sqrtval	$⊢ A \in ℂ \to \sqrt{A} = (ι x \in ℂ \| (x^{2} = A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+}))$

Step	Hyp	Ref	Expression
1		eqeq2	$⊢ y = A \to (x^{2} = y \leftrightarrow x^{2} = A)$
2	1	3anbi1d	$⊢ y = A \to ((x^{2} = y \land 0 \leq ℜ (x) \land i x \notin ℝ^{+}) \leftrightarrow (x^{2} = A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+}))$
3	2	riotabidv	$⊢ y = A \to (ι x \in ℂ \| (x^{2} = y \land 0 \leq ℜ (x) \land i x \notin ℝ^{+})) = (ι x \in ℂ \| (x^{2} = A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+}))$
4		df-sqrt	$⊢ \sqrt = (y \in ℂ ⟼ (ι x \in ℂ \| (x^{2} = y \land 0 \leq ℜ (x) \land i x \notin ℝ^{+})))$
5		riotaex	$⊢ (ι x \in ℂ \| (x^{2} = A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+})) \in V$
6	3 4 5	fvmpt	$⊢ A \in ℂ \to \sqrt{A} = (ι x \in ℂ \| (x^{2} = A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+}))$

Metamath Proof Explorer