Metamath Proof Explorer


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 ‘ ( 𝐴𝐵 ) ) ≤ 𝐶 ↔ ( ( 𝐵𝐶 ) ≤ 𝐴𝐴 ≤ ( 𝐵 + 𝐶 ) ) ) )