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 ⊢ D = abs ∘ − ↾ ℝ 2
Assertion ioo2blex ⊢ A ∈ ℝ ∧ B ∈ ℝ → A B ∈ ran ⁡ ball ⁡ D

Proof

Step Hyp Ref Expression
1 remet.1 ⊢ D = abs ∘ − ↾ ℝ 2
2 1 ioo2bl ⊢ A ∈ ℝ ∧ B ∈ ℝ → A B = A + B 2 ball ⁡ D B − A 2
3 1 rexmet ⊢ D ∈ ∞Met ⁡ ℝ
4 readdcl ⊢ A ∈ ℝ ∧ B ∈ ℝ → A + B ∈ ℝ
5 4 rehalfcld ⊢ A ∈ ℝ ∧ B ∈ ℝ → A + B 2 ∈ ℝ
6 resubcl ⊢ B ∈ ℝ ∧ A ∈ ℝ → B − A ∈ ℝ
7 6 ancoms ⊢ A ∈ ℝ ∧ B ∈ ℝ → B − A ∈ ℝ
8 7 rehalfcld ⊢ A ∈ ℝ ∧ B ∈ ℝ → B − A 2 ∈ ℝ
9 8 rexrd ⊢ A ∈ ℝ ∧ B ∈ ℝ → B − A 2 ∈ ℝ *
10 blelrn ⊢ D ∈ ∞Met ⁡ ℝ ∧ A + B 2 ∈ ℝ ∧ B − A 2 ∈ ℝ * → A + B 2 ball ⁡ D B − A 2 ∈ ran ⁡ ball ⁡ D
11 3 5 9 10 mp3an2i ⊢ A ∈ ℝ ∧ B ∈ ℝ → A + B 2 ball ⁡ D B − A 2 ∈ ran ⁡ ball ⁡ D
12 2 11 eqeltrd ⊢ A ∈ ℝ ∧ B ∈ ℝ → A B ∈ ran ⁡ ball ⁡ D