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

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