Theorem ex-abs

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

	Ref	Expression
Assertion	ex-abs	⊢ ( abs ‘ - 2 ) = 2

Proof

Step	Hyp	Ref	Expression
1		2cn	⊢ 2 ∈ ℂ
2	1	absnegi	⊢ ( abs ‘ - 2 ) = ( abs ‘ 2 )
3		2re	⊢ 2 ∈ ℝ
4		0le2	⊢ 0 ≤ 2
5		absid	⊢ ( ( 2 ∈ ℝ ∧ 0 ≤ 2 ) → ( abs ‘ 2 ) = 2 )
6	3 4 5	mp2an	⊢ ( abs ‘ 2 ) = 2
7	2 6	eqtri	⊢ ( abs ‘ - 2 ) = 2