# Metamath Proof Explorer

## Theorem abs3dif

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

Ref Expression
Assertion abs3dif ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( abs ‘ ( 𝐴𝐵 ) ) ≤ ( ( abs ‘ ( 𝐴𝐶 ) ) + ( abs ‘ ( 𝐶𝐵 ) ) ) )

### Proof

Step Hyp Ref Expression
1 npncan ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴𝐶 ) + ( 𝐶𝐵 ) ) = ( 𝐴𝐵 ) )
2 1 3com23 ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴𝐶 ) + ( 𝐶𝐵 ) ) = ( 𝐴𝐵 ) )
3 2 fveq2d ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( abs ‘ ( ( 𝐴𝐶 ) + ( 𝐶𝐵 ) ) ) = ( abs ‘ ( 𝐴𝐵 ) ) )
4 subcl ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴𝐶 ) ∈ ℂ )
5 4 3adant2 ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴𝐶 ) ∈ ℂ )
6 subcl ( ( 𝐶 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐶𝐵 ) ∈ ℂ )
7 6 ancoms ( ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐶𝐵 ) ∈ ℂ )
8 7 3adant1 ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐶𝐵 ) ∈ ℂ )
9 abstri ( ( ( 𝐴𝐶 ) ∈ ℂ ∧ ( 𝐶𝐵 ) ∈ ℂ ) → ( abs ‘ ( ( 𝐴𝐶 ) + ( 𝐶𝐵 ) ) ) ≤ ( ( abs ‘ ( 𝐴𝐶 ) ) + ( abs ‘ ( 𝐶𝐵 ) ) ) )
10 5 8 9 syl2anc ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( abs ‘ ( ( 𝐴𝐶 ) + ( 𝐶𝐵 ) ) ) ≤ ( ( abs ‘ ( 𝐴𝐶 ) ) + ( abs ‘ ( 𝐶𝐵 ) ) ) )
11 3 10 eqbrtrrd ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( abs ‘ ( 𝐴𝐵 ) ) ≤ ( ( abs ‘ ( 𝐴𝐶 ) ) + ( abs ‘ ( 𝐶𝐵 ) ) ) )