Metamath Proof Explorer

Theorem cnblcld

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

Ref Expression
Hypothesis cnblcld.1 ⊢ D = abs ∘ −
Assertion cnblcld ⊢ R ∈ ℝ * → abs -1 0 R = x ∈ ℂ | 0 D x ≤ R

Proof

Step Hyp Ref Expression
1 cnblcld.1 ⊢ D = abs ∘ −
2 absf ⊢ abs : ℂ ⟶ ℝ
3 ffn ⊢ abs : ℂ ⟶ ℝ → abs Fn ℂ
4 elpreima ⊢ abs Fn ℂ → x ∈ abs -1 0 R ↔ x ∈ ℂ ∧ x ∈ 0 R
5 2 3 4 mp2b ⊢ x ∈ abs -1 0 R ↔ x ∈ ℂ ∧ x ∈ 0 R
6 df-3an ⊢ x ∈ ℝ * ∧ 0 ≤ x ∧ x ≤ R ↔ x ∈ ℝ * ∧ 0 ≤ x ∧ x ≤ R
7 abscl ⊢ x ∈ ℂ → x ∈ ℝ
8 7 rexrd ⊢ x ∈ ℂ → x ∈ ℝ *
9 absge0 ⊢ x ∈ ℂ → 0 ≤ x
10 8 9 jca ⊢ x ∈ ℂ → x ∈ ℝ * ∧ 0 ≤ x
11 10 adantl ⊢ R ∈ ℝ * ∧ x ∈ ℂ → x ∈ ℝ * ∧ 0 ≤ x
12 11 biantrurd ⊢ R ∈ ℝ * ∧ x ∈ ℂ → x ≤ R ↔ x ∈ ℝ * ∧ 0 ≤ x ∧ x ≤ R
13 6 12 bitr4id ⊢ R ∈ ℝ * ∧ x ∈ ℂ → x ∈ ℝ * ∧ 0 ≤ x ∧ x ≤ R ↔ x ≤ R
14 0xr ⊢ 0 ∈ ℝ *
15 simpl ⊢ R ∈ ℝ * ∧ x ∈ ℂ → R ∈ ℝ *
16 elicc1 ⊢ 0 ∈ ℝ * ∧ R ∈ ℝ * → x ∈ 0 R ↔ x ∈ ℝ * ∧ 0 ≤ x ∧ x ≤ R
17 14 15 16 sylancr ⊢ R ∈ ℝ * ∧ x ∈ ℂ → x ∈ 0 R ↔ x ∈ ℝ * ∧ 0 ≤ x ∧ x ≤ R
18 0cn ⊢ 0 ∈ ℂ
19 1 cnmetdval ⊢ 0 ∈ ℂ ∧ x ∈ ℂ → 0 D x = 0 − x
20 abssub ⊢ 0 ∈ ℂ ∧ x ∈ ℂ → 0 − x = x − 0
21 19 20 eqtrd ⊢ 0 ∈ ℂ ∧ x ∈ ℂ → 0 D x = x − 0
22 18 21 mpan ⊢ x ∈ ℂ → 0 D x = x − 0
23 subid1 ⊢ x ∈ ℂ → x − 0 = x
24 23 fveq2d ⊢ x ∈ ℂ → x − 0 = x
25 22 24 eqtrd ⊢ x ∈ ℂ → 0 D x = x
26 25 adantl ⊢ R ∈ ℝ * ∧ x ∈ ℂ → 0 D x = x
27 26 breq1d ⊢ R ∈ ℝ * ∧ x ∈ ℂ → 0 D x ≤ R ↔ x ≤ R
28 13 17 27 3bitr4d ⊢ R ∈ ℝ * ∧ x ∈ ℂ → x ∈ 0 R ↔ 0 D x ≤ R
29 28 pm5.32da ⊢ R ∈ ℝ * → x ∈ ℂ ∧ x ∈ 0 R ↔ x ∈ ℂ ∧ 0 D x ≤ R
30 5 29 bitrid ⊢ R ∈ ℝ * → x ∈ abs -1 0 R ↔ x ∈ ℂ ∧ 0 D x ≤ R
31 30 eqabdv ⊢ R ∈ ℝ * → abs -1 0 R = x | x ∈ ℂ ∧ 0 D x ≤ R
32 df-rab ⊢ x ∈ ℂ | 0 D x ≤ R = x | x ∈ ℂ ∧ 0 D x ≤ R
33 31 32 eqtr4di ⊢ R ∈ ℝ * → abs -1 0 R = x ∈ ℂ | 0 D x ≤ R