Metamath Proof Explorer

Theorem abs3dif

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

Ref Expression
Assertion abs3dif ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A − B ≤ A − C + C − B

Proof

Step Hyp Ref Expression
1 npncan ⊢ A ∈ ℂ ∧ C ∈ ℂ ∧ B ∈ ℂ → A − C + C - B = A − B
2 1 3com23 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A − C + C - B = A − B
3 2 fveq2d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A − C + C - B = A − B
4 subcl ⊢ A ∈ ℂ ∧ C ∈ ℂ → A − C ∈ ℂ
5 4 3adant2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A − C ∈ ℂ
6 subcl ⊢ C ∈ ℂ ∧ B ∈ ℂ → C − B ∈ ℂ
7 6 ancoms ⊢ B ∈ ℂ ∧ C ∈ ℂ → C − B ∈ ℂ
8 7 3adant1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → C − B ∈ ℂ
9 abstri ⊢ A − C ∈ ℂ ∧ C − B ∈ ℂ → A − C + C - B ≤ A − C + C − B
10 5 8 9 syl2anc ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A − C + C - B ≤ A − C + C − B
11 3 10 eqbrtrrd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A − B ≤ A − C + C − B