Theorem absor

Description: The absolute value of a real number is either that number or its negative. (Contributed by NM, 27-Feb-2005)

	Ref	Expression
Assertion	absor	|- ( A e. RR -> ( ( abs ` A ) = A \/ ( abs ` A ) = -u A ) )

Proof

Step	Hyp	Ref	Expression
1		0re	|- 0 e. RR
2		letric	|- ( ( 0 e. RR /\ A e. RR ) -> ( 0 <_ A \/ A <_ 0 ) )
3	1 2	mpan	|- ( A e. RR -> ( 0 <_ A \/ A <_ 0 ) )
4		absid	|- ( ( A e. RR /\ 0 <_ A ) -> ( abs ` A ) = A )
5	4	ex	|- ( A e. RR -> ( 0 <_ A -> ( abs ` A ) = A ) )
6		absnid	|- ( ( A e. RR /\ A <_ 0 ) -> ( abs ` A ) = -u A )
7	6	ex	|- ( A e. RR -> ( A <_ 0 -> ( abs ` A ) = -u A ) )
8	5 7	orim12d	|- ( A e. RR -> ( ( 0 <_ A \/ A <_ 0 ) -> ( ( abs ` A ) = A \/ ( abs ` A ) = -u A ) ) )
9	3 8	mpd	|- ( A e. RR -> ( ( abs ` A ) = A \/ ( abs ` A ) = -u A ) )