Metamath Proof Explorer

Theorem bl2ioo

Description: A ball in terms of an open interval of reals. (Contributed by NM, 18-May-2007) (Revised by Mario Carneiro, 13-Nov-2013)

Ref Expression
Hypothesis remet.1 ⊢ D = abs ∘ − ↾ ℝ 2
Assertion bl2ioo ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ball ⁡ D B = A − B A + B

Proof

Step Hyp Ref Expression
1 remet.1 ⊢ D = abs ∘ − ↾ ℝ 2
2 1 remetdval ⊢ A ∈ ℝ ∧ x ∈ ℝ → A D x = A − x
3 recn ⊢ A ∈ ℝ → A ∈ ℂ
4 recn ⊢ x ∈ ℝ → x ∈ ℂ
5 abssub ⊢ A ∈ ℂ ∧ x ∈ ℂ → A − x = x − A
6 3 4 5 syl2an ⊢ A ∈ ℝ ∧ x ∈ ℝ → A − x = x − A
7 2 6 eqtrd ⊢ A ∈ ℝ ∧ x ∈ ℝ → A D x = x − A
8 7 breq1d ⊢ A ∈ ℝ ∧ x ∈ ℝ → A D x < B ↔ x − A < B
9 8 adantlr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ x ∈ ℝ → A D x < B ↔ x − A < B
10 absdiflt ⊢ x ∈ ℝ ∧ A ∈ ℝ ∧ B ∈ ℝ → x − A < B ↔ A − B < x ∧ x < A + B
11 10 3expb ⊢ x ∈ ℝ ∧ A ∈ ℝ ∧ B ∈ ℝ → x − A < B ↔ A − B < x ∧ x < A + B
12 11 ancoms ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ x ∈ ℝ → x − A < B ↔ A − B < x ∧ x < A + B
13 9 12 bitrd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ x ∈ ℝ → A D x < B ↔ A − B < x ∧ x < A + B
14 13 pm5.32da ⊢ A ∈ ℝ ∧ B ∈ ℝ → x ∈ ℝ ∧ A D x < B ↔ x ∈ ℝ ∧ A − B < x ∧ x < A + B
15 3anass ⊢ x ∈ ℝ ∧ A − B < x ∧ x < A + B ↔ x ∈ ℝ ∧ A − B < x ∧ x < A + B
16 14 15 bitr4di ⊢ A ∈ ℝ ∧ B ∈ ℝ → x ∈ ℝ ∧ A D x < B ↔ x ∈ ℝ ∧ A − B < x ∧ x < A + B
17 rexr ⊢ B ∈ ℝ → B ∈ ℝ *
18 1 rexmet ⊢ D ∈ ∞Met ⁡ ℝ
19 elbl ⊢ D ∈ ∞Met ⁡ ℝ ∧ A ∈ ℝ ∧ B ∈ ℝ * → x ∈ A ball ⁡ D B ↔ x ∈ ℝ ∧ A D x < B
20 18 19 mp3an1 ⊢ A ∈ ℝ ∧ B ∈ ℝ * → x ∈ A ball ⁡ D B ↔ x ∈ ℝ ∧ A D x < B
21 17 20 sylan2 ⊢ A ∈ ℝ ∧ B ∈ ℝ → x ∈ A ball ⁡ D B ↔ x ∈ ℝ ∧ A D x < B
22 resubcl ⊢ A ∈ ℝ ∧ B ∈ ℝ → A − B ∈ ℝ
23 readdcl ⊢ A ∈ ℝ ∧ B ∈ ℝ → A + B ∈ ℝ
24 rexr ⊢ A − B ∈ ℝ → A − B ∈ ℝ *
25 rexr ⊢ A + B ∈ ℝ → A + B ∈ ℝ *
26 elioo2 ⊢ A − B ∈ ℝ * ∧ A + B ∈ ℝ * → x ∈ A − B A + B ↔ x ∈ ℝ ∧ A − B < x ∧ x < A + B
27 24 25 26 syl2an ⊢ A − B ∈ ℝ ∧ A + B ∈ ℝ → x ∈ A − B A + B ↔ x ∈ ℝ ∧ A − B < x ∧ x < A + B
28 22 23 27 syl2anc ⊢ A ∈ ℝ ∧ B ∈ ℝ → x ∈ A − B A + B ↔ x ∈ ℝ ∧ A − B < x ∧ x < A + B
29 16 21 28 3bitr4d ⊢ A ∈ ℝ ∧ B ∈ ℝ → x ∈ A ball ⁡ D B ↔ x ∈ A − B A + B
30 29 eqrdv ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ball ⁡ D B = A − B A + B