Theorem ioo2blex

Description: An open interval of reals in terms of a ball. (Contributed by Mario Carneiro, 14-Nov-2013)

	Ref	Expression
Hypothesis	remet.1	⊢ 𝐷 = ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) )
Assertion	ioo2blex	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 (,) 𝐵 ) ∈ ran ( ball ‘ 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		remet.1	⊢ 𝐷 = ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) )
2	1	ioo2bl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 (,) 𝐵 ) = ( ( ( 𝐴 + 𝐵 ) / 2 ) ( ball ‘ 𝐷 ) ( ( 𝐵 − 𝐴 ) / 2 ) ) )
3	1	rexmet	⊢ 𝐷 ∈ ( ∞Met ‘ ℝ )
4		readdcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 + 𝐵 ) ∈ ℝ )
5	4	rehalfcld	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 + 𝐵 ) / 2 ) ∈ ℝ )
6		resubcl	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 𝐵 − 𝐴 ) ∈ ℝ )
7	6	ancoms	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐵 − 𝐴 ) ∈ ℝ )
8	7	rehalfcld	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐵 − 𝐴 ) / 2 ) ∈ ℝ )
9	8	rexrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐵 − 𝐴 ) / 2 ) ∈ ℝ* )
10		blelrn	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ ℝ ) ∧ ( ( 𝐴 + 𝐵 ) / 2 ) ∈ ℝ ∧ ( ( 𝐵 − 𝐴 ) / 2 ) ∈ ℝ* ) → ( ( ( 𝐴 + 𝐵 ) / 2 ) ( ball ‘ 𝐷 ) ( ( 𝐵 − 𝐴 ) / 2 ) ) ∈ ran ( ball ‘ 𝐷 ) )
11	3 5 9 10	mp3an2i	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( ( 𝐴 + 𝐵 ) / 2 ) ( ball ‘ 𝐷 ) ( ( 𝐵 − 𝐴 ) / 2 ) ) ∈ ran ( ball ‘ 𝐷 ) )
12	2 11	eqeltrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 (,) 𝐵 ) ∈ ran ( ball ‘ 𝐷 ) )