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 ⊢ 𝐷 = ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) )
Assertion bl2ioo ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ( ball ‘ 𝐷 ) 𝐵 ) = ( ( 𝐴 − 𝐵 ) (,) ( 𝐴 + 𝐵 ) ) )

Proof

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