Metamath Proof Explorer


Theorem abssuble0

Description: Absolute value of a nonpositive difference. (Contributed by FL, 3-Jan-2008)

Ref Expression
Assertion abssuble0 ABABAB=BA

Proof

Step Hyp Ref Expression
1 recn AA
2 recn BB
3 abssub ABAB=BA
4 1 2 3 syl2an ABAB=BA
5 4 3adant3 ABABAB=BA
6 abssubge0 ABABBA=BA
7 5 6 eqtrd ABABAB=BA