Theorem ex-abs

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

	Ref	Expression
Assertion	ex-abs	|- ( abs ` -u 2 ) = 2

Proof

Step	Hyp	Ref	Expression
1		2cn	|- 2 e. CC
2	1	absnegi	|- ( abs ` -u 2 ) = ( abs ` 2 )
3		2re	|- 2 e. RR
4		0le2	|- 0 <_ 2
5		absid	|- ( ( 2 e. RR /\ 0 <_ 2 ) -> ( abs ` 2 ) = 2 )
6	3 4 5	mp2an	|- ( abs ` 2 ) = 2
7	2 6	eqtri	|- ( abs ` -u 2 ) = 2