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∈ℝ→Aball⁡DB=A−BA+B

Proof

Step Hyp Ref Expression
1 remet.1 ⊢D=abs∘−↾ℝ2
2 1 remetdval ⊢A∈ℝ∧x∈ℝ→ADx=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∈ℝ→ADx=x−A
8 7 breq1d ⊢A∈ℝ∧x∈ℝ→ADx<B↔x−A<B
9 8 adantlr ⊢A∈ℝ∧B∈ℝ∧x∈ℝ→ADx<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∈ℝ→ADx<B↔A−B<x∧x<A+B
14 13 pm5.32da ⊢A∈ℝ∧B∈ℝ→x∈ℝ∧ADx<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∈ℝ∧ADx<B↔x∈ℝ∧A−B<x∧x<A+B
17 rexr ⊢B∈ℝ→B∈ℝ*
18 1 rexmet ⊢D∈∞Met⁡ℝ
19 elbl ⊢D∈∞Met⁡ℝ∧A∈ℝ∧B∈ℝ*→x∈Aball⁡DB↔x∈ℝ∧ADx<B
20 18 19 mp3an1 ⊢A∈ℝ∧B∈ℝ*→x∈Aball⁡DB↔x∈ℝ∧ADx<B
21 17 20 sylan2 ⊢A∈ℝ∧B∈ℝ→x∈Aball⁡DB↔x∈ℝ∧ADx<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−BA+B↔x∈ℝ∧A−B<x∧x<A+B
27 24 25 26 syl2an ⊢A−B∈ℝ∧A+B∈ℝ→x∈A−BA+B↔x∈ℝ∧A−B<x∧x<A+B
28 22 23 27 syl2anc ⊢A∈ℝ∧B∈ℝ→x∈A−BA+B↔x∈ℝ∧A−B<x∧x<A+B
29 16 21 28 3bitr4d ⊢A∈ℝ∧B∈ℝ→x∈Aball⁡DB↔x∈A−BA+B
30 29 eqrdv ⊢A∈ℝ∧B∈ℝ→Aball⁡DB=A−BA+B