sqrt0

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

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

Proof

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		sqeq0	$⊢ x \in ℂ \to (x^{2} = 0 \leftrightarrow x = 0)$
6	5	biimpa	$⊢ (x \in ℂ \land x^{2} = 0) \to x = 0$
7	6	3ad2antr1	$⊢ (x \in ℂ \land (x^{2} = 0 \land 0 \leq ℜ (x) \land i x \notin ℝ^{+})) \to x = 0$
8	7	ex	$⊢ x \in ℂ \to ((x^{2} = 0 \land 0 \leq ℜ (x) \land i x \notin ℝ^{+}) \to x = 0)$
9		sq0i	$⊢ x = 0 \to x^{2} = 0$
10		0le0	$⊢ 0 \leq 0$
11		fveq2	$⊢ x = 0 \to ℜ (x) = ℜ (0)$
12		re0	$⊢ ℜ (0) = 0$
13	11 12	eqtrdi	$⊢ x = 0 \to ℜ (x) = 0$
14	10 13	breqtrrid	$⊢ x = 0 \to 0 \leq ℜ (x)$
15		0re	$⊢ 0 \in ℝ$
16		eleq1	$⊢ x = 0 \to (x \in ℝ \leftrightarrow 0 \in ℝ)$
17	15 16	mpbiri	$⊢ x = 0 \to x \in ℝ$
18		rennim	$⊢ x \in ℝ \to i x \notin ℝ^{+}$
19	17 18	syl	$⊢ x = 0 \to i x \notin ℝ^{+}$
20	9 14 19	3jca	$⊢ x = 0 \to (x^{2} = 0 \land 0 \leq ℜ (x) \land i x \notin ℝ^{+})$
21	8 20	impbid1	$⊢ x \in ℂ \to ((x^{2} = 0 \land 0 \leq ℜ (x) \land i x \notin ℝ^{+}) \leftrightarrow x = 0)$
22	21	adantl	$⊢ (0 \in ℂ \land x \in ℂ) \to ((x^{2} = 0 \land 0 \leq ℜ (x) \land i x \notin ℝ^{+}) \leftrightarrow x = 0)$
23	4 22	riota5	$⊢ 0 \in ℂ \to (ι x \in ℂ \| (x^{2} = 0 \land 0 \leq ℜ (x) \land i x \notin ℝ^{+})) = 0$
24	1 23	ax-mp	$⊢ (ι x \in ℂ \| (x^{2} = 0 \land 0 \leq ℜ (x) \land i x \notin ℝ^{+})) = 0$
25	3 24	eqtri	$⊢ \sqrt{0} = 0$

Metamath Proof Explorer

Theorem sqrt0

Proof