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∞MetXPXR*APballDR0<R

Proof

Step Hyp Ref Expression
1 0xr 0*
2 1 a1i D∞MetXPXR*APballDR0*
3 simpl1 D∞MetXPXR*APballDRD∞MetX
4 simpl2 D∞MetXPXR*APballDRPX
5 elbl D∞MetXPXR*APballDRAXPDA<R
6 5 simprbda D∞MetXPXR*APballDRAX
7 xmetcl D∞MetXPXAXPDA*
8 3 4 6 7 syl3anc D∞MetXPXR*APballDRPDA*
9 simpl3 D∞MetXPXR*APballDRR*
10 xmetge0 D∞MetXPXAX0PDA
11 3 4 6 10 syl3anc D∞MetXPXR*APballDR0PDA
12 5 simplbda D∞MetXPXR*APballDRPDA<R
13 2 8 9 11 12 xrlelttrd D∞MetXPXR*APballDR0<R