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

Metamath Proof Explorer

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 ) )