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-10R=x∈ℂ|0Dx≤R

Proof

Step Hyp Ref Expression
1 cnblcld.1 ⊢D=abs∘−
2 absf ⊢abs:ℂ⟶ℝ
3 ffn ⊢abs:ℂ⟶ℝ→absFnℂ
4 elpreima ⊢absFnℂ→x∈abs-10R↔x∈ℂ∧x∈0R
5 2 3 4 mp2b ⊢x∈abs-10R↔x∈ℂ∧x∈0R
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∈0R↔x∈ℝ*∧0≤x∧x≤R
17 14 15 16 sylancr ⊢R∈ℝ*∧x∈ℂ→x∈0R↔x∈ℝ*∧0≤x∧x≤R
18 0cn ⊢0∈ℂ
19 1 cnmetdval ⊢0∈ℂ∧x∈ℂ→0Dx=0−x
20 abssub ⊢0∈ℂ∧x∈ℂ→0−x=x−0
21 19 20 eqtrd ⊢0∈ℂ∧x∈ℂ→0Dx=x−0
22 18 21 mpan ⊢x∈ℂ→0Dx=x−0
23 subid1 ⊢x∈ℂ→x−0=x
24 23 fveq2d ⊢x∈ℂ→x−0=x
25 22 24 eqtrd ⊢x∈ℂ→0Dx=x
26 25 adantl ⊢R∈ℝ*∧x∈ℂ→0Dx=x
27 26 breq1d ⊢R∈ℝ*∧x∈ℂ→0Dx≤R↔x≤R
28 13 17 27 3bitr4d ⊢R∈ℝ*∧x∈ℂ→x∈0R↔0Dx≤R
29 28 pm5.32da ⊢R∈ℝ*→x∈ℂ∧x∈0R↔x∈ℂ∧0Dx≤R
30 5 29 bitrid ⊢R∈ℝ*→x∈abs-10R↔x∈ℂ∧0Dx≤R
31 30 eqabdv ⊢R∈ℝ*→abs-10R=x|x∈ℂ∧0Dx≤R
32 df-rab ⊢x∈ℂ|0Dx≤R=x|x∈ℂ∧0Dx≤R
33 31 32 eqtr4di ⊢R∈ℝ*→abs-10R=x∈ℂ|0Dx≤R