# Metamath Proof Explorer

## Theorem abs3dif

Description: Absolute value of differences around common element. (Contributed by FL, 9-Oct-2006)

Ref Expression
Assertion abs3dif ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to \left|{A}-{B}\right|\le \left|{A}-{C}\right|+\left|{C}-{B}\right|$

### Proof

Step Hyp Ref Expression
1 npncan ${⊢}\left({A}\in ℂ\wedge {C}\in ℂ\wedge {B}\in ℂ\right)\to \left({A}-{C}\right)+{C}-{B}={A}-{B}$
2 1 3com23 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to \left({A}-{C}\right)+{C}-{B}={A}-{B}$
3 2 fveq2d ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to \left|\left({A}-{C}\right)+{C}-{B}\right|=\left|{A}-{B}\right|$
4 subcl ${⊢}\left({A}\in ℂ\wedge {C}\in ℂ\right)\to {A}-{C}\in ℂ$
5 4 3adant2 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to {A}-{C}\in ℂ$
6 subcl ${⊢}\left({C}\in ℂ\wedge {B}\in ℂ\right)\to {C}-{B}\in ℂ$
7 6 ancoms ${⊢}\left({B}\in ℂ\wedge {C}\in ℂ\right)\to {C}-{B}\in ℂ$
8 7 3adant1 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to {C}-{B}\in ℂ$
9 abstri ${⊢}\left({A}-{C}\in ℂ\wedge {C}-{B}\in ℂ\right)\to \left|\left({A}-{C}\right)+{C}-{B}\right|\le \left|{A}-{C}\right|+\left|{C}-{B}\right|$
10 5 8 9 syl2anc ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to \left|\left({A}-{C}\right)+{C}-{B}\right|\le \left|{A}-{C}\right|+\left|{C}-{B}\right|$
11 3 10 eqbrtrrd ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to \left|{A}-{B}\right|\le \left|{A}-{C}\right|+\left|{C}-{B}\right|$