This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem abs0

Description: The absolute value of 0. (Contributed by NM, 26-Mar-2005) (Revised by Mario Carneiro, 29-May-2016)

		Ref	Expression
	Assertion	abs0	$⊢ \|0\| = 0$

Step	Hyp	Ref	Expression
1		0cn	$⊢ 0 \in ℂ$
2		absval	$⊢ 0 \in ℂ \to \|0\| = \sqrt{0 \cdot \overline{0}}$
3	1 2	ax-mp	$⊢ \|0\| = \sqrt{0 \cdot \overline{0}}$
4	1	cjcli	$⊢ \overline{0} \in ℂ$
5	4	mul02i	$⊢ 0 \cdot \overline{0} = 0$
6	5	fveq2i	$⊢ \sqrt{0 \cdot \overline{0}} = \sqrt{0}$
7		sqrt0	$⊢ \sqrt{0} = 0$
8	3 6 7	3eqtri	$⊢ \|0\| = 0$