Metamath Proof Explorer

Theorem cnbl0

Description: Two ways to write the open ball centered at zero. (Contributed by Mario Carneiro, 8-Sep-2015)

Ref Expression
Hypothesis cnblcld.1 ⊢ D = abs ∘ −
Assertion cnbl0 ⊢ R ∈ ℝ * → abs -1 0 R = 0 ball ⁡ D R

Proof

Step Hyp Ref Expression
1 cnblcld.1 ⊢ D = abs ∘ −
2 df-3an ⊢ x ∈ ℝ ∧ 0 ≤ x ∧ x < R ↔ x ∈ ℝ ∧ 0 ≤ x ∧ x < R
3 abscl ⊢ x ∈ ℂ → x ∈ ℝ
4 absge0 ⊢ x ∈ ℂ → 0 ≤ x
5 3 4 jca ⊢ x ∈ ℂ → x ∈ ℝ ∧ 0 ≤ x
6 5 adantl ⊢ R ∈ ℝ * ∧ x ∈ ℂ → x ∈ ℝ ∧ 0 ≤ x
7 6 biantrurd ⊢ R ∈ ℝ * ∧ x ∈ ℂ → x < R ↔ x ∈ ℝ ∧ 0 ≤ x ∧ x < R
8 2 7 bitr4id ⊢ R ∈ ℝ * ∧ x ∈ ℂ → x ∈ ℝ ∧ 0 ≤ x ∧ x < R ↔ x < R
9 0re ⊢ 0 ∈ ℝ
10 simpl ⊢ R ∈ ℝ * ∧ x ∈ ℂ → R ∈ ℝ *
11 elico2 ⊢ 0 ∈ ℝ ∧ R ∈ ℝ * → x ∈ 0 R ↔ x ∈ ℝ ∧ 0 ≤ x ∧ x < R
12 9 10 11 sylancr ⊢ R ∈ ℝ * ∧ x ∈ ℂ → x ∈ 0 R ↔ x ∈ ℝ ∧ 0 ≤ x ∧ x < R
13 0cn ⊢ 0 ∈ ℂ
14 1 cnmetdval ⊢ 0 ∈ ℂ ∧ x ∈ ℂ → 0 D x = 0 − x
15 abssub ⊢ 0 ∈ ℂ ∧ x ∈ ℂ → 0 − x = x − 0
16 14 15 eqtrd ⊢ 0 ∈ ℂ ∧ x ∈ ℂ → 0 D x = x − 0
17 13 16 mpan ⊢ x ∈ ℂ → 0 D x = x − 0
18 subid1 ⊢ x ∈ ℂ → x − 0 = x
19 18 fveq2d ⊢ x ∈ ℂ → x − 0 = x
20 17 19 eqtrd ⊢ x ∈ ℂ → 0 D x = x
21 20 adantl ⊢ R ∈ ℝ * ∧ x ∈ ℂ → 0 D x = x
22 21 breq1d ⊢ R ∈ ℝ * ∧ x ∈ ℂ → 0 D x < R ↔ x < R
23 8 12 22 3bitr4d ⊢ R ∈ ℝ * ∧ x ∈ ℂ → x ∈ 0 R ↔ 0 D x < R
24 23 pm5.32da ⊢ R ∈ ℝ * → x ∈ ℂ ∧ x ∈ 0 R ↔ x ∈ ℂ ∧ 0 D x < R
25 absf ⊢ abs : ℂ ⟶ ℝ
26 ffn ⊢ abs : ℂ ⟶ ℝ → abs Fn ℂ
27 25 26 ax-mp ⊢ abs Fn ℂ
28 elpreima ⊢ abs Fn ℂ → x ∈ abs -1 0 R ↔ x ∈ ℂ ∧ x ∈ 0 R
29 27 28 mp1i ⊢ R ∈ ℝ * → x ∈ abs -1 0 R ↔ x ∈ ℂ ∧ x ∈ 0 R
30 cnxmet ⊢ abs ∘ − ∈ ∞Met ⁡ ℂ
31 1 30 eqeltri ⊢ D ∈ ∞Met ⁡ ℂ
32 elbl ⊢ D ∈ ∞Met ⁡ ℂ ∧ 0 ∈ ℂ ∧ R ∈ ℝ * → x ∈ 0 ball ⁡ D R ↔ x ∈ ℂ ∧ 0 D x < R
33 31 13 32 mp3an12 ⊢ R ∈ ℝ * → x ∈ 0 ball ⁡ D R ↔ x ∈ ℂ ∧ 0 D x < R
34 24 29 33 3bitr4d ⊢ R ∈ ℝ * → x ∈ abs -1 0 R ↔ x ∈ 0 ball ⁡ D R
35 34 eqrdv ⊢ R ∈ ℝ * → abs -1 0 R = 0 ball ⁡ D R