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

Metamath Proof Explorer

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 ‘ 𝐷 ) )