sqrt0

Description: Square root of zero. (Contributed by Mario Carneiro, 9-Jul-2013)

		Ref	Expression
	Assertion	sqrt0	$⊢ \sqrt{0} = 0$

Step	Hyp	Ref	Expression
1		0cn	$⊢ 0 \in ℂ$
2		sqrtval	$⊢ 0 \in ℂ \to \sqrt{0} = (ι x \in ℂ \| (x^{2} = 0 \land 0 \leq ℜ (x) \land i x \notin ℝ^{+}))$
3	1 2	ax-mp	$⊢ \sqrt{0} = (ι x \in ℂ \| (x^{2} = 0 \land 0 \leq ℜ (x) \land i x \notin ℝ^{+}))$
4		id	$⊢ 0 \in ℂ \to 0 \in ℂ$
5		sqr0lem	$⊢ (x \in ℂ \land (x^{2} = 0 \land 0 \leq ℜ (x) \land i x \notin ℝ^{+})) \leftrightarrow x = 0$
6	5	biimpi	$⊢ (x \in ℂ \land (x^{2} = 0 \land 0 \leq ℜ (x) \land i x \notin ℝ^{+})) \to x = 0$
7	6	ex	$⊢ x \in ℂ \to ((x^{2} = 0 \land 0 \leq ℜ (x) \land i x \notin ℝ^{+}) \to x = 0)$
8		simpr	$⊢ (x \in ℂ \land (x^{2} = 0 \land 0 \leq ℜ (x) \land i x \notin ℝ^{+})) \to (x^{2} = 0 \land 0 \leq ℜ (x) \land i x \notin ℝ^{+})$
9	5 8	sylbir	$⊢ x = 0 \to (x^{2} = 0 \land 0 \leq ℜ (x) \land i x \notin ℝ^{+})$
10	7 9	impbid1	$⊢ x \in ℂ \to ((x^{2} = 0 \land 0 \leq ℜ (x) \land i x \notin ℝ^{+}) \leftrightarrow x = 0)$
11	10	adantl	$⊢ (0 \in ℂ \land x \in ℂ) \to ((x^{2} = 0 \land 0 \leq ℜ (x) \land i x \notin ℝ^{+}) \leftrightarrow x = 0)$
12	4 11	riota5	$⊢ 0 \in ℂ \to (ι x \in ℂ \| (x^{2} = 0 \land 0 \leq ℜ (x) \land i x \notin ℝ^{+})) = 0$
13	1 12	ax-mp	$⊢ (ι x \in ℂ \| (x^{2} = 0 \land 0 \leq ℜ (x) \land i x \notin ℝ^{+})) = 0$
14	3 13	eqtri	$⊢ \sqrt{0} = 0$

Metamath Proof Explorer