Description: Swapping order of subtraction doesn't change the absolute value. (Contributed by NM, 1-Oct-1999) (Proof shortened by Mario Carneiro, 29-May-2016)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | abssub | |- ( ( A e. CC /\ B e. CC ) -> ( abs ` ( A - B ) ) = ( abs ` ( B - A ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | subcl | |- ( ( A e. CC /\ B e. CC ) -> ( A - B ) e. CC ) |
|
| 2 | absneg | |- ( ( A - B ) e. CC -> ( abs ` -u ( A - B ) ) = ( abs ` ( A - B ) ) ) |
|
| 3 | 1 2 | syl | |- ( ( A e. CC /\ B e. CC ) -> ( abs ` -u ( A - B ) ) = ( abs ` ( A - B ) ) ) |
| 4 | negsubdi2 | |- ( ( A e. CC /\ B e. CC ) -> -u ( A - B ) = ( B - A ) ) |
|
| 5 | 4 | fveq2d | |- ( ( A e. CC /\ B e. CC ) -> ( abs ` -u ( A - B ) ) = ( abs ` ( B - A ) ) ) |
| 6 | 3 5 | eqtr3d | |- ( ( A e. CC /\ B e. CC ) -> ( abs ` ( A - B ) ) = ( abs ` ( B - A ) ) ) |