Theorem absnid

Description: For a negative number, its absolute value is its negation. (Contributed by NM, 27-Feb-2005)

	Ref	Expression
Assertion	absnid	|- ( ( A e. RR /\ A <_ 0 ) -> ( abs ` A ) = -u A )

Proof

Step	Hyp	Ref	Expression
1		le0neg1	|- ( A e. RR -> ( A <_ 0 <-> 0 <_ -u A ) )
2		recn	|- ( A e. RR -> A e. CC )
3		absneg	|- ( A e. CC -> ( abs ` -u A ) = ( abs ` A ) )
4	2 3	syl	|- ( A e. RR -> ( abs ` -u A ) = ( abs ` A ) )
5	4	adantr	|- ( ( A e. RR /\ 0 <_ -u A ) -> ( abs ` -u A ) = ( abs ` A ) )
6		renegcl	|- ( A e. RR -> -u A e. RR )
7		absid	|- ( ( -u A e. RR /\ 0 <_ -u A ) -> ( abs ` -u A ) = -u A )
8	6 7	sylan	|- ( ( A e. RR /\ 0 <_ -u A ) -> ( abs ` -u A ) = -u A )
9	5 8	eqtr3d	|- ( ( A e. RR /\ 0 <_ -u A ) -> ( abs ` A ) = -u A )
10	9	ex	|- ( A e. RR -> ( 0 <_ -u A -> ( abs ` A ) = -u A ) )
11	1 10	sylbid	|- ( A e. RR -> ( A <_ 0 -> ( abs ` A ) = -u A ) )
12	11	imp	|- ( ( A e. RR /\ A <_ 0 ) -> ( abs ` A ) = -u A )