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

Metamath Proof Explorer

Theorem ex-abs

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

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

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