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 ‘ ( 𝐶 − 𝐵 ) ) ) )