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