Metamath Proof Explorer


Theorem abssubi

Description: Swapping order of subtraction doesn't change the absolute value. Example of Apostol p. 363. (Contributed by NM, 1-Oct-1999)

Ref Expression
Hypotheses absvalsqi.1 A
abssub.2 B
Assertion abssubi A B = B A

Proof

Step Hyp Ref Expression
1 absvalsqi.1 A
2 abssub.2 B
3 abssub A B A B = B A
4 1 2 3 mp2an A B = B A