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	$$⊢\left|0\right|=0$$

Proof

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