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 AB=BA

Proof

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