Theorem ex-abs

Description: Example for df-abs . (Contributed by AV, 4-Sep-2021)

	Ref	Expression
Assertion	ex-abs	$$⊢\left|-2\right|=2$$

Proof

Step	Hyp	Ref	Expression
1		2cn	$$⊢2\in ℂ$$
2	1	absnegi	$$⊢\left|-2\right|=\left|2\right|$$
3		2re	$$⊢2\in ℝ$$
4		0le2	$$⊢0\le 2$$
5		absid	$$⊢\left(2\in ℝ\wedge 0\le 2\right)\to \left|2\right|=2$$
6	3 4 5	mp2an	$$⊢\left|2\right|=2$$
7	2 6	eqtri	$$⊢\left|-2\right|=2$$