Metamath Proof Explorer


Theorem blgt0

Description: A nonempty ball implies that the radius is positive. (Contributed by NM, 11-Mar-2007) (Revised by Mario Carneiro, 23-Aug-2015)

Ref Expression
Assertion blgt0 D ∞Met X P X R * A P ball D R 0 < R

Proof

Step Hyp Ref Expression
1 0xr 0 *
2 1 a1i D ∞Met X P X R * A P ball D R 0 *
3 simpl1 D ∞Met X P X R * A P ball D R D ∞Met X
4 simpl2 D ∞Met X P X R * A P ball D R P X
5 elbl D ∞Met X P X R * A P ball D R A X P D A < R
6 5 simprbda D ∞Met X P X R * A P ball D R A X
7 xmetcl D ∞Met X P X A X P D A *
8 3 4 6 7 syl3anc D ∞Met X P X R * A P ball D R P D A *
9 simpl3 D ∞Met X P X R * A P ball D R R *
10 xmetge0 D ∞Met X P X A X 0 P D A
11 3 4 6 10 syl3anc D ∞Met X P X R * A P ball D R 0 P D A
12 5 simplbda D ∞Met X P X R * A P ball D R P D A < R
13 2 8 9 11 12 xrlelttrd D ∞Met X P X R * A P ball D R 0 < R