This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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