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