Theorem absdifle

Description: The absolute value of a difference and 'less than or equal to' relation. (Contributed by Paul Chapman, 18-Sep-2007)

	Ref	Expression
Assertion	absdifle	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( abs ‘ ( 𝐴 − 𝐵 ) ) ≤ 𝐶 ↔ ( ( 𝐵 − 𝐶 ) ≤ 𝐴 ∧ 𝐴 ≤ ( 𝐵 + 𝐶 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		resubcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 − 𝐵 ) ∈ ℝ )
2		absle	⊢ ( ( ( 𝐴 − 𝐵 ) ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( abs ‘ ( 𝐴 − 𝐵 ) ) ≤ 𝐶 ↔ ( - 𝐶 ≤ ( 𝐴 − 𝐵 ) ∧ ( 𝐴 − 𝐵 ) ≤ 𝐶 ) ) )
3	1 2	stoic3	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( abs ‘ ( 𝐴 − 𝐵 ) ) ≤ 𝐶 ↔ ( - 𝐶 ≤ ( 𝐴 − 𝐵 ) ∧ ( 𝐴 − 𝐵 ) ≤ 𝐶 ) ) )
4		renegcl	⊢ ( 𝐶 ∈ ℝ → - 𝐶 ∈ ℝ )
5		leaddsub2	⊢ ( ( 𝐵 ∈ ℝ ∧ - 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( ( 𝐵 + - 𝐶 ) ≤ 𝐴 ↔ - 𝐶 ≤ ( 𝐴 − 𝐵 ) ) )
6	4 5	syl3an2	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( ( 𝐵 + - 𝐶 ) ≤ 𝐴 ↔ - 𝐶 ≤ ( 𝐴 − 𝐵 ) ) )
7	6	3comr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐵 + - 𝐶 ) ≤ 𝐴 ↔ - 𝐶 ≤ ( 𝐴 − 𝐵 ) ) )
8		recn	⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℂ )
9		recn	⊢ ( 𝐶 ∈ ℝ → 𝐶 ∈ ℂ )
10		negsub	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐵 + - 𝐶 ) = ( 𝐵 − 𝐶 ) )
11	8 9 10	syl2an	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 + - 𝐶 ) = ( 𝐵 − 𝐶 ) )
12	11	3adant1	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 + - 𝐶 ) = ( 𝐵 − 𝐶 ) )
13	12	breq1d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐵 + - 𝐶 ) ≤ 𝐴 ↔ ( 𝐵 − 𝐶 ) ≤ 𝐴 ) )
14	7 13	bitr3d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( - 𝐶 ≤ ( 𝐴 − 𝐵 ) ↔ ( 𝐵 − 𝐶 ) ≤ 𝐴 ) )
15		lesubadd2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 − 𝐵 ) ≤ 𝐶 ↔ 𝐴 ≤ ( 𝐵 + 𝐶 ) ) )
16	14 15	anbi12d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( - 𝐶 ≤ ( 𝐴 − 𝐵 ) ∧ ( 𝐴 − 𝐵 ) ≤ 𝐶 ) ↔ ( ( 𝐵 − 𝐶 ) ≤ 𝐴 ∧ 𝐴 ≤ ( 𝐵 + 𝐶 ) ) ) )
17	3 16	bitrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( abs ‘ ( 𝐴 − 𝐵 ) ) ≤ 𝐶 ↔ ( ( 𝐵 − 𝐶 ) ≤ 𝐴 ∧ 𝐴 ≤ ( 𝐵 + 𝐶 ) ) ) )