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 ℂ$

Step	Hyp	Ref	Expression
1		sqrtval	$⊢ A \in ℂ \to \sqrt{A} = (ι x \in ℂ \| (x^{2} = A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+}))$
2		sqreu	$⊢ A \in ℂ \to \exists! x \in ℂ (x^{2} = A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+})$
3		riotacl	$⊢ \exists! x \in ℂ (x^{2} = A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+}) \to (ι x \in ℂ \| (x^{2} = A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+})) \in ℂ$
4	2 3	syl	$⊢ A \in ℂ \to (ι x \in ℂ \| (x^{2} = A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+})) \in ℂ$
5	1 4	eqeltrd	$⊢ A \in ℂ \to \sqrt{A} \in ℂ$

Metamath Proof Explorer