Metamath Proof Explorer


Theorem elicc4abs

Description: Membership in a symmetric closed real interval. (Contributed by Stefan O'Rear, 16-Nov-2014)

Ref Expression
Assertion elicc4abs ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐶 ∈ ( ( 𝐴𝐵 ) [,] ( 𝐴 + 𝐵 ) ) ↔ ( abs ‘ ( 𝐶𝐴 ) ) ≤ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 resubcl ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴𝐵 ) ∈ ℝ )
2 1 3adant3 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴𝐵 ) ∈ ℝ )
3 2 rexrd ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴𝐵 ) ∈ ℝ* )
4 readdcl ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 + 𝐵 ) ∈ ℝ )
5 4 3adant3 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 + 𝐵 ) ∈ ℝ )
6 5 rexrd ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 + 𝐵 ) ∈ ℝ* )
7 rexr ( 𝐶 ∈ ℝ → 𝐶 ∈ ℝ* )
8 7 3ad2ant3 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐶 ∈ ℝ* )
9 elicc4 ( ( ( 𝐴𝐵 ) ∈ ℝ* ∧ ( 𝐴 + 𝐵 ) ∈ ℝ*𝐶 ∈ ℝ* ) → ( 𝐶 ∈ ( ( 𝐴𝐵 ) [,] ( 𝐴 + 𝐵 ) ) ↔ ( ( 𝐴𝐵 ) ≤ 𝐶𝐶 ≤ ( 𝐴 + 𝐵 ) ) ) )
10 3 6 8 9 syl3anc ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐶 ∈ ( ( 𝐴𝐵 ) [,] ( 𝐴 + 𝐵 ) ) ↔ ( ( 𝐴𝐵 ) ≤ 𝐶𝐶 ≤ ( 𝐴 + 𝐵 ) ) ) )
11 absdifle ( ( 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( abs ‘ ( 𝐶𝐴 ) ) ≤ 𝐵 ↔ ( ( 𝐴𝐵 ) ≤ 𝐶𝐶 ≤ ( 𝐴 + 𝐵 ) ) ) )
12 11 3coml ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( abs ‘ ( 𝐶𝐴 ) ) ≤ 𝐵 ↔ ( ( 𝐴𝐵 ) ≤ 𝐶𝐶 ≤ ( 𝐴 + 𝐵 ) ) ) )
13 10 12 bitr4d ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐶 ∈ ( ( 𝐴𝐵 ) [,] ( 𝐴 + 𝐵 ) ) ↔ ( abs ‘ ( 𝐶𝐴 ) ) ≤ 𝐵 ) )