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