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 AA=AA=A

Proof

Step Hyp Ref Expression
1 0re 0
2 letric 0A0AA0
3 1 2 mpan A0AA0
4 absid A0AA=A
5 4 ex A0AA=A
6 absnid AA0A=A
7 6 ex AA0A=A
8 5 7 orim12d A0AA0A=AA=A
9 3 8 mpd AA=AA=A